<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: CVC3::SearchSat Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a> </li>
<li class="navelem"><a class="el" href="classCVC3_1_1SearchSat.html">SearchSat</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#nested-classes">Classes</a> |
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-methods">Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> |
<a href="#friends">Friends</a> </div>
<div class="headertitle">
<div class="title">CVC3::SearchSat Class Reference<div class="ingroups"><a class="el" href="group__SE.html">Search Engine</a></div></div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::SearchSat" --><!-- doxytag: inherits="CVC3::SearchEngine" -->
<p>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></p>
<p><code>#include <<a class="el" href="search__sat_8h_source.html">search_sat.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for CVC3::SearchSat:</div>
<div class="dyncontent">
<div class="center">
<img src="classCVC3_1_1SearchSat.png" usemap="#CVC3::SearchSat_map" alt=""/>
<map id="CVC3::SearchSat_map" name="CVC3::SearchSat_map">
<area href="classCVC3_1_1SearchEngine.html" title="API to to a generic proof search engine." alt="CVC3::SearchEngine" shape="rect" coords="0,0,132,24"/>
</map>
</div></div>
<p><a href="classCVC3_1_1SearchSat-members.html">List of all members.</a></p>
<h2><a name="nested-classes"></a>
Classes</h2>
<ul>
<li>class <a class="el" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html">LitPriorityPair</a>
<dl class="el"><dd class="mdescRight">Pair of Lit and priority of this Lit. <a href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#details">More...</a><br/></dl><li>class <a class="el" href="classCVC3_1_1SearchSat_1_1Restorer.html">Restorer</a>
</ul>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classCVC3_1_1SearchSat.html#a8298bda3d71fc4f613476d49c8270ecc">SearchSat</a> (<a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> *core, const std::string &name)
<li>virtual <a class="el" href="classCVC3_1_1SearchSat.html#ad2e00c54dd9d8d8f1e674065f255a28b">~SearchSat</a> ()
<dl class="el"><dd class="mdescRight">Destructor. <a href="#ad2e00c54dd9d8d8f1e674065f255a28b"></a><br/></dl><li>virtual const std::string & <a class="el" href="classCVC3_1_1SearchSat.html#a40df6c2ecc6cf95be36169849da3fd3a">getName</a> ()
<dl class="el"><dd class="mdescRight">Name of this search engine. <a href="#a40df6c2ecc6cf95be36169849da3fd3a"></a><br/></dl><li>virtual void <a class="el" href="classCVC3_1_1SearchSat.html#a2ca4a66d1bf7d0227e646edd3c9b9964">registerAtom</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Register an atomic formula of interest. <a href="#a2ca4a66d1bf7d0227e646edd3c9b9964"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchSat.html#a737cf8f3791197c405017db18163ce6b">getImpliedLiteral</a> ()
<dl class="el"><dd 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="#a737cf8f3791197c405017db18163ce6b"></a><br/></dl><li>virtual void <a class="el" href="classCVC3_1_1SearchSat.html#a9f129c2415d3eef0d73ad6d98ff13d44">push</a> ()
<dl class="el"><dd class="mdescRight">Push a checkpoint. <a href="#a9f129c2415d3eef0d73ad6d98ff13d44"></a><br/></dl><li>virtual void <a class="el" href="classCVC3_1_1SearchSat.html#a5c3eeec4b2c970f9d503b2892c9eb770">pop</a> ()
<dl class="el"><dd class="mdescRight">Restore last checkpoint. <a href="#a5c3eeec4b2c970f9d503b2892c9eb770"></a><br/></dl><li>virtual <a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="el" href="classCVC3_1_1SearchSat.html#a2921a84d2f2f33413ccda78789f40147">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)
<dl class="el"><dd class="mdescRight">Checks the validity of a formula in the current context. <a href="#a2921a84d2f2f33413ccda78789f40147"></a><br/></dl><li>virtual <a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="el" href="classCVC3_1_1SearchSat.html#ae7bf52f7780c6f2e085cf23c507fc3e1">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)
<dl class="el"><dd class="mdescRight">Reruns last check with e as an additional assumption. <a href="#ae7bf52f7780c6f2e085cf23c507fc3e1"></a><br/></dl><li>virtual void <a class="el" href="classCVC3_1_1SearchSat.html#a43a09dbf7232bfdb6f10aee4df1add94">returnFromCheck</a> ()
<dl class="el"><dd class="mdescRight">Returns to context immediately before last call to checkValid. <a href="#a43a09dbf7232bfdb6f10aee4df1add94"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchSat.html#a0828289ad2b19cc7fac453b41287ca50">lastThm</a> ()
<dl class="el"><dd class="mdescRight">Returns the result of the most recent valid theorem. <a href="#a0828289ad2b19cc7fac453b41287ca50"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchSat.html#a859331cc6fc93adfdd09cb848cd6de0b">newUserAssumption</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Generate and add an assumption to the set of assumptions in the current context. <a href="#a859331cc6fc93adfdd09cb848cd6de0b"></a><br/></dl><li>virtual void <a class="el" href="classCVC3_1_1SearchSat.html#a7344ad67225c0d6e30f8c2215bc7e0b0">getUserAssumptions</a> (std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &assumptions)
<dl class="el"><dd class="mdescRight">Get all user assumptions made in this and all previous contexts. <a href="#a7344ad67225c0d6e30f8c2215bc7e0b0"></a><br/></dl><li>virtual void <a class="el" href="classCVC3_1_1SearchSat.html#acee513ead4033fd5bfc16cbab7951dc7">getInternalAssumptions</a> (std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &assumptions)
<dl class="el"><dd class="mdescRight">Get assumptions made internally in this and all previous contexts. <a href="#acee513ead4033fd5bfc16cbab7951dc7"></a><br/></dl><li>virtual void <a class="el" href="classCVC3_1_1SearchSat.html#a63ffdace5647b9d783e4a4a0dd90fb0b">getAssumptions</a> (std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &assumptions)
<dl class="el"><dd class="mdescRight">Get all assumptions made in this and all previous contexts. <a href="#a63ffdace5647b9d783e4a4a0dd90fb0b"></a><br/></dl><li>virtual bool <a class="el" href="classCVC3_1_1SearchSat.html#a4ec713d6bbbd5d4bd6a9fcacc42a044e">isAssumption</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Check if the formula has already been assumed previously. <a href="#a4ec713d6bbbd5d4bd6a9fcacc42a044e"></a><br/></dl><li>virtual void <a class="el" href="classCVC3_1_1SearchSat.html#af2296bfb7f363cb9b83ca2fa6042d496">getCounterExample</a> (std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &assertions, bool inOrder=true)
<dl class="el"><dd class="mdescRight">Will return the set of assertions which make the queried formula false. <a href="#af2296bfb7f363cb9b83ca2fa6042d496"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Proof.html">Proof</a> <a class="el" href="classCVC3_1_1SearchSat.html#aa8b7c9812f7f61fc567c502ef3240d85">getProof</a> ()
<dl class="el"><dd class="mdescRight">Returns the proof term for the last proven query. <a href="#aa8b7c9812f7f61fc567c502ef3240d85"></a><br/></dl><li>virtual <a class="el" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bf">FormulaValue</a> <a class="el" href="classCVC3_1_1SearchSat.html#ad3267f576f114e049609a8c3c4f01118">getValue</a> (const <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a> &e)
</ul>
<h2><a name="pri-methods"></a>
Private Member Functions</h2>
<ul>
<li>void <a class="el" href="classCVC3_1_1SearchSat.html#aff33fe25d0761167062aa871e1992ded">restorePre</a> ()
<dl class="el"><dd class="mdescRight">Get rid of bottom scope entries in prioritySet. <a href="#aff33fe25d0761167062aa871e1992ded"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1SearchSat.html#a41d79aff18a635a5cdc2c789bb784a0a">restore</a> ()
<dl class="el"><dd class="mdescRight">Get rid of entries in prioritySet and pendingLemmas added since last push. <a href="#a41d79aff18a635a5cdc2c789bb784a0a"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1SearchSat.html#a0f3b2311296e520c22aea55c68c4b477">recordNewRootLit</a> (<a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> lit, int priority=0, bool atBottomScope=false)
<dl class="el"><dd class="mdescRight">Helper for addLemma and check. <a href="#a0f3b2311296e520c22aea55c68c4b477"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1SearchSat.html#ad7abbaa4ca4528eb0cdfcbce26d05ea4">addLemma</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm, int priority=0, bool atBotomScope=false)
<dl class="el"><dd class="mdescRight">Core theory callback which adds a new lemma from the core theory. <a href="#ad7abbaa4ca4528eb0cdfcbce26d05ea4"></a><br/></dl><li>int <a class="el" href="classCVC3_1_1SearchSat.html#a7dd555ba6043bd8019091ac6289233d6">getBottomScope</a> ()
<dl class="el"><dd class="mdescRight">Core theory callback which asks for the bottom scope for current query. <a href="#a7dd555ba6043bd8019091ac6289233d6"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1SearchSat.html#a98359a6ceb891ac5d12030aa42210b3d">addSplitter</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int priority)
<dl class="el"><dd class="mdescRight">Core theory callback which suggests a splitter. <a href="#a98359a6ceb891ac5d12030aa42210b3d"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1SearchSat.html#a14cf6695839ff6ac2a0fc0f134c26d47">assertLit</a> (<a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> l)
<dl class="el"><dd class="mdescRight">DPLLT callback to inform theory that a literal has been assigned. <a href="#a14cf6695839ff6ac2a0fc0f134c26d47"></a><br/></dl><li><a class="el" href="classSAT_1_1DPLLT.html#ac612908684032ffe76ad97f04afd0ca8">SAT::DPLLT::ConsistentResult</a> <a class="el" href="classCVC3_1_1SearchSat.html#aba13a4e3105c6d8ed6ae960a35ac0831">checkConsistent</a> (<a class="el" href="classSAT_1_1CNF__Formula.html">SAT::CNF_Formula</a> &cnf, bool fullEffort)
<dl class="el"><dd class="mdescRight">DPLLT callback to ask if theory has detected inconsistency. <a href="#aba13a4e3105c6d8ed6ae960a35ac0831"></a><br/></dl><li><a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> <a class="el" href="classCVC3_1_1SearchSat.html#a87c52cad8178ab644a84e31ab0290f95">getImplication</a> ()
<dl class="el"><dd class="mdescRight">DPLLT callback to get theory propagations. <a href="#a87c52cad8178ab644a84e31ab0290f95"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1SearchSat.html#a6347fa89942c705786dece8175c2bf6c">getExplanation</a> (<a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> l, <a class="el" href="classSAT_1_1CNF__Formula.html">SAT::CNF_Formula</a> &cnf)
<dl class="el"><dd class="mdescRight">DPLLT callback to explain a theory propagation. <a href="#a6347fa89942c705786dece8175c2bf6c"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1SearchSat.html#a858da2f6e8aefe2aeb124eececd45e3a">getNewClauses</a> (<a class="el" href="classSAT_1_1CNF__Formula.html">SAT::CNF_Formula</a> &cnf)
<dl class="el"><dd class="mdescRight">DPLLT callback to get more general theory clauses. <a href="#a858da2f6e8aefe2aeb124eececd45e3a"></a><br/></dl><li><a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> <a class="el" href="classCVC3_1_1SearchSat.html#afa9bdddd9bef64500f6a958d90682c37">makeDecision</a> ()
<dl class="el"><dd class="mdescRight">DPLLT callback to decide which literal to split on next. <a href="#afa9bdddd9bef64500f6a958d90682c37"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1SearchSat.html#a9b9c34dcc6d7deab8d54c1d03e5b7a2e">findSplitterRec</a> (<a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> lit, <a class="el" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">SAT::Var::Val</a> value, <a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> *litDecision)
<dl class="el"><dd class="mdescRight">Recursively traverse DAG looking for a splitter. <a href="#a9b9c34dcc6d7deab8d54c1d03e5b7a2e"></a><br/></dl><li><a class="el" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">SAT::Var::Val</a> <a class="el" href="classCVC3_1_1SearchSat.html#ad0e5b15a0bee268c25db7ee980320e67">getValue</a> (<a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> c)
<dl class="el"><dd class="mdescRight">Get the value of a CNF <a class="el" href="classCVC3_1_1Literal.html">Literal</a>. <a href="#ad0e5b15a0bee268c25db7ee980320e67"></a><br/></dl><li><a class="el" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">SAT::Var::Val</a> <a class="el" href="classCVC3_1_1SearchSat.html#a333a205198c7df1975fe460bce80ae6a">getValue</a> (<a class="el" href="classSAT_1_1Var.html">SAT::Var</a> v)
<li>void <a class="el" href="classCVC3_1_1SearchSat.html#a94c52626fff5a5c7563285f3571ddcc5">setValue</a> (<a class="el" href="classSAT_1_1Var.html">SAT::Var</a> v, <a class="el" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">SAT::Var::Val</a> val)
<dl class="el"><dd class="mdescRight">Set the value of a variable. <a href="#a94c52626fff5a5c7563285f3571ddcc5"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1SearchSat.html#a74be94781b15e4c9c7787161264066c9">checkJustified</a> (<a class="el" href="classSAT_1_1Var.html">SAT::Var</a> v)
<dl class="el"><dd class="mdescRight">Check whether this variable's value is justified. <a href="#a74be94781b15e4c9c7787161264066c9"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1SearchSat.html#a628753b6aaaabd0e67a7405d543f8ed0">setJustified</a> (<a class="el" href="classSAT_1_1Var.html">SAT::Var</a> v)
<dl class="el"><dd class="mdescRight">Mark this variable as justified. <a href="#a628753b6aaaabd0e67a7405d543f8ed0"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="el" href="classCVC3_1_1SearchSat.html#a720aba611f6cf6fd78bc3a0ede54564b">check</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &result, bool isRestart=false)
<dl class="el"><dd class="mdescRight">Main checking procedure shared by checkValid and restart. <a href="#a720aba611f6cf6fd78bc3a0ede54564b"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1SearchSat.html#a4bc91d2be335eabdcd6174cf634fe9e3">newUserAssumptionIntHelper</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm, <a class="el" href="classSAT_1_1CNF__Formula__Impl.html">SAT::CNF_Formula_Impl</a> &cnf, bool atBottomScope)
<dl class="el"><dd class="mdescRight">Helper for newUserAssumptionInt. <a href="#a4bc91d2be335eabdcd6174cf634fe9e3"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchSat.html#ab9c866f4bb3ba8f3662a8ee99760f257">newUserAssumptionInt</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classSAT_1_1CNF__Formula__Impl.html">SAT::CNF_Formula_Impl</a> &cnf, bool atBottomScope)
<dl class="el"><dd class="mdescRight">Helper for newUserAssumption. <a href="#ab9c866f4bb3ba8f3662a8ee99760f257"></a><br/></dl></ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li>std::string <a class="el" href="classCVC3_1_1SearchSat.html#ab7dd09d7a8ea0c87e2e1ec42a837160b">d_name</a>
<dl class="el"><dd class="mdescRight">Name of search engine. <a href="#ab7dd09d7a8ea0c87e2e1ec42a837160b"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< int > <a class="el" href="classCVC3_1_1SearchSat.html#a8153b8d7b772217bafddf3d92be4759b">d_bottomScope</a>
<dl class="el"><dd class="mdescRight">Bottom scope for current query. <a href="#a8153b8d7b772217bafddf3d92be4759b"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > <a class="el" href="classCVC3_1_1SearchSat.html#ac318c6520fbea766517991127affaafc">d_lastCheck</a>
<dl class="el"><dd class="mdescRight">Last expr checked for validity. <a href="#ac318c6520fbea766517991127affaafc"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > <a class="el" href="classCVC3_1_1SearchSat.html#ab41637f4522c5e3f318993392adf84bb">d_lastValid</a>
<dl class="el"><dd 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="#ab41637f4522c5e3f318993392adf84bb"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDList.html">CDList</a>< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > <a class="el" href="classCVC3_1_1SearchSat.html#a3b9b2371a24908e62ec71b6f141afea8">d_userAssumptions</a>
<dl class="el"><dd class="mdescRight">List of all user assumptions. <a href="#a3b9b2371a24908e62ec71b6f141afea8"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDList.html">CDList</a>< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > <a class="el" href="classCVC3_1_1SearchSat.html#ad3b9879d655cf3fce1a70de7b1d6fedc">d_intAssumptions</a>
<dl class="el"><dd class="mdescRight">List of all internal assumptions. <a href="#ad3b9879d655cf3fce1a70de7b1d6fedc"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< unsigned > <a class="el" href="classCVC3_1_1SearchSat.html#a23b0c38d89ce24f463f2c2fc929df879">d_idxUserAssump</a>
<dl class="el"><dd class="mdescRight">Index to where unprocessed assumptions start. <a href="#a23b0c38d89ce24f463f2c2fc929df879"></a><br/></dl><li><a class="el" href="classCVC3_1_1TheoryCore_1_1CoreSatAPI.html">TheoryCore::CoreSatAPI</a> * <a class="el" href="classCVC3_1_1SearchSat.html#aab55d9ceeb2a938841230c920762ba77">d_coreSatAPI</a>
<li><a class="el" href="classSAT_1_1DPLLT.html">SAT::DPLLT</a> * <a class="el" href="classCVC3_1_1SearchSat.html#a884c103ef1313d56a3a42d4e3e8468cb">d_dpllt</a>
<dl class="el"><dd class="mdescRight">Pointer to DPLLT implementation. <a href="#a884c103ef1313d56a3a42d4e3e8468cb"></a><br/></dl><li><a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">SAT::DPLLT::TheoryAPI</a> * <a class="el" href="classCVC3_1_1SearchSat.html#a8abc1b647affa60cc367e0eeaa52cdf4">d_theoryAPI</a>
<dl class="el"><dd class="mdescRight">Implementation of TheoryAPI for DPLLT. <a href="#a8abc1b647affa60cc367e0eeaa52cdf4"></a><br/></dl><li><a class="el" href="classSAT_1_1DPLLT_1_1Decider.html">SAT::DPLLT::Decider</a> * <a class="el" href="classCVC3_1_1SearchSat.html#aa4be1d02557a46fbbdc32deefc4f3a32">d_decider</a>
<dl class="el"><dd class="mdescRight">Implementation of Decider for DPLLT. <a href="#aa4be1d02557a46fbbdc32deefc4f3a32"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDMap.html">CDMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > <a class="el" href="classCVC3_1_1SearchSat.html#a3e6b8d2d1d9513329fbbb80464053b39">d_theorems</a>
<dl class="el"><dd class="mdescRight">Store of theorems for expressions sent to DPLLT. <a href="#a3e6b8d2d1d9513329fbbb80464053b39"></a><br/></dl><li><a class="el" href="classSAT_1_1CNF__Manager.html">SAT::CNF_Manager</a> * <a class="el" href="classCVC3_1_1SearchSat.html#a996335737d383fd882b6f1085f72b964">d_cnfManager</a>
<dl class="el"><dd class="mdescRight">Manages CNF formula and its relationship to original Exprs and Theorems. <a href="#a996335737d383fd882b6f1085f72b964"></a><br/></dl><li><a class="el" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html">SAT::CNF_Manager::CNFCallback</a> * <a class="el" href="classCVC3_1_1SearchSat.html#a158485ff14b490fc2c91936a4e72bf5b">d_cnfCallback</a>
<dl class="el"><dd class="mdescRight">Callback for CNF_Manager. <a href="#a158485ff14b490fc2c91936a4e72bf5b"></a><br/></dl><li>std::vector< <a class="el" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">SAT::Var::Val</a> > <a class="el" href="classCVC3_1_1SearchSat.html#a455c295a13215ddc99b8df18f4598af4">d_vars</a>
<dl class="el"><dd class="mdescRight">Cached values of variables. <a href="#a455c295a13215ddc99b8df18f4598af4"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1SearchSat.html#a00573a594dd2b83cbb6f2997516862d3">d_inCheckSat</a>
<dl class="el"><dd class="mdescRight">Whether we are currently in a call to dpllt->checkSat. <a href="#a00573a594dd2b83cbb6f2997516862d3"></a><br/></dl><li><a class="el" href="classSAT_1_1CD__CNF__Formula.html">SAT::CD_CNF_Formula</a> <a class="el" href="classCVC3_1_1SearchSat.html#aed781537ef3315ffa019cdd7f02f0f8e">d_lemmas</a>
<dl class="el"><dd class="mdescRight">CNF Formula used for theory lemmas. <a href="#aed781537ef3315ffa019cdd7f02f0f8e"></a><br/></dl><li>std::vector< std::pair<br class="typebreak"/>
< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>, int > > <a class="el" href="classCVC3_1_1SearchSat.html#a3997be227d7cd36e1f29f71a683f1428">d_pendingLemmas</a>
<dl class="el"><dd class="mdescRight">Lemmas waiting to be translated since last call to <a class="el" href="classCVC3_1_1SearchSat.html#a858da2f6e8aefe2aeb124eececd45e3a" title="DPLLT callback to get more general theory clauses.">getNewClauses()</a> <a href="#a3997be227d7cd36e1f29f71a683f1428"></a><br/></dl><li>std::vector< bool > <a class="el" href="classCVC3_1_1SearchSat.html#a83bb96cd69f2673e370e536a7946c5c3">d_pendingScopes</a>
<dl class="el"><dd class="mdescRight"><a class="el" href="classCVC3_1_1Scope.html">Scope</a> parameter for lemmas waiting to be translated since last call to <a class="el" href="classCVC3_1_1SearchSat.html#a858da2f6e8aefe2aeb124eececd45e3a" title="DPLLT callback to get more general theory clauses.">getNewClauses()</a> <a href="#a83bb96cd69f2673e370e536a7946c5c3"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< unsigned > <a class="el" href="classCVC3_1_1SearchSat.html#ab309591a57e34a9166c3baa056e2857f">d_pendingLemmasSize</a>
<dl class="el"><dd class="mdescRight">Backtracking size of d_pendingLemmas. <a href="#ab309591a57e34a9166c3baa056e2857f"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< unsigned > <a class="el" href="classCVC3_1_1SearchSat.html#a8de03d523c9b0304eb95e72ec923274b">d_pendingLemmasNext</a>
<dl class="el"><dd class="mdescRight">Backtracking next item in d_pendingLemmas. <a href="#a8de03d523c9b0304eb95e72ec923274b"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< unsigned > <a class="el" href="classCVC3_1_1SearchSat.html#a819ee9729fd633651eb2cf27f7175d8a">d_lemmasNext</a>
<dl class="el"><dd class="mdescRight">Current position in d_lemmas. <a href="#a819ee9729fd633651eb2cf27f7175d8a"></a><br/></dl><li>std::vector< unsigned > <a class="el" href="classCVC3_1_1SearchSat.html#a78ea4f3b48395a88f42bb4db58c44541">d_varsUndoList</a>
<dl class="el"><dd class="mdescRight">List for backtracking var values. <a href="#a78ea4f3b48395a88f42bb4db58c44541"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< unsigned > <a class="el" href="classCVC3_1_1SearchSat.html#a6c7fadcd8cd61189c6c3c38a28035993">d_varsUndoListSize</a>
<dl class="el"><dd class="mdescRight">Backtracking size of d_varsUndoList. <a href="#a6c7fadcd8cd61189c6c3c38a28035993"></a><br/></dl><li>std::set< <a class="el" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html">LitPriorityPair</a> > <a class="el" href="classCVC3_1_1SearchSat.html#ab4dbd42cf98469a2abb679024a402b77">d_prioritySet</a>
<dl class="el"><dd class="mdescRight">Used to determine order to find splitters. <a href="#ab4dbd42cf98469a2abb679024a402b77"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< std::set< <a class="el" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html">LitPriorityPair</a> ><br class="typebreak"/>
::const_iterator > <a class="el" href="classCVC3_1_1SearchSat.html#ad7b3c57fadbc655bddd204b9ea122a62">d_prioritySetStart</a>
<dl class="el"><dd class="mdescRight">Current position in prioritySet. <a href="#ad7b3c57fadbc655bddd204b9ea122a62"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< unsigned > <a class="el" href="classCVC3_1_1SearchSat.html#a3495b7cac1dc81f07f54dc8d0b17b17a">d_prioritySetEntriesSize</a>
<dl class="el"><dd class="mdescRight">Backtracking size of priority set entries. <a href="#a3495b7cac1dc81f07f54dc8d0b17b17a"></a><br/></dl><li>std::vector< std::set<br class="typebreak"/>
< <a class="el" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html">LitPriorityPair</a> >::iterator > <a class="el" href="classCVC3_1_1SearchSat.html#ab57f9f48af74c9a6493986b8cb0c720d">d_prioritySetEntries</a>
<dl class="el"><dd class="mdescRight">Entries in priority set in insertion order (so set can be backtracked) <a href="#ab57f9f48af74c9a6493986b8cb0c720d"></a><br/></dl><li>std::vector< unsigned > <a class="el" href="classCVC3_1_1SearchSat.html#a99063dd2470eae948fa85d460a9b3868">d_prioritySetBottomEntriesSizeStack</a>
<dl class="el"><dd class="mdescRight">Backtracking size of priority set entries at bottom scope. <a href="#a99063dd2470eae948fa85d460a9b3868"></a><br/></dl><li>unsigned <a class="el" href="classCVC3_1_1SearchSat.html#ab8e5996fd3e75c5b3c45f611d3639535">d_prioritySetBottomEntriesSize</a>
<dl class="el"><dd class="mdescRight">Current size of bottom entries. <a href="#ab8e5996fd3e75c5b3c45f611d3639535"></a><br/></dl><li>std::vector< std::set<br class="typebreak"/>
< <a class="el" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html">LitPriorityPair</a> >::iterator > <a class="el" href="classCVC3_1_1SearchSat.html#a6d963065a2df65795626cf6d70f8fe99">d_prioritySetBottomEntries</a>
<dl class="el"><dd class="mdescRight">Entries in priority set in insertion order (so set can be backtracked) <a href="#a6d963065a2df65795626cf6d70f8fe99"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< unsigned > <a class="el" href="classCVC3_1_1SearchSat.html#a217f464659b186330934d046aa7cc764">d_lastRegisteredVar</a>
<dl class="el"><dd class="mdescRight">Last Var registered with core theory. <a href="#a217f464659b186330934d046aa7cc764"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< bool > <a class="el" href="classCVC3_1_1SearchSat.html#af0953025654043f6f76040df7abf2658">d_dplltReady</a>
<dl class="el"><dd class="mdescRight">Whether it's OK to call DPLLT solver from the current scope. <a href="#af0953025654043f6f76040df7abf2658"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< unsigned > <a class="el" href="classCVC3_1_1SearchSat.html#ae97f61c9a0ae9ed8186929e15892ad73">d_nextImpliedLiteral</a>
<li><a class="el" href="classCVC3_1_1SearchSat_1_1Restorer.html">Restorer</a> <a class="el" href="classCVC3_1_1SearchSat.html#a5b7313c3933e04b894089b1c2e09c57e">d_restorer</a>
<dl class="el"><dd class="mdescRight">Instance of <a class="el" href="classCVC3_1_1SearchSat_1_1Restorer.html">Restorer</a> class. <a href="#a5b7313c3933e04b894089b1c2e09c57e"></a><br/></dl></ul>
<h2><a name="friends"></a>
Friends</h2>
<ul>
<li>class <a class="el" href="classCVC3_1_1SearchSat.html#aa9f952c8606458f1e777d9a05b11550d">Restorer</a>
<dl class="el"><dd class="mdescRight">Helper class for resetting DPLLT engine. <a href="#aa9f952c8606458f1e777d9a05b11550d"></a><br/></dl><li>class <a class="el" href="classCVC3_1_1SearchSat.html#a71c71132ecb225ad44dd66fc2c3505f3">SearchSatCoreSatAPI</a>
<li>class <a class="el" href="classCVC3_1_1SearchSat.html#acfd18b3733ce33513e1e5ddaad615624">SearchSatCNFCallback</a>
<li>class <a class="el" href="classCVC3_1_1SearchSat.html#a8cb09d5d17839a0377e369713fcbbedf">SearchSatTheoryAPI</a>
<li>class <a class="el" href="classCVC3_1_1SearchSat.html#a447de240c99ed9d998d211b07609bc5d">SearchSatDecider</a>
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock"><p>Search engine that connects to a generic <a class="el" href="namespaceSAT.html">SAT</a> reasoning module. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00040">40</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a8298bda3d71fc4f613476d49c8270ecc"></a><!-- doxytag: member="CVC3::SearchSat::SearchSat" ref="a8298bda3d71fc4f613476d49c8270ecc" args="(TheoryCore *core, const std::string &name)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">SearchSat::SearchSat </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> * </td>
<td class="paramname"><em>core</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>name</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Constructor name is the name of the dpllt engine to use, as returned by <a class="el" href="classCVC3_1_1SearchSat.html#a40df6c2ecc6cf95be36169849da3fd3a" title="Name of this search engine.">getName()</a> </p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00936">936</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="search__sat_8h_source.html#l00082">d_cnfCallback</a>, <a class="el" href="search__sat_8h_source.html#l00079">d_cnfManager</a>, <a class="el" href="search__sat_8h_source.html#l00064">d_coreSatAPI</a>, <a class="el" href="search__sat_8h_source.html#l00073">d_decider</a>, <a class="el" href="search__sat_8h_source.html#l00067">d_dpllt</a>, <a class="el" href="search__sat_8h_source.html#l00131">d_prioritySet</a>, <a class="el" href="search__sat_8h_source.html#l00133">d_prioritySetStart</a>, <a class="el" href="search__sat_8h_source.html#l00070">d_theoryAPI</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="theory__core_8h_source.html#l00351">CVC3::TheoryCore::getStatistics()</a>, <a class="el" href="theory__core_8h_source.html#l00349">CVC3::TheoryCore::getTM()</a>, <a class="el" href="cnf__manager_8h_source.html#l00166">SAT::CNF_Manager::registerCNFCallback()</a>, <a class="el" href="theory__core_8h_source.html#l00340">CVC3::TheoryCore::registerCoreSatAPI()</a>, <a class="el" href="search__sat_8h_source.html#l00180">SearchSatCNFCallback</a>, <a class="el" href="search__sat_8h_source.html#l00179">SearchSatCoreSatAPI</a>, <a class="el" href="search__sat_8h_source.html#l00200">SearchSatDecider</a>, <a class="el" href="search__sat_8h_source.html#l00188">SearchSatTheoryAPI</a>, and <a class="el" href="theorem__manager_8h_source.html#l00091">CVC3::TheoremManager::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="ad2e00c54dd9d8d8f1e674065f255a28b"></a><!-- doxytag: member="CVC3::SearchSat::~SearchSat" ref="ad2e00c54dd9d8d8f1e674065f255a28b" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">SearchSat::~SearchSat </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Destructor. </p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00991">991</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="search__sat_8h_source.html#l00082">d_cnfCallback</a>, <a class="el" href="search__sat_8h_source.html#l00079">d_cnfManager</a>, <a class="el" href="search__sat_8h_source.html#l00064">d_coreSatAPI</a>, <a class="el" href="search__sat_8h_source.html#l00073">d_decider</a>, <a class="el" href="search__sat_8h_source.html#l00067">d_dpllt</a>, and <a class="el" href="search__sat_8h_source.html#l00070">d_theoryAPI</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="aff33fe25d0761167062aa871e1992ded"></a><!-- doxytag: member="CVC3::SearchSat::restorePre" ref="aff33fe25d0761167062aa871e1992ded" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchSat::restorePre </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Get rid of bottom scope entries in prioritySet. </p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00115">115</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8h_source.html#l00164">CVC3::SearchSat::Restorer::notifyPre()</a>.</p>
</div>
</div>
<a class="anchor" id="a41d79aff18a635a5cdc2c789bb784a0a"></a><!-- doxytag: member="CVC3::SearchSat::restore" ref="a41d79aff18a635a5cdc2c789bb784a0a" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchSat::restore </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Get rid of entries in prioritySet and pendingLemmas added since last push. </p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00129">129</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8h_source.html#l00165">CVC3::SearchSat::Restorer::notify()</a>.</p>
</div>
</div>
<a class="anchor" id="a0f3b2311296e520c22aea55c68c4b477"></a><!-- doxytag: member="CVC3::SearchSat::recordNewRootLit" ref="a0f3b2311296e520c22aea55c68c4b477" args="(SAT::Lit lit, int priority=0, bool atBottomScope=false)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool SearchSat::recordNewRootLit </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> </td>
<td class="paramname"><em>lit</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>priority</em> = <code>0</code>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>atBottomScope</em> = <code>false</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Helper for addLemma and check. </p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00146">146</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l01042">newUserAssumptionIntHelper()</a>.</p>
</div>
</div>
<a class="anchor" id="ad7abbaa4ca4528eb0cdfcbce26d05ea4"></a><!-- doxytag: member="CVC3::SearchSat::addLemma" ref="ad7abbaa4ca4528eb0cdfcbce26d05ea4" args="(const Theorem &thm, int priority=0, bool atBotomScope=false)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchSat::addLemma </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">int </td>
<td class="paramname"><em>priority</em> = <code>0</code>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>atBotomScope</em> = <code>false</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Core theory callback which adds a new lemma from the core theory. </p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00170">170</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <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="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="lang_8h_source.html#l00032">CVC3::PRESENTATION_LANG</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="a7dd555ba6043bd8019091ac6289233d6"></a><!-- doxytag: member="CVC3::SearchSat::getBottomScope" ref="a7dd555ba6043bd8019091ac6289233d6" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVC3::SearchSat::getBottomScope </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Core theory callback which asks for the bottom scope for current query. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00184">184</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>References <a class="el" href="search__sat_8h_source.html#l00046">d_bottomScope</a>.</p>
</div>
</div>
<a class="anchor" id="a98359a6ceb891ac5d12030aa42210b3d"></a><!-- doxytag: member="CVC3::SearchSat::addSplitter" ref="a98359a6ceb891ac5d12030aa42210b3d" args="(const Expr &e, int priority)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchSat::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><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Core theory callback which suggests a splitter. </p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00186">186</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="expr_8h_source.html#l00419">CVC3::Expr::isEq()</a>.</p>
</div>
</div>
<a class="anchor" id="a14cf6695839ff6ac2a0fc0f134c26d47"></a><!-- doxytag: member="CVC3::SearchSat::assertLit" ref="a14cf6695839ff6ac2a0fc0f134c26d47" args="(SAT::Lit l)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchSat::assertLit </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> </td>
<td class="paramname"><em>l</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>DPLLT callback to inform theory that a literal has been assigned. </p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00193">193</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="formula__value_8h_source.html#l00033">CVC3::FALSE_VAL</a>, <a class="el" href="cnf_8h_source.html#l00070">SAT::Lit::getVar()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="expr_8h_source.html#l00406">CVC3::Expr::isAbsLiteral()</a>, <a class="el" href="expr_8h_source.html#l01362">CVC3::Expr::isIntAssumption()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>, <a class="el" href="cnf_8h_source.html#l00064">SAT::Lit::isPositive()</a>, <a class="el" href="expr_8h_source.html#l01508">CVC3::Expr::setIntAssumption()</a>, <a class="el" href="theorem_8cpp_source.html#l00504">CVC3::Theorem::setQuantLevel()</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="formula__value_8h_source.html#l00032">CVC3::TRUE_VAL</a>, and <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</a>.</p>
</div>
</div>
<a class="anchor" id="aba13a4e3105c6d8ed6ae960a35ac0831"></a><!-- doxytag: member="CVC3::SearchSat::checkConsistent" ref="aba13a4e3105c6d8ed6ae960a35ac0831" args="(SAT::CNF_Formula &cnf, bool fullEffort)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1DPLLT.html#ac612908684032ffe76ad97f04afd0ca8">SAT::DPLLT::ConsistentResult</a> SearchSat::checkConsistent </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1CNF__Formula.html">SAT::CNF_Formula</a> & </td>
<td class="paramname"><em>cnf</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>fullEffort</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>DPLLT callback to ask if theory has detected inconsistency. </p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00258">258</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</a>.</p>
</div>
</div>
<a class="anchor" id="a87c52cad8178ab644a84e31ab0290f95"></a><!-- doxytag: member="CVC3::SearchSat::getImplication" ref="a87c52cad8178ab644a84e31ab0290f95" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1Lit.html">Lit</a> SearchSat::getImplication </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>DPLLT callback to get theory propagations. </p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00284">284</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <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="cnf_8h_source.html#l00063">SAT::Lit::isNull()</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, <a class="el" href="expr_8h_source.html#l01374">CVC3::Expr::isUserRegisteredAtom()</a>, <a class="el" href="cnf_8h_source.html#l00074">SAT::Lit::reset()</a>, <a class="el" href="formula__value_8h_source.html#l00032">CVC3::TRUE_VAL</a>, and <a class="el" href="expr_8h_source.html#l00506">CVC3::Expr::unnegate()</a>.</p>
</div>
</div>
<a class="anchor" id="a6347fa89942c705786dece8175c2bf6c"></a><!-- doxytag: member="CVC3::SearchSat::getExplanation" ref="a6347fa89942c705786dece8175c2bf6c" args="(SAT::Lit l, SAT::CNF_Formula &cnf)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchSat::getExplanation </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> </td>
<td class="paramname"><em>l</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classSAT_1_1CNF__Formula.html">SAT::CNF_Formula</a> & </td>
<td class="paramname"><em>cnf</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>DPLLT callback to explain a theory propagation. </p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00304">304</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="classSAT_1_1CNF__Formula.html#a15e2d3d65a38c23558a0ae8cf35f1938">SAT::CNF_Formula::empty()</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>, and <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</a>.</p>
</div>
</div>
<a class="anchor" id="a858da2f6e8aefe2aeb124eececd45e3a"></a><!-- doxytag: member="CVC3::SearchSat::getNewClauses" ref="a858da2f6e8aefe2aeb124eececd45e3a" args="(SAT::CNF_Formula &cnf)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool SearchSat::getNewClauses </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1CNF__Formula.html">SAT::CNF_Formula</a> & </td>
<td class="paramname"><em>cnf</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>DPLLT callback to get more general theory clauses. </p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00318">318</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</a>.</p>
</div>
</div>
<a class="anchor" id="afa9bdddd9bef64500f6a958d90682c37"></a><!-- doxytag: member="CVC3::SearchSat::makeDecision" ref="afa9bdddd9bef64500f6a958d90682c37" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1Lit.html">Lit</a> SearchSat::makeDecision </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>DPLLT callback to decide which literal to split on next. </p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00346">346</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>.</p>
</div>
</div>
<a class="anchor" id="a9b9c34dcc6d7deab8d54c1d03e5b7a2e"></a><!-- doxytag: member="CVC3::SearchSat::findSplitterRec" ref="a9b9c34dcc6d7deab8d54c1d03e5b7a2e" args="(SAT::Lit lit, SAT::Var::Val value, SAT::Lit *litDecision)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool SearchSat::findSplitterRec </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> </td>
<td class="paramname"><em>lit</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">SAT::Var::Val</a> </td>
<td class="paramname"><em>value</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> * </td>
<td class="paramname"><em>litDecision</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Recursively traverse DAG looking for a splitter. </p>
<p>Returns true if a splitter is found, false otherwise. The splitter is returned in lit (lit should be set to true). Nodes whose current value is fully justified are marked by calling setFlag to avoid searching them in the future. </p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00364">364</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00067">AND</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="formula__value_8h_source.html#l00033">CVC3::FALSE_VAL</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="cnf_8h_source.html#l00070">SAT::Lit::getVar()</a>, <a class="el" href="kinds_8h_source.html#l00070">IFF</a>, <a class="el" href="kinds_8h_source.html#l00071">IMPLIES</a>, <a class="el" href="cnf_8h_source.html#l00066">SAT::Lit::isFalse()</a>, <a class="el" href="cnf_8h_source.html#l00065">SAT::Lit::isInverted()</a>, <a class="el" href="cnf_8h_source.html#l00067">SAT::Lit::isTrue()</a>, <a class="el" href="cnf_8h_source.html#l00068">SAT::Lit::isVar()</a>, <a class="el" href="kinds_8h_source.html#l00081">ITE</a>, <a class="el" href="kinds_8h_source.html#l00068">OR</a>, <a class="el" href="formula__value_8h_source.html#l00032">CVC3::TRUE_VAL</a>, <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</a>, and <a class="el" href="kinds_8h_source.html#l00069">XOR</a>.</p>
</div>
</div>
<a class="anchor" id="ad0e5b15a0bee268c25db7ee980320e67"></a><!-- doxytag: member="CVC3::SearchSat::getValue" ref="ad0e5b15a0bee268c25db7ee980320e67" args="(SAT::Lit c)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">SAT::Var::Val</a> CVC3::SearchSat::getValue </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> </td>
<td class="paramname"><em>c</em></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Get the value of a CNF <a class="el" href="classCVC3_1_1Literal.html">Literal</a>. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00214">214</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>References <a class="el" href="search__sat_8h_source.html#l00085">d_vars</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="formula__value_8h_source.html#l00033">CVC3::FALSE_VAL</a>, <a class="el" href="cnf_8h_source.html#l00070">SAT::Lit::getVar()</a>, <a class="el" href="cnf_8h_source.html#l00048">SAT::Var::invertValue()</a>, <a class="el" href="cnf_8h_source.html#l00065">SAT::Lit::isInverted()</a>, <a class="el" href="cnf_8h_source.html#l00063">SAT::Lit::isNull()</a>, <a class="el" href="cnf_8h_source.html#l00064">SAT::Lit::isPositive()</a>, <a class="el" href="cnf_8h_source.html#l00067">SAT::Lit::isTrue()</a>, <a class="el" href="cnf_8h_source.html#l00068">SAT::Lit::isVar()</a>, and <a class="el" href="cnf_8h_source.html#l00037">SAT::Var::TRUE_VAL</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8h_source.html#l00289">getValue()</a>.</p>
</div>
</div>
<a class="anchor" id="a333a205198c7df1975fe460bce80ae6a"></a><!-- doxytag: member="CVC3::SearchSat::getValue" ref="a333a205198c7df1975fe460bce80ae6a" args="(SAT::Var v)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">SAT::Var::Val</a> CVC3::SearchSat::getValue </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Var.html">SAT::Var</a> </td>
<td class="paramname"><em>v</em></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00223">223</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>References <a class="el" href="search__sat_8h_source.html#l00085">d_vars</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="cnf_8h_source.html#l00045">SAT::Var::isVar()</a>.</p>
</div>
</div>
<a class="anchor" id="a94c52626fff5a5c7563285f3571ddcc5"></a><!-- doxytag: member="CVC3::SearchSat::setValue" ref="a94c52626fff5a5c7563285f3571ddcc5" args="(SAT::Var v, SAT::Var::Val val)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::SearchSat::setValue </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Var.html">SAT::Var</a> </td>
<td class="paramname"><em>v</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">SAT::Var::Val</a> </td>
<td class="paramname"><em>val</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Set the value of a variable. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00229">229</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>References <a class="el" href="search__sat_8h_source.html#l00085">d_vars</a>, <a class="el" href="search__sat_8h_source.html#l00109">d_varsUndoList</a>, <a class="el" href="search__sat_8h_source.html#l00112">d_varsUndoListSize</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cnf_8h_source.html#l00042">SAT::Var::isNull()</a>, and <a class="el" href="cnf_8h_source.html#l00037">SAT::Var::UNKNOWN</a>.</p>
</div>
</div>
<a class="anchor" id="a74be94781b15e4c9c7787161264066c9"></a><!-- doxytag: member="CVC3::SearchSat::checkJustified" ref="a74be94781b15e4c9c7787161264066c9" args="(SAT::Var v)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::SearchSat::checkJustified </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Var.html">SAT::Var</a> </td>
<td class="paramname"><em>v</em></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Check whether this variable's value is justified. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00241">241</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>References <a class="el" href="cnf__manager_8h_source.html#l00223">SAT::CNF_Manager::concreteLit()</a>, <a class="el" href="search__sat_8h_source.html#l00079">d_cnfManager</a>, and <a class="el" href="expr_8h_source.html#l01366">CVC3::Expr::isJustified()</a>.</p>
</div>
</div>
<a class="anchor" id="a628753b6aaaabd0e67a7405d543f8ed0"></a><!-- doxytag: member="CVC3::SearchSat::setJustified" ref="a628753b6aaaabd0e67a7405d543f8ed0" args="(SAT::Var v)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::SearchSat::setJustified </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Var.html">SAT::Var</a> </td>
<td class="paramname"><em>v</em></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Mark this variable as justified. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00245">245</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>References <a class="el" href="cnf__manager_8h_source.html#l00223">SAT::CNF_Manager::concreteLit()</a>, <a class="el" href="search__sat_8h_source.html#l00079">d_cnfManager</a>, and <a class="el" href="expr_8h_source.html#l01513">CVC3::Expr::setJustified()</a>.</p>
</div>
</div>
<a class="anchor" id="a720aba611f6cf6fd78bc3a0ede54564b"></a><!-- doxytag: member="CVC3::SearchSat::check" ref="a720aba611f6cf6fd78bc3a0ede54564b" args="(const Expr &e, Theorem &result, bool isRestart=false)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> SearchSat::check </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 class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>isRestart</em> = <code>false</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Main checking procedure shared by checkValid and restart. </p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00638">638</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="kinds_8h_source.html#l00084">FORALL</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="cnf_8h_source.html#l00070">SAT::Lit::getVar()</a>, <a class="el" href="queryresult_8h_source.html#l00034">CVC3::INVALID</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l00419">CVC3::Expr::isEq()</a>, <a class="el" href="expr_8h_source.html#l00429">CVC3::Expr::isExists()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l00428">CVC3::Expr::isForall()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="cnf_8h_source.html#l00064">SAT::Lit::isPositive()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00301">CVC3::pop()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00298">CVC3::push()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00055">SATISFIABLE</a>, <a class="el" href="cdlist_8h_source.html#l00064">CVC3::CDList< T >::size()</a>, <a class="el" href="type_8h_source.html#l00080">CVC3::Type::toString()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</a>, <a class="el" href="xchaff__solver_8h_source.html#l00054">UNSATISFIABLE</a>, and <a class="el" href="queryresult_8h_source.html#l00035">CVC3::VALID</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8h_source.html#l00273">checkValid()</a>, and <a class="el" href="search__sat_8h_source.html#l00275">restart()</a>.</p>
</div>
</div>
<a class="anchor" id="a4bc91d2be335eabdcd6174cf634fe9e3"></a><!-- doxytag: member="CVC3::SearchSat::newUserAssumptionIntHelper" ref="a4bc91d2be335eabdcd6174cf634fe9e3" args="(const Theorem &thm, SAT::CNF_Formula_Impl &cnf, bool atBottomScope)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchSat::newUserAssumptionIntHelper </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"><a class="el" href="classSAT_1_1CNF__Formula__Impl.html">SAT::CNF_Formula_Impl</a> & </td>
<td class="paramname"><em>cnf</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>atBottomScope</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Helper for newUserAssumptionInt. </p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l01042">1042</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="cnf__manager_8cpp_source.html#l00623">SAT::CNF_Manager::addAssumption()</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__sat_8h_source.html#l00079">d_cnfManager</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="cnf_8h_source.html#l00162">SAT::CNF_Formula_Impl::deleteLast()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theory__core_8h_source.html#l00350">CVC3::TheoryCore::getFlags()</a>, <a class="el" href="expr_8h_source.html#l00421">CVC3::Expr::isAnd()</a>, and <a class="el" href="search__sat_8cpp_source.html#l00146">recordNewRootLit()</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l01064">newUserAssumptionInt()</a>.</p>
</div>
</div>
<a class="anchor" id="ab9c866f4bb3ba8f3662a8ee99760f257"></a><!-- doxytag: member="CVC3::SearchSat::newUserAssumptionInt" ref="ab9c866f4bb3ba8f3662a8ee99760f257" args="(const Expr &e, SAT::CNF_Formula_Impl &cnf, bool atBottomScope)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchSat::newUserAssumptionInt </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="classSAT_1_1CNF__Formula__Impl.html">SAT::CNF_Formula_Impl</a> & </td>
<td class="paramname"><em>cnf</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>atBottomScope</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Helper for newUserAssumption. </p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l01064">1064</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.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="search__sat_8h_source.html#l00046">d_bottomScope</a>, <a class="el" href="search__sat_8h_source.html#l00079">d_cnfManager</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__sat_8h_source.html#l00088">d_inCheckSat</a>, <a class="el" href="search__sat_8h_source.html#l00056">d_userAssumptions</a>, <a class="el" href="search__sat_8h_source.html#l00085">d_vars</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theory__core_8h_source.html#l00348">CVC3::TheoryCore::getCM()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theory__core_8h_source.html#l00352">CVC3::TheoryCore::getExprTrans()</a>, <a class="el" href="search__sat_8cpp_source.html#l01163">isAssumption()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, <a class="el" href="search__sat_8cpp_source.html#l01042">newUserAssumptionIntHelper()</a>, <a class="el" href="cnf__manager_8h_source.html#l00173">SAT::CNF_Manager::numVars()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00079">CVC3::ExprTransform::preprocess()</a>, <a class="el" href="cdlist_8h_source.html#l00066">CVC3::CDList< T >::push_back()</a>, <a class="el" href="context_8h_source.html#l00404">CVC3::ContextManager::scopeLevel()</a>, <a class="el" href="search__sat_8cpp_source.html#l01032">setRecursiveInUserAssumption()</a>, <a class="el" href="expr_8h_source.html#l01498">CVC3::Expr::setUserAssumption()</a>, and <a class="el" href="queryresult_8h_source.html#l00038">CVC3::UNKNOWN</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l01102">newUserAssumption()</a>.</p>
</div>
</div>
<a class="anchor" id="a40df6c2ecc6cf95be36169849da3fd3a"></a><!-- doxytag: member="CVC3::SearchSat::getName" ref="a40df6c2ecc6cf95be36169849da3fd3a" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual const std::string& CVC3::SearchSat::getName </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Name of this search engine. </p>
<p>Implements <a class="el" href="group__SE.html#ga942b3cc50f5ea9da1b3117ee23eff9c2">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00268">268</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>References <a class="el" href="search__sat_8h_source.html#l00043">d_name</a>.</p>
</div>
</div>
<a class="anchor" id="a2ca4a66d1bf7d0227e646edd3c9b9964"></a><!-- doxytag: member="CVC3::SearchSat::registerAtom" ref="a2ca4a66d1bf7d0227e646edd3c9b9964" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchSat::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><code> [virtual]</code></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__sat_8cpp_source.html#l01002">1002</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="expr_8h_source.html#l01378">CVC3::Expr::isRegisteredAtom()</a>, <a class="el" href="theory__core_8cpp_source.html#l03541">CVC3::TheoryCore::registerAtom()</a>, and <a class="el" href="expr_8h_source.html#l01523">CVC3::Expr::setUserRegisteredAtom()</a>.</p>
</div>
</div>
<a class="anchor" id="a737cf8f3791197c405017db18163ce6b"></a><!-- doxytag: member="CVC3::SearchSat::getImpliedLiteral" ref="a737cf8f3791197c405017db18163ce6b" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchSat::getImpliedLiteral </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [virtual]</code></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__sat_8cpp_source.html#l01010">1010</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__sat_8h_source.html#l00151">d_nextImpliedLiteral</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theory__core_8cpp_source.html#l03582">CVC3::TheoryCore::getImpliedLiteralByIndex()</a>, <a class="el" href="expr_8h_source.html#l01374">CVC3::Expr::isUserRegisteredAtom()</a>, and <a class="el" href="expr_8h_source.html#l00506">CVC3::Expr::unnegate()</a>.</p>
</div>
</div>
<a class="anchor" id="a9f129c2415d3eef0d73ad6d98ff13d44"></a><!-- doxytag: member="CVC3::SearchSat::push" ref="a9f129c2415d3eef0d73ad6d98ff13d44" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::SearchSat::push </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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__sat_8h_source.html#l00271">271</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>References <a class="el" href="search__sat_8h_source.html#l00067">d_dpllt</a>, and <a class="el" href="classSAT_1_1DPLLT.html#aa074d69f0937b579b5f6cfefabadd083">SAT::DPLLT::push()</a>.</p>
</div>
</div>
<a class="anchor" id="a5c3eeec4b2c970f9d503b2892c9eb770"></a><!-- doxytag: member="CVC3::SearchSat::pop" ref="a5c3eeec4b2c970f9d503b2892c9eb770" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::SearchSat::pop </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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__sat_8h_source.html#l00272">272</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>References <a class="el" href="search__sat_8h_source.html#l00067">d_dpllt</a>, and <a class="el" href="classSAT_1_1DPLLT.html#a59925cdeed3751c4fe4b5d759ebd755c">SAT::DPLLT::pop()</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l01022">returnFromCheck()</a>.</p>
</div>
</div>
<a class="anchor" id="a2921a84d2f2f33413ccda78789f40147"></a><!-- doxytag: member="CVC3::SearchSat::checkValid" ref="a2921a84d2f2f33413ccda78789f40147" args="(const Expr &e, Theorem &result)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> CVC3::SearchSat::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><code> [inline, virtual]</code></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><dt><b>Parameters:</b></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>Implements <a class="el" href="group__SE.html#ga34a9133f5342719526863d24cd1a0fcc">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00273">273</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>References <a class="el" href="search__sat_8cpp_source.html#l00638">check()</a>.</p>
</div>
</div>
<a class="anchor" id="ae7bf52f7780c6f2e085cf23c507fc3e1"></a><!-- doxytag: member="CVC3::SearchSat::restart" ref="ae7bf52f7780c6f2e085cf23c507fc3e1" args="(const Expr &e, Theorem &result)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> CVC3::SearchSat::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><code> [inline, virtual]</code></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><dt><b>Parameters:</b></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>Implements <a class="el" href="group__SE.html#ga715936653b5bef3e3d9fd2a8a873bafd">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00275">275</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>References <a class="el" href="search__sat_8cpp_source.html#l00638">check()</a>.</p>
</div>
</div>
<a class="anchor" id="a43a09dbf7232bfdb6f10aee4df1add94"></a><!-- doxytag: member="CVC3::SearchSat::returnFromCheck" ref="a43a09dbf7232bfdb6f10aee4df1add94" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchSat::returnFromCheck </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [virtual]</code></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__sat_8cpp_source.html#l01022">1022</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="search__sat_8h_source.html#l00046">d_bottomScope</a>, and <a class="el" href="search__sat_8h_source.html#l00272">pop()</a>.</p>
</div>
</div>
<a class="anchor" id="a0828289ad2b19cc7fac453b41287ca50"></a><!-- doxytag: member="CVC3::SearchSat::lastThm" ref="a0828289ad2b19cc7fac453b41287ca50" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::SearchSat::lastThm </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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__sat_8h_source.html#l00278">278</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>References <a class="el" href="search__sat_8h_source.html#l00053">d_lastValid</a>.</p>
</div>
</div>
<a class="anchor" id="a859331cc6fc93adfdd09cb848cd6de0b"></a><!-- doxytag: member="CVC3::SearchSat::newUserAssumption" ref="a859331cc6fc93adfdd09cb848cd6de0b" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchSat::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><code> [virtual]</code></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>Implements <a class="el" href="group__SE.html#ga5782663fc8ae00ec2965506c8ba65a86">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l01102">1102</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="classSAT_1_1DPLLT.html#aaaa6884de9ebd8b9596e85167e8f9273">SAT::DPLLT::addAssertion()</a>, <a class="el" href="search__sat_8h_source.html#l00067">d_dpllt</a>, and <a class="el" href="search__sat_8cpp_source.html#l01064">newUserAssumptionInt()</a>.</p>
</div>
</div>
<a class="anchor" id="a7344ad67225c0d6e30f8c2215bc7e0b0"></a><!-- doxytag: member="CVC3::SearchSat::getUserAssumptions" ref="a7344ad67225c0d6e30f8c2215bc7e0b0" args="(std::vector< Expr > &assumptions)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchSat::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><code> [virtual]</code></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><dt><b>Parameters:</b></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#ga43f52699cddc6e0feffffaf22424fe47">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l01111">1111</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="cdlist_8h_source.html#l00088">CVC3::CDList< T >::begin()</a>, <a class="el" href="search__sat_8h_source.html#l00056">d_userAssumptions</a>, and <a class="el" href="cdlist_8h_source.html#l00091">CVC3::CDList< T >::end()</a>.</p>
</div>
</div>
<a class="anchor" id="acee513ead4033fd5bfc16cbab7951dc7"></a><!-- doxytag: member="CVC3::SearchSat::getInternalAssumptions" ref="acee513ead4033fd5bfc16cbab7951dc7" args="(std::vector< Expr > &assumptions)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchSat::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><code> [virtual]</code></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><dt><b>Parameters:</b></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__sat_8cpp_source.html#l01119">1119</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="cdlist_8h_source.html#l00088">CVC3::CDList< T >::begin()</a>, <a class="el" href="search__sat_8h_source.html#l00059">d_intAssumptions</a>, and <a class="el" href="cdlist_8h_source.html#l00091">CVC3::CDList< T >::end()</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l01169">getCounterExample()</a>.</p>
</div>
</div>
<a class="anchor" id="a63ffdace5647b9d783e4a4a0dd90fb0b"></a><!-- doxytag: member="CVC3::SearchSat::getAssumptions" ref="a63ffdace5647b9d783e4a4a0dd90fb0b" args="(std::vector< Expr > &assumptions)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchSat::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><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Get all assumptions made in this and all previous contexts. </p>
<dl><dt><b>Parameters:</b></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__sat_8cpp_source.html#l01128">1128</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="cdlist_8h_source.html#l00088">CVC3::CDList< T >::begin()</a>, <a class="el" href="search__sat_8h_source.html#l00059">d_intAssumptions</a>, <a class="el" href="search__sat_8h_source.html#l00056">d_userAssumptions</a>, <a class="el" href="cdlist_8h_source.html#l00091">CVC3::CDList< T >::end()</a>, and <a class="el" href="expr_8h_source.html#l01354">CVC3::Expr::isUserAssumption()</a>.</p>
</div>
</div>
<a class="anchor" id="a4ec713d6bbbd5d4bd6a9fcacc42a044e"></a><!-- doxytag: member="CVC3::SearchSat::isAssumption" ref="a4ec713d6bbbd5d4bd6a9fcacc42a044e" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool SearchSat::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><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Check if the formula has already been assumed previously. </p>
<p>Implements <a class="el" href="group__SE.html#ga20730f5acacc4b18d29031632d88904c">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l01163">1163</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01362">CVC3::Expr::isIntAssumption()</a>, and <a class="el" href="expr_8h_source.html#l01354">CVC3::Expr::isUserAssumption()</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l01064">newUserAssumptionInt()</a>.</p>
</div>
</div>
<a class="anchor" id="af2296bfb7f363cb9b83ca2fa6042d496"></a><!-- doxytag: member="CVC3::SearchSat::getCounterExample" ref="af2296bfb7f363cb9b83ca2fa6042d496" args="(std::vector< Expr > &assertions, bool inOrder=true)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchSat::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><code> [virtual]</code></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><dt><b>Parameters:</b></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__sat_8cpp_source.html#l01169">1169</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="search__sat_8h_source.html#l00053">d_lastValid</a>, <a class="el" href="cdo_8h_source.html#l00064">CVC3::CDO< T >::get()</a>, <a class="el" href="search__sat_8cpp_source.html#l01119">getInternalAssumptions()</a>, and <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>.</p>
</div>
</div>
<a class="anchor" id="aa8b7c9812f7f61fc567c502ef3240d85"></a><!-- doxytag: member="CVC3::SearchSat::getProof" ref="aa8b7c9812f7f61fc567c502ef3240d85" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Proof.html">Proof</a> SearchSat::getProof </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [virtual]</code></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>Implements <a class="el" href="group__SE.html#gaa0ce3839d5f7b64168d62ff5eb59cf1f">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l01178">1178</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__sat_8h_source.html#l00053">d_lastValid</a>, <a class="el" href="cdo_8h_source.html#l00064">CVC3::CDO< T >::get()</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="ad3267f576f114e049609a8c3c4f01118"></a><!-- doxytag: member="CVC3::SearchSat::getValue" ref="ad3267f576f114e049609a8c3c4f01118" args="(const CVC3::Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bf">FormulaValue</a> CVC3::SearchSat::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><code> [inline, virtual]</code></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__sat_8h_source.html#l00289">289</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>References <a class="el" href="search__sat_8h_source.html#l00079">d_cnfManager</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="formula__value_8h_source.html#l00033">CVC3::FALSE_VAL</a>, <a class="el" href="cnf_8h_source.html#l00037">SAT::Var::FALSE_VAL</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="cnf__manager_8h_source.html#l00236">SAT::CNF_Manager::getCNFLit()</a>, <a class="el" href="search__sat_8h_source.html#l00214">getValue()</a>, <a class="el" href="cnf_8h_source.html#l00063">SAT::Lit::isNull()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="formula__value_8h_source.html#l00032">CVC3::TRUE_VAL</a>, <a class="el" href="cnf_8h_source.html#l00037">SAT::Var::TRUE_VAL</a>, <a class="el" href="cnf_8h_source.html#l00037">SAT::Var::UNKNOWN</a>, and <a class="el" href="formula__value_8h_source.html#l00034">CVC3::UNKNOWN_VAL</a>.</p>
</div>
</div>
<hr/><h2>Friends And Related Function Documentation</h2>
<a class="anchor" id="aa9f952c8606458f1e777d9a05b11550d"></a><!-- doxytag: member="CVC3::SearchSat::Restorer" ref="aa9f952c8606458f1e777d9a05b11550d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1SearchSat_1_1Restorer.html">Restorer</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Helper class for resetting DPLLT engine. </p>
<p>We need to be notified when the scope goes below the scope from which the last invalid call to checkValid originated. This helper class ensures that this happens. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00158">158</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<a class="anchor" id="a71c71132ecb225ad44dd66fc2c3505f3"></a><!-- doxytag: member="CVC3::SearchSat::SearchSatCoreSatAPI" ref="a71c71132ecb225ad44dd66fc2c3505f3" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1SearchSatCoreSatAPI.html">SearchSatCoreSatAPI</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00179">179</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l00936">SearchSat()</a>.</p>
</div>
</div>
<a class="anchor" id="acfd18b3733ce33513e1e5ddaad615624"></a><!-- doxytag: member="CVC3::SearchSat::SearchSatCNFCallback" ref="acfd18b3733ce33513e1e5ddaad615624" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1SearchSatCNFCallback.html">SearchSatCNFCallback</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00180">180</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l00936">SearchSat()</a>.</p>
</div>
</div>
<a class="anchor" id="a8cb09d5d17839a0377e369713fcbbedf"></a><!-- doxytag: member="CVC3::SearchSat::SearchSatTheoryAPI" ref="a8cb09d5d17839a0377e369713fcbbedf" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1SearchSatTheoryAPI.html">SearchSatTheoryAPI</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00188">188</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l00936">SearchSat()</a>.</p>
</div>
</div>
<a class="anchor" id="a447de240c99ed9d998d211b07609bc5d"></a><!-- doxytag: member="CVC3::SearchSat::SearchSatDecider" ref="a447de240c99ed9d998d211b07609bc5d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1SearchSatDecider.html">SearchSatDecider</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00200">200</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l00936">SearchSat()</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="ab7dd09d7a8ea0c87e2e1ec42a837160b"></a><!-- doxytag: member="CVC3::SearchSat::d_name" ref="ab7dd09d7a8ea0c87e2e1ec42a837160b" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string <a class="el" href="classCVC3_1_1SearchSat.html#ab7dd09d7a8ea0c87e2e1ec42a837160b">CVC3::SearchSat::d_name</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Name of search engine. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00043">43</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8h_source.html#l00268">getName()</a>.</p>
</div>
</div>
<a class="anchor" id="a8153b8d7b772217bafddf3d92be4759b"></a><!-- doxytag: member="CVC3::SearchSat::d_bottomScope" ref="a8153b8d7b772217bafddf3d92be4759b" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><int> <a class="el" href="classCVC3_1_1SearchSat.html#a8153b8d7b772217bafddf3d92be4759b">CVC3::SearchSat::d_bottomScope</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Bottom scope for current query. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00046">46</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8h_source.html#l00184">getBottomScope()</a>, <a class="el" href="search__sat_8cpp_source.html#l01064">newUserAssumptionInt()</a>, and <a class="el" href="search__sat_8cpp_source.html#l01022">returnFromCheck()</a>.</p>
</div>
</div>
<a class="anchor" id="ac318c6520fbea766517991127affaafc"></a><!-- doxytag: member="CVC3::SearchSat::d_lastCheck" ref="ac318c6520fbea766517991127affaafc" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><<a class="el" href="classCVC3_1_1Expr.html">Expr</a>> <a class="el" href="classCVC3_1_1SearchSat.html#ac318c6520fbea766517991127affaafc">CVC3::SearchSat::d_lastCheck</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Last expr checked for validity. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00049">49</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<a class="anchor" id="ab41637f4522c5e3f318993392adf84bb"></a><!-- doxytag: member="CVC3::SearchSat::d_lastValid" ref="ab41637f4522c5e3f318993392adf84bb" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><<a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>> <a class="el" href="classCVC3_1_1SearchSat.html#ab41637f4522c5e3f318993392adf84bb">CVC3::SearchSat::d_lastValid</a><code> [private]</code></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__sat_8h_source.html#l00053">53</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l01169">getCounterExample()</a>, <a class="el" href="search__sat_8cpp_source.html#l01178">getProof()</a>, and <a class="el" href="search__sat_8h_source.html#l00278">lastThm()</a>.</p>
</div>
</div>
<a class="anchor" id="a3b9b2371a24908e62ec71b6f141afea8"></a><!-- doxytag: member="CVC3::SearchSat::d_userAssumptions" ref="a3b9b2371a24908e62ec71b6f141afea8" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDList.html">CDList</a><<a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>> <a class="el" href="classCVC3_1_1SearchSat.html#a3b9b2371a24908e62ec71b6f141afea8">CVC3::SearchSat::d_userAssumptions</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>List of all user assumptions. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00056">56</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l01128">getAssumptions()</a>, <a class="el" href="search__sat_8cpp_source.html#l01111">getUserAssumptions()</a>, and <a class="el" href="search__sat_8cpp_source.html#l01064">newUserAssumptionInt()</a>.</p>
</div>
</div>
<a class="anchor" id="ad3b9879d655cf3fce1a70de7b1d6fedc"></a><!-- doxytag: member="CVC3::SearchSat::d_intAssumptions" ref="ad3b9879d655cf3fce1a70de7b1d6fedc" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDList.html">CDList</a><<a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>> <a class="el" href="classCVC3_1_1SearchSat.html#ad3b9879d655cf3fce1a70de7b1d6fedc">CVC3::SearchSat::d_intAssumptions</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>List of all internal assumptions. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00059">59</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l01128">getAssumptions()</a>, and <a class="el" href="search__sat_8cpp_source.html#l01119">getInternalAssumptions()</a>.</p>
</div>
</div>
<a class="anchor" id="a23b0c38d89ce24f463f2c2fc929df879"></a><!-- doxytag: member="CVC3::SearchSat::d_idxUserAssump" ref="a23b0c38d89ce24f463f2c2fc929df879" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><unsigned> <a class="el" href="classCVC3_1_1SearchSat.html#a23b0c38d89ce24f463f2c2fc929df879">CVC3::SearchSat::d_idxUserAssump</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Index to where unprocessed assumptions start. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00062">62</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<a class="anchor" id="aab55d9ceeb2a938841230c920762ba77"></a><!-- doxytag: member="CVC3::SearchSat::d_coreSatAPI" ref="aab55d9ceeb2a938841230c920762ba77" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoryCore_1_1CoreSatAPI.html">TheoryCore::CoreSatAPI</a>* <a class="el" href="classCVC3_1_1SearchSat.html#aab55d9ceeb2a938841230c920762ba77">CVC3::SearchSat::d_coreSatAPI</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00064">64</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l00936">SearchSat()</a>, and <a class="el" href="search__sat_8cpp_source.html#l00991">~SearchSat()</a>.</p>
</div>
</div>
<a class="anchor" id="a884c103ef1313d56a3a42d4e3e8468cb"></a><!-- doxytag: member="CVC3::SearchSat::d_dpllt" ref="a884c103ef1313d56a3a42d4e3e8468cb" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1DPLLT.html">SAT::DPLLT</a>* <a class="el" href="classCVC3_1_1SearchSat.html#a884c103ef1313d56a3a42d4e3e8468cb">CVC3::SearchSat::d_dpllt</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Pointer to DPLLT implementation. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00067">67</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l01102">newUserAssumption()</a>, <a class="el" href="search__sat_8h_source.html#l00272">pop()</a>, <a class="el" href="search__sat_8h_source.html#l00271">push()</a>, <a class="el" href="search__sat_8cpp_source.html#l00936">SearchSat()</a>, and <a class="el" href="search__sat_8cpp_source.html#l00991">~SearchSat()</a>.</p>
</div>
</div>
<a class="anchor" id="a8abc1b647affa60cc367e0eeaa52cdf4"></a><!-- doxytag: member="CVC3::SearchSat::d_theoryAPI" ref="a8abc1b647affa60cc367e0eeaa52cdf4" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">SAT::DPLLT::TheoryAPI</a>* <a class="el" href="classCVC3_1_1SearchSat.html#a8abc1b647affa60cc367e0eeaa52cdf4">CVC3::SearchSat::d_theoryAPI</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implementation of TheoryAPI for DPLLT. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00070">70</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l00936">SearchSat()</a>, and <a class="el" href="search__sat_8cpp_source.html#l00991">~SearchSat()</a>.</p>
</div>
</div>
<a class="anchor" id="aa4be1d02557a46fbbdc32deefc4f3a32"></a><!-- doxytag: member="CVC3::SearchSat::d_decider" ref="aa4be1d02557a46fbbdc32deefc4f3a32" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1DPLLT_1_1Decider.html">SAT::DPLLT::Decider</a>* <a class="el" href="classCVC3_1_1SearchSat.html#aa4be1d02557a46fbbdc32deefc4f3a32">CVC3::SearchSat::d_decider</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implementation of Decider for DPLLT. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00073">73</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l00936">SearchSat()</a>, and <a class="el" href="search__sat_8cpp_source.html#l00991">~SearchSat()</a>.</p>
</div>
</div>
<a class="anchor" id="a3e6b8d2d1d9513329fbbb80464053b39"></a><!-- doxytag: member="CVC3::SearchSat::d_theorems" ref="a3e6b8d2d1d9513329fbbb80464053b39" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDMap.html">CDMap</a><<a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>> <a class="el" href="classCVC3_1_1SearchSat.html#a3e6b8d2d1d9513329fbbb80464053b39">CVC3::SearchSat::d_theorems</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Store of theorems for expressions sent to DPLLT. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00076">76</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<a class="anchor" id="a996335737d383fd882b6f1085f72b964"></a><!-- doxytag: member="CVC3::SearchSat::d_cnfManager" ref="a996335737d383fd882b6f1085f72b964" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1CNF__Manager.html">SAT::CNF_Manager</a>* <a class="el" href="classCVC3_1_1SearchSat.html#a996335737d383fd882b6f1085f72b964">CVC3::SearchSat::d_cnfManager</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Manages CNF formula and its relationship to original Exprs and Theorems. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00079">79</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8h_source.html#l00241">checkJustified()</a>, <a class="el" href="search__sat_8h_source.html#l00289">getValue()</a>, <a class="el" href="search__sat_8cpp_source.html#l01064">newUserAssumptionInt()</a>, <a class="el" href="search__sat_8cpp_source.html#l01042">newUserAssumptionIntHelper()</a>, <a class="el" href="search__sat_8cpp_source.html#l00936">SearchSat()</a>, <a class="el" href="search__sat_8h_source.html#l00245">setJustified()</a>, and <a class="el" href="search__sat_8cpp_source.html#l00991">~SearchSat()</a>.</p>
</div>
</div>
<a class="anchor" id="a158485ff14b490fc2c91936a4e72bf5b"></a><!-- doxytag: member="CVC3::SearchSat::d_cnfCallback" ref="a158485ff14b490fc2c91936a4e72bf5b" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html">SAT::CNF_Manager::CNFCallback</a>* <a class="el" href="classCVC3_1_1SearchSat.html#a158485ff14b490fc2c91936a4e72bf5b">CVC3::SearchSat::d_cnfCallback</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Callback for CNF_Manager. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00082">82</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l00936">SearchSat()</a>, and <a class="el" href="search__sat_8cpp_source.html#l00991">~SearchSat()</a>.</p>
</div>
</div>
<a class="anchor" id="a455c295a13215ddc99b8df18f4598af4"></a><!-- doxytag: member="CVC3::SearchSat::d_vars" ref="a455c295a13215ddc99b8df18f4598af4" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">SAT::Var::Val</a>> <a class="el" href="classCVC3_1_1SearchSat.html#a455c295a13215ddc99b8df18f4598af4">CVC3::SearchSat::d_vars</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Cached values of variables. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00085">85</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8h_source.html#l00214">getValue()</a>, <a class="el" href="search__sat_8cpp_source.html#l01064">newUserAssumptionInt()</a>, and <a class="el" href="search__sat_8h_source.html#l00229">setValue()</a>.</p>
</div>
</div>
<a class="anchor" id="a00573a594dd2b83cbb6f2997516862d3"></a><!-- doxytag: member="CVC3::SearchSat::d_inCheckSat" ref="a00573a594dd2b83cbb6f2997516862d3" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1SearchSat.html#a00573a594dd2b83cbb6f2997516862d3">CVC3::SearchSat::d_inCheckSat</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Whether we are currently in a call to dpllt->checkSat. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00088">88</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l01064">newUserAssumptionInt()</a>.</p>
</div>
</div>
<a class="anchor" id="aed781537ef3315ffa019cdd7f02f0f8e"></a><!-- doxytag: member="CVC3::SearchSat::d_lemmas" ref="aed781537ef3315ffa019cdd7f02f0f8e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1CD__CNF__Formula.html">SAT::CD_CNF_Formula</a> <a class="el" href="classCVC3_1_1SearchSat.html#aed781537ef3315ffa019cdd7f02f0f8e">CVC3::SearchSat::d_lemmas</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>CNF Formula used for theory lemmas. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00091">91</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<a class="anchor" id="a3997be227d7cd36e1f29f71a683f1428"></a><!-- doxytag: member="CVC3::SearchSat::d_pendingLemmas" ref="a3997be227d7cd36e1f29f71a683f1428" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<std::pair<<a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>, int> > <a class="el" href="classCVC3_1_1SearchSat.html#a3997be227d7cd36e1f29f71a683f1428">CVC3::SearchSat::d_pendingLemmas</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Lemmas waiting to be translated since last call to <a class="el" href="classCVC3_1_1SearchSat.html#a858da2f6e8aefe2aeb124eececd45e3a" title="DPLLT callback to get more general theory clauses.">getNewClauses()</a> </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00094">94</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<a class="anchor" id="a83bb96cd69f2673e370e536a7946c5c3"></a><!-- doxytag: member="CVC3::SearchSat::d_pendingScopes" ref="a83bb96cd69f2673e370e536a7946c5c3" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<bool> <a class="el" href="classCVC3_1_1SearchSat.html#a83bb96cd69f2673e370e536a7946c5c3">CVC3::SearchSat::d_pendingScopes</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><a class="el" href="classCVC3_1_1Scope.html">Scope</a> parameter for lemmas waiting to be translated since last call to <a class="el" href="classCVC3_1_1SearchSat.html#a858da2f6e8aefe2aeb124eececd45e3a" title="DPLLT callback to get more general theory clauses.">getNewClauses()</a> </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00097">97</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<a class="anchor" id="ab309591a57e34a9166c3baa056e2857f"></a><!-- doxytag: member="CVC3::SearchSat::d_pendingLemmasSize" ref="ab309591a57e34a9166c3baa056e2857f" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><unsigned> <a class="el" href="classCVC3_1_1SearchSat.html#ab309591a57e34a9166c3baa056e2857f">CVC3::SearchSat::d_pendingLemmasSize</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Backtracking size of d_pendingLemmas. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00100">100</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<a class="anchor" id="a8de03d523c9b0304eb95e72ec923274b"></a><!-- doxytag: member="CVC3::SearchSat::d_pendingLemmasNext" ref="a8de03d523c9b0304eb95e72ec923274b" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><unsigned> <a class="el" href="classCVC3_1_1SearchSat.html#a8de03d523c9b0304eb95e72ec923274b">CVC3::SearchSat::d_pendingLemmasNext</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Backtracking next item in d_pendingLemmas. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00103">103</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<a class="anchor" id="a819ee9729fd633651eb2cf27f7175d8a"></a><!-- doxytag: member="CVC3::SearchSat::d_lemmasNext" ref="a819ee9729fd633651eb2cf27f7175d8a" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><unsigned> <a class="el" href="classCVC3_1_1SearchSat.html#a819ee9729fd633651eb2cf27f7175d8a">CVC3::SearchSat::d_lemmasNext</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Current position in d_lemmas. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00106">106</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<a class="anchor" id="a78ea4f3b48395a88f42bb4db58c44541"></a><!-- doxytag: member="CVC3::SearchSat::d_varsUndoList" ref="a78ea4f3b48395a88f42bb4db58c44541" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<unsigned> <a class="el" href="classCVC3_1_1SearchSat.html#a78ea4f3b48395a88f42bb4db58c44541">CVC3::SearchSat::d_varsUndoList</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>List for backtracking var values. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00109">109</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8h_source.html#l00229">setValue()</a>.</p>
</div>
</div>
<a class="anchor" id="a6c7fadcd8cd61189c6c3c38a28035993"></a><!-- doxytag: member="CVC3::SearchSat::d_varsUndoListSize" ref="a6c7fadcd8cd61189c6c3c38a28035993" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><unsigned> <a class="el" href="classCVC3_1_1SearchSat.html#a6c7fadcd8cd61189c6c3c38a28035993">CVC3::SearchSat::d_varsUndoListSize</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Backtracking size of d_varsUndoList. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00112">112</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8h_source.html#l00229">setValue()</a>.</p>
</div>
</div>
<a class="anchor" id="ab4dbd42cf98469a2abb679024a402b77"></a><!-- doxytag: member="CVC3::SearchSat::d_prioritySet" ref="ab4dbd42cf98469a2abb679024a402b77" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::set<<a class="el" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html">LitPriorityPair</a>> <a class="el" href="classCVC3_1_1SearchSat.html#ab4dbd42cf98469a2abb679024a402b77">CVC3::SearchSat::d_prioritySet</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Used to determine order to find splitters. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00131">131</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l00936">SearchSat()</a>.</p>
</div>
</div>
<a class="anchor" id="ad7b3c57fadbc655bddd204b9ea122a62"></a><!-- doxytag: member="CVC3::SearchSat::d_prioritySetStart" ref="ad7b3c57fadbc655bddd204b9ea122a62" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><std::set<<a class="el" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html">LitPriorityPair</a>>::const_iterator> <a class="el" href="classCVC3_1_1SearchSat.html#ad7b3c57fadbc655bddd204b9ea122a62">CVC3::SearchSat::d_prioritySetStart</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Current position in prioritySet. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00133">133</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l00936">SearchSat()</a>.</p>
</div>
</div>
<a class="anchor" id="a3495b7cac1dc81f07f54dc8d0b17b17a"></a><!-- doxytag: member="CVC3::SearchSat::d_prioritySetEntriesSize" ref="a3495b7cac1dc81f07f54dc8d0b17b17a" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><unsigned> <a class="el" href="classCVC3_1_1SearchSat.html#a3495b7cac1dc81f07f54dc8d0b17b17a">CVC3::SearchSat::d_prioritySetEntriesSize</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Backtracking size of priority set entries. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00135">135</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<a class="anchor" id="ab57f9f48af74c9a6493986b8cb0c720d"></a><!-- doxytag: member="CVC3::SearchSat::d_prioritySetEntries" ref="ab57f9f48af74c9a6493986b8cb0c720d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<std::set<<a class="el" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html">LitPriorityPair</a>>::iterator> <a class="el" href="classCVC3_1_1SearchSat.html#ab57f9f48af74c9a6493986b8cb0c720d">CVC3::SearchSat::d_prioritySetEntries</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Entries in priority set in insertion order (so set can be backtracked) </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00137">137</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<a class="anchor" id="a99063dd2470eae948fa85d460a9b3868"></a><!-- doxytag: member="CVC3::SearchSat::d_prioritySetBottomEntriesSizeStack" ref="a99063dd2470eae948fa85d460a9b3868" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<unsigned> <a class="el" href="classCVC3_1_1SearchSat.html#a99063dd2470eae948fa85d460a9b3868">CVC3::SearchSat::d_prioritySetBottomEntriesSizeStack</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Backtracking size of priority set entries at bottom scope. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00139">139</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<a class="anchor" id="ab8e5996fd3e75c5b3c45f611d3639535"></a><!-- doxytag: member="CVC3::SearchSat::d_prioritySetBottomEntriesSize" ref="ab8e5996fd3e75c5b3c45f611d3639535" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned <a class="el" href="classCVC3_1_1SearchSat.html#ab8e5996fd3e75c5b3c45f611d3639535">CVC3::SearchSat::d_prioritySetBottomEntriesSize</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Current size of bottom entries. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00141">141</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<a class="anchor" id="a6d963065a2df65795626cf6d70f8fe99"></a><!-- doxytag: member="CVC3::SearchSat::d_prioritySetBottomEntries" ref="a6d963065a2df65795626cf6d70f8fe99" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<std::set<<a class="el" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html">LitPriorityPair</a>>::iterator> <a class="el" href="classCVC3_1_1SearchSat.html#a6d963065a2df65795626cf6d70f8fe99">CVC3::SearchSat::d_prioritySetBottomEntries</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Entries in priority set in insertion order (so set can be backtracked) </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00143">143</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<a class="anchor" id="a217f464659b186330934d046aa7cc764"></a><!-- doxytag: member="CVC3::SearchSat::d_lastRegisteredVar" ref="a217f464659b186330934d046aa7cc764" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><unsigned> <a class="el" href="classCVC3_1_1SearchSat.html#a217f464659b186330934d046aa7cc764">CVC3::SearchSat::d_lastRegisteredVar</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Last Var registered with core theory. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00146">146</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<a class="anchor" id="af0953025654043f6f76040df7abf2658"></a><!-- doxytag: member="CVC3::SearchSat::d_dplltReady" ref="af0953025654043f6f76040df7abf2658" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><bool> <a class="el" href="classCVC3_1_1SearchSat.html#af0953025654043f6f76040df7abf2658">CVC3::SearchSat::d_dplltReady</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Whether it's OK to call DPLLT solver from the current scope. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00149">149</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<a class="anchor" id="ae97f61c9a0ae9ed8186929e15892ad73"></a><!-- doxytag: member="CVC3::SearchSat::d_nextImpliedLiteral" ref="ae97f61c9a0ae9ed8186929e15892ad73" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><unsigned> <a class="el" href="classCVC3_1_1SearchSat.html#ae97f61c9a0ae9ed8186929e15892ad73">CVC3::SearchSat::d_nextImpliedLiteral</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00151">151</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l01010">getImpliedLiteral()</a>.</p>
</div>
</div>
<a class="anchor" id="a5b7313c3933e04b894089b1c2e09c57e"></a><!-- doxytag: member="CVC3::SearchSat::d_restorer" ref="a5b7313c3933e04b894089b1c2e09c57e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1SearchSat_1_1Restorer.html">Restorer</a> <a class="el" href="classCVC3_1_1SearchSat.html#a5b7313c3933e04b894089b1c2e09c57e">CVC3::SearchSat::d_restorer</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Instance of <a class="el" href="classCVC3_1_1SearchSat_1_1Restorer.html">Restorer</a> class. </p>
<p>Definition at line <a class="el" href="search__sat_8h_source.html#l00168">168</a> of file <a class="el" href="search__sat_8h_source.html">search_sat.h</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="search__sat_8h_source.html">search_sat.h</a></li>
<li><a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a></li>
</ul>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
