Sophie

Sophie

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

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: 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&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>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 &lt;iterator&gt;</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&amp;#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&amp;#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&amp;#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&lt;pointer_type&gt;::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&amp;#39;s zero-suppressed decision diagram...">dd_base</a>&amp; 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>&amp; 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>&amp; 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>&amp; 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-&gt;</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&lt;</span><span class="keywordtype">long</span><span class="keyword">&gt;</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>&amp; 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>&amp; 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() &amp;&amp; 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() &amp;&amp; !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&lt;</a>(<span class="keyword">const</span> <span class="keyword">self</span>&amp; rhs)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> (pNode &lt; 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&lt;=</a>(<span class="keyword">const</span> <span class="keyword">self</span>&amp; rhs)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> (pNode &lt;= 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&gt;</a>(<span class="keyword">const</span> <span class="keyword">self</span>&amp; rhs)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> (pNode &gt; 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&gt;=</a>(<span class="keyword">const</span> <span class="keyword">self</span>&amp; rhs)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> (pNode &gt;= 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> &lt;<span class="keyword">class</span> MgrType&gt;
<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&amp; 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)-&gt;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>&amp;
<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>&amp;
<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&amp;#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&amp;#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&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>