<!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 Page</span></a></li> <li><a href="pages.html"><span>Related 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 List</span></a></li> <li><a href="globals.html"><span>File 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 <algorithm></span> <a name="l00055"></a>00055 <a name="l00056"></a>00056 <span class="preprocessor">#include <boost/shared_ptr.hpp></span> <a name="l00057"></a>00057 <span class="preprocessor">#include <boost/scoped_array.hpp></span> <a name="l00058"></a>00058 <a name="l00059"></a>00059 <span class="preprocessor">#include <boost/weak_ptr.hpp></span> <a name="l00060"></a>00060 <a name="l00061"></a>00061 <span class="preprocessor">#include <boost/intrusive_ptr.hpp></span> <a name="l00062"></a>00062 <a name="l00063"></a>00063 <span class="preprocessor">#include <boost/preprocessor/cat.hpp></span> <a name="l00064"></a>00064 <span class="preprocessor">#include <boost/preprocessor/seq/for_each.hpp></span> <a name="l00065"></a>00065 <span class="preprocessor">#include <boost/preprocessor/facilities/expand.hpp></span> <a name="l00066"></a>00066 <span class="preprocessor">#include <boost/preprocessor/stringize.hpp></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&#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->verbose) \</span> <a name="l00076"></a>00076 <span class="preprocessor"> std::cout << text << " for node " << node << \</span> <a name="l00077"></a>00077 <span class="preprocessor"> " ref = " << refCount() << std::endl;</span> <a name="l00078"></a>00078 <span class="preprocessor"></span> <a name="l00091"></a>00091 <span class="keyword">template</span> <<span class="keyword">class</span> DiagramType> <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&#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&#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&#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&#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&#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&#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&#39;s decision diagram structure...">CCuddDDBase</a>(<span class="keyword">const</span> <span class="keyword">self</span>& 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->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)->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&#39;s zero-suppressed decision diagram...">diagram_type</a>& 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->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<></a>(ddMgr->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&#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&#39;s zero-suppressed decision diagram...">diagram_type</a>& 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&#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&#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&#39;s zero-suppressed decision diagram...">diagram_type</a>& first, <span class="keyword">const</span> <a class="code" href="classpolybori_1_1CCuddZDD.html" title="This class defines a C++ interface to CUDD&#39;s zero-suppressed decision diagram...">diagram_type</a>& 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&#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&#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> <<span class="keyword">class</span> ResultType> <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> <<span class="keyword">class</span> ResultType> <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& operator BOOST_PP_CAT(op, =)(const self& 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& 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&#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&#39;s decision diagram structure...">CCuddDDBase</a><CCuddZDD> { <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&#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&#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&#39;s decision diagram structure...">CCuddDDBase<self></a> <a class="code" href="classpolybori_1_1CCuddDDBase.html" title="This template class defines a C++ interface to CUDD&#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&#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&#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> &from): <a class="code" href="classpolybori_1_1CCuddDDBase.html" title="This template class defines a C++ interface to CUDD&#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>& operator=(<span class="keyword">const</span> <span class="keyword">self</span>& 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>& 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>& 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<=</a>(<span class="keyword">const</span> <span class="keyword">self</span>& 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>=</a>(<span class="keyword">const</span> <span class="keyword">self</span>& other)<span class="keyword"> const </span>{ <a name="l00283"></a>00283 <span class="keywordflow">return</span> (other <= *<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<</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{ <a name="l00286"></a>00286 <span class="keywordflow">return</span> (*<span class="keyword">this</span> != rhs) && (*<span class="keyword">this</span> <= 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></a>(<span class="keyword">const</span> <span class="keyword">self</span>& other)<span class="keyword"> const </span>{ <a name="l00289"></a>00289 <span class="keywordflow">return</span> (*<span class="keyword">this</span> != other) && (*<span class="keyword">this</span> >= 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, (*)(&)) <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, (*)(&)(+)(|)(-)) <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&, <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& g, const self& 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->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& <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&#39;s zero-suppressed decision diagram...">CCuddZDD</a>& 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> == &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&#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 <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>