<!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: SAT::CNF_Manager 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="namespaceSAT.html">SAT</a></li><li class="navelem"><a class="el" href="classSAT_1_1CNF__Manager.html">CNF_Manager</a></li> </ul>
</div>
</div><!-- top -->
<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="classSAT_1_1CNF__Manager-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">SAT::CNF_Manager Class Reference</div> </div>
</div><!--header-->
<div class="contents">
<p><code>#include <<a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>></code></p>
<div class="dynheader">
Collaboration diagram for SAT::CNF_Manager:</div>
<div class="dyncontent">
<div class="center"><img src="classSAT_1_1CNF__Manager__coll__graph.gif" border="0" usemap="#SAT_1_1CNF__Manager_coll__map" alt="Collaboration graph"/></div>
<map name="SAT_1_1CNF__Manager_coll__map" id="SAT_1_1CNF__Manager_coll__map">
</map>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="nested-classes"></a>
Classes</h2></td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html">CNFCallback</a></td></tr>
<tr class="memdesc:"><td class="mdescLeft"> </td><td class="mdescRight">Abstract class for callbacks. <a href="classSAT_1_1CNF__Manager_1_1CNFCallback.html#details">More...</a><br/></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">struct  </td><td class="memItemRight" valign="bottom"><a class="el" href="structSAT_1_1CNF__Manager_1_1Varinfo.html">Varinfo</a></td></tr>
<tr class="memdesc:"><td class="mdescLeft"> </td><td class="mdescRight">Information kept for each CNF variable. <a href="structSAT_1_1CNF__Manager_1_1Varinfo.html#details">More...</a><br/></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-methods"></a>
Public Member Functions</h2></td></tr>
<tr class="memitem:a7bb76ec26a37645bd0183715af69966f"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a7bb76ec26a37645bd0183715af69966f">CNF_Manager</a> (<a class="el" href="classCVC3_1_1TheoremManager.html">CVC3::TheoremManager</a> *tm, <a class="el" href="classCVC3_1_1Statistics.html">CVC3::Statistics</a> &statistics, const <a class="el" href="classCVC3_1_1CLFlags.html">CVC3::CLFlags</a> &flags)</td></tr>
<tr class="separator:a7bb76ec26a37645bd0183715af69966f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a14a7c3223d238a6d9d0864692c450774"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a14a7c3223d238a6d9d0864692c450774">~CNF_Manager</a> ()</td></tr>
<tr class="separator:a14a7c3223d238a6d9d0864692c450774"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0d2b7a6369e9e7ad4ae6aca1398e404d"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a0d2b7a6369e9e7ad4ae6aca1398e404d">registerCNFCallback</a> (<a class="el" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html">CNFCallback</a> *cnfCallback)</td></tr>
<tr class="memdesc:a0d2b7a6369e9e7ad4ae6aca1398e404d"><td class="mdescLeft"> </td><td class="mdescRight">Register CNF callback. <a href="#a0d2b7a6369e9e7ad4ae6aca1398e404d"></a><br/></td></tr>
<tr class="separator:a0d2b7a6369e9e7ad4ae6aca1398e404d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a919041a34faf71a4c194be3da0b7dd23"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a919041a34faf71a4c194be3da0b7dd23">setBottomScope</a> (int scope)</td></tr>
<tr class="memdesc:a919041a34faf71a4c194be3da0b7dd23"><td class="mdescLeft"> </td><td class="mdescRight">Set scope for translation. <a href="#a919041a34faf71a4c194be3da0b7dd23"></a><br/></td></tr>
<tr class="separator:a919041a34faf71a4c194be3da0b7dd23"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad6052496e803e074e91efe7212360b23"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#ad6052496e803e074e91efe7212360b23">numVars</a> ()</td></tr>
<tr class="memdesc:ad6052496e803e074e91efe7212360b23"><td class="mdescLeft"> </td><td class="mdescRight">Return the number of variables being managed. <a href="#ad6052496e803e074e91efe7212360b23"></a><br/></td></tr>
<tr class="separator:ad6052496e803e074e91efe7212360b23"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:abfe9063da71565718c194cfa04e65805"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#abfe9063da71565718c194cfa04e65805">numFanins</a> (<a class="el" href="classSAT_1_1Var.html">Var</a> c)</td></tr>
<tr class="memdesc:abfe9063da71565718c194cfa04e65805"><td class="mdescLeft"> </td><td class="mdescRight">Return number of fanins for CNF node c. <a href="#abfe9063da71565718c194cfa04e65805"></a><br/></td></tr>
<tr class="separator:abfe9063da71565718c194cfa04e65805"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a80f7c509fd352dd5ba7920ce1b6329a0"><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="classSAT_1_1CNF__Manager.html#a80f7c509fd352dd5ba7920ce1b6329a0">getFanin</a> (<a class="el" href="classSAT_1_1Var.html">Var</a> c, unsigned i)</td></tr>
<tr class="memdesc:a80f7c509fd352dd5ba7920ce1b6329a0"><td class="mdescLeft"> </td><td class="mdescRight">Returns the ith fanin of c. <a href="#a80f7c509fd352dd5ba7920ce1b6329a0"></a><br/></td></tr>
<tr class="separator:a80f7c509fd352dd5ba7920ce1b6329a0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a33ea4af8007dfd674a152e84d0df32a4"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a33ea4af8007dfd674a152e84d0df32a4">numFanouts</a> (<a class="el" href="classSAT_1_1Var.html">Var</a> c)</td></tr>
<tr class="memdesc:a33ea4af8007dfd674a152e84d0df32a4"><td class="mdescLeft"> </td><td class="mdescRight">Return number of fanins for c. <a href="#a33ea4af8007dfd674a152e84d0df32a4"></a><br/></td></tr>
<tr class="separator:a33ea4af8007dfd674a152e84d0df32a4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3ea642d608115a728fb6454731f18549"><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="classSAT_1_1CNF__Manager.html#a3ea642d608115a728fb6454731f18549">getFanout</a> (<a class="el" href="classSAT_1_1Var.html">Var</a> c, unsigned i)</td></tr>
<tr class="memdesc:a3ea642d608115a728fb6454731f18549"><td class="mdescLeft"> </td><td class="mdescRight">Returns the ith fanout of c. <a href="#a3ea642d608115a728fb6454731f18549"></a><br/></td></tr>
<tr class="separator:a3ea642d608115a728fb6454731f18549"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2c10ef5b4dff560013835d79c7e5fe74"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a2c10ef5b4dff560013835d79c7e5fe74">concreteVar</a> (<a class="el" href="classSAT_1_1Var.html">Var</a> v)</td></tr>
<tr class="memdesc:a2c10ef5b4dff560013835d79c7e5fe74"><td class="mdescLeft"> </td><td class="mdescRight">Convert a CNF literal to an Expr literal. <a href="#a2c10ef5b4dff560013835d79c7e5fe74"></a><br/></td></tr>
<tr class="separator:a2c10ef5b4dff560013835d79c7e5fe74"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a42c3cbd432324757f09ffd622ab1f057"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a42c3cbd432324757f09ffd622ab1f057">concreteLit</a> (<a class="el" href="classSAT_1_1Lit.html">Lit</a> l, bool checkTranslated=true)</td></tr>
<tr class="memdesc:a42c3cbd432324757f09ffd622ab1f057"><td class="mdescLeft"> </td><td class="mdescRight">Convert a CNF literal to an Expr literal. <a href="#a42c3cbd432324757f09ffd622ab1f057"></a><br/></td></tr>
<tr class="separator:a42c3cbd432324757f09ffd622ab1f057"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a78c85b8b8b747f72d973ed0835294c5e"><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="classSAT_1_1CNF__Manager.html#a78c85b8b8b747f72d973ed0835294c5e">getCNFLit</a> (const <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a> &e)</td></tr>
<tr class="memdesc:a78c85b8b8b747f72d973ed0835294c5e"><td class="mdescLeft"> </td><td class="mdescRight">Look up the CNF literal for an Expr. <a href="#a78c85b8b8b747f72d973ed0835294c5e"></a><br/></td></tr>
<tr class="separator:a78c85b8b8b747f72d973ed0835294c5e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a56db0a07323ee4b11df78f88c8022db5"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a56db0a07323ee4b11df78f88c8022db5">cons</a> (unsigned lb, unsigned ub, const <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a> &e2, std::vector< unsigned > &newLits)</td></tr>
<tr class="separator:a56db0a07323ee4b11df78f88c8022db5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad8e26f917ea3a87a1013cbd154d16069"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#ad8e26f917ea3a87a1013cbd154d16069">convertLemma</a> (const <a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> &thm, <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf)</td></tr>
<tr class="memdesc:ad8e26f917ea3a87a1013cbd154d16069"><td class="mdescLeft"> </td><td class="mdescRight">Convert thm A |- B (A is a set of literals) into one or more clauses. <a href="#ad8e26f917ea3a87a1013cbd154d16069"></a><br/></td></tr>
<tr class="separator:ad8e26f917ea3a87a1013cbd154d16069"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5cf1943a3bc3773fd0d8f64c123478f7"><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="classSAT_1_1CNF__Manager.html#a5cf1943a3bc3773fd0d8f64c123478f7">addAssumption</a> (const <a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> &thm, <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf)</td></tr>
<tr class="memdesc:a5cf1943a3bc3773fd0d8f64c123478f7"><td class="mdescLeft"> </td><td class="mdescRight">Given thm of form A |- B, convert B to CNF and add it to cnf. <a href="#a5cf1943a3bc3773fd0d8f64c123478f7"></a><br/></td></tr>
<tr class="separator:a5cf1943a3bc3773fd0d8f64c123478f7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aac0a2f51c8376029b88e1febc4cbd669"><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="classSAT_1_1CNF__Manager.html#aac0a2f51c8376029b88e1febc4cbd669">addLemma</a> (<a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> thm, <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf)</td></tr>
<tr class="memdesc:aac0a2f51c8376029b88e1febc4cbd669"><td class="mdescLeft"> </td><td class="mdescRight">Convert thm to CNF and add it to the current formula. <a href="#aac0a2f51c8376029b88e1febc4cbd669"></a><br/></td></tr>
<tr class="separator:aac0a2f51c8376029b88e1febc4cbd669"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-methods"></a>
Private Member Functions</h2></td></tr>
<tr class="memitem:a4caaeae8fffbb938e8b723c0b0cfe98e"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1CNF__Rules.html">CVC3::CNF_Rules</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a4caaeae8fffbb938e8b723c0b0cfe98e">createProofRules</a> (<a class="el" href="classCVC3_1_1TheoremManager.html">CVC3::TheoremManager</a> *tm, const <a class="el" href="classCVC3_1_1CLFlags.html">CVC3::CLFlags</a> &)</td></tr>
<tr class="separator:a4caaeae8fffbb938e8b723c0b0cfe98e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aad4c1fe260c5c15d94a4010d82569e74"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#aad4c1fe260c5c15d94a4010d82569e74">registerAtom</a> (const <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a> &e, const <a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> &thm)</td></tr>
<tr class="memdesc:aad4c1fe260c5c15d94a4010d82569e74"><td class="mdescLeft"> </td><td class="mdescRight">Register a new atomic formula. <a href="#aad4c1fe260c5c15d94a4010d82569e74"></a><br/></td></tr>
<tr class="separator:aad4c1fe260c5c15d94a4010d82569e74"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a41ad958fb86a4da62890caf922250551"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a41ad958fb86a4da62890caf922250551">concreteExpr</a> (const <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a> &e, const <a class="el" href="classSAT_1_1Lit.html">Lit</a> &literal)</td></tr>
<tr class="memdesc:a41ad958fb86a4da62890caf922250551"><td class="mdescLeft"> </td><td class="mdescRight">Return the expr corresponding to the literal unless the expr is TRUE of FALSE. <a href="#a41ad958fb86a4da62890caf922250551"></a><br/></td></tr>
<tr class="separator:a41ad958fb86a4da62890caf922250551"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:acc9e77affcd72a13f95e7f68ed944935"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#acc9e77affcd72a13f95e7f68ed944935">concreteThm</a> (const <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a> &e)</td></tr>
<tr class="memdesc:acc9e77affcd72a13f95e7f68ed944935"><td class="mdescLeft"> </td><td class="mdescRight">Return the theorem if e is not as concreteExpr(e). <a href="#acc9e77affcd72a13f95e7f68ed944935"></a><br/></td></tr>
<tr class="separator:acc9e77affcd72a13f95e7f68ed944935"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4810c6cb09582d0b2bb41057753d0ae4"><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="classSAT_1_1CNF__Manager.html#a4810c6cb09582d0b2bb41057753d0ae4">translateExprRec</a> (const <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a> &e, <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf, const <a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> &thmIn)</td></tr>
<tr class="memdesc:a4810c6cb09582d0b2bb41057753d0ae4"><td class="mdescLeft"> </td><td class="mdescRight">Recursively translate e into cnf. <a href="#a4810c6cb09582d0b2bb41057753d0ae4"></a><br/></td></tr>
<tr class="separator:a4810c6cb09582d0b2bb41057753d0ae4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9c44bb0556800d1f05eca51d68a73e67"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a9c44bb0556800d1f05eca51d68a73e67">replaceITErec</a> (const <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a> &e, <a class="el" href="classSAT_1_1Var.html">Var</a> v, bool translateOnly)</td></tr>
<tr class="memdesc:a9c44bb0556800d1f05eca51d68a73e67"><td class="mdescLeft"> </td><td class="mdescRight">Recursively traverse an expression with an embedded term ITE. <a href="#a9c44bb0556800d1f05eca51d68a73e67"></a><br/></td></tr>
<tr class="separator:a9c44bb0556800d1f05eca51d68a73e67"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:abc4a95f97c6d2aa7a7584cd1bc30b743"><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="classSAT_1_1CNF__Manager.html#abc4a95f97c6d2aa7a7584cd1bc30b743">translateExpr</a> (const <a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> &thmIn, <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf)</td></tr>
<tr class="memdesc:abc4a95f97c6d2aa7a7584cd1bc30b743"><td class="mdescLeft"> </td><td class="mdescRight">Recursively translate e into cnf. <a href="#abc4a95f97c6d2aa7a7584cd1bc30b743"></a><br/></td></tr>
<tr class="separator:abc4a95f97c6d2aa7a7584cd1bc30b743"><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:accef3514f49a030e3000e933a0cb7f34"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#accef3514f49a030e3000e933a0cb7f34">d_vc</a></td></tr>
<tr class="memdesc:accef3514f49a030e3000e933a0cb7f34"><td class="mdescLeft"> </td><td class="mdescRight">For clause minimization. <a href="#accef3514f49a030e3000e933a0cb7f34"></a><br/></td></tr>
<tr class="separator:accef3514f49a030e3000e933a0cb7f34"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab69cb1473b3b452517ccd6d57d011a02"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#ab69cb1473b3b452517ccd6d57d011a02">d_minimizeClauses</a></td></tr>
<tr class="memdesc:ab69cb1473b3b452517ccd6d57d011a02"><td class="mdescLeft"> </td><td class="mdescRight">Whether to use brute-force clause minimization. <a href="#ab69cb1473b3b452517ccd6d57d011a02"></a><br/></td></tr>
<tr class="separator:ab69cb1473b3b452517ccd6d57d011a02"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aff2bf1721ef06059d56936a62fc2b82e"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#aff2bf1721ef06059d56936a62fc2b82e">d_commonRules</a></td></tr>
<tr class="memdesc:aff2bf1721ef06059d56936a62fc2b82e"><td class="mdescLeft"> </td><td class="mdescRight">Common proof rules. <a href="#aff2bf1721ef06059d56936a62fc2b82e"></a><br/></td></tr>
<tr class="separator:aff2bf1721ef06059d56936a62fc2b82e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5b7d49543538f5dc44fc89e132d0b5d5"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1CNF__Rules.html">CVC3::CNF_Rules</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a5b7d49543538f5dc44fc89e132d0b5d5">d_rules</a></td></tr>
<tr class="memdesc:a5b7d49543538f5dc44fc89e132d0b5d5"><td class="mdescLeft"> </td><td class="mdescRight">Rules for manipulating CNF. <a href="#a5b7d49543538f5dc44fc89e132d0b5d5"></a><br/></td></tr>
<tr class="separator:a5b7d49543538f5dc44fc89e132d0b5d5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af6bda95f4cc0f85ac6cba04c66bd4a69"><td class="memItemLeft" align="right" valign="top">std::vector< <a class="el" href="structSAT_1_1CNF__Manager_1_1Varinfo.html">Varinfo</a> > </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#af6bda95f4cc0f85ac6cba04c66bd4a69">d_varInfo</a></td></tr>
<tr class="memdesc:af6bda95f4cc0f85ac6cba04c66bd4a69"><td class="mdescLeft"> </td><td class="mdescRight">vector that maps a variable index to information for that variable <a href="#af6bda95f4cc0f85ac6cba04c66bd4a69"></a><br/></td></tr>
<tr class="separator:af6bda95f4cc0f85ac6cba04c66bd4a69"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad3d2c901c7b8cc277639fb2aff90797b"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< <a class="el" href="classSAT_1_1Var.html">Var</a> > </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#ad3d2c901c7b8cc277639fb2aff90797b">d_cnfVars</a></td></tr>
<tr class="memdesc:ad3d2c901c7b8cc277639fb2aff90797b"><td class="mdescLeft"> </td><td class="mdescRight">Map from Exprs to Vars representing those Exprs. <a href="#ad3d2c901c7b8cc277639fb2aff90797b"></a><br/></td></tr>
<tr class="separator:ad3d2c901c7b8cc277639fb2aff90797b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a29c5c9b3c09bb443e806ed51bd78d3b5"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< <a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> > </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a29c5c9b3c09bb443e806ed51bd78d3b5">d_iteMap</a></td></tr>
<tr class="memdesc:a29c5c9b3c09bb443e806ed51bd78d3b5"><td class="mdescLeft"> </td><td class="mdescRight">Cached translation of term-ite-containing expressions. <a href="#a29c5c9b3c09bb443e806ed51bd78d3b5"></a><br/></td></tr>
<tr class="separator:a29c5c9b3c09bb443e806ed51bd78d3b5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7d0482a19f8088da32cf12e512fc6a1c"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a7d0482a19f8088da32cf12e512fc6a1c">d_clauseIdNext</a></td></tr>
<tr class="memdesc:a7d0482a19f8088da32cf12e512fc6a1c"><td class="mdescLeft"> </td><td class="mdescRight">Map of possibly useful lemmas. <a href="#a7d0482a19f8088da32cf12e512fc6a1c"></a><br/></td></tr>
<tr class="separator:a7d0482a19f8088da32cf12e512fc6a1c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a60a763224b0c38233c65bfa1374f6ab0"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a60a763224b0c38233c65bfa1374f6ab0">d_bottomScope</a></td></tr>
<tr class="memdesc:a60a763224b0c38233c65bfa1374f6ab0"><td class="mdescLeft"> </td><td class="mdescRight">Whether expr has already been translated. <a href="#a60a763224b0c38233c65bfa1374f6ab0"></a><br/></td></tr>
<tr class="separator:a60a763224b0c38233c65bfa1374f6ab0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5ef71065232a1ffbdce52398b1faafc4"><td class="memItemLeft" align="right" valign="top">std::deque< <a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> > </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a5ef71065232a1ffbdce52398b1faafc4">d_translateQueueThms</a></td></tr>
<tr class="memdesc:a5ef71065232a1ffbdce52398b1faafc4"><td class="mdescLeft"> </td><td class="mdescRight">Queue of theorems to translate. <a href="#a5ef71065232a1ffbdce52398b1faafc4"></a><br/></td></tr>
<tr class="separator:a5ef71065232a1ffbdce52398b1faafc4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac2f7df4bf6d27d29de19037e34d08df7"><td class="memItemLeft" align="right" valign="top">std::deque< <a class="el" href="classSAT_1_1Var.html">Var</a> > </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#ac2f7df4bf6d27d29de19037e34d08df7">d_translateQueueVars</a></td></tr>
<tr class="memdesc:ac2f7df4bf6d27d29de19037e34d08df7"><td class="mdescLeft"> </td><td class="mdescRight">Queue of fanouts corresponding to thms to translate. <a href="#ac2f7df4bf6d27d29de19037e34d08df7"></a><br/></td></tr>
<tr class="separator:ac2f7df4bf6d27d29de19037e34d08df7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae23cfc40d069a750c70dd4ed99a18564"><td class="memItemLeft" align="right" valign="top">std::deque< bool > </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#ae23cfc40d069a750c70dd4ed99a18564">d_translateQueueFlags</a></td></tr>
<tr class="memdesc:ae23cfc40d069a750c70dd4ed99a18564"><td class="mdescLeft"> </td><td class="mdescRight">Whether thm to translate is "translate only". <a href="#ae23cfc40d069a750c70dd4ed99a18564"></a><br/></td></tr>
<tr class="separator:ae23cfc40d069a750c70dd4ed99a18564"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae131042e189e22c41482ff5224661b25"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Statistics.html">CVC3::Statistics</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#ae131042e189e22c41482ff5224661b25">d_statistics</a></td></tr>
<tr class="memdesc:ae131042e189e22c41482ff5224661b25"><td class="mdescLeft"> </td><td class="mdescRight">Reference to statistics object. <a href="#ae131042e189e22c41482ff5224661b25"></a><br/></td></tr>
<tr class="separator:ae131042e189e22c41482ff5224661b25"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6d98dc9308632f87bfff6a121a33d4ba"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1CLFlags.html">CVC3::CLFlags</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a6d98dc9308632f87bfff6a121a33d4ba">d_flags</a></td></tr>
<tr class="memdesc:a6d98dc9308632f87bfff6a121a33d4ba"><td class="mdescLeft"> </td><td class="mdescRight">Reference to command-line flags. <a href="#a6d98dc9308632f87bfff6a121a33d4ba"></a><br/></td></tr>
<tr class="separator:a6d98dc9308632f87bfff6a121a33d4ba"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af62a616e36e64bd10ddf06ec58b7caae"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#af62a616e36e64bd10ddf06ec58b7caae">d_nullExpr</a></td></tr>
<tr class="memdesc:af62a616e36e64bd10ddf06ec58b7caae"><td class="mdescLeft"> </td><td class="mdescRight">Reference to null Expr. <a href="#af62a616e36e64bd10ddf06ec58b7caae"></a><br/></td></tr>
<tr class="separator:af62a616e36e64bd10ddf06ec58b7caae"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a81c6d45a1864f4266197e90de4649c14"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html">CNFCallback</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1CNF__Manager.html#a81c6d45a1864f4266197e90de4649c14">d_cnfCallback</a></td></tr>
<tr class="memdesc:a81c6d45a1864f4266197e90de4649c14"><td class="mdescLeft"> </td><td class="mdescRight">Instance of CNF_CallBack: must be registered. <a href="#a81c6d45a1864f4266197e90de4649c14"></a><br/></td></tr>
<tr class="separator:a81c6d45a1864f4266197e90de4649c14"><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="cnf__manager_8h_source.html#l00041">41</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
</div><h2 class="groupheader">Constructor & Destructor Documentation</h2>
<a class="anchor" id="a7bb76ec26a37645bd0183715af69966f"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CNF_Manager::CNF_Manager </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoremManager.html">CVC3::TheoremManager</a> * </td>
<td class="paramname"><em>tm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Statistics.html">CVC3::Statistics</a> & </td>
<td class="paramname"><em>statistics</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1CLFlags.html">CVC3::CLFlags</a> & </td>
<td class="paramname"><em>flags</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="cnf__manager_8cpp_source.html#l00035">35</a> of file <a class="el" href="cnf__manager_8cpp_source.html">cnf_manager.cpp</a>.</p>
<p>References <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00038">createProofRules()</a>, <a class="el" href="cnf__manager_8h_source.html#l00053">d_rules</a>, <a class="el" href="cnf__manager_8h_source.html#l00063">d_varInfo</a>, <a class="el" href="cnf__manager_8h_source.html#l00044">d_vc</a>, and <a class="el" href="command__line__flags_8h_source.html#l00302">CVC3::CLFlags::setFlag()</a>.</p>
</div>
</div>
<a class="anchor" id="a14a7c3223d238a6d9d0864692c450774"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CNF_Manager::~CNF_Manager </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="cnf__manager_8cpp_source.html#l00060">60</a> of file <a class="el" href="cnf__manager_8cpp_source.html">cnf_manager.cpp</a>.</p>
<p>References <a class="el" href="cnf__manager_8h_source.html#l00053">d_rules</a>, and <a class="el" href="cnf__manager_8h_source.html#l00044">d_vc</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Function Documentation</h2>
<a class="anchor" id="a4caaeae8fffbb938e8b723c0b0cfe98e"></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_1CNF__Rules.html">CNF_Rules</a> * CNF_Manager::createProofRules </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoremManager.html">CVC3::TheoremManager</a> * </td>
<td class="paramname"><em>tm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1CLFlags.html">CVC3::CLFlags</a> & </td>
<td class="paramname"><em>flags</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">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00038">38</a> of file <a class="el" href="cnf__theorem__producer_8cpp_source.html">cnf_theorem_producer.cpp</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00035">CNF_Manager()</a>.</p>
</div>
</div>
<a class="anchor" id="aad4c1fe260c5c15d94a4010d82569e74"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CNF_Manager::registerAtom </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>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> & </td>
<td class="paramname"><em>thm</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">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Register a new atomic formula. </p>
<p>Definition at line <a class="el" href="cnf__manager_8cpp_source.html#l00067">67</a> of file <a class="el" href="cnf__manager_8cpp_source.html">cnf_manager.cpp</a>.</p>
<p>References <a class="el" href="cnf__manager_8h_source.html#l00120">d_cnfCallback</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01378">CVC3::Expr::isRegisteredAtom()</a>, <a class="el" href="expr_8h_source.html#l01374">CVC3::Expr::isUserRegisteredAtom()</a>, and <a class="el" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html#a5bfb2992c14e9a7a1c824f1df49aa8b3">SAT::CNF_Manager::CNFCallback::registerAtom()</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00147">translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="a41ad958fb86a4da62890caf922250551"></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_1Expr.html">Expr</a> CNF_Manager::concreteExpr </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>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classSAT_1_1Lit.html">Lit</a> & </td>
<td class="paramname"><em>literal</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">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Return the expr corresponding to the literal unless the expr is TRUE of FALSE. </p>
<p>Definition at line <a class="el" href="cnf__manager_8cpp_source.html#l00131">131</a> of file <a class="el" href="cnf__manager_8cpp_source.html">cnf_manager.cpp</a>.</p>
<p>References <a class="el" href="cnf__manager_8h_source.html#l00223">concreteLit()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, and <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00147">translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="acc9e77affcd72a13f95e7f68ed944935"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CNF_Manager::concreteThm </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Return the theorem if e is not as concreteExpr(e). </p>
<p>Definition at line <a class="el" href="cnf__manager_8cpp_source.html#l00139">139</a> of file <a class="el" href="cnf__manager_8cpp_source.html">cnf_manager.cpp</a>.</p>
<p>References <a class="el" href="cnf__manager_8h_source.html#l00050">d_commonRules</a>, <a class="el" href="cnf__manager_8h_source.html#l00069">d_iteMap</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, and <a class="el" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">CVC3::CommonProofRules::reflexivityRule()</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00147">translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="a4810c6cb09582d0b2bb41057753d0ae4"></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> CNF_Manager::translateExprRec </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>
</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>cnf</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> & </td>
<td class="paramname"><em>thmIn</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">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Recursively translate e into cnf. </p>
<p>A non-context dependent cache, d_cnfVars is used to remember translations of expressions. A context-dependent attribute, isTranslated, is used to remember whether an expression has been translated in the current context </p>
<p>Definition at line <a class="el" href="cnf__manager_8cpp_source.html#l00147">147</a> of file <a class="el" href="cnf__manager_8cpp_source.html">cnf_manager.cpp</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00134">SAT::CNF_Formula::addLiteral()</a>, <a class="el" href="kinds_8h_source.html#l00067">AND</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="group__CNF__Rules.html#gad68b269642c7545c0fc119b7a74a3f32">CVC3::CNF_Rules::CNFITEtranslate()</a>, <a class="el" href="group__CNF__Rules.html#gae66dc0ceb7b55eeeea57187e0acd4bd5">CVC3::CNF_Rules::CNFtranslate()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00131">concreteExpr()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00139">concreteThm()</a>, <a class="el" href="cnf__manager_8h_source.html#l00087">d_bottomScope</a>, <a class="el" href="cnf__manager_8h_source.html#l00066">d_cnfVars</a>, <a class="el" href="cnf__manager_8h_source.html#l00050">d_commonRules</a>, <a class="el" href="cnf__manager_8h_source.html#l00102">d_flags</a>, <a class="el" href="cnf__manager_8h_source.html#l00069">d_iteMap</a>, <a class="el" href="cnf__manager_8h_source.html#l00053">d_rules</a>, <a class="el" href="cnf__manager_8h_source.html#l00090">d_translateQueueThms</a>, <a class="el" href="cnf__manager_8h_source.html#l00093">d_translateQueueVars</a>, <a class="el" href="cnf__manager_8h_source.html#l00063">d_varInfo</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__map_8h_source.html#l00326">CVC3::ExprHashMap< Data >::end()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr__map_8h_source.html#l00329">CVC3::ExprHashMap< Data >::find()</a>, <a class="el" href="cnf__manager_8h_source.html#l00236">getCNFLit()</a>, <a class="el" href="cnf_8h_source.html#l00138">SAT::CNF_Formula::getCurrentClause()</a>, <a class="el" href="cnf_8h_source.html#l00061">SAT::Lit::getFalse()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="cnf_8h_source.html#l00060">SAT::Lit::getTrue()</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="expr_8h_source.html#l00965">CVC3::Expr::iffExpr()</a>, <a class="el" href="expr_8h_source.html#l00969">CVC3::Expr::impExpr()</a>, <a class="el" href="kinds_8h_source.html#l00071">IMPLIES</a>, <a class="el" href="expr_8h_source.html#l00398">CVC3::Expr::isAbsAtomicFormula()</a>, <a class="el" href="expr_8h_source.html#l00419">CVC3::Expr::isEq()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="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#l01370">CVC3::Expr::isTranslated()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::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="minisat__heap_8h_source.html#l00053">MiniSat::left()</a>, <a class="el" href="classSAT_1_1CNF__Formula.html#ab9f3ffd03469b827138a14392960ba30">SAT::CNF_Formula::newClause()</a>, <a class="el" href="kinds_8h_source.html#l00068">OR</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">CVC3::CommonProofRules::reflexivityRule()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00067">registerAtom()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00074">replaceITErec()</a>, <a class="el" href="minisat__heap_8h_source.html#l00054">MiniSat::right()</a>, <a class="el" href="cnf_8h_source.html#l00106">SAT::Clause::setClauseTheorem()</a>, <a class="el" href="expr_8h_source.html#l01518">CVC3::Expr::setTranslated()</a>, <a class="el" href="kinds_8h_source.html#l00069">XOR</a>, and <a class="el" href="expr_8h_source.html#l00973">CVC3::Expr::xorExpr()</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00623">addAssumption()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00510">translateExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="a9c44bb0556800d1f05eca51d68a73e67"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CNF_Manager::replaceITErec </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>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classSAT_1_1Var.html">Var</a> </td>
<td class="paramname"><em>v</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>translateOnly</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">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Recursively traverse an expression with an embedded term ITE. </p>
<p>Term ITE's are handled by introducing a skolem variable for the ITE term and then adding new constraints describing the ITE in terms of the new variable. </p>
<p>Definition at line <a class="el" href="cnf__manager_8cpp_source.html#l00074">74</a> of file <a class="el" href="cnf__manager_8cpp_source.html">cnf_manager.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="cnf__manager_8h_source.html#l00050">d_commonRules</a>, <a class="el" href="cnf__manager_8h_source.html#l00069">d_iteMap</a>, <a class="el" href="cnf__manager_8h_source.html#l00053">d_rules</a>, <a class="el" href="cnf__manager_8h_source.html#l00096">d_translateQueueFlags</a>, <a class="el" href="cnf__manager_8h_source.html#l00090">d_translateQueueThms</a>, <a class="el" href="cnf__manager_8h_source.html#l00093">d_translateQueueVars</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__map_8h_source.html#l00326">CVC3::ExprHashMap< Data >::end()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr__map_8h_source.html#l00329">CVC3::ExprHashMap< Data >::find()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#aebbcd4a194e4fdca0bcd16143fb03a75">CVC3::CommonProofRules::iffMP()</a>, <a class="el" href="group__CNF__Rules.html#ga941f65f9beb6d3233a6d628c83731960">CVC3::CNF_Rules::ifLiftRule()</a>, <a class="el" href="expr_8cpp_source.html#l00550">CVC3::Expr::isAtomic()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="theorem_8h_source.html#l00171">CVC3::Theorem::isRefl()</a>, <a class="el" href="kinds_8h_source.html#l00081">ITE</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">CVC3::CommonProofRules::reflexivityRule()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f">CVC3::CommonProofRules::substitutivityRule()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a0a87e88508f49b73037e0024afa841bf">CVC3::CommonProofRules::symmetryRule()</a>, and <a class="el" href="classCVC3_1_1CommonProofRules.html#a10fa187373ec24079c10874d8e804ecb">CVC3::CommonProofRules::varIntroSkolem()</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00147">translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="abc4a95f97c6d2aa7a7584cd1bc30b743"></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> CNF_Manager::translateExpr </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> & </td>
<td class="paramname"><em>thmIn</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>cnf</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">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Recursively translate e into cnf. </p>
<p>Call translateExprRec. If additional expressions are queued up, translate them too, until none are left. </p>
<p>Definition at line <a class="el" href="cnf__manager_8cpp_source.html#l00510">510</a> of file <a class="el" href="cnf__manager_8cpp_source.html">cnf_manager.cpp</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00134">SAT::CNF_Formula::addLiteral()</a>, <a class="el" href="group__CNF__Rules.html#ga0aaf202cffbc31fe85e7599ec2906319">CVC3::CNF_Rules::CNFAddUnit()</a>, <a class="el" href="cnf__manager_8h_source.html#l00053">d_rules</a>, <a class="el" href="cnf__manager_8h_source.html#l00096">d_translateQueueFlags</a>, <a class="el" href="cnf__manager_8h_source.html#l00090">d_translateQueueThms</a>, <a class="el" href="cnf__manager_8h_source.html#l00093">d_translateQueueVars</a>, <a class="el" href="cnf__manager_8h_source.html#l00063">d_varInfo</a>, <a class="el" href="cnf_8h_source.html#l00138">SAT::CNF_Formula::getCurrentClause()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="cnf_8h_source.html#l00070">SAT::Lit::getVar()</a>, <a class="el" href="classSAT_1_1CNF__Formula.html#ab9f3ffd03469b827138a14392960ba30">SAT::CNF_Formula::newClause()</a>, <a class="el" href="classSAT_1_1CNF__Formula.html#a3b0eb426b9713bbc92041f046dd83ab5">SAT::CNF_Formula::registerUnit()</a>, <a class="el" href="cnf_8h_source.html#l00106">SAT::Clause::setClauseTheorem()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00147">translateExprRec()</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00623">addAssumption()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00674">addLemma()</a>.</p>
</div>
</div>
<a class="anchor" id="a0d2b7a6369e9e7ad4ae6aca1398e404d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void SAT::CNF_Manager::registerCNFCallback </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html">CNFCallback</a> * </td>
<td class="paramname"><em>cnfCallback</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>Register CNF callback. </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00166">166</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>References <a class="el" href="cnf__manager_8h_source.html#l00120">d_cnfCallback</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l00936">CVC3::SearchSat::SearchSat()</a>.</p>
</div>
</div>
<a class="anchor" id="a919041a34faf71a4c194be3da0b7dd23"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void SAT::CNF_Manager::setBottomScope </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>scope</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>Set scope for translation. </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00170">170</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>References <a class="el" href="cnf__manager_8h_source.html#l00087">d_bottomScope</a>.</p>
</div>
</div>
<a class="anchor" id="ad6052496e803e074e91efe7212360b23"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned SAT::CNF_Manager::numVars </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>Return the number of variables being managed. </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00173">173</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>References <a class="el" href="cnf__manager_8h_source.html#l00063">d_varInfo</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l01064">CVC3::SearchSat::newUserAssumptionInt()</a>.</p>
</div>
</div>
<a class="anchor" id="abfe9063da71565718c194cfa04e65805"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned SAT::CNF_Manager::numFanins </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Var.html">Var</a> </td>
<td class="paramname"><em>c</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>Return number of fanins for CNF node c. </p>
<p>A CNF node x is a fanin of CNF node y if the expr for x is a child of the expr for y or if y is an ITE leaf and x is a new CNF node obtained by translating the ITE leaf y. </p>
<dl class="section see"><dt>See Also</dt><dd>isITELeaf() </dd></dl>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00181">181</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>References <a class="el" href="cnf__manager_8h_source.html#l00063">d_varInfo</a>, and <a class="el" href="cnf_8h_source.html#l00045">SAT::Var::isVar()</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8h_source.html#l00188">getFanin()</a>.</p>
</div>
</div>
<a class="anchor" id="a80f7c509fd352dd5ba7920ce1b6329a0"></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> SAT::CNF_Manager::getFanin </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Var.html">Var</a> </td>
<td class="paramname"><em>c</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">unsigned </td>
<td class="paramname"><em>i</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> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Returns the ith fanin of c. </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00188">188</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>References <a class="el" href="cnf__manager_8h_source.html#l00063">d_varInfo</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="cnf__manager_8h_source.html#l00181">numFanins()</a>.</p>
</div>
</div>
<a class="anchor" id="a33ea4af8007dfd674a152e84d0df32a4"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned SAT::CNF_Manager::numFanouts </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Var.html">Var</a> </td>
<td class="paramname"><em>c</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>Return number of fanins for c. </p>
<p>x is a fanout of y if y is a fanin of x </p>
<dl class="section see"><dt>See Also</dt><dd><a class="el" href="classSAT_1_1CNF__Manager.html#abfe9063da71565718c194cfa04e65805" title="Return number of fanins for CNF node c.">numFanins</a> </dd></dl>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00197">197</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>References <a class="el" href="cnf__manager_8h_source.html#l00063">d_varInfo</a>, and <a class="el" href="cnf_8h_source.html#l00045">SAT::Var::isVar()</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8h_source.html#l00204">getFanout()</a>.</p>
</div>
</div>
<a class="anchor" id="a3ea642d608115a728fb6454731f18549"></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> SAT::CNF_Manager::getFanout </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Var.html">Var</a> </td>
<td class="paramname"><em>c</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">unsigned </td>
<td class="paramname"><em>i</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> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Returns the ith fanout of c. </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00204">204</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>References <a class="el" href="cnf__manager_8h_source.html#l00063">d_varInfo</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="cnf__manager_8h_source.html#l00197">numFanouts()</a>.</p>
</div>
</div>
<a class="anchor" id="a2c10ef5b4dff560013835d79c7e5fe74"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a>& SAT::CNF_Manager::concreteVar </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Var.html">Var</a> </td>
<td class="paramname"><em>v</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>Convert a CNF literal to an Expr literal. </p>
<p>Returns a NULL Expr if there is no corresponding Expr for l </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00212">212</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>References <a class="el" href="cnf__manager_8h_source.html#l00105">d_nullExpr</a>, <a class="el" href="cnf__manager_8h_source.html#l00063">d_varInfo</a>, and <a class="el" href="cnf_8h_source.html#l00042">SAT::Var::isNull()</a>.</p>
</div>
</div>
<a class="anchor" id="a42c3cbd432324757f09ffd622ab1f057"></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_1Expr.html">CVC3::Expr</a> SAT::CNF_Manager::concreteLit </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">bool </td>
<td class="paramname"><em>checkTranslated</em> = <code>true</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Convert a CNF literal to an Expr literal. </p>
<p>Returns a NULL Expr if there is no corresponding Expr for l </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00223">223</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>References <a class="el" href="cnf__manager_8h_source.html#l00105">d_nullExpr</a>, <a class="el" href="cnf__manager_8h_source.html#l00063">d_varInfo</a>, <a class="el" href="cnf_8h_source.html#l00070">SAT::Lit::getVar()</a>, <a class="el" href="cnf_8h_source.html#l00063">SAT::Lit::isNull()</a>, and <a class="el" href="cnf_8h_source.html#l00064">SAT::Lit::isPositive()</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8h_source.html#l00241">CVC3::SearchSat::checkJustified()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00131">concreteExpr()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00258">generateSatProof()</a>, and <a class="el" href="search__sat_8h_source.html#l00245">CVC3::SearchSat::setJustified()</a>.</p>
</div>
</div>
<a class="anchor" id="a78c85b8b8b747f72d973ed0835294c5e"></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> SAT::CNF_Manager::getCNFLit </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Look up the CNF literal for an Expr. </p>
<p>Returns a NULL <a class="el" href="classSAT_1_1Lit.html">Lit</a> if there is no corresponding CNF literal for e </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00236">236</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>References <a class="el" href="cnf__manager_8h_source.html#l00066">d_cnfVars</a>, <a class="el" href="expr__map_8h_source.html#l00326">CVC3::ExprHashMap< Data >::end()</a>, <a class="el" href="expr__map_8h_source.html#l00329">CVC3::ExprHashMap< Data >::find()</a>, <a class="el" href="cnf_8h_source.html#l00061">SAT::Lit::getFalse()</a>, <a class="el" href="cnf_8h_source.html#l00060">SAT::Lit::getTrue()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="expr_8h_source.html#l01370">CVC3::Expr::isTranslated()</a>, and <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00593">convertLemma()</a>, <a class="el" href="search__sat_8h_source.html#l00289">CVC3::SearchSat::getValue()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00147">translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="a56db0a07323ee4b11df78f88c8022db5"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CNF_Manager::cons </td>
<td>(</td>
<td class="paramtype">unsigned </td>
<td class="paramname"><em>lb</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">unsigned </td>
<td class="paramname"><em>ub</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a> & </td>
<td class="paramname"><em>e2</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< unsigned > & </td>
<td class="paramname"><em>newLits</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="cnf__manager_8cpp_source.html#l00550">550</a> of file <a class="el" href="cnf__manager_8cpp_source.html">cnf_manager.cpp</a>.</p>
<p>References <a class="el" href="classCVC3_1_1ValidityChecker.html#ad57f0a783141d3c7b0424102ea8724ac">CVC3::ValidityChecker::assertFormula()</a>, <a class="el" href="cnf__manager_8h_source.html#l00044">d_vc</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a9050dd9dbfb463a488d6f9fe98ef968a">CVC3::ValidityChecker::falseExpr()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a3cee14a9c3b852b501a0594dd951f60c">CVC3::ValidityChecker::pop()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a93cbbe8c21c2404b03ccaa43636d5f59">CVC3::ValidityChecker::push()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a93b515a079fc8fdae5826dfcc343909e">CVC3::ValidityChecker::query()</a>, and <a class="el" href="queryresult_8h_source.html#l00035">CVC3::VALID</a>.</p>
</div>
</div>
<a class="anchor" id="ad8e26f917ea3a87a1013cbd154d16069"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CNF_Manager::convertLemma </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">CVC3::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.html">CNF_Formula</a> & </td>
<td class="paramname"><em>cnf</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Convert thm A |- B (A is a set of literals) into one or more clauses. </p>
<p>cnf should be empty – it will be filled with the result </p>
<p>Definition at line <a class="el" href="cnf__manager_8cpp_source.html#l00593">593</a> of file <a class="el" href="cnf__manager_8cpp_source.html">cnf_manager.cpp</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00134">SAT::CNF_Formula::addLiteral()</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="group__CNF__Rules.html#ga0aaf202cffbc31fe85e7599ec2906319">CVC3::CNF_Rules::CNFAddUnit()</a>, <a class="el" href="group__CNF__Rules.html#ga218381b5e2fddbd76c0c81ca3013c0f8">CVC3::CNF_Rules::CNFConvert()</a>, <a class="el" href="cnf__manager_8h_source.html#l00053">d_rules</a>, <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="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="cnf__manager_8h_source.html#l00236">getCNFLit()</a>, <a class="el" href="cnf_8h_source.html#l00138">SAT::CNF_Formula::getCurrentClause()</a>, <a class="el" href="cnf_8h_source.html#l00063">SAT::Lit::isNull()</a>, <a class="el" href="expr_8h_source.html#l00422">CVC3::Expr::isOr()</a>, <a class="el" href="group__CNF__Rules.html#ga95a3d54cd5764e677d565f227b07eace">CVC3::CNF_Rules::learnedClauses()</a>, <a class="el" href="classSAT_1_1CNF__Formula.html#ab9f3ffd03469b827138a14392960ba30">SAT::CNF_Formula::newClause()</a>, <a class="el" href="classSAT_1_1CNF__Formula.html#a3b0eb426b9713bbc92041f046dd83ab5">SAT::CNF_Formula::registerUnit()</a>, and <a class="el" href="cnf_8h_source.html#l00106">SAT::Clause::setClauseTheorem()</a>.</p>
</div>
</div>
<a class="anchor" id="a5cf1943a3bc3773fd0d8f64c123478f7"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1Lit.html">Lit</a> CNF_Manager::addAssumption </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">CVC3::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.html">CNF_Formula</a> & </td>
<td class="paramname"><em>cnf</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Given thm of form A |- B, convert B to CNF and add it to cnf. </p>
<p>Returns <a class="el" href="classSAT_1_1Lit.html">Lit</a> corresponding to the root of the expression that was translated. </p>
<p>Definition at line <a class="el" href="cnf__manager_8cpp_source.html#l00623">623</a> of file <a class="el" href="cnf__manager_8cpp_source.html">cnf_manager.cpp</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00134">SAT::CNF_Formula::addLiteral()</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="group__CNF__Rules.html#ga0aaf202cffbc31fe85e7599ec2906319">CVC3::CNF_Rules::CNFAddUnit()</a>, <a class="el" href="cnf__manager_8h_source.html#l00102">d_flags</a>, <a class="el" href="cnf__manager_8h_source.html#l00053">d_rules</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cnf_8h_source.html#l00138">SAT::CNF_Formula::getCurrentClause()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="expr_8h_source.html#l00422">CVC3::Expr::isOr()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, <a class="el" href="classSAT_1_1CNF__Formula.html#ab9f3ffd03469b827138a14392960ba30">SAT::CNF_Formula::newClause()</a>, <a class="el" href="classSAT_1_1CNF__Formula.html#a3b0eb426b9713bbc92041f046dd83ab5">SAT::CNF_Formula::registerUnit()</a>, <a class="el" href="cnf_8h_source.html#l00106">SAT::Clause::setClauseTheorem()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00510">translateExpr()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00147">translateExprRec()</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l01042">CVC3::SearchSat::newUserAssumptionIntHelper()</a>.</p>
</div>
</div>
<a class="anchor" id="aac0a2f51c8376029b88e1febc4cbd669"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1Lit.html">Lit</a> CNF_Manager::addLemma </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::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.html">CNF_Formula</a> & </td>
<td class="paramname"><em>cnf</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Convert thm to CNF and add it to the current formula. </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">thm</td><td>should be of form A |- B where A is a set of literals. </td></tr>
<tr><td class="paramname">cnf</td><td>the new clauses are added to cnf. Returns <a class="el" href="classSAT_1_1Lit.html">Lit</a> corresponding to the root of the expression that was translated. </td></tr>
</table>
</dd>
</dl>
<p>Definition at line <a class="el" href="cnf__manager_8cpp_source.html#l00674">674</a> of file <a class="el" href="cnf__manager_8cpp_source.html">cnf_manager.cpp</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00134">SAT::CNF_Formula::addLiteral()</a>, <a class="el" href="group__CNF__Rules.html#ga0aaf202cffbc31fe85e7599ec2906319">CVC3::CNF_Rules::CNFAddUnit()</a>, <a class="el" href="cnf__manager_8h_source.html#l00053">d_rules</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cnf_8h_source.html#l00138">SAT::CNF_Formula::getCurrentClause()</a>, <a class="el" href="group__CNF__Rules.html#ga95a3d54cd5764e677d565f227b07eace">CVC3::CNF_Rules::learnedClauses()</a>, <a class="el" href="classSAT_1_1CNF__Formula.html#ab9f3ffd03469b827138a14392960ba30">SAT::CNF_Formula::newClause()</a>, <a class="el" href="classSAT_1_1CNF__Formula.html#a3b0eb426b9713bbc92041f046dd83ab5">SAT::CNF_Formula::registerUnit()</a>, <a class="el" href="cnf_8h_source.html#l00106">SAT::Clause::setClauseTheorem()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00510">translateExpr()</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Data Documentation</h2>
<a class="anchor" id="accef3514f49a030e3000e933a0cb7f34"></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_1ValidityChecker.html">CVC3::ValidityChecker</a>* SAT::CNF_Manager::d_vc</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>For clause minimization. </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00044">44</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00035">CNF_Manager()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00550">cons()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00060">~CNF_Manager()</a>.</p>
</div>
</div>
<a class="anchor" id="ab69cb1473b3b452517ccd6d57d011a02"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool SAT::CNF_Manager::d_minimizeClauses</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>Whether to use brute-force clause minimization. </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00047">47</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="aff2bf1721ef06059d56936a62fc2b82e"></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_1CommonProofRules.html">CVC3::CommonProofRules</a>* SAT::CNF_Manager::d_commonRules</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>Common proof rules. </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00050">50</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00139">concreteThm()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00074">replaceITErec()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00147">translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="a5b7d49543538f5dc44fc89e132d0b5d5"></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_1CNF__Rules.html">CVC3::CNF_Rules</a>* SAT::CNF_Manager::d_rules</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>Rules for manipulating CNF. </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00053">53</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00623">addAssumption()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00674">addLemma()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00035">CNF_Manager()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00593">convertLemma()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00074">replaceITErec()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00510">translateExpr()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00147">translateExprRec()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00060">~CNF_Manager()</a>.</p>
</div>
</div>
<a class="anchor" id="af6bda95f4cc0f85ac6cba04c66bd4a69"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="structSAT_1_1CNF__Manager_1_1Varinfo.html">Varinfo</a>> SAT::CNF_Manager::d_varInfo</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>vector that maps a variable index to information for that variable </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00063">63</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00035">CNF_Manager()</a>, <a class="el" href="cnf__manager_8h_source.html#l00223">concreteLit()</a>, <a class="el" href="cnf__manager_8h_source.html#l00212">concreteVar()</a>, <a class="el" href="cnf__manager_8h_source.html#l00188">getFanin()</a>, <a class="el" href="cnf__manager_8h_source.html#l00204">getFanout()</a>, <a class="el" href="cnf__manager_8h_source.html#l00181">numFanins()</a>, <a class="el" href="cnf__manager_8h_source.html#l00197">numFanouts()</a>, <a class="el" href="cnf__manager_8h_source.html#l00173">numVars()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00510">translateExpr()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00147">translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="ad3d2c901c7b8cc277639fb2aff90797b"></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_1ExprHashMap.html">CVC3::ExprHashMap</a><<a class="el" href="classSAT_1_1Var.html">Var</a>> SAT::CNF_Manager::d_cnfVars</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>Map from Exprs to Vars representing those Exprs. </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00066">66</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8h_source.html#l00236">getCNFLit()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00147">translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="a29c5c9b3c09bb443e806ed51bd78d3b5"></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_1ExprHashMap.html">CVC3::ExprHashMap</a><<a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a>> SAT::CNF_Manager::d_iteMap</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>Cached translation of term-ite-containing expressions. </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00069">69</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00139">concreteThm()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00074">replaceITErec()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00147">translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="a7d0482a19f8088da32cf12e512fc6a1c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int SAT::CNF_Manager::d_clauseIdNext</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>Map of possibly useful lemmas. </p>
<p>Maps a clause id to the theorem justifying that clause</p>
<p>Note that clauses created by simple CNF translation are not given id's. This is because theorems for these clauses can be created lazily later. Next clause id </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00081">81</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="a60a763224b0c38233c65bfa1374f6ab0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int SAT::CNF_Manager::d_bottomScope</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>Whether expr has already been translated. </p>
<p>Bottom scope in which translation is valid </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00087">87</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8h_source.html#l00170">setBottomScope()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00147">translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="a5ef71065232a1ffbdce52398b1faafc4"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::deque<<a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a>> SAT::CNF_Manager::d_translateQueueThms</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>Queue of theorems to translate. </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00090">90</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00074">replaceITErec()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00510">translateExpr()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00147">translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="ac2f7df4bf6d27d29de19037e34d08df7"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::deque<<a class="el" href="classSAT_1_1Var.html">Var</a>> SAT::CNF_Manager::d_translateQueueVars</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>Queue of fanouts corresponding to thms to translate. </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00093">93</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00074">replaceITErec()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00510">translateExpr()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00147">translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="ae23cfc40d069a750c70dd4ed99a18564"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::deque<bool> SAT::CNF_Manager::d_translateQueueFlags</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>Whether thm to translate is "translate only". </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00096">96</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00074">replaceITErec()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00510">translateExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="ae131042e189e22c41482ff5224661b25"></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_1Statistics.html">CVC3::Statistics</a>& SAT::CNF_Manager::d_statistics</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>Reference to statistics object. </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00099">99</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="a6d98dc9308632f87bfff6a121a33d4ba"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1CLFlags.html">CVC3::CLFlags</a>& SAT::CNF_Manager::d_flags</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>Reference to command-line flags. </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00102">102</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00623">addAssumption()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00147">translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="af62a616e36e64bd10ddf06ec58b7caae"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a>& SAT::CNF_Manager::d_nullExpr</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>Reference to null Expr. </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00105">105</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8h_source.html#l00223">concreteLit()</a>, and <a class="el" href="cnf__manager_8h_source.html#l00212">concreteVar()</a>.</p>
</div>
</div>
<a class="anchor" id="a81c6d45a1864f4266197e90de4649c14"></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_1CNF__Manager_1_1CNFCallback.html">CNFCallback</a>* SAT::CNF_Manager::d_cnfCallback</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>Instance of CNF_CallBack: must be registered. </p>
<p>Definition at line <a class="el" href="cnf__manager_8h_source.html#l00120">120</a> of file <a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00067">registerAtom()</a>, and <a class="el" href="cnf__manager_8h_source.html#l00166">registerCNFCallback()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="cnf__manager_8h_source.html">cnf_manager.h</a></li>
<li><a class="el" href="cnf__manager_8cpp_source.html">cnf_manager.cpp</a></li>
<li><a class="el" href="cnf__theorem__producer_8cpp_source.html">cnf_theorem_producer.cpp</a></li>
</ul>
</div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:20 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>
