<!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: CCuddNavigator.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>CCuddNavigator.h</h1><a href="CCuddNavigator_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="l00093"></a>00093 <span class="comment"></span><span class="comment">//*****************************************************************************</span> <a name="l00094"></a>00094 <a name="l00095"></a>00095 <span class="preprocessor">#include <iterator></span> <a name="l00096"></a>00096 <a name="l00097"></a>00097 <span class="comment">// include basic definitions</span> <a name="l00098"></a>00098 <span class="preprocessor">#include "<a class="code" href="pbori__defs_8h.html">pbori_defs.h</a>"</span> <a name="l00099"></a>00099 <span class="preprocessor">#include "<a class="code" href="pbori__tags_8h.html">pbori_tags.h</a>"</span> <a name="l00100"></a>00100 <a name="l00101"></a>00101 <span class="preprocessor">#include "<a class="code" href="CCuddInterface_8h.html">CCuddInterface.h</a>"</span> <a name="l00102"></a>00102 <a name="l00103"></a>00103 <a name="l00104"></a>00104 <span class="preprocessor">#ifndef CCuddNavigator_h_</span> <a name="l00105"></a>00105 <span class="preprocessor"></span><span class="preprocessor">#define CCuddNavigator_h_</span> <a name="l00106"></a>00106 <span class="preprocessor"></span> <a name="l00107"></a>00107 <a class="code" href="pbori__defs_8h.html#6ae360a591580558f31b6157ee792a10" title="Start project&#39;s namespace.">BEGIN_NAMESPACE_PBORI</a> <a name="l00108"></a>00108 <a name="l00115"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html">00115</a> <span class="keyword">class </span><a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">CCuddNavigator</a> { <a name="l00116"></a>00116 <a name="l00117"></a>00117 <span class="keyword">public</span>: <a name="l00119"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#8c2a3518d0c3b93751586e7ff67f578f">00119</a> <span class="keyword">typedef</span> DdNode* pointer_type; <a name="l00120"></a>00120 <a name="l00122"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#f28e183b4366310d51d848171f03f46d">00122</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...">CTypes::dd_base</a> <a class="code" href="classpolybori_1_1CCuddZDD.html" title="This class defines a C++ interface to CUDD&#39;s zero-suppressed decision diagram...">dd_base</a>; <a name="l00123"></a>00123 <a name="l00125"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#79d298c75097aea886d3843ac4ba27a1">00125</a> <span class="keyword">typedef</span> <span class="keyword">const</span> pointer_type const_access_type; <a name="l00126"></a>00126 <a name="l00128"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#8de42543eb01b34efac8e963752c3be9">00128</a> <span class="keyword">typedef</span> <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">CTypes::idx_type</a> <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a>; <a name="l00129"></a>00129 <a name="l00131"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#164825b7261631e0ebe683cd4d9713a8">00131</a> <span class="keyword">typedef</span> CTypes::size_type size_type; <a name="l00132"></a>00132 <a name="l00134"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#067c677f8731ac1ffd4a53e3e2926e8e">00134</a> <span class="keyword">typedef</span> CTypes::hash_type hash_type; <a name="l00135"></a>00135 <a name="l00137"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#8be6ae464c6a121b7daa58a665f9c3b5">00137</a> <span class="keyword">typedef</span> CTypes::bool_type bool_type; <a name="l00138"></a>00138 <a name="l00140"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#5f265068f97d3a335d30c65ba9d5d8fd">00140</a> <span class="keyword">typedef</span> <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> value_type; <a name="l00141"></a>00141 <a name="l00143"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#be2a710c2a21e85039423376066fd16f">00143</a> <span class="keyword">typedef</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">CCuddNavigator</a> <span class="keyword">self</span>; <a name="l00144"></a>00144 <a name="l00146"></a>00146 <a name="l00147"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#5905cb8634f62f371054b74c8e56dc51">00147</a> <span class="keyword">typedef</span> <a class="code" href="structpolybori_1_1navigator__tag.html" title="for iterator_category">navigator_tag</a> <a class="code" href="structpolybori_1_1navigator__tag.html" title="for iterator_category">iterator_category</a>; <a name="l00148"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#2c71fe8b0785e3b97fa8a16e804ba91a">00148</a> <span class="keyword">typedef</span> std::iterator_traits<pointer_type>::difference_type difference_type; <a name="l00149"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#3ecaa70dba4ec25cccdb22549d280134">00149</a> <span class="keyword">typedef</span> <span class="keywordtype">void</span> pointer; <a name="l00150"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#dbf2ab6a790006de8d83150e01fbf865">00150</a> <span class="keyword">typedef</span> value_type reference; <a name="l00152"></a>00152 <a name="l00154"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#a66dc44b2f904dcbee61d2af816869a0">00154</a> <a class="code" href="classpolybori_1_1CCuddNavigator.html#a66dc44b2f904dcbee61d2af816869a0" title="Default constructor.">CCuddNavigator</a>(): pNode(NULL) {} <a name="l00155"></a>00155 <a name="l00157"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#692d0757032fc8b46801d2ecd3e8311a">00157</a> <span class="keyword">explicit</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html#692d0757032fc8b46801d2ecd3e8311a" title="Construct from node pointer.">CCuddNavigator</a>(pointer_type ptr): pNode(ptr) { <a name="l00158"></a>00158 assert(isValid()); <a name="l00159"></a>00159 } <a name="l00160"></a>00160 <a name="l00162"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#ee88d365e69eb33d1f05a4ec28f28d31">00162</a> <span class="keyword">explicit</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html#ee88d365e69eb33d1f05a4ec28f28d31" title="Construct from decision diagram.">CCuddNavigator</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...">dd_base</a>& rhs): pNode(rhs.getNode()) {} <a name="l00163"></a>00163 <a name="l00165"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#626f0cc9014ea4e2ff695120a9842f74">00165</a> <a class="code" href="classpolybori_1_1CCuddNavigator.html#626f0cc9014ea4e2ff695120a9842f74" title="Copy Constructor.">CCuddNavigator</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs): pNode(rhs.pNode) {} <a name="l00166"></a>00166 <a name="l00168"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#b4c25e02c22615c49f5e6e74eadf649a">00168</a> <a class="code" href="classpolybori_1_1CCuddNavigator.html#b4c25e02c22615c49f5e6e74eadf649a" title="Destructor.">~CCuddNavigator</a>() {} <a name="l00169"></a>00169 <a name="l00171"></a>00171 <span class="keyword">self</span>& incrementThen(); <span class="comment">// inlined below</span> <a name="l00172"></a>00172 <a name="l00174"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#f2d46ab831a4baaefdce05fb686b07f5">00174</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html#f2d46ab831a4baaefdce05fb686b07f5" title="Increment in then direction.">thenBranch</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <span class="keyword">self</span>(*this).<a class="code" href="classpolybori_1_1CCuddNavigator.html#509ef978bd47f74e651411ec2fe50ad3" title="Increment in then direction.">incrementThen</a>(); } <a name="l00175"></a>00175 <a name="l00177"></a>00177 <span class="keyword">self</span>& incrementElse(); <span class="comment">// inlined below</span> <a name="l00178"></a>00178 <a name="l00180"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#bad998777186a38fa0db7acf2ac086d6">00180</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html#bad998777186a38fa0db7acf2ac086d6" title="Increment in else direction.">elseBranch</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <span class="keyword">self</span>(*this).<a class="code" href="classpolybori_1_1CCuddNavigator.html#347269fc9b99ffec1b93bbd6f44bcf27" title="Increment in else direction.">incrementElse</a>(); } <a name="l00181"></a>00181 <a name="l00183"></a>00183 reference <a class="code" href="namespacepolybori.html#77e199828cafa5b365a0bd01d8ba7e02" title="Multiplication of monomials.">operator*</a>() <span class="keyword">const</span>; <span class="comment">// inlined below</span> <a name="l00184"></a>00184 <a name="l00186"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#62c601bf5bb0935aedafa980c237feff">00186</a> const_access_type <a class="code" href="classpolybori_1_1CCuddNavigator.html#62c601bf5bb0935aedafa980c237feff" title="Constant pointer access operator.">operator-></a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> pNode; } <a name="l00187"></a>00187 <a name="l00189"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#0244a90132338327589f7447edadfe56">00189</a> const_access_type <a class="code" href="classpolybori_1_1CCuddNavigator.html#0244a90132338327589f7447edadfe56" title="Constant pointer access operator.">getNode</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> pNode; } <a name="l00190"></a>00190 <a name="l00192"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#9dcf1d9c2cae3f72cdb2ecb0d0380d7e">00192</a> hash_type <a class="code" href="classpolybori_1_1CCuddNavigator.html#9dcf1d9c2cae3f72cdb2ecb0d0380d7e" title="Constant pointer access operator.">hash</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <span class="keyword">reinterpret_cast<</span><span class="keywordtype">long</span><span class="keyword">></span>(pNode); } <a name="l00193"></a>00193 <a name="l00195"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#0f63f52b4bc8bd6195ea6cb9cf6a9e93">00195</a> bool_type <a class="code" href="classpolybori_1_1CCuddNavigator.html#0f63f52b4bc8bd6195ea6cb9cf6a9e93" title="Equality test.">operator==</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> (pNode == rhs.pNode); } <a name="l00196"></a>00196 <a name="l00198"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#83b7f2331a2a14729e3c9e7226af159a">00198</a> bool_type <a class="code" href="classpolybori_1_1CCuddNavigator.html#83b7f2331a2a14729e3c9e7226af159a" title="Nonequality test.">operator!=</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> (pNode != rhs.pNode); } <a name="l00199"></a>00199 <a name="l00201"></a>00201 bool_type isConstant() <span class="keyword">const</span>; <span class="comment">// inlined below</span> <a name="l00202"></a>00202 <a name="l00204"></a>00204 bool_type terminalValue() <span class="keyword">const</span>; <span class="comment">// inlined below</span> <a name="l00205"></a>00205 <a name="l00207"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#458deac816e54ad5d5293b2461d4e36e">00207</a> bool_type <a class="code" href="classpolybori_1_1CCuddNavigator.html#458deac816e54ad5d5293b2461d4e36e" title="Check whether *this is not the default iterator self() (NULL pointer).">isValid</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> (pNode != NULL); } <a name="l00208"></a>00208 <a name="l00210"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#f175a18a699044106209a27129cdb41f">00210</a> bool_type <a class="code" href="classpolybori_1_1CCuddNavigator.html#f175a18a699044106209a27129cdb41f" title="Check whether end of path was reached.">isTerminated</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> isConstant() && terminalValue(); } <a name="l00211"></a>00211 <a name="l00213"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#381305661115f5a32d727c82649a066f">00213</a> bool_type <a class="code" href="classpolybori_1_1CCuddNavigator.html#381305661115f5a32d727c82649a066f" title="Check whether dead end was reached.">isEmpty</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> isConstant() && !terminalValue(); } <a name="l00214"></a>00214 <a name="l00216"></a>00216 <a name="l00217"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#56e9a97f4a6a08cfdbc37bae0ff230bb">00217</a> bool_type <a class="code" href="classpolybori_1_1CCuddNavigator.html#56e9a97f4a6a08cfdbc37bae0ff230bb">operator<</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> (pNode < rhs.pNode); } <a name="l00218"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#73646f1587f490dfde10ad2169f59a21">00218</a> bool_type <a class="code" href="classpolybori_1_1CCuddNavigator.html#73646f1587f490dfde10ad2169f59a21">operator<=</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> (pNode <= rhs.pNode); } <a name="l00219"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#585ab4594c351307e7fa158f41072dbb">00219</a> bool_type <a class="code" href="classpolybori_1_1CCuddNavigator.html#585ab4594c351307e7fa158f41072dbb">operator></a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> (pNode > rhs.pNode); } <a name="l00220"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#ff30ee566b63e53e8701d65e38e8c5b2">00220</a> bool_type <a class="code" href="classpolybori_1_1CCuddNavigator.html#ff30ee566b63e53e8701d65e38e8c5b2">operator>=</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> (pNode >= rhs.pNode); } <a name="l00222"></a>00222 <a name="l00224"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#ab995a3941060c3745506044c8a91da7">00224</a> <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html#ab995a3941060c3745506044c8a91da7" title="Force incrementation of reference count.">incRef</a>()<span class="keyword"> const </span>{ assert(isValid()); Cudd_Ref(pNode); } <a name="l00225"></a>00225 <a name="l00227"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#d0d404eebf6c0b8ef38377a3b9eb4c0a">00227</a> <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html#d0d404eebf6c0b8ef38377a3b9eb4c0a" title="Force decrementation of reference count.">decRef</a>()<span class="keyword"> const </span>{ assert(isValid()); Cudd_Deref(pNode); } <a name="l00228"></a>00228 <a name="l00230"></a>00230 <span class="keyword">template</span> <<span class="keyword">class</span> MgrType> <a name="l00231"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#2c9629342083e284ef9ef68242df950a">00231</a> <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html#2c9629342083e284ef9ef68242df950a" title="Force recursive decrementation of reference count.">recursiveDecRef</a>(<span class="keyword">const</span> MgrType& mgr)<span class="keyword"> const </span>{ <a name="l00232"></a>00232 assert(isValid()); <a name="l00233"></a>00233 Cudd_RecursiveDerefZdd(mgr, pNode); <a name="l00234"></a>00234 } <a name="l00235"></a>00235 <a name="l00236"></a>00236 <span class="keyword">private</span>: <a name="l00238"></a>00238 pointer_type pNode; <a name="l00239"></a>00239 }; <a name="l00240"></a>00240 <a name="l00241"></a>00241 <span class="comment">// Inlined member functions</span> <a name="l00242"></a>00242 <a name="l00243"></a>00243 <span class="comment">// constant pointer access operator</span> <a name="l00244"></a>00244 <span class="keyword">inline</span> CCuddNavigator::value_type <a name="l00245"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#91712f6cf663ad2783e4b4939ffa5b64">00245</a> <a class="code" href="namespacepolybori.html#77e199828cafa5b365a0bd01d8ba7e02" title="Multiplication of monomials.">CCuddNavigator::operator*</a>()<span class="keyword"> const </span>{ <a name="l00246"></a>00246 <a name="l00247"></a>00247 <a class="code" href="pbori__defs_8h.html#652ef33086b990b913379bf2f5b9a99e" title="Generate trace function if debugging.">PBORI_TRACE_FUNC</a>( <span class="stringliteral">"CCuddNavigator::operator*() const"</span> ); <a name="l00248"></a>00248 assert(<a class="code" href="classpolybori_1_1CCuddNavigator.html#458deac816e54ad5d5293b2461d4e36e" title="Check whether *this is not the default iterator self() (NULL pointer).">isValid</a>()); <a name="l00249"></a>00249 <span class="keywordflow">return</span> Cudd_Regular(pNode)->index; <a name="l00250"></a>00250 } <a name="l00251"></a>00251 <a name="l00252"></a>00252 <span class="comment">// whether constant node was reached</span> <a name="l00253"></a>00253 <span class="keyword">inline</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html#8be6ae464c6a121b7daa58a665f9c3b5" title="Type for boolean results.">CCuddNavigator::bool_type</a> <a name="l00254"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#565297a790f653c7c68bbe329f20061e">00254</a> <a class="code" href="classpolybori_1_1CCuddNavigator.html#565297a790f653c7c68bbe329f20061e" title="Check whether constant node was reached.">CCuddNavigator::isConstant</a>()<span class="keyword"> const </span>{ <a name="l00255"></a>00255 <a name="l00256"></a>00256 <a class="code" href="pbori__defs_8h.html#652ef33086b990b913379bf2f5b9a99e" title="Generate trace function if debugging.">PBORI_TRACE_FUNC</a>( <span class="stringliteral">"CCuddNavigator::isConstant() const"</span> ); <a name="l00257"></a>00257 assert(<a class="code" href="classpolybori_1_1CCuddNavigator.html#458deac816e54ad5d5293b2461d4e36e" title="Check whether *this is not the default iterator self() (NULL pointer).">isValid</a>()); <a name="l00258"></a>00258 <span class="keywordflow">return</span> Cudd_IsConstant(pNode); <a name="l00259"></a>00259 } <a name="l00260"></a>00260 <a name="l00261"></a>00261 <span class="comment">// constant node value</span> <a name="l00262"></a>00262 <span class="keyword">inline</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html#8be6ae464c6a121b7daa58a665f9c3b5" title="Type for boolean results.">CCuddNavigator::bool_type</a> <a name="l00263"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#5a22617f92b0d88e461d922efec2c93c">00263</a> <a class="code" href="classpolybori_1_1CCuddNavigator.html#5a22617f92b0d88e461d922efec2c93c" title="Check whether terminal node marks end of path.">CCuddNavigator::terminalValue</a>()<span class="keyword"> const </span>{ <a name="l00264"></a>00264 <a name="l00265"></a>00265 <a class="code" href="pbori__defs_8h.html#652ef33086b990b913379bf2f5b9a99e" title="Generate trace function if debugging.">PBORI_TRACE_FUNC</a>( <span class="stringliteral">"CCuddNavigator::terminalValue() const"</span> ); <a name="l00266"></a>00266 assert(<a class="code" href="classpolybori_1_1CCuddNavigator.html#565297a790f653c7c68bbe329f20061e" title="Check whether constant node was reached.">isConstant</a>()); <a name="l00267"></a>00267 <span class="keywordflow">return</span> Cudd_V(pNode); <a name="l00268"></a>00268 } <a name="l00269"></a>00269 <a name="l00270"></a>00270 <a name="l00271"></a>00271 <span class="comment">// increment in then direction</span> <a name="l00272"></a>00272 <span class="keyword">inline</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">CCuddNavigator</a>& <a name="l00273"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#509ef978bd47f74e651411ec2fe50ad3">00273</a> <a class="code" href="classpolybori_1_1CCuddNavigator.html#509ef978bd47f74e651411ec2fe50ad3" title="Increment in then direction.">CCuddNavigator::incrementThen</a>() { <a name="l00274"></a>00274 <a name="l00275"></a>00275 <a class="code" href="pbori__defs_8h.html#652ef33086b990b913379bf2f5b9a99e" title="Generate trace function if debugging.">PBORI_TRACE_FUNC</a>( <span class="stringliteral">"CCuddNavigator::incrementThen()"</span> ); <a name="l00276"></a>00276 <a name="l00277"></a>00277 assert(<a class="code" href="classpolybori_1_1CCuddNavigator.html#458deac816e54ad5d5293b2461d4e36e" title="Check whether *this is not the default iterator self() (NULL pointer).">isValid</a>()); <a name="l00278"></a>00278 pNode = Cudd_T(pNode); <a name="l00279"></a>00279 <a name="l00280"></a>00280 <span class="keywordflow">return</span> *<span class="keyword">this</span>; <a name="l00281"></a>00281 } <a name="l00282"></a>00282 <a name="l00283"></a>00283 <span class="comment">// increment in else direction</span> <a name="l00284"></a>00284 <span class="keyword">inline</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">CCuddNavigator</a>& <a name="l00285"></a><a class="code" href="classpolybori_1_1CCuddNavigator.html#347269fc9b99ffec1b93bbd6f44bcf27">00285</a> <a class="code" href="classpolybori_1_1CCuddNavigator.html#347269fc9b99ffec1b93bbd6f44bcf27" title="Increment in else direction.">CCuddNavigator::incrementElse</a>() { <a name="l00286"></a>00286 <a name="l00287"></a>00287 <a class="code" href="pbori__defs_8h.html#652ef33086b990b913379bf2f5b9a99e" title="Generate trace function if debugging.">PBORI_TRACE_FUNC</a>( <span class="stringliteral">"CCuddNavigator::incrementElse()"</span> ); <a name="l00288"></a>00288 <a name="l00289"></a>00289 assert(<a class="code" href="classpolybori_1_1CCuddNavigator.html#458deac816e54ad5d5293b2461d4e36e" title="Check whether *this is not the default iterator self() (NULL pointer).">isValid</a>()); <a name="l00290"></a>00290 pNode = Cudd_E(pNode); <a name="l00291"></a>00291 <a name="l00292"></a>00292 <span class="keywordflow">return</span> *<span class="keyword">this</span>; <a name="l00293"></a>00293 } <a name="l00294"></a>00294 <a name="l00295"></a>00295 <span class="keyword">inline</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">CCuddNavigator</a> <a name="l00296"></a><a class="code" href="namespacepolybori.html#2ce0359685ce17072aa1d5af3663dd0c">00296</a> <a class="code" href="namespacepolybori.html#2ce0359685ce17072aa1d5af3663dd0c">explicit_navigator_cast</a>(<a class="code" href="classpolybori_1_1CCuddNavigator.html#8c2a3518d0c3b93751586e7ff67f578f" title="Cudd&#39;s node pointer.">CCuddNavigator::pointer_type</a> ptr) { <a name="l00297"></a>00297 <a name="l00298"></a>00298 <span class="preprocessor">#ifndef NDEBUG</span> <a name="l00299"></a>00299 <span class="preprocessor"></span> <span class="keywordflow">if</span> (ptr == NULL) <a name="l00300"></a>00300 <span class="keywordflow">return</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">CCuddNavigator</a>(); <a name="l00301"></a>00301 <span class="keywordflow">else</span> <a name="l00302"></a>00302 <span class="preprocessor">#endif</span> <a name="l00303"></a>00303 <span class="preprocessor"></span> <span class="keywordflow">return</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">CCuddNavigator</a>(ptr); <a name="l00304"></a>00304 } <a name="l00305"></a>00305 <a name="l00306"></a>00306 <a name="l00307"></a>00307 <a class="code" href="pbori__defs_8h.html#faf094fde6c1a7f1aad18bcb455f3b06" title="Finish project&#39;s namespace.">END_NAMESPACE_PBORI</a> <a name="l00308"></a>00308 <a name="l00309"></a>00309 <span class="preprocessor">#endif</span> </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>