<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: CVC3::SearchSatTheoryAPI Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li 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="inherits.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_1SearchSatTheoryAPI.html">SearchSatTheoryAPI</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> |
<a href="classCVC3_1_1SearchSatTheoryAPI-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">CVC3::SearchSatTheoryAPI Class Reference</div> </div>
</div><!--header-->
<div class="contents">
<p>Inherits <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">SAT::DPLLT::TheoryAPI</a>.</p>
<div class="dynheader">
Collaboration diagram for CVC3::SearchSatTheoryAPI:</div>
<div class="dyncontent">
<div class="center"><img src="classCVC3_1_1SearchSatTheoryAPI__coll__graph.gif" border="0" usemap="#CVC3_1_1SearchSatTheoryAPI_coll__map" alt="Collaboration graph"/></div>
<map name="CVC3_1_1SearchSatTheoryAPI_coll__map" id="CVC3_1_1SearchSatTheoryAPI_coll__map">
</map>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-methods"></a>
Public Member Functions</h2></td></tr>
<tr class="memitem:ae37ebadf06bdc0116ff7850bc2ea5dc6"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1SearchSatTheoryAPI.html#ae37ebadf06bdc0116ff7850bc2ea5dc6">SearchSatTheoryAPI</a> (<a class="el" href="classCVC3_1_1SearchSat.html">SearchSat</a> *ss)</td></tr>
<tr class="separator:ae37ebadf06bdc0116ff7850bc2ea5dc6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4fe19299e276955c5c2f653510b98ef3"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1SearchSatTheoryAPI.html#a4fe19299e276955c5c2f653510b98ef3">~SearchSatTheoryAPI</a> ()</td></tr>
<tr class="separator:a4fe19299e276955c5c2f653510b98ef3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab315cba0a7157225c0355b1136b511fc"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1SearchSatTheoryAPI.html#ab315cba0a7157225c0355b1136b511fc">push</a> ()</td></tr>
<tr class="memdesc:ab315cba0a7157225c0355b1136b511fc"><td class="mdescLeft"> </td><td class="mdescRight">Set a checkpoint for backtracking. <a href="#ab315cba0a7157225c0355b1136b511fc"></a><br/></td></tr>
<tr class="separator:ab315cba0a7157225c0355b1136b511fc"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a22e462ee6d70a81cdf6610921068c9ed"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1SearchSatTheoryAPI.html#a22e462ee6d70a81cdf6610921068c9ed">pop</a> ()</td></tr>
<tr class="memdesc:a22e462ee6d70a81cdf6610921068c9ed"><td class="mdescLeft"> </td><td class="mdescRight">Restore most recent checkpoint. <a href="#a22e462ee6d70a81cdf6610921068c9ed"></a><br/></td></tr>
<tr class="separator:a22e462ee6d70a81cdf6610921068c9ed"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a11363a1236f9d2520119a0d4533087a6"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1SearchSatTheoryAPI.html#a11363a1236f9d2520119a0d4533087a6">assertLit</a> (<a class="el" href="classSAT_1_1Lit.html">Lit</a> l)</td></tr>
<tr class="memdesc:a11363a1236f9d2520119a0d4533087a6"><td class="mdescLeft"> </td><td class="mdescRight">Notify theory when a literal is set to true. <a href="#a11363a1236f9d2520119a0d4533087a6"></a><br/></td></tr>
<tr class="separator:a11363a1236f9d2520119a0d4533087a6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5f294c37fc9ba581b542a0639e47865f"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classSAT_1_1DPLLT.html#ac612908684032ffe76ad97f04afd0ca8">SAT::DPLLT::ConsistentResult</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1SearchSatTheoryAPI.html#a5f294c37fc9ba581b542a0639e47865f">checkConsistent</a> (<a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf, bool fullEffort)</td></tr>
<tr class="memdesc:a5f294c37fc9ba581b542a0639e47865f"><td class="mdescLeft"> </td><td class="mdescRight">Check consistency of the current assignment. <a href="#a5f294c37fc9ba581b542a0639e47865f"></a><br/></td></tr>
<tr class="separator:a5f294c37fc9ba581b542a0639e47865f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aad2fecc1799c5b79199995cf02fcd3fb"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1SearchSatTheoryAPI.html#aad2fecc1799c5b79199995cf02fcd3fb">outOfResources</a> ()</td></tr>
<tr class="memdesc:aad2fecc1799c5b79199995cf02fcd3fb"><td class="mdescLeft"> </td><td class="mdescRight">Check if the work budget has been exceeded. <a href="#aad2fecc1799c5b79199995cf02fcd3fb"></a><br/></td></tr>
<tr class="separator:aad2fecc1799c5b79199995cf02fcd3fb"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a06f33ae2c4b9020c9dd5c05b4dc3345f"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classSAT_1_1Lit.html">Lit</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1SearchSatTheoryAPI.html#a06f33ae2c4b9020c9dd5c05b4dc3345f">getImplication</a> ()</td></tr>
<tr class="memdesc:a06f33ae2c4b9020c9dd5c05b4dc3345f"><td class="mdescLeft"> </td><td class="mdescRight">Get a literal that is implied by the current assignment. <a href="#a06f33ae2c4b9020c9dd5c05b4dc3345f"></a><br/></td></tr>
<tr class="separator:a06f33ae2c4b9020c9dd5c05b4dc3345f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5faff1f37c64447f406fbd6c377f6cd2"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1SearchSatTheoryAPI.html#a5faff1f37c64447f406fbd6c377f6cd2">getExplanation</a> (<a class="el" href="classSAT_1_1Lit.html">Lit</a> l, <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf)</td></tr>
<tr class="memdesc:a5faff1f37c64447f406fbd6c377f6cd2"><td class="mdescLeft"> </td><td class="mdescRight">Get an explanation for a literal that was implied. <a href="#a5faff1f37c64447f406fbd6c377f6cd2"></a><br/></td></tr>
<tr class="separator:a5faff1f37c64447f406fbd6c377f6cd2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2e715dfb82483c9a78e80eea7dbb97aa"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1SearchSatTheoryAPI.html#a2e715dfb82483c9a78e80eea7dbb97aa">getNewClauses</a> (<a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf)</td></tr>
<tr class="memdesc:a2e715dfb82483c9a78e80eea7dbb97aa"><td class="mdescLeft"> </td><td class="mdescRight">Get new clauses from the theory. <a href="#a2e715dfb82483c9a78e80eea7dbb97aa"></a><br/></td></tr>
<tr class="separator:a2e715dfb82483c9a78e80eea7dbb97aa"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="inherit_header pub_methods_classSAT_1_1DPLLT_1_1TheoryAPI"><td colspan="2" onclick="javascript:toggleInherit('pub_methods_classSAT_1_1DPLLT_1_1TheoryAPI')"><img src="closed.png" alt="-"/> Public Member Functions inherited from <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">SAT::DPLLT::TheoryAPI</a></td></tr>
<tr class="memitem:a87a03cac4fa22a6211ff22ff2bedefef inherit pub_methods_classSAT_1_1DPLLT_1_1TheoryAPI"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a87a03cac4fa22a6211ff22ff2bedefef">TheoryAPI</a> ()</td></tr>
<tr class="separator:a87a03cac4fa22a6211ff22ff2bedefef inherit pub_methods_classSAT_1_1DPLLT_1_1TheoryAPI"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a74605aae23f2c5b78c220bd37a02d6d0 inherit pub_methods_classSAT_1_1DPLLT_1_1TheoryAPI"><td class="memItemLeft" align="right" valign="top">virtual </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a74605aae23f2c5b78c220bd37a02d6d0">~TheoryAPI</a> ()</td></tr>
<tr class="separator:a74605aae23f2c5b78c220bd37a02d6d0 inherit pub_methods_classSAT_1_1DPLLT_1_1TheoryAPI"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-attribs"></a>
Private Attributes</h2></td></tr>
<tr class="memitem:a23c983838f09ca499abe23c09381292c"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ContextManager.html">ContextManager</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1SearchSatTheoryAPI.html#a23c983838f09ca499abe23c09381292c">d_cm</a></td></tr>
<tr class="separator:a23c983838f09ca499abe23c09381292c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac1c134629294189ad3728762588c51cd"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1SearchSat.html">SearchSat</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1SearchSatTheoryAPI.html#ac1c134629294189ad3728762588c51cd">d_ss</a></td></tr>
<tr class="separator:ac1c134629294189ad3728762588c51cd"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<a name="details" id="details"></a><h2 class="groupheader">Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00072">72</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
</div><h2 class="groupheader">Constructor & Destructor Documentation</h2>
<a class="anchor" id="ae37ebadf06bdc0116ff7850bc2ea5dc6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CVC3::SearchSatTheoryAPI::SearchSatTheoryAPI </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1SearchSat.html">SearchSat</a> * </td>
<td class="paramname"><em>ss</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00076">76</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a4fe19299e276955c5c2f653510b98ef3"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CVC3::SearchSatTheoryAPI::~SearchSatTheoryAPI </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00078">78</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Function Documentation</h2>
<a class="anchor" id="ab315cba0a7157225c0355b1136b511fc"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::SearchSatTheoryAPI::push </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Set a checkpoint for backtracking. </p>
<p>Implements <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a771e84ea6308cb7d3f7d02e7858b37db">SAT::DPLLT::TheoryAPI</a>.</p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00079">79</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a22e462ee6d70a81cdf6610921068c9ed"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::SearchSatTheoryAPI::pop </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Restore most recent checkpoint. </p>
<p>Implements <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a51a08aab04c2185513676a316aee14b4">SAT::DPLLT::TheoryAPI</a>.</p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00080">80</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a11363a1236f9d2520119a0d4533087a6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::SearchSatTheoryAPI::assertLit </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>l</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Notify theory when a literal is set to true. </p>
<p>Implements <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a3b3ef70567e0298cd3e971fd57d26fa6">SAT::DPLLT::TheoryAPI</a>.</p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00081">81</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a5f294c37fc9ba581b542a0639e47865f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1DPLLT.html#ac612908684032ffe76ad97f04afd0ca8">SAT::DPLLT::ConsistentResult</a> CVC3::SearchSatTheoryAPI::checkConsistent </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1CNF__Formula.html">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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Check consistency of the current assignment. </p>
<p>The result is either INCONSISTENT, MAYBE_CONSISTENT, or CONSISTENT Most of the time, fullEffort should be false, and the result will most likely be either INCONSISTENT or MAYBE_CONSISTENT. To force a full check, set fullEffort to true. When fullEffort is set to true, the only way the result can be MAYBE_CONSISTENT is if there are new clauses to get (via getNewClauses). </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">cnf</td><td>should be empty initially. If INCONSISTENT is returned, then cnf will contain one or more clauses ruling out the current assignment when it returns. Otherwise, cnf is unchanged. </td></tr>
<tr><td class="paramname">fullEffort</td><td>true for a full check, false for a fast check </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a4b3f4a97dbac21236e479a157d866545">SAT::DPLLT::TheoryAPI</a>.</p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00082">82</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="aad2fecc1799c5b79199995cf02fcd3fb"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::SearchSatTheoryAPI::outOfResources </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Check if the work budget has been exceeded. </p>
<p>If true, it means that the engine should quit and return ABORT. Otherwise, it should proceed normally. This should be checked regularly. </p>
<p>Implements <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a6484231750edf5bd9d10d9408c6b5a59">SAT::DPLLT::TheoryAPI</a>.</p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00084">84</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a06f33ae2c4b9020c9dd5c05b4dc3345f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1Lit.html">Lit</a> CVC3::SearchSatTheoryAPI::getImplication </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Get a literal that is implied by the current assignment. </p>
<p>This is theory propagation. It can be called repeatedly and returns a Null literal when there are no more literals to propagate. It should only be called when the assignment is not known to be inconsistent. </p>
<p>Implements <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#ad61236a10860b9771e1e09505ab501b5">SAT::DPLLT::TheoryAPI</a>.</p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00085">85</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a5faff1f37c64447f406fbd6c377f6cd2"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::SearchSatTheoryAPI::getExplanation </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Lit.html">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">CNF_Formula</a> & </td>
<td class="paramname"><em>c</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Get an explanation for a literal that was implied. </p>
<p>Given a literal l that is true in the current assignment as a result of an earlier call to <a class="el" href="classCVC3_1_1SearchSatTheoryAPI.html#a06f33ae2c4b9020c9dd5c05b4dc3345f" title="Get a literal that is implied by the current assignment.">getImplication()</a>, this method returns a set of clauses which justifies the propagation of that literal. The clauses will contain the literal l as well as other literals that are in the current assignment. The clauses are such that they would have propagated l via unit propagation at the time <a class="el" href="classCVC3_1_1SearchSatTheoryAPI.html#a06f33ae2c4b9020c9dd5c05b4dc3345f" title="Get a literal that is implied by the current assignment.">getImplication()</a> was called. </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">l</td><td>the literal </td></tr>
<tr><td class="paramname">c</td><td>should be empty initially. </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#ab7a85a15823cb0771d1e9bb4c0ce0703">SAT::DPLLT::TheoryAPI</a>.</p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00086">86</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a2e715dfb82483c9a78e80eea7dbb97aa"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::SearchSatTheoryAPI::getNewClauses </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> & </td>
<td class="paramname"><em>cnf</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Get new clauses from the theory. </p>
<p>This is extended theory learning. Returns false if there are no new clauses to get. Otherwise, returns true and new clauses are added to cnf. Note that the new clauses (if any) are theory lemmas, i.e. clauses that are valid in the theory and not dependent on the current assignment. The clauses may contain new literals as well as literals that are true in the current assignment. </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">cnf</td><td>should be empty initially. </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a7d4bf4b22f7e9f19174a4f2813294acd">SAT::DPLLT::TheoryAPI</a>.</p>
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00087">87</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Data Documentation</h2>
<a class="anchor" id="a23c983838f09ca499abe23c09381292c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ContextManager.html">ContextManager</a>* CVC3::SearchSatTheoryAPI::d_cm</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00073">73</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="ac1c134629294189ad3728762588c51cd"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1SearchSat.html">SearchSat</a>* CVC3::SearchSatTheoryAPI::d_ss</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="search__sat_8cpp_source.html#l00074">74</a> of file <a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following file:<ul>
<li><a class="el" href="search__sat_8cpp_source.html">search_sat.cpp</a></li>
</ul>
</div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:19 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
