<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: cnf_manager.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div class="header">
<div class="headertitle">
<div class="title">cnf_manager.h</div> </div>
</div>
<div class="contents">
<a href="cnf__manager_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00002"></a>00002 <span class="comment">/*!</span>
<a name="l00003"></a>00003 <span class="comment"> *\file cnf_manager.h</span>
<a name="l00004"></a>00004 <span class="comment"> *\brief Manager for conversion to and traversal of CNF formulas</span>
<a name="l00005"></a>00005 <span class="comment"> *</span>
<a name="l00006"></a>00006 <span class="comment"> * Author: Clark Barrett</span>
<a name="l00007"></a>00007 <span class="comment"> *</span>
<a name="l00008"></a>00008 <span class="comment"> * Created: Thu Dec 15 13:53:16 2005</span>
<a name="l00009"></a>00009 <span class="comment"> *</span>
<a name="l00010"></a>00010 <span class="comment"> * <hr></span>
<a name="l00011"></a>00011 <span class="comment"> *</span>
<a name="l00012"></a>00012 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00013"></a>00013 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00014"></a>00014 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00015"></a>00015 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00016"></a>00016 <span class="comment"> * </span>
<a name="l00017"></a>00017 <span class="comment"> * <hr></span>
<a name="l00018"></a>00018 <span class="comment"> */</span>
<a name="l00019"></a>00019 <span class="comment">/*****************************************************************************/</span>
<a name="l00020"></a>00020
<a name="l00021"></a>00021 <span class="preprocessor">#ifndef _cvc3__include__cnf_manager_h_</span>
<a name="l00022"></a>00022 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__cnf_manager_h_</span>
<a name="l00023"></a>00023 <span class="preprocessor"></span>
<a name="l00024"></a>00024 <span class="preprocessor">#include "<a class="code" href="cnf_8h.html" title="Basic classes for reasoning about formulas in CNF.">cnf.h</a>"</span>
<a name="l00025"></a>00025 <span class="preprocessor">#include "<a class="code" href="expr_8h.html" title="Definition of the API to expression package. See class Expr for details.">expr.h</a>"</span>
<a name="l00026"></a>00026 <span class="preprocessor">#include "<a class="code" href="expr__map_8h.html">expr_map.h</a>"</span>
<a name="l00027"></a>00027 <span class="preprocessor">#include "<a class="code" href="cdmap_8h.html">cdmap.h</a>"</span>
<a name="l00028"></a>00028 <span class="preprocessor">#include "<a class="code" href="statistics_8h.html" title="Description: Counters and flags for collecting run-time statistics.">statistics.h</a>"</span>
<a name="l00029"></a>00029
<a name="l00030"></a>00030 <span class="keyword">namespace </span>CVC3 {
<a name="l00031"></a>00031
<a name="l00032"></a>00032 <span class="keyword">class </span>CommonProofRules;
<a name="l00033"></a>00033 <span class="keyword">class </span>CNF_Rules;
<a name="l00034"></a>00034 <span class="keyword">class </span>ValidityChecker;
<a name="l00035"></a>00035 <span class="keyword">class </span>Statistics;
<a name="l00036"></a>00036
<a name="l00037"></a>00037 }
<a name="l00038"></a>00038
<a name="l00039"></a>00039 <span class="keyword">namespace </span>SAT {
<a name="l00040"></a>00040
<a name="l00041"></a><a class="code" href="classSAT_1_1CNF__Manager.html">00041</a> <span class="keyword">class </span><a class="code" href="classSAT_1_1CNF__Manager.html">CNF_Manager</a> {
<a name="l00042"></a>00042 <span class="comment"></span>
<a name="l00043"></a>00043 <span class="comment"> //! For clause minimization</span>
<a name="l00044"></a><a class="code" href="classSAT_1_1CNF__Manager.html#accef3514f49a030e3000e933a0cb7f34">00044</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ValidityChecker.html" title="Generic API for a validity checker.">CVC3::ValidityChecker</a>* <a class="code" href="classSAT_1_1CNF__Manager.html#accef3514f49a030e3000e933a0cb7f34" title="For clause minimization.">d_vc</a>;
<a name="l00045"></a>00045 <span class="comment"></span>
<a name="l00046"></a>00046 <span class="comment"> //! Whether to use brute-force clause minimization</span>
<a name="l00047"></a><a class="code" href="classSAT_1_1CNF__Manager.html#ab69cb1473b3b452517ccd6d57d011a02">00047</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classSAT_1_1CNF__Manager.html#ab69cb1473b3b452517ccd6d57d011a02" title="Whether to use brute-force clause minimization.">d_minimizeClauses</a>;
<a name="l00048"></a>00048 <span class="comment"></span>
<a name="l00049"></a>00049 <span class="comment"> //! Common proof rules</span>
<a name="l00050"></a><a class="code" href="classSAT_1_1CNF__Manager.html#aff2bf1721ef06059d56936a62fc2b82e">00050</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a>* <a class="code" href="classSAT_1_1CNF__Manager.html#aff2bf1721ef06059d56936a62fc2b82e" title="Common proof rules.">d_commonRules</a>;
<a name="l00051"></a>00051 <span class="comment"></span>
<a name="l00052"></a>00052 <span class="comment"> //! Rules for manipulating CNF</span>
<a name="l00053"></a><a class="code" href="classSAT_1_1CNF__Manager.html#a5b7d49543538f5dc44fc89e132d0b5d5">00053</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CNF__Rules.html" title="API to the CNF proof rules.">CVC3::CNF_Rules</a>* <a class="code" href="classSAT_1_1CNF__Manager.html#a5b7d49543538f5dc44fc89e132d0b5d5" title="Rules for manipulating CNF.">d_rules</a>;
<a name="l00054"></a>00054 <span class="comment"></span>
<a name="l00055"></a>00055 <span class="comment"> //! Information kept for each CNF variable</span>
<a name="l00056"></a><a class="code" href="structSAT_1_1CNF__Manager_1_1Varinfo.html">00056</a> <span class="comment"></span> <span class="keyword">struct </span><a class="code" href="structSAT_1_1CNF__Manager_1_1Varinfo.html" title="Information kept for each CNF variable.">Varinfo</a> {
<a name="l00057"></a><a class="code" href="structSAT_1_1CNF__Manager_1_1Varinfo.html#a35836ffaaf58a8ce90213c074503c5e7">00057</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">CVC3::Expr</a> <a class="code" href="structSAT_1_1CNF__Manager_1_1Varinfo.html#a35836ffaaf58a8ce90213c074503c5e7">expr</a>;
<a name="l00058"></a><a class="code" href="structSAT_1_1CNF__Manager_1_1Varinfo.html#a3c4e0d97b297cdc5983618feef8cef21">00058</a> std::vector<Lit> <a class="code" href="structSAT_1_1CNF__Manager_1_1Varinfo.html#a3c4e0d97b297cdc5983618feef8cef21">fanins</a>;
<a name="l00059"></a><a class="code" href="structSAT_1_1CNF__Manager_1_1Varinfo.html#afeb507d2c6774855c837a944de70da02">00059</a> std::vector<Var> <a class="code" href="structSAT_1_1CNF__Manager_1_1Varinfo.html#afeb507d2c6774855c837a944de70da02">fanouts</a>;
<a name="l00060"></a>00060 };
<a name="l00061"></a>00061 <span class="comment"></span>
<a name="l00062"></a>00062 <span class="comment"> //! vector that maps a variable index to information for that variable</span>
<a name="l00063"></a><a class="code" href="classSAT_1_1CNF__Manager.html#af6bda95f4cc0f85ac6cba04c66bd4a69">00063</a> <span class="comment"></span> std::vector<Varinfo> <a class="code" href="classSAT_1_1CNF__Manager.html#af6bda95f4cc0f85ac6cba04c66bd4a69" title="vector that maps a variable index to information for that variable">d_varInfo</a>;
<a name="l00064"></a>00064 <span class="comment"></span>
<a name="l00065"></a>00065 <span class="comment"> //! Map from Exprs to Vars representing those Exprs</span>
<a name="l00066"></a><a class="code" href="classSAT_1_1CNF__Manager.html#ad3d2c901c7b8cc277639fb2aff90797b">00066</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap<Var></a> <a class="code" href="classSAT_1_1CNF__Manager.html#ad3d2c901c7b8cc277639fb2aff90797b" title="Map from Exprs to Vars representing those Exprs.">d_cnfVars</a>;
<a name="l00067"></a>00067 <span class="comment"></span>
<a name="l00068"></a>00068 <span class="comment"> //! Cached translation of term-ite-containing expressions</span>
<a name="l00069"></a><a class="code" href="classSAT_1_1CNF__Manager.html#a29c5c9b3c09bb443e806ed51bd78d3b5">00069</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap<CVC3::Theorem></a> <a class="code" href="classSAT_1_1CNF__Manager.html#a29c5c9b3c09bb443e806ed51bd78d3b5" title="Cached translation of term-ite-containing expressions.">d_iteMap</a>;
<a name="l00070"></a>00070 <span class="comment"></span>
<a name="l00071"></a>00071 <span class="comment"> //! Map of possibly useful lemmas</span>
<a name="l00072"></a>00072 <span class="comment"></span> <span class="comment">// CVC3::ExprMap<int> d_usefulLemmas;</span>
<a name="l00073"></a>00073 <span class="comment"></span>
<a name="l00074"></a>00074 <span class="comment"> //! Maps a clause id to the theorem justifying that clause</span>
<a name="l00075"></a>00075 <span class="comment"></span><span class="comment"> /*! Note that clauses created by simple CNF translation are not given id's.</span>
<a name="l00076"></a>00076 <span class="comment"> * This is because theorems for these clauses can be created lazily later. */</span>
<a name="l00077"></a>00077 <span class="comment">// CVC3::CDMap<int, CVC3::Theorem> d_theorems;</span>
<a name="l00078"></a>00078 <span class="comment">// CVC3::CDMap<int, CVC3::Theorem> d_theorems;</span>
<a name="l00079"></a>00079 <span class="comment"></span>
<a name="l00080"></a>00080 <span class="comment"> //! Next clause id</span>
<a name="l00081"></a><a class="code" href="classSAT_1_1CNF__Manager.html#a7d0482a19f8088da32cf12e512fc6a1c">00081</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classSAT_1_1CNF__Manager.html#a7d0482a19f8088da32cf12e512fc6a1c" title="Map of possibly useful lemmas.">d_clauseIdNext</a>;
<a name="l00082"></a>00082 <span class="comment"></span>
<a name="l00083"></a>00083 <span class="comment"> //! Whether expr has already been translated</span>
<a name="l00084"></a>00084 <span class="comment"></span> <span class="comment">// CVC3::CDMap<CVC3::Expr, bool> d_translated;</span>
<a name="l00085"></a>00085 <span class="comment"></span>
<a name="l00086"></a>00086 <span class="comment"> //! Bottom scope in which translation is valid</span>
<a name="l00087"></a><a class="code" href="classSAT_1_1CNF__Manager.html#a60a763224b0c38233c65bfa1374f6ab0">00087</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classSAT_1_1CNF__Manager.html#a60a763224b0c38233c65bfa1374f6ab0" title="Whether expr has already been translated.">d_bottomScope</a>;
<a name="l00088"></a>00088 <span class="comment"></span>
<a name="l00089"></a>00089 <span class="comment"> //! Queue of theorems to translate</span>
<a name="l00090"></a><a class="code" href="classSAT_1_1CNF__Manager.html#a5ef71065232a1ffbdce52398b1faafc4">00090</a> <span class="comment"></span> std::deque<CVC3::Theorem> <a class="code" href="classSAT_1_1CNF__Manager.html#a5ef71065232a1ffbdce52398b1faafc4" title="Queue of theorems to translate.">d_translateQueueThms</a>;
<a name="l00091"></a>00091 <span class="comment"></span>
<a name="l00092"></a>00092 <span class="comment"> //! Queue of fanouts corresponding to thms to translate</span>
<a name="l00093"></a><a class="code" href="classSAT_1_1CNF__Manager.html#ac2f7df4bf6d27d29de19037e34d08df7">00093</a> <span class="comment"></span> std::deque<Var> <a class="code" href="classSAT_1_1CNF__Manager.html#ac2f7df4bf6d27d29de19037e34d08df7" title="Queue of fanouts corresponding to thms to translate.">d_translateQueueVars</a>;
<a name="l00094"></a>00094 <span class="comment"></span>
<a name="l00095"></a>00095 <span class="comment"> //! Whether thm to translate is "translate only"</span>
<a name="l00096"></a><a class="code" href="classSAT_1_1CNF__Manager.html#ae23cfc40d069a750c70dd4ed99a18564">00096</a> <span class="comment"></span> std::deque<bool> <a class="code" href="classSAT_1_1CNF__Manager.html#ae23cfc40d069a750c70dd4ed99a18564" title="Whether thm to translate is "translate only".">d_translateQueueFlags</a>;
<a name="l00097"></a>00097 <span class="comment"></span>
<a name="l00098"></a>00098 <span class="comment"> //! Reference to statistics object</span>
<a name="l00099"></a><a class="code" href="classSAT_1_1CNF__Manager.html#ae131042e189e22c41482ff5224661b25">00099</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Statistics.html">CVC3::Statistics</a>& <a class="code" href="classSAT_1_1CNF__Manager.html#ae131042e189e22c41482ff5224661b25" title="Reference to statistics object.">d_statistics</a>;
<a name="l00100"></a>00100 <span class="comment"></span>
<a name="l00101"></a>00101 <span class="comment"> //! Reference to command-line flags</span>
<a name="l00102"></a><a class="code" href="classSAT_1_1CNF__Manager.html#a6d98dc9308632f87bfff6a121a33d4ba">00102</a> <span class="comment"></span> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CLFlags.html">CVC3::CLFlags</a>& <a class="code" href="classSAT_1_1CNF__Manager.html#a6d98dc9308632f87bfff6a121a33d4ba" title="Reference to command-line flags.">d_flags</a>;
<a name="l00103"></a>00103 <span class="comment"></span>
<a name="l00104"></a>00104 <span class="comment"> //! Reference to null Expr</span>
<a name="l00105"></a><a class="code" href="classSAT_1_1CNF__Manager.html#af62a616e36e64bd10ddf06ec58b7caae">00105</a> <span class="comment"></span> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">CVC3::Expr</a>& <a class="code" href="classSAT_1_1CNF__Manager.html#af62a616e36e64bd10ddf06ec58b7caae" title="Reference to null Expr.">d_nullExpr</a>;
<a name="l00106"></a>00106
<a name="l00107"></a>00107 <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00108"></a>00108 <span class="comment"> //! Abstract class for callbacks</span>
<a name="l00109"></a><a class="code" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html">00109</a> <span class="comment"></span> <span class="keyword">class </span><a class="code" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html" title="Abstract class for callbacks.">CNFCallback</a> {
<a name="l00110"></a>00110 <span class="keyword">public</span>:
<a name="l00111"></a><a class="code" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html#aa7b783bd19107e5a7534eef4c701aefa">00111</a> <a class="code" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html#aa7b783bd19107e5a7534eef4c701aefa">CNFCallback</a>() {}
<a name="l00112"></a><a class="code" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html#a16ded168ad5cc36a8d1dee929a0470e5">00112</a> <span class="keyword">virtual</span> <a class="code" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html#a16ded168ad5cc36a8d1dee929a0470e5">~CNFCallback</a>() {}<span class="comment"></span>
<a name="l00113"></a>00113 <span class="comment"> //! Register an atom</span>
<a name="l00114"></a>00114 <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html#a5bfb2992c14e9a7a1c824f1df49aa8b3" title="Register an atom.">registerAtom</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">CVC3::Expr</a>& e,
<a name="l00115"></a>00115 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a>& thm) = 0;
<a name="l00116"></a>00116 };
<a name="l00117"></a>00117
<a name="l00118"></a>00118 <span class="keyword">private</span>:<span class="comment"></span>
<a name="l00119"></a>00119 <span class="comment"> //! Instance of CNF_CallBack: must be registered</span>
<a name="l00120"></a><a class="code" href="classSAT_1_1CNF__Manager.html#a81c6d45a1864f4266197e90de4649c14">00120</a> <span class="comment"></span> <a class="code" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html" title="Abstract class for callbacks.">CNFCallback</a>* <a class="code" href="classSAT_1_1CNF__Manager.html#a81c6d45a1864f4266197e90de4649c14" title="Instance of CNF_CallBack: must be registered.">d_cnfCallback</a>;
<a name="l00121"></a>00121
<a name="l00122"></a>00122 <a class="code" href="classCVC3_1_1CNF__Rules.html" title="API to the CNF proof rules.">CVC3::CNF_Rules</a>* <a class="code" href="classSAT_1_1CNF__Manager.html#a4caaeae8fffbb938e8b723c0b0cfe98e">createProofRules</a>(<a class="code" href="classCVC3_1_1TheoremManager.html">CVC3::TheoremManager</a>* tm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CLFlags.html">CVC3::CLFlags</a>&);
<a name="l00123"></a>00123 <span class="comment"></span>
<a name="l00124"></a>00124 <span class="comment"> //! Register a new atomic formula</span>
<a name="l00125"></a>00125 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Manager.html#aad4c1fe260c5c15d94a4010d82569e74" title="Register a new atomic formula.">registerAtom</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">CVC3::Expr</a>& e, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a>& thm);
<a name="l00126"></a>00126 <span class="comment"></span>
<a name="l00127"></a>00127 <span class="comment"> //! Return the expr corresponding to the literal unless the expr is TRUE of FALSE</span>
<a name="l00128"></a>00128 <span class="comment"></span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">CVC3::Expr</a> <a class="code" href="classSAT_1_1CNF__Manager.html#a41ad958fb86a4da62890caf922250551" title="Return the expr corresponding to the literal unless the expr is TRUE of FALSE.">concreteExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">CVC3::Expr</a>& e, <span class="keyword">const</span> <a class="code" href="classSAT_1_1Lit.html">Lit</a>& literal);
<a name="l00129"></a>00129 <span class="comment"></span>
<a name="l00130"></a>00130 <span class="comment"> //! Return the theorem if e is not as concreteExpr(e).</span>
<a name="l00131"></a>00131 <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> <a class="code" href="classSAT_1_1CNF__Manager.html#acc9e77affcd72a13f95e7f68ed944935" title="Return the theorem if e is not as concreteExpr(e).">concreteThm</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">CVC3::Expr</a>& e);
<a name="l00132"></a>00132 <span class="comment"></span>
<a name="l00133"></a>00133 <span class="comment"> //! Recursively translate e into cnf</span>
<a name="l00134"></a>00134 <span class="comment"></span><span class="comment"> /*! A non-context dependent cache, d_cnfVars is used to remember translations</span>
<a name="l00135"></a>00135 <span class="comment"> * of expressions. A context-dependent attribute, isTranslated, is used to</span>
<a name="l00136"></a>00136 <span class="comment"> * remember whether an expression has been translated in the current context */</span>
<a name="l00137"></a>00137 <a class="code" href="classSAT_1_1Lit.html">Lit</a> <a class="code" href="classSAT_1_1CNF__Manager.html#a4810c6cb09582d0b2bb41057753d0ae4" title="Recursively translate e into cnf.">translateExprRec</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">CVC3::Expr</a>& e, <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>& cnf,
<a name="l00138"></a>00138 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a>& thmIn);
<a name="l00139"></a>00139 <span class="comment"></span>
<a name="l00140"></a>00140 <span class="comment"> //! Recursively traverse an expression with an embedded term ITE</span>
<a name="l00141"></a>00141 <span class="comment"></span><span class="comment"> /*! Term ITE's are handled by introducing a skolem variable for the ITE term</span>
<a name="l00142"></a>00142 <span class="comment"> * and then adding new constraints describing the ITE in terms of the new variable.</span>
<a name="l00143"></a>00143 <span class="comment"> */</span>
<a name="l00144"></a>00144 <a class="code" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> <a class="code" href="classSAT_1_1CNF__Manager.html#a9c44bb0556800d1f05eca51d68a73e67" title="Recursively traverse an expression with an embedded term ITE.">replaceITErec</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">CVC3::Expr</a>& e, <a class="code" href="classSAT_1_1Var.html">Var</a> v, <span class="keywordtype">bool</span> translateOnly);
<a name="l00145"></a>00145 <span class="comment"></span>
<a name="l00146"></a>00146 <span class="comment"> //! Recursively translate e into cnf</span>
<a name="l00147"></a>00147 <span class="comment"></span><span class="comment"> /*! Call translateExprRec. If additional expressions are queued up,</span>
<a name="l00148"></a>00148 <span class="comment"> * translate them too, until none are left. */</span>
<a name="l00149"></a>00149 <a class="code" href="classSAT_1_1Lit.html">Lit</a> <a class="code" href="classSAT_1_1CNF__Manager.html#abc4a95f97c6d2aa7a7584cd1bc30b743" title="Recursively translate e into cnf.">translateExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a>& thmIn, <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>& cnf);
<a name="l00150"></a>00150
<a name="l00151"></a>00151 <span class="comment">// bool isTranslated(const CVC3::Expr& e)</span>
<a name="l00152"></a>00152 <span class="comment">// { CVC3::CDMap<CVC3::Expr, bool>::iterator i = d_translated.find(e);</span>
<a name="l00153"></a>00153 <span class="comment">// return i != d_translated.end() && (*i).second; }</span>
<a name="l00154"></a>00154 <span class="comment">// void setTranslated(const CVC3::Expr& e)</span>
<a name="l00155"></a>00155 <span class="comment">// { DebugAssert(!isTranslated(e),"already set");</span>
<a name="l00156"></a>00156 <span class="comment">// d_translated.insert(e, true, d_bottomScope); }</span>
<a name="l00157"></a>00157 <span class="comment">// void clearTranslated(const CVC3::Expr& e)</span>
<a name="l00158"></a>00158 <span class="comment">// { d_translated.insert(e, false, d_bottomScope); }</span>
<a name="l00159"></a>00159
<a name="l00160"></a>00160 <span class="keyword">public</span>:
<a name="l00161"></a>00161 <a class="code" href="classSAT_1_1CNF__Manager.html#a7bb76ec26a37645bd0183715af69966f">CNF_Manager</a>(<a class="code" href="classCVC3_1_1TheoremManager.html">CVC3::TheoremManager</a>* tm, <a class="code" href="classCVC3_1_1Statistics.html">CVC3::Statistics</a>& statistics,
<a name="l00162"></a>00162 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CLFlags.html">CVC3::CLFlags</a>& flags);
<a name="l00163"></a>00163 <a class="code" href="classSAT_1_1CNF__Manager.html#a14a7c3223d238a6d9d0864692c450774">~CNF_Manager</a>();
<a name="l00164"></a>00164 <span class="comment"></span>
<a name="l00165"></a>00165 <span class="comment"> //! Register CNF callback</span>
<a name="l00166"></a><a class="code" href="classSAT_1_1CNF__Manager.html#a0d2b7a6369e9e7ad4ae6aca1398e404d">00166</a> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Manager.html#a0d2b7a6369e9e7ad4ae6aca1398e404d" title="Register CNF callback.">registerCNFCallback</a>(<a class="code" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html" title="Abstract class for callbacks.">CNFCallback</a>* cnfCallback)
<a name="l00167"></a>00167 { <a class="code" href="classSAT_1_1CNF__Manager.html#a81c6d45a1864f4266197e90de4649c14" title="Instance of CNF_CallBack: must be registered.">d_cnfCallback</a> = cnfCallback; }
<a name="l00168"></a>00168 <span class="comment"></span>
<a name="l00169"></a>00169 <span class="comment"> //! Set scope for translation</span>
<a name="l00170"></a><a class="code" href="classSAT_1_1CNF__Manager.html#a919041a34faf71a4c194be3da0b7dd23">00170</a> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Manager.html#a919041a34faf71a4c194be3da0b7dd23" title="Set scope for translation.">setBottomScope</a>(<span class="keywordtype">int</span> scope) { <a class="code" href="classSAT_1_1CNF__Manager.html#a60a763224b0c38233c65bfa1374f6ab0" title="Whether expr has already been translated.">d_bottomScope</a> = scope; }
<a name="l00171"></a>00171 <span class="comment"></span>
<a name="l00172"></a>00172 <span class="comment"> //! Return the number of variables being managed</span>
<a name="l00173"></a><a class="code" href="classSAT_1_1CNF__Manager.html#ad6052496e803e074e91efe7212360b23">00173</a> <span class="comment"></span> <span class="keywordtype">unsigned</span> <a class="code" href="classSAT_1_1CNF__Manager.html#ad6052496e803e074e91efe7212360b23" title="Return the number of variables being managed.">numVars</a>() { <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CNF__Manager.html#af6bda95f4cc0f85ac6cba04c66bd4a69" title="vector that maps a variable index to information for that variable">d_varInfo</a>.size(); }
<a name="l00174"></a>00174 <span class="comment"></span>
<a name="l00175"></a>00175 <span class="comment"> //! Return number of fanins for CNF node c</span>
<a name="l00176"></a>00176 <span class="comment"></span><span class="comment"> /*! A CNF node x is a fanin of CNF node y if the expr for x is a child of the</span>
<a name="l00177"></a>00177 <span class="comment"> * expr for y or if y is an ITE leaf and x is a new CNF node obtained by</span>
<a name="l00178"></a>00178 <span class="comment"> * translating the ITE leaf y.</span>
<a name="l00179"></a>00179 <span class="comment"> * \sa isITELeaf()</span>
<a name="l00180"></a>00180 <span class="comment"> */</span>
<a name="l00181"></a><a class="code" href="classSAT_1_1CNF__Manager.html#abfe9063da71565718c194cfa04e65805">00181</a> <span class="keywordtype">unsigned</span> <a class="code" href="classSAT_1_1CNF__Manager.html#abfe9063da71565718c194cfa04e65805" title="Return number of fanins for CNF node c.">numFanins</a>(<a class="code" href="classSAT_1_1Var.html">Var</a> c) {
<a name="l00182"></a>00182 <span class="keywordflow">if</span> (!c.<a class="code" href="classSAT_1_1Var.html#a685cd5d7b11f6ce00074de3e1241c708">isVar</a>()) <span class="keywordflow">return</span> 0;
<a name="l00183"></a>00183 <span class="keywordflow">if</span> (<span class="keywordtype">unsigned</span>(c) >= <a class="code" href="classSAT_1_1CNF__Manager.html#af6bda95f4cc0f85ac6cba04c66bd4a69" title="vector that maps a variable index to information for that variable">d_varInfo</a>.size()) <span class="keywordflow">return</span> 0;
<a name="l00184"></a>00184 <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CNF__Manager.html#af6bda95f4cc0f85ac6cba04c66bd4a69" title="vector that maps a variable index to information for that variable">d_varInfo</a>[c].fanins.size();
<a name="l00185"></a>00185 }
<a name="l00186"></a>00186 <span class="comment"></span>
<a name="l00187"></a>00187 <span class="comment"> //! Returns the ith fanin of c.</span>
<a name="l00188"></a><a class="code" href="classSAT_1_1CNF__Manager.html#a80f7c509fd352dd5ba7920ce1b6329a0">00188</a> <span class="comment"></span> <a class="code" href="classSAT_1_1Lit.html">Lit</a> <a class="code" href="classSAT_1_1CNF__Manager.html#a80f7c509fd352dd5ba7920ce1b6329a0" title="Returns the ith fanin of c.">getFanin</a>(<a class="code" href="classSAT_1_1Var.html">Var</a> c, <span class="keywordtype">unsigned</span> i) {
<a name="l00189"></a>00189 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(i < <a class="code" href="classSAT_1_1CNF__Manager.html#abfe9063da71565718c194cfa04e65805" title="Return number of fanins for CNF node c.">numFanins</a>(c), <span class="stringliteral">"attempt to access unknown fanin"</span>);
<a name="l00190"></a>00190 <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CNF__Manager.html#af6bda95f4cc0f85ac6cba04c66bd4a69" title="vector that maps a variable index to information for that variable">d_varInfo</a>[c].fanins[i];
<a name="l00191"></a>00191 }
<a name="l00192"></a>00192 <span class="comment"></span>
<a name="l00193"></a>00193 <span class="comment"> //! Return number of fanins for c</span>
<a name="l00194"></a>00194 <span class="comment"></span><span class="comment"> /*! x is a fanout of y if y is a fanin of x</span>
<a name="l00195"></a>00195 <span class="comment"> * \sa numFanins</span>
<a name="l00196"></a>00196 <span class="comment"> */</span>
<a name="l00197"></a><a class="code" href="classSAT_1_1CNF__Manager.html#a33ea4af8007dfd674a152e84d0df32a4">00197</a> <span class="keywordtype">unsigned</span> <a class="code" href="classSAT_1_1CNF__Manager.html#a33ea4af8007dfd674a152e84d0df32a4" title="Return number of fanins for c.">numFanouts</a>(<a class="code" href="classSAT_1_1Var.html">Var</a> c) {
<a name="l00198"></a>00198 <span class="keywordflow">if</span> (!c.<a class="code" href="classSAT_1_1Var.html#a685cd5d7b11f6ce00074de3e1241c708">isVar</a>()) <span class="keywordflow">return</span> 0;
<a name="l00199"></a>00199 <span class="keywordflow">if</span> (<span class="keywordtype">unsigned</span>(c) >= <a class="code" href="classSAT_1_1CNF__Manager.html#af6bda95f4cc0f85ac6cba04c66bd4a69" title="vector that maps a variable index to information for that variable">d_varInfo</a>.size()) <span class="keywordflow">return</span> 0;
<a name="l00200"></a>00200 <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CNF__Manager.html#af6bda95f4cc0f85ac6cba04c66bd4a69" title="vector that maps a variable index to information for that variable">d_varInfo</a>[c].fanouts.size();
<a name="l00201"></a>00201 }
<a name="l00202"></a>00202 <span class="comment"></span>
<a name="l00203"></a>00203 <span class="comment"> //! Returns the ith fanout of c.</span>
<a name="l00204"></a><a class="code" href="classSAT_1_1CNF__Manager.html#a3ea642d608115a728fb6454731f18549">00204</a> <span class="comment"></span> <a class="code" href="classSAT_1_1Lit.html">Lit</a> <a class="code" href="classSAT_1_1CNF__Manager.html#a3ea642d608115a728fb6454731f18549" title="Returns the ith fanout of c.">getFanout</a>(<a class="code" href="classSAT_1_1Var.html">Var</a> c, <span class="keywordtype">unsigned</span> i) {
<a name="l00205"></a>00205 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(i < <a class="code" href="classSAT_1_1CNF__Manager.html#a33ea4af8007dfd674a152e84d0df32a4" title="Return number of fanins for c.">numFanouts</a>(c), <span class="stringliteral">"attempt to access unknown fanin"</span>);
<a name="l00206"></a>00206 <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Lit.html">Lit</a>(<a class="code" href="classSAT_1_1CNF__Manager.html#af6bda95f4cc0f85ac6cba04c66bd4a69" title="vector that maps a variable index to information for that variable">d_varInfo</a>[c].fanouts[i]);
<a name="l00207"></a>00207 }
<a name="l00208"></a>00208 <span class="comment"></span>
<a name="l00209"></a>00209 <span class="comment"> //! Convert a CNF literal to an Expr literal</span>
<a name="l00210"></a>00210 <span class="comment"></span><span class="comment"> /*! Returns a NULL Expr if there is no corresponding Expr for l</span>
<a name="l00211"></a>00211 <span class="comment"> */</span>
<a name="l00212"></a><a class="code" href="classSAT_1_1CNF__Manager.html#a2c10ef5b4dff560013835d79c7e5fe74">00212</a> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">CVC3::Expr</a>& <a class="code" href="classSAT_1_1CNF__Manager.html#a2c10ef5b4dff560013835d79c7e5fe74" title="Convert a CNF literal to an Expr literal.">concreteVar</a>(<a class="code" href="classSAT_1_1Var.html">Var</a> v) {
<a name="l00213"></a>00213 <span class="keywordflow">if</span> (v.<a class="code" href="classSAT_1_1Var.html#a95b8a85adb5fa5eba0fc090c240558b9">isNull</a>()) <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CNF__Manager.html#af62a616e36e64bd10ddf06ec58b7caae" title="Reference to null Expr.">d_nullExpr</a>;
<a name="l00214"></a>00214 <span class="keywordflow">if</span> (<span class="keywordtype">unsigned</span>(v) >= <a class="code" href="classSAT_1_1CNF__Manager.html#af6bda95f4cc0f85ac6cba04c66bd4a69" title="vector that maps a variable index to information for that variable">d_varInfo</a>.size() ||
<a name="l00215"></a>00215 (!<a class="code" href="classSAT_1_1CNF__Manager.html#af6bda95f4cc0f85ac6cba04c66bd4a69" title="vector that maps a variable index to information for that variable">d_varInfo</a>[v].expr.isTranslated()))
<a name="l00216"></a>00216 <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CNF__Manager.html#af62a616e36e64bd10ddf06ec58b7caae" title="Reference to null Expr.">d_nullExpr</a>;
<a name="l00217"></a>00217 <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CNF__Manager.html#af6bda95f4cc0f85ac6cba04c66bd4a69" title="vector that maps a variable index to information for that variable">d_varInfo</a>[v].expr;
<a name="l00218"></a>00218 }
<a name="l00219"></a>00219 <span class="comment"></span>
<a name="l00220"></a>00220 <span class="comment"> //! Convert a CNF literal to an Expr literal</span>
<a name="l00221"></a>00221 <span class="comment"></span><span class="comment"> /*! Returns a NULL Expr if there is no corresponding Expr for l</span>
<a name="l00222"></a>00222 <span class="comment"> */</span>
<a name="l00223"></a><a class="code" href="classSAT_1_1CNF__Manager.html#a42c3cbd432324757f09ffd622ab1f057">00223</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">CVC3::Expr</a> <a class="code" href="classSAT_1_1CNF__Manager.html#a42c3cbd432324757f09ffd622ab1f057" title="Convert a CNF literal to an Expr literal.">concreteLit</a>(<a class="code" href="classSAT_1_1Lit.html">Lit</a> l, <span class="keywordtype">bool</span> checkTranslated = <span class="keyword">true</span>) {
<a name="l00224"></a>00224 <span class="keywordflow">if</span> (l.<a class="code" href="classSAT_1_1Lit.html#ad5f6236c582c95356d720a7401623f36">isNull</a>()) <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CNF__Manager.html#af62a616e36e64bd10ddf06ec58b7caae" title="Reference to null Expr.">d_nullExpr</a>;
<a name="l00225"></a>00225 <span class="keywordtype">bool</span> inverted = !l.<a class="code" href="classSAT_1_1Lit.html#ada14f3ca2b88500b5c2500d60e7f554b">isPositive</a>();
<a name="l00226"></a>00226 <span class="keywordtype">int</span> index = l.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>();
<a name="l00227"></a>00227 <span class="keywordflow">if</span> ((<span class="keywordtype">unsigned</span>)index >= <a class="code" href="classSAT_1_1CNF__Manager.html#af6bda95f4cc0f85ac6cba04c66bd4a69" title="vector that maps a variable index to information for that variable">d_varInfo</a>.size() ||
<a name="l00228"></a>00228 (checkTranslated && !<a class="code" href="classSAT_1_1CNF__Manager.html#af6bda95f4cc0f85ac6cba04c66bd4a69" title="vector that maps a variable index to information for that variable">d_varInfo</a>[index].expr.isTranslated()))
<a name="l00229"></a>00229 <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CNF__Manager.html#af62a616e36e64bd10ddf06ec58b7caae" title="Reference to null Expr.">d_nullExpr</a>;
<a name="l00230"></a>00230 <span class="keywordflow">return</span> inverted ? !<a class="code" href="classSAT_1_1CNF__Manager.html#af6bda95f4cc0f85ac6cba04c66bd4a69" title="vector that maps a variable index to information for that variable">d_varInfo</a>[index].expr : <a class="code" href="classSAT_1_1CNF__Manager.html#af6bda95f4cc0f85ac6cba04c66bd4a69" title="vector that maps a variable index to information for that variable">d_varInfo</a>[index].expr;
<a name="l00231"></a>00231 }
<a name="l00232"></a>00232 <span class="comment"></span>
<a name="l00233"></a>00233 <span class="comment"> //! Look up the CNF literal for an Expr</span>
<a name="l00234"></a>00234 <span class="comment"></span><span class="comment"> /*! Returns a NULL Lit if there is no corresponding CNF literal for e</span>
<a name="l00235"></a>00235 <span class="comment"> */</span>
<a name="l00236"></a><a class="code" href="classSAT_1_1CNF__Manager.html#a78c85b8b8b747f72d973ed0835294c5e">00236</a> <a class="code" href="classSAT_1_1Lit.html">Lit</a> <a class="code" href="classSAT_1_1CNF__Manager.html#a78c85b8b8b747f72d973ed0835294c5e" title="Look up the CNF literal for an Expr.">getCNFLit</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">CVC3::Expr</a>& e) {
<a name="l00237"></a>00237 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#ga6173f64b22cba76472cd0c814bbf6dae">isFalse</a>()) <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Lit.html#af31c280c018065d2c1232a2cb8503fa7">Lit::getFalse</a>();
<a name="l00238"></a>00238 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#gadf8596df73fa69ff8e6a22b9321f5c34">isTrue</a>()) <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Lit.html#ae639d83f877c976508d280a25c54e12b">Lit::getTrue</a>();
<a name="l00239"></a>00239 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>()) <span class="keywordflow">return</span> !<a class="code" href="classSAT_1_1CNF__Manager.html#a78c85b8b8b747f72d973ed0835294c5e" title="Look up the CNF literal for an Expr.">getCNFLit</a>(e[0]);
<a name="l00240"></a>00240 <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html">CVC3::ExprHashMap<Var>::iterator</a> i = <a class="code" href="classSAT_1_1CNF__Manager.html#ad3d2c901c7b8cc277639fb2aff90797b" title="Map from Exprs to Vars representing those Exprs.">d_cnfVars</a>.<a class="code" href="classCVC3_1_1ExprHashMap.html#aeffd58f05fbeb8f381ba2050adef7a2d">find</a>(e);
<a name="l00241"></a>00241 <span class="keywordflow">if</span> (!e.<a class="code" href="group__ExprPkg.html#gabe0b99a2c155f75ceedd4f06263ddebb">isTranslated</a>() || i == <a class="code" href="classSAT_1_1CNF__Manager.html#ad3d2c901c7b8cc277639fb2aff90797b" title="Map from Exprs to Vars representing those Exprs.">d_cnfVars</a>.<a class="code" href="classCVC3_1_1ExprHashMap.html#a0ea2aa250fd1431c311d83f32862bba7">end</a>()) <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Lit.html">Lit</a>();
<a name="l00242"></a>00242 <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Lit.html">Lit</a>((*i).second);
<a name="l00243"></a>00243 }
<a name="l00244"></a>00244
<a name="l00245"></a>00245 <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Manager.html#a56db0a07323ee4b11df78f88c8022db5">cons</a>(<span class="keywordtype">unsigned</span> lb, <span class="keywordtype">unsigned</span> ub, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">CVC3::Expr</a>& e2, std::vector<unsigned>& newLits);
<a name="l00246"></a>00246 <span class="comment"></span>
<a name="l00247"></a>00247 <span class="comment"> //! Convert thm A |- B (A is a set of literals) into one or more clauses</span>
<a name="l00248"></a>00248 <span class="comment"></span><span class="comment"> /*! cnf should be empty -- it will be filled with the result */</span>
<a name="l00249"></a>00249 <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Manager.html#ad8e26f917ea3a87a1013cbd154d16069" title="Convert thm A |- B (A is a set of literals) into one or more clauses.">convertLemma</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a>& thm, <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>& cnf);
<a name="l00250"></a>00250 <span class="comment"></span>
<a name="l00251"></a>00251 <span class="comment"> //! Given thm of form A |- B, convert B to CNF and add it to cnf</span>
<a name="l00252"></a>00252 <span class="comment"></span><span class="comment"> /*! Returns Lit corresponding to the root of the expression that was</span>
<a name="l00253"></a>00253 <span class="comment"> * translated. */</span>
<a name="l00254"></a>00254 <a class="code" href="classSAT_1_1Lit.html">Lit</a> <a class="code" href="classSAT_1_1CNF__Manager.html#a5cf1943a3bc3773fd0d8f64c123478f7" title="Given thm of form A |- B, convert B to CNF and add it to cnf.">addAssumption</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a>& thm, <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>& cnf);
<a name="l00255"></a>00255 <span class="comment"></span>
<a name="l00256"></a>00256 <span class="comment"> //! Convert thm to CNF and add it to the current formula</span>
<a name="l00257"></a>00257 <span class="comment"></span><span class="comment"> /*! \param thm should be of form A |- B where A is a set of literals.</span>
<a name="l00258"></a>00258 <span class="comment"> * \param cnf the new clauses are added to cnf.</span>
<a name="l00259"></a>00259 <span class="comment"> * Returns Lit corresponding to the root of the expression that was</span>
<a name="l00260"></a>00260 <span class="comment"> * translated. */</span>
<a name="l00261"></a>00261 <a class="code" href="classSAT_1_1Lit.html">Lit</a> <a class="code" href="classSAT_1_1CNF__Manager.html#aac0a2f51c8376029b88e1febc4cbd669" title="Convert thm to CNF and add it to the current formula.">addLemma</a>(<a class="code" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> thm, <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>& cnf);
<a name="l00262"></a>00262
<a name="l00263"></a>00263 };
<a name="l00264"></a>00264
<a name="l00265"></a>00265 }
<a name="l00266"></a>00266
<a name="l00267"></a>00267 <span class="preprocessor">#endif</span>
</pre></div></div>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
