Sophie

Sophie

distrib > Mandriva > 2010.0 > i586 > media > contrib-release > by-pkgid > a24e1a39141f9b4ca49bd1e2e23a54ba > files > 55

polybori-doc-0.5rc.p9-6mdv2010.0.i586.rpm

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html><head><meta http-equiv="Content-Type" content="text/html;charset=UTF-8">
<title>PolyBoRi: CCuddZDD.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.5.9 -->
<div class="navigation" id="top">
  <div class="tabs">
    <ul>
      <li><a href="index.html"><span>Main&nbsp;Page</span></a></li>
      <li><a href="pages.html"><span>Related&nbsp;Pages</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 class="tabs">
    <ul>
      <li><a href="files.html"><span>File&nbsp;List</span></a></li>
      <li><a href="globals.html"><span>File&nbsp;Members</span></a></li>
    </ul>
  </div>
<h1>CCuddZDD.h</h1><a href="CCuddZDD_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">// -*- c++ -*-</span>
<a name="l00002"></a>00002 <span class="comment">//*****************************************************************************</span>
<a name="l00046"></a>00046 <span class="comment"></span><span class="comment">//*****************************************************************************</span>
<a name="l00047"></a>00047 
<a name="l00048"></a>00048 <span class="preprocessor">#ifndef CCuddZDD_h</span>
<a name="l00049"></a>00049 <span class="preprocessor"></span><span class="preprocessor">#define CCuddZDD_h</span>
<a name="l00050"></a>00050 <span class="preprocessor"></span>
<a name="l00051"></a>00051 <span class="comment">// include basic definitions</span>
<a name="l00052"></a>00052 <span class="preprocessor">#include "<a class="code" href="pbori__defs_8h.html">pbori_defs.h</a>"</span>
<a name="l00053"></a>00053 
<a name="l00054"></a>00054 <span class="preprocessor">#include &lt;algorithm&gt;</span>
<a name="l00055"></a>00055 
<a name="l00056"></a>00056 <span class="preprocessor">#include &lt;boost/shared_ptr.hpp&gt;</span>
<a name="l00057"></a>00057 <span class="preprocessor">#include &lt;boost/scoped_array.hpp&gt;</span>
<a name="l00058"></a>00058 
<a name="l00059"></a>00059 <span class="preprocessor">#include &lt;boost/weak_ptr.hpp&gt;</span>
<a name="l00060"></a>00060 
<a name="l00061"></a>00061 <span class="preprocessor">#include &lt;boost/intrusive_ptr.hpp&gt;</span>
<a name="l00062"></a>00062 
<a name="l00063"></a>00063 <span class="preprocessor">#include &lt;boost/preprocessor/cat.hpp&gt;</span>
<a name="l00064"></a>00064 <span class="preprocessor">#include &lt;boost/preprocessor/seq/for_each.hpp&gt;</span>
<a name="l00065"></a>00065 <span class="preprocessor">#include &lt;boost/preprocessor/facilities/expand.hpp&gt;</span>
<a name="l00066"></a>00066 <span class="preprocessor">#include &lt;boost/preprocessor/stringize.hpp&gt;</span>
<a name="l00067"></a>00067 
<a name="l00068"></a>00068 <span class="preprocessor">#include "<a class="code" href="pbori__func_8h.html">pbori_func.h</a>"</span>
<a name="l00069"></a>00069 <span class="preprocessor">#include "<a class="code" href="pbori__traits_8h.html">pbori_traits.h</a>"</span>
<a name="l00070"></a>00070 <span class="preprocessor">#include "<a class="code" href="CCuddCore_8h.html">CCuddCore.h</a>"</span>
<a name="l00071"></a>00071 
<a name="l00072"></a>00072 <a class="code" href="pbori__defs_8h.html#6ae360a591580558f31b6157ee792a10" title="Start project&amp;#39;s namespace.">BEGIN_NAMESPACE_PBORI</a>
<a name="l00073"></a>00073 
<a name="l00075"></a><a class="code" href="CCuddZDD_8h.html#238faddb2cb93ac90a60b290544f2478">00075</a> <span class="preprocessor">#define PB_DD_VERBOSE(text) if (ddMgr-&gt;verbose) \</span>
<a name="l00076"></a>00076 <span class="preprocessor">  std::cout &lt;&lt; text &lt;&lt; " for node " &lt;&lt; node &lt;&lt;  \</span>
<a name="l00077"></a>00077 <span class="preprocessor">  " ref = " &lt;&lt; refCount() &lt;&lt; std::endl;</span>
<a name="l00078"></a>00078 <span class="preprocessor"></span>
<a name="l00091"></a>00091 <span class="keyword">template</span> &lt;<span class="keyword">class</span> DiagramType&gt;
<a name="l00092"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html">00092</a> <span class="keyword">class </span><a class="code" href="classpolybori_1_1CCuddDDBase.html" title="This template class defines a C++ interface to CUDD&amp;#39;s decision diagram structure...">CCuddDDBase</a> {
<a name="l00093"></a>00093 
<a name="l00094"></a>00094 <span class="keyword">public</span>:
<a name="l00096"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#391b1ffc855218622a50828e60a8b81b">00096</a>   <span class="keyword">typedef</span> DiagramType <a class="code" href="classpolybori_1_1CCuddZDD.html" title="This class defines a C++ interface to CUDD&amp;#39;s zero-suppressed decision diagram...">diagram_type</a>;
<a name="l00097"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#48b1110773e989dd749f90b32b4a2f7d">00097</a>   <span class="keyword">typedef</span> <a class="code" href="classpolybori_1_1CCuddDDBase.html" title="This template class defines a C++ interface to CUDD&amp;#39;s decision diagram structure...">CCuddDDBase</a> <span class="keyword">self</span>;
<a name="l00098"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#f69191c127eda8bec7d92b0442175722">00098</a>   <a class="code" href="pbori__traits_8h.html#71c5e229a8a64d32fbf0a45acce725a4">PB_DECLARE_CUDD_TYPES</a>(<a class="code" href="classpolybori_1_1CCuddCore.html" title="This class prepares the CUDD&amp;#39;s raw decision diagram manager structure for the...">CCuddCore</a>)
<a name="l00099"></a>00099 
<a name="l00100"></a>00100   
<a name="l00101"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#d97630bfe1a2281ef8a8e1e592e7fe6c">00101</a>   typedef typename <a class="code" href="classpolybori_1_1CCuddCore.html" title="This class prepares the CUDD&amp;#39;s raw decision diagram manager structure for the...">CCuddCore</a>::mgrcore_ptr mgrcore_ptr;
<a name="l00102"></a>00102 
<a name="l00104"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#54b223d77e9f38554e8608e972f9738a">00104</a>   <a class="code" href="classpolybori_1_1CCuddDDBase.html" title="This template class defines a C++ interface to CUDD&amp;#39;s decision diagram structure...">CCuddDDBase</a>(mgrcore_ptr ddManager, node_type ddNode): 
<a name="l00105"></a>00105     ddMgr(ddManager), node(ddNode) {
<a name="l00106"></a>00106     <span class="keywordflow">if</span> (node) Cudd_Ref(node);
<a name="l00107"></a>00107     <a class="code" href="CCuddZDD_8h.html#238faddb2cb93ac90a60b290544f2478" title="Define code for verbosity.">PB_DD_VERBOSE</a>(<span class="stringliteral">"Standard DD constructor"</span>);
<a name="l00108"></a>00108   }
<a name="l00109"></a>00109 
<a name="l00111"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#cf757afe175b2fbb1f4588941701962e">00111</a>   <a class="code" href="classpolybori_1_1CCuddDDBase.html" title="This template class defines a C++ interface to CUDD&amp;#39;s decision diagram structure...">CCuddDDBase</a>(<span class="keyword">const</span> <span class="keyword">self</span>&amp; from): 
<a name="l00112"></a>00112     ddMgr(from.ddMgr), node(from.node) {
<a name="l00113"></a>00113     <span class="keywordflow">if</span> (node) {
<a name="l00114"></a>00114       Cudd_Ref(node);
<a name="l00115"></a>00115       <a class="code" href="CCuddZDD_8h.html#238faddb2cb93ac90a60b290544f2478" title="Define code for verbosity.">PB_DD_VERBOSE</a>(<span class="stringliteral">"Copy DD constructor"</span>);
<a name="l00116"></a>00116     }
<a name="l00117"></a>00117   } 
<a name="l00118"></a>00118 
<a name="l00120"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#3644d297a92973d85c50a3c4028f2ed8">00120</a>   <a class="code" href="classpolybori_1_1CCuddDDBase.html#3644d297a92973d85c50a3c4028f2ed8" title="Default constructor.">CCuddDDBase</a>(): ddMgr(mgrcore_ptr()), node(NULL) {}
<a name="l00121"></a>00121 
<a name="l00123"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#62a8036bffec87b45672752686a04d3e">00123</a>   mgrcore_ptr <a class="code" href="classpolybori_1_1CCuddDDBase.html#62a8036bffec87b45672752686a04d3e" title="Get (shared) pointer to decision diagram manager.">manager</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> ddMgr; }
<a name="l00124"></a>00124 
<a name="l00126"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#b6bd2a5d6c2d60fde0f8b1014c0828e3">00126</a>   mgrcore_type <a class="code" href="classpolybori_1_1CCuddDDBase.html#b6bd2a5d6c2d60fde0f8b1014c0828e3" title="Get raw decision diagram manager.">getManager</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> ddMgr-&gt;manager; }
<a name="l00127"></a>00127 
<a name="l00129"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#06ac24d1a26a7d8c747446ac3c366ae3">00129</a>   node_type <a class="code" href="classpolybori_1_1CCuddDDBase.html#06ac24d1a26a7d8c747446ac3c366ae3" title="Get raw node structure.">getNode</a>()<span class="keyword"> const</span>{  <span class="keywordflow">return</span> node; }
<a name="l00130"></a>00130 
<a name="l00132"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#0bf668194d6ec1daca72e5b00ef912b8">00132</a>   size_type <a class="code" href="classpolybori_1_1CCuddDDBase.html#0bf668194d6ec1daca72e5b00ef912b8" title="Get index of curent node.">NodeReadIndex</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> Cudd_NodeReadIndex(node); }
<a name="l00133"></a>00133 
<a name="l00135"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#3bc0fe9f735dc69549f1470b58fcd465">00135</a>   size_type <a class="code" href="classpolybori_1_1CCuddDDBase.html#3bc0fe9f735dc69549f1470b58fcd465" title="Number of nodes in the current decision diagram.">nodeCount</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> (size_type)(Cudd_DagSize(node)); }
<a name="l00136"></a>00136 
<a name="l00138"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#e9dbfa150d454a862e89df86387b8b11">00138</a>   size_type <a class="code" href="classpolybori_1_1CCuddDDBase.html#e9dbfa150d454a862e89df86387b8b11" title="Number of references pointing here.">refCount</a>()<span class="keyword"> const </span>{ 
<a name="l00139"></a>00139     assert(node != NULL);
<a name="l00140"></a>00140     <span class="keywordflow">return</span> Cudd_Regular(node)-&gt;ref;
<a name="l00141"></a>00141   }
<a name="l00142"></a>00142 
<a name="l00144"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#21fb4ba7b2c5ebfd589d8165b80e0295">00144</a>   <span class="keywordtype">bool</span> <a class="code" href="classpolybori_1_1CCuddDDBase.html#21fb4ba7b2c5ebfd589d8165b80e0295" title="Test whether diagram represents the empty set.">isZero</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> node == Cudd_ReadZero(getManager()); }
<a name="l00145"></a>00145 
<a name="l00146"></a>00146 <span class="keyword">protected</span>:
<a name="l00147"></a>00147 
<a name="l00149"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#fe4d5ec8989e7288c3b7d4b4eb0b7e61">00149</a>   <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1CCuddDDBase.html#fe4d5ec8989e7288c3b7d4b4eb0b7e61" title="Test, whether both operands.">checkSameManager</a>(<span class="keyword">const</span> <a class="code" href="classpolybori_1_1CCuddZDD.html" title="This class defines a C++ interface to CUDD&amp;#39;s zero-suppressed decision diagram...">diagram_type</a>&amp; other)<span class="keyword"> const </span>{
<a name="l00150"></a>00150     <span class="keywordflow">if</span> (getManager() != other.<a class="code" href="classpolybori_1_1CCuddDDBase.html#b6bd2a5d6c2d60fde0f8b1014c0828e3" title="Get raw decision diagram manager.">getManager</a>()) 
<a name="l00151"></a>00151       ddMgr-&gt;errorHandler(<span class="stringliteral">"Operands come from different manager."</span>);
<a name="l00152"></a>00152   }
<a name="l00153"></a>00153 
<a name="l00155"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#15929bf2955abb55a92d2f52ecf71d7c">00155</a>   <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1CCuddDDBase.html#15929bf2955abb55a92d2f52ecf71d7c" title="Check whether decision diagram operation in computing result was valid.">checkReturnValue</a>(<span class="keyword">const</span> node_type result)<span class="keyword"> const </span>{
<a name="l00156"></a>00156     checkReturnValue(result != NULL);
<a name="l00157"></a>00157   }
<a name="l00158"></a>00158 
<a name="l00160"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#be6c7c1eea057734a00785b4cdd398dd">00160</a>   <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1CCuddDDBase.html#be6c7c1eea057734a00785b4cdd398dd" title="Check whether previous decision diagram operation for validity.">checkReturnValue</a>(<span class="keyword">const</span> <span class="keywordtype">int</span> result, <span class="keyword">const</span> <span class="keywordtype">int</span> expected = 1)<span class="keyword"> const </span>{
<a name="l00161"></a>00161     <span class="keywordflow">if</span> <a class="code" href="pbori__defs_8h.html#2e5f5338d3e6181b9083eff7b9a3a50c">UNLIKELY</a>(result != expected)
<a name="l00162"></a>00162       <a class="code" href="structpolybori_1_1handle__error.html">handle_error&lt;&gt;</a>(ddMgr-&gt;errorHandler)(Cudd_ReadErrorCode( getManager() ));
<a name="l00163"></a>00163   } 
<a name="l00164"></a>00164 
<a name="l00166"></a>00166 
<a name="l00167"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#c8b0d225e46d231ee2231d8ff9a55da3">00167</a>   <a class="code" href="classpolybori_1_1CCuddZDD.html" title="This class defines a C++ interface to CUDD&amp;#39;s zero-suppressed decision diagram...">diagram_type</a> <a class="code" href="classpolybori_1_1CCuddDDBase.html#c8b0d225e46d231ee2231d8ff9a55da3">apply</a>(binary_function func, <span class="keyword">const</span> <a class="code" href="classpolybori_1_1CCuddZDD.html" title="This class defines a C++ interface to CUDD&amp;#39;s zero-suppressed decision diagram...">diagram_type</a>&amp; rhs)<span class="keyword"> const </span>{
<a name="l00168"></a>00168     checkSameManager(rhs);
<a name="l00169"></a>00169     <span class="keywordflow">return</span> checkedResult(func(getManager(), getNode(), rhs.<a class="code" href="classpolybori_1_1CCuddDDBase.html#06ac24d1a26a7d8c747446ac3c366ae3" title="Get raw node structure.">getNode</a>()));
<a name="l00170"></a>00170   }
<a name="l00171"></a>00171 
<a name="l00172"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#cf4a02bd71c486d5e21853128becade3">00172</a>   <a class="code" href="classpolybori_1_1CCuddZDD.html" title="This class defines a C++ interface to CUDD&amp;#39;s zero-suppressed decision diagram...">diagram_type</a> <a class="code" href="classpolybori_1_1CCuddDDBase.html#cf4a02bd71c486d5e21853128becade3">apply</a>(binary_int_function func, <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> idx)<span class="keyword"> const </span>{
<a name="l00173"></a>00173     <span class="keywordflow">return</span> checkedResult(func(getManager(), getNode(), idx) );
<a name="l00174"></a>00174   }
<a name="l00175"></a>00175 
<a name="l00176"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#4f67b58ba90935172f5f379ff0a17e29">00176</a>   <a class="code" href="classpolybori_1_1CCuddZDD.html" title="This class defines a C++ interface to CUDD&amp;#39;s zero-suppressed decision diagram...">diagram_type</a> apply(ternary_function func, 
<a name="l00177"></a>00177              <span class="keyword">const</span> <a class="code" href="classpolybori_1_1CCuddZDD.html" title="This class defines a C++ interface to CUDD&amp;#39;s zero-suppressed decision diagram...">diagram_type</a>&amp; first, <span class="keyword">const</span> <a class="code" href="classpolybori_1_1CCuddZDD.html" title="This class defines a C++ interface to CUDD&amp;#39;s zero-suppressed decision diagram...">diagram_type</a>&amp; second)<span class="keyword"> const </span>{
<a name="l00178"></a>00178     checkSameManager(first);
<a name="l00179"></a>00179     checkSameManager(second);
<a name="l00180"></a>00180     <span class="keywordflow">return</span> checkedResult(func(getManager(), getNode(), 
<a name="l00181"></a>00181                               first.<a class="code" href="classpolybori_1_1CCuddDDBase.html#06ac24d1a26a7d8c747446ac3c366ae3" title="Get raw node structure.">getNode</a>(), second.<a class="code" href="classpolybori_1_1CCuddDDBase.html#06ac24d1a26a7d8c747446ac3c366ae3" title="Get raw node structure.">getNode</a>()) );
<a name="l00182"></a>00182   }
<a name="l00183"></a>00183 
<a name="l00184"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#2595f576b6ccd83bdc8948fe03b89d54">00184</a>   <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> <a class="code" href="classpolybori_1_1CCuddDDBase.html#2595f576b6ccd83bdc8948fe03b89d54">apply</a>(int_unary_function func)<span class="keyword"> const </span>{
<a name="l00185"></a>00185     <span class="keywordflow">return</span> checkedResult(func(getManager(), getNode()) );
<a name="l00186"></a>00186   }
<a name="l00188"></a>00188 
<a name="l00190"></a>00190 
<a name="l00191"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#cd2bc6bf37f9eed1cc8d83a130f80ddf">00191</a>   <a class="code" href="classpolybori_1_1CCuddZDD.html" title="This class defines a C++ interface to CUDD&amp;#39;s zero-suppressed decision diagram...">diagram_type</a> <a class="code" href="classpolybori_1_1CCuddDDBase.html#cd2bc6bf37f9eed1cc8d83a130f80ddf">checkedResult</a>(node_type result)<span class="keyword"> const </span>{
<a name="l00192"></a>00192     checkReturnValue(result);
<a name="l00193"></a>00193     <span class="keywordflow">return</span> <a class="code" href="classpolybori_1_1CCuddZDD.html" title="This class defines a C++ interface to CUDD&amp;#39;s zero-suppressed decision diagram...">diagram_type</a>(manager(), result);
<a name="l00194"></a>00194   }
<a name="l00195"></a>00195 
<a name="l00196"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#3201741b2a68cc49d2d59e09e260d167">00196</a>   <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> <a class="code" href="classpolybori_1_1CCuddDDBase.html#3201741b2a68cc49d2d59e09e260d167">checkedResult</a>(<a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> result)<span class="keyword"> const </span>{
<a name="l00197"></a>00197     checkReturnValue(result);
<a name="l00198"></a>00198     <span class="keywordflow">return</span> result;
<a name="l00199"></a>00199   }
<a name="l00200"></a>00200 
<a name="l00201"></a>00201   <span class="keyword">template</span> &lt;<span class="keyword">class</span> ResultType&gt;
<a name="l00202"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#fbe5583631d0dd179981fbec39fcf03e">00202</a>   ResultType <a class="code" href="classpolybori_1_1CCuddDDBase.html#fbe5583631d0dd179981fbec39fcf03e">memApply</a>(ResultType (*func)(DdManager *, node_type))<span class="keyword"> const </span>{
<a name="l00203"></a>00203     <span class="keywordflow">return</span> memChecked(func(getManager(), getNode()) );
<a name="l00204"></a>00204   }
<a name="l00205"></a>00205 
<a name="l00206"></a>00206   <span class="keyword">template</span> &lt;<span class="keyword">class</span> ResultType&gt;
<a name="l00207"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#cd8e2c336b08d3e2b8df33fc06308a5e">00207</a>   ResultType <a class="code" href="classpolybori_1_1CCuddDDBase.html#cd8e2c336b08d3e2b8df33fc06308a5e">memChecked</a>(ResultType result)<span class="keyword"> const </span>{
<a name="l00208"></a>00208     checkReturnValue(result != (ResultType) CUDD_OUT_OF_MEM);
<a name="l00209"></a>00209     <span class="keywordflow">return</span> result;
<a name="l00210"></a>00210   }
<a name="l00211"></a>00211   <span class="comment">// @}</span>
<a name="l00212"></a>00212 
<a name="l00214"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#7a58ac30da7ec910e04fd7337f71a45f">00214</a>   mgrcore_ptr ddMgr;
<a name="l00215"></a>00215 
<a name="l00217"></a><a class="code" href="classpolybori_1_1CCuddDDBase.html#24f2ee03c37ed349f712265c1dc07648">00217</a>   node_type node;
<a name="l00218"></a>00218 }; <span class="comment">// CCuddDD</span>
<a name="l00219"></a>00219 
<a name="l00220"></a>00220 
<a name="l00221"></a><a class="code" href="CCuddZDD_8h.html#37e1a57a295d5cf6ff43d7f2269dc6bf">00221</a> <span class="preprocessor">#define PB_ZDD_APPLY(count, data, funcname) \</span>
<a name="l00222"></a>00222 <span class="preprocessor">  self funcname(data rhs) const {    \</span>
<a name="l00223"></a>00223 <span class="preprocessor">    return apply(BOOST_PP_CAT(Cudd_zdd, funcname), rhs); }</span>
<a name="l00224"></a>00224 <span class="preprocessor"></span>
<a name="l00225"></a><a class="code" href="CCuddZDD_8h.html#3e8be5cb01ea1e4fe17555995d61954d">00225</a> <span class="preprocessor">#define PB_ZDD_OP_ASSIGN(count, data, op) \</span>
<a name="l00226"></a>00226 <span class="preprocessor">  self&amp; operator BOOST_PP_CAT(op, =)(const self&amp; other) { \</span>
<a name="l00227"></a>00227 <span class="preprocessor">    return *this = (*this op other); }</span>
<a name="l00228"></a>00228 <span class="preprocessor"></span>
<a name="l00229"></a><a class="code" href="CCuddZDD_8h.html#b882caa7956b268673cb9b32ee235fcd">00229</a> <span class="preprocessor">#define PB_ZDD_OP(count, data, op) \</span>
<a name="l00230"></a>00230 <span class="preprocessor">  self operator op(const self&amp; other) const { return data(other); }</span>
<a name="l00231"></a>00231 <span class="preprocessor"></span>
<a name="l00232"></a>00232 
<a name="l00245"></a><a class="code" href="classpolybori_1_1CCuddZDD.html">00245</a> <span class="keyword">class </span><a class="code" href="classpolybori_1_1CCuddZDD.html" title="This class defines a C++ interface to CUDD&amp;#39;s zero-suppressed decision diagram...">CCuddZDD</a> : 
<a name="l00246"></a>00246   <span class="keyword">public</span> <a class="code" href="classpolybori_1_1CCuddDDBase.html" title="This template class defines a C++ interface to CUDD&amp;#39;s decision diagram structure...">CCuddDDBase</a>&lt;CCuddZDD&gt; {
<a name="l00247"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#8240dd6eb05b5479a1da9d0d4b3a7809">00247</a>     <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classpolybori_1_1CCuddInterface.html" title="This class defines a C++ interface to CUDD&amp;#39;s decicion diagram manager.">CCuddInterface</a>;
<a name="l00248"></a>00248 
<a name="l00249"></a>00249 <span class="keyword">public</span>:
<a name="l00251"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#5482a8472d5ec705d90b9daf501acd98">00251</a>   <span class="keyword">typedef</span> <a class="code" href="classpolybori_1_1CCuddZDD.html" title="This class defines a C++ interface to CUDD&amp;#39;s zero-suppressed decision diagram...">CCuddZDD</a> <span class="keyword">self</span>;
<a name="l00252"></a>00252 
<a name="l00254"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#2f77fafcaf70b2c8431f1fc004ab67e9">00254</a>   <span class="keyword">typedef</span> <a class="code" href="classpolybori_1_1CCuddDDBase.html" title="This template class defines a C++ interface to CUDD&amp;#39;s decision diagram structure...">CCuddDDBase&lt;self&gt;</a> <a class="code" href="classpolybori_1_1CCuddDDBase.html" title="This template class defines a C++ interface to CUDD&amp;#39;s decision diagram structure...">base</a>;
<a name="l00255"></a>00255  
<a name="l00257"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#8f99d6ca90ddda22d92ef9cfae6c38b6">00257</a>   <a class="code" href="classpolybori_1_1CCuddZDD.html#8f99d6ca90ddda22d92ef9cfae6c38b6" title="Construct ZDD from manager core and node.">CCuddZDD</a>(mgrcore_ptr mgr, node_type bddNode): <a class="code" href="classpolybori_1_1CCuddDDBase.html" title="This template class defines a C++ interface to CUDD&amp;#39;s decision diagram structure...">base</a>(mgr, bddNode) {}
<a name="l00258"></a>00258 
<a name="l00260"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#049af7c62f4ba0a24f6b453bf4ecef03">00260</a>   <a class="code" href="classpolybori_1_1CCuddZDD.html#049af7c62f4ba0a24f6b453bf4ecef03" title="Default constructor.">CCuddZDD</a>(): <a class="code" href="classpolybori_1_1CCuddDDBase.html" title="This template class defines a C++ interface to CUDD&amp;#39;s decision diagram structure...">base</a>() {}
<a name="l00261"></a>00261 
<a name="l00263"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#759b8d3882d8b4b20e9d62f3ced096b0">00263</a>   <a class="code" href="classpolybori_1_1CCuddZDD.html#759b8d3882d8b4b20e9d62f3ced096b0" title="Copy constructor.">CCuddZDD</a>(<span class="keyword">const</span> <span class="keyword">self</span> &amp;from): <a class="code" href="classpolybori_1_1CCuddDDBase.html" title="This template class defines a C++ interface to CUDD&amp;#39;s decision diagram structure...">base</a>(from) {}
<a name="l00264"></a>00264 
<a name="l00266"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#dd23220e968a4dc137ee15ffd03c61d4">00266</a>   <a class="code" href="classpolybori_1_1CCuddZDD.html#dd23220e968a4dc137ee15ffd03c61d4" title="Destructor.">~CCuddZDD</a>() { deref(); }
<a name="l00267"></a>00267 
<a name="l00269"></a>00269   <span class="keyword">self</span>&amp; operator=(<span class="keyword">const</span> <span class="keyword">self</span>&amp; right); <span class="comment">// inlined below</span>
<a name="l00270"></a>00270 
<a name="l00272"></a>00272 
<a name="l00273"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#64e6e8619c967aa056e3ccd18a6da548">00273</a>   <span class="keywordtype">bool</span> <a class="code" href="classpolybori_1_1CCuddZDD.html#64e6e8619c967aa056e3ccd18a6da548">operator==</a>(<span class="keyword">const</span> <span class="keyword">self</span>&amp; other)<span class="keyword"> const </span>{
<a name="l00274"></a>00274     checkSameManager(other);
<a name="l00275"></a>00275     <span class="keywordflow">return</span> node == other.node;
<a name="l00276"></a>00276   }
<a name="l00277"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#a46b34d67465b10942c9b4feb44eff63">00277</a>   <span class="keywordtype">bool</span> <a class="code" href="classpolybori_1_1CCuddZDD.html#a46b34d67465b10942c9b4feb44eff63">operator!=</a>(<span class="keyword">const</span> <span class="keyword">self</span>&amp; other)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> !(*<span class="keyword">this</span> == other); }
<a name="l00278"></a>00278 
<a name="l00279"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#88ce5eb97971f981d4722e66986c1124">00279</a>   <span class="keywordtype">bool</span> <a class="code" href="classpolybori_1_1CCuddZDD.html#88ce5eb97971f981d4722e66986c1124">operator&lt;=</a>(<span class="keyword">const</span> <span class="keyword">self</span>&amp; other)<span class="keyword"> const </span>{
<a name="l00280"></a>00280     <span class="keywordflow">return</span> apply(Cudd_zddDiffConst, other).isZero(); 
<a name="l00281"></a>00281   }
<a name="l00282"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#6b95e930ed06438b0f59f70fcdfc23a3">00282</a>   <span class="keywordtype">bool</span> <a class="code" href="classpolybori_1_1CCuddZDD.html#6b95e930ed06438b0f59f70fcdfc23a3">operator&gt;=</a>(<span class="keyword">const</span> <span class="keyword">self</span>&amp; other)<span class="keyword"> const </span>{
<a name="l00283"></a>00283     <span class="keywordflow">return</span> (other &lt;= *<span class="keyword">this</span>); 
<a name="l00284"></a>00284   }
<a name="l00285"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#9e4f8a58dae680ac2f116079fd1487c3">00285</a>   <span class="keywordtype">bool</span> <a class="code" href="classpolybori_1_1CCuddZDD.html#9e4f8a58dae680ac2f116079fd1487c3">operator&lt;</a>(<span class="keyword">const</span> <span class="keyword">self</span>&amp; rhs)<span class="keyword"> const </span>{ 
<a name="l00286"></a>00286     <span class="keywordflow">return</span> (*<span class="keyword">this</span> != rhs) &amp;&amp; (*<span class="keyword">this</span> &lt;= rhs);  
<a name="l00287"></a>00287   }
<a name="l00288"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#de2663a7b133e774581de9369c2204f6">00288</a>   <span class="keywordtype">bool</span> <a class="code" href="classpolybori_1_1CCuddZDD.html#de2663a7b133e774581de9369c2204f6">operator&gt;</a>(<span class="keyword">const</span> <span class="keyword">self</span>&amp; other)<span class="keyword"> const </span>{ 
<a name="l00289"></a>00289     <span class="keywordflow">return</span> (*<span class="keyword">this</span> != other) &amp;&amp; (*<span class="keyword">this</span> &gt;= other); 
<a name="l00290"></a>00290   }
<a name="l00292"></a>00292 
<a name="l00295"></a>00295   BOOST_PP_SEQ_FOR_EACH(<a class="code" href="CCuddZDD_8h.html#b882caa7956b268673cb9b32ee235fcd">PB_ZDD_OP</a>, Intersect, (*)(&amp;))
<a name="l00296"></a>00296   BOOST_PP_SEQ_FOR_EACH(<a class="code" href="CCuddZDD_8h.html#b882caa7956b268673cb9b32ee235fcd">PB_ZDD_OP</a>, Union, (+)(|))
<a name="l00297"></a>00297   BOOST_PP_SEQ_FOR_EACH(PB_ZDD_OP, Diff, (-))
<a name="l00298"></a>00298 
<a name="l00299"></a>00299   BOOST_PP_SEQ_FOR_EACH(<a class="code" href="CCuddZDD_8h.html#3e8be5cb01ea1e4fe17555995d61954d">PB_ZDD_OP_ASSIGN</a>, BOOST_PP_NIL, (*)(&amp;)(+)(|)(-))
<a name="l00300"></a>00300 
<a name="l00301"></a>00301   BOOST_PP_SEQ_FOR_EACH(<a class="code" href="CCuddZDD_8h.html#37e1a57a295d5cf6ff43d7f2269dc6bf">PB_ZDD_APPLY</a>, const self&amp;, 
<a name="l00302"></a>00302     (Product)(UnateProduct)(WeakDiv)(Divide)(WeakDivF)(DivideF)
<a name="l00303"></a>00303     (Union)(Intersect)(Diff)(DiffConst))
<a name="l00304"></a>00304 
<a name="l00305"></a>00305   BOOST_PP_SEQ_FOR_EACH(PB_ZDD_APPLY, <span class="keywordtype">int</span>, (Subset1)(Subset0)(Change))
<a name="l00308"></a>00308 
<a name="l00309"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#ce06e0bef564385e00db52bd5d527db5">00309</a>   self Ite(const self&amp; g, const self&amp; h)<span class="keyword"> const </span>{ 
<a name="l00310"></a>00310     <span class="keywordflow">return</span> apply(Cudd_zddIte, g, h); 
<a name="l00311"></a>00311   }
<a name="l00312"></a>00312 
<a name="l00314"></a>00314 
<a name="l00315"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#64e8985c7638d23261d89c19f7310c28">00315</a>   <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1CCuddZDD.html#64e8985c7638d23261d89c19f7310c28">print</a>(<span class="keywordtype">int</span> nvars, <span class="keywordtype">int</span> verbosity = 1)<span class="keyword"> const </span>{ std::cout.flush(); 
<a name="l00316"></a>00316     <span class="keywordflow">if</span> <a class="code" href="pbori__defs_8h.html#2e5f5338d3e6181b9083eff7b9a3a50c">UNLIKELY</a>(!Cudd_zddPrintDebug(getManager(), node, nvars, verbosity))
<a name="l00317"></a>00317       ddMgr-&gt;errorHandler(<span class="stringliteral">"print failed"</span>);
<a name="l00318"></a>00318   }
<a name="l00319"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#a6b8b7ee12fda518f1e2347d971a38ae">00319</a>   <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1CCuddZDD.html#a6b8b7ee12fda518f1e2347d971a38ae">PrintMinterm</a>()<span class="keyword"> const  </span>{ apply(Cudd_zddPrintMinterm); }
<a name="l00320"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#434a08016f9e62bebf5c080e7a3cf3da">00320</a>   <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1CCuddZDD.html#434a08016f9e62bebf5c080e7a3cf3da">PrintCover</a>()<span class="keyword"> const    </span>{ apply(Cudd_zddPrintCover); }
<a name="l00322"></a>00322 
<a name="l00324"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#5b697219f5bc607d12d39d6ca807a5a3">00324</a>   <span class="keywordtype">int</span> <a class="code" href="classpolybori_1_1CCuddZDD.html#5b697219f5bc607d12d39d6ca807a5a3" title="Determine the number of minterms.">Count</a>()<span class="keyword"> const          </span>{ <span class="keywordflow">return</span> memApply(Cudd_zddCount); }
<a name="l00325"></a>00325 
<a name="l00327"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#3b0f406e8338a5a465eda97a988c5fbc">00327</a>   <span class="keywordtype">double</span> <a class="code" href="classpolybori_1_1CCuddZDD.html#3b0f406e8338a5a465eda97a988c5fbc" title="Determine the number of minterms.">CountDouble</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> memApply(Cudd_zddCountDouble); }
<a name="l00328"></a>00328 
<a name="l00330"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#e4fd8fbe27e4c52be9a070ed90512f8d">00330</a>   <span class="keywordtype">double</span> <a class="code" href="classpolybori_1_1CCuddZDD.html#e4fd8fbe27e4c52be9a070ed90512f8d" title="Counts minterms; takes a path specifing variables number in the support.">CountMinterm</a>(<span class="keywordtype">int</span> path)<span class="keyword"> const </span>{ 
<a name="l00331"></a>00331     <span class="keywordflow">return</span> memChecked(Cudd_zddCountMinterm(getManager(), getNode(), path));
<a name="l00332"></a>00332   }
<a name="l00333"></a>00333 
<a name="l00334"></a>00334 <span class="keyword">protected</span>:
<a name="l00335"></a>00335 
<a name="l00336"></a>00336 
<a name="l00338"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#5b4d07cc47ca31b01d4fffbfe6c6eb3d">00338</a>   <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1CCuddZDD.html#5b4d07cc47ca31b01d4fffbfe6c6eb3d" title="Derefering current diagram node, if unused.">deref</a>() {
<a name="l00339"></a>00339     <span class="keywordflow">if</span> (node != 0) {
<a name="l00340"></a>00340       Cudd_RecursiveDerefZdd(getManager(), node);
<a name="l00341"></a>00341       <a class="code" href="CCuddZDD_8h.html#238faddb2cb93ac90a60b290544f2478" title="Define code for verbosity.">PB_DD_VERBOSE</a>(<span class="stringliteral">"CCuddZDD dereferencing"</span>);
<a name="l00342"></a>00342     }
<a name="l00343"></a>00343   }
<a name="l00344"></a>00344 }; <span class="comment">//CCuddZDD</span>
<a name="l00345"></a>00345 
<a name="l00346"></a>00346 <span class="preprocessor">#undef PB_ZDD_APPLY</span>
<a name="l00347"></a>00347 <span class="preprocessor"></span><span class="preprocessor">#undef PB_ZDD_OP_ASSIGN</span>
<a name="l00348"></a>00348 <span class="preprocessor"></span><span class="preprocessor">#undef PB_ZDD_OP</span>
<a name="l00349"></a>00349 <span class="preprocessor"></span>
<a name="l00350"></a>00350 <span class="comment">// ---------------------------------------------------------------------------</span>
<a name="l00351"></a>00351 <span class="comment">// Members of class CCuddZDD</span>
<a name="l00352"></a>00352 <span class="comment">// ---------------------------------------------------------------------------</span>
<a name="l00353"></a>00353 
<a name="l00354"></a>00354 <span class="keyword">inline</span> CCuddZDD&amp; 
<a name="l00355"></a><a class="code" href="classpolybori_1_1CCuddZDD.html#fa54de9d0aec31e35f49e2fe2a3a82a6">00355</a> CCuddZDD::operator=(<span class="keyword">const</span> <a class="code" href="classpolybori_1_1CCuddZDD.html" title="This class defines a C++ interface to CUDD&amp;#39;s zero-suppressed decision diagram...">CCuddZDD</a>&amp; right) {
<a name="l00356"></a>00356 
<a name="l00357"></a>00357   <span class="keywordflow">if</span> <a class="code" href="pbori__defs_8h.html#2e5f5338d3e6181b9083eff7b9a3a50c">UNLIKELY</a>(<span class="keyword">this</span> == &amp;right) <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00358"></a>00358   <span class="keywordflow">if</span> <a class="code" href="pbori__defs_8h.html#1c5951c9a391674be15ca2883c98c7e1" title="For optimizing if-branches.">LIKELY</a>(right.<a class="code" href="classpolybori_1_1CCuddDDBase.html#24f2ee03c37ed349f712265c1dc07648" title="Raw pointer to decision diagram node.">node</a>) Cudd_Ref(right.<a class="code" href="classpolybori_1_1CCuddDDBase.html#24f2ee03c37ed349f712265c1dc07648" title="Raw pointer to decision diagram node.">node</a>);
<a name="l00359"></a>00359   <a class="code" href="classpolybori_1_1CCuddZDD.html#5b4d07cc47ca31b01d4fffbfe6c6eb3d" title="Derefering current diagram node, if unused.">deref</a>();
<a name="l00360"></a>00360   
<a name="l00361"></a>00361   <a class="code" href="classpolybori_1_1CCuddDDBase.html#24f2ee03c37ed349f712265c1dc07648" title="Raw pointer to decision diagram node.">node</a> = right.<a class="code" href="classpolybori_1_1CCuddDDBase.html#24f2ee03c37ed349f712265c1dc07648" title="Raw pointer to decision diagram node.">node</a>;
<a name="l00362"></a>00362   <a class="code" href="classpolybori_1_1CCuddDDBase.html#7a58ac30da7ec910e04fd7337f71a45f" title="(Smart) pointer to decsion diagram management">ddMgr</a> = right.<a class="code" href="classpolybori_1_1CCuddDDBase.html#7a58ac30da7ec910e04fd7337f71a45f" title="(Smart) pointer to decsion diagram management">ddMgr</a>;
<a name="l00363"></a>00363   <span class="keywordflow">if</span> (<a class="code" href="classpolybori_1_1CCuddDDBase.html#24f2ee03c37ed349f712265c1dc07648" title="Raw pointer to decision diagram node.">node</a>)
<a name="l00364"></a>00364     <a class="code" href="CCuddZDD_8h.html#238faddb2cb93ac90a60b290544f2478" title="Define code for verbosity.">PB_DD_VERBOSE</a>(<span class="stringliteral">"CCuddZDD assignment"</span>);
<a name="l00365"></a>00365   
<a name="l00366"></a>00366   <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00367"></a>00367 }
<a name="l00368"></a>00368 
<a name="l00369"></a>00369 <span class="preprocessor">#undef PB_DD_VERBOSE</span>
<a name="l00370"></a>00370 <span class="preprocessor"></span>
<a name="l00371"></a>00371 <a class="code" href="pbori__defs_8h.html#faf094fde6c1a7f1aad18bcb455f3b06" title="Finish project&amp;#39;s namespace.">END_NAMESPACE_PBORI</a>
<a name="l00372"></a>00372 
<a name="l00373"></a>00373 <span class="preprocessor">#endif</span>
<a name="l00374"></a>00374 <span class="preprocessor"></span>
<a name="l00375"></a>00375 
</pre></div></div>
<hr size="1"><address style="text-align: right;"><small>Generated on Wed Sep 9 14:30:54 2009 for PolyBoRi by&nbsp;
<a href="http://www.doxygen.org/index.html">
<img src="doxygen.png" alt="doxygen" align="middle" border="0"></a> 1.5.9 </small></address>
</body>
</html>