<!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: pbori_algo.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>pbori_algo.h</h1><a href="pbori__algo_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="l00150"></a>00150 <span class="comment"></span><span class="comment">//*****************************************************************************</span>
<a name="l00151"></a>00151
<a name="l00152"></a>00152 <span class="comment">// include polybori's definitions</span>
<a name="l00153"></a>00153 <span class="preprocessor">#include "<a class="code" href="pbori__defs_8h.html">pbori_defs.h</a>"</span>
<a name="l00154"></a>00154
<a name="l00155"></a>00155 <span class="comment">// get polybori's functionals</span>
<a name="l00156"></a>00156 <span class="preprocessor">#include "<a class="code" href="pbori__func_8h.html">pbori_func.h</a>"</span>
<a name="l00157"></a>00157 <span class="preprocessor">#include "<a class="code" href="pbori__traits_8h.html">pbori_traits.h</a>"</span>
<a name="l00158"></a>00158
<a name="l00159"></a>00159 <span class="comment">// temporarily</span>
<a name="l00160"></a>00160 <span class="preprocessor">#include "cudd.h"</span>
<a name="l00161"></a>00161 <span class="preprocessor">#include "cuddInt.h"</span>
<a name="l00162"></a>00162 <span class="preprocessor">#include "<a class="code" href="CCuddInterface_8h.html">CCuddInterface.h</a>"</span>
<a name="l00163"></a>00163
<a name="l00164"></a>00164 <span class="preprocessor">#ifndef pbori_algo_h_</span>
<a name="l00165"></a>00165 <span class="preprocessor"></span><span class="preprocessor">#define pbori_algo_h_</span>
<a name="l00166"></a>00166 <span class="preprocessor"></span>
<a name="l00167"></a>00167 <a class="code" href="pbori__defs_8h.html#6ae360a591580558f31b6157ee792a10" title="Start project&#39;s namespace.">BEGIN_NAMESPACE_PBORI</a>
<a name="l00168"></a>00168
<a name="l00169"></a>00169
<a name="l00171"></a>00171 <span class="keyword">template</span>< <span class="keyword">class </span>NaviType, <span class="keyword">class </span>TermType,
<a name="l00172"></a>00172 <span class="keyword">class </span>TernaryOperator,
<a name="l00173"></a>00173 <span class="keyword">class </span>TerminalOperator >
<a name="l00174"></a>00174 TermType
<a name="l00175"></a><a class="code" href="namespacepolybori.html#681b961708e4781decc938ba35aafe34">00175</a> <a class="code" href="namespacepolybori.html#681b961708e4781decc938ba35aafe34" title="Function templates for transforming decision diagrams.">dd_backward_transform</a>( NaviType navi, TermType init, TernaryOperator newNode,
<a name="l00176"></a>00176 TerminalOperator terminate ) {
<a name="l00177"></a>00177
<a name="l00178"></a>00178 TermType result = init;
<a name="l00179"></a>00179
<a name="l00180"></a>00180 <span class="keywordflow">if</span> (navi.isConstant()) { <span class="comment">// Reached end of path</span>
<a name="l00181"></a>00181 <span class="keywordflow">if</span> (navi.terminalValue()){ <span class="comment">// Case of a valid path</span>
<a name="l00182"></a>00182 result = terminate();
<a name="l00183"></a>00183 }
<a name="l00184"></a>00184 }
<a name="l00185"></a>00185 <span class="keywordflow">else</span> {
<a name="l00186"></a>00186 result = <a class="code" href="namespacepolybori.html#681b961708e4781decc938ba35aafe34" title="Function templates for transforming decision diagrams.">dd_backward_transform</a>(navi.thenBranch(), init, newNode, terminate);
<a name="l00187"></a>00187 result = newNode(*navi, result,
<a name="l00188"></a>00188 <a class="code" href="namespacepolybori.html#681b961708e4781decc938ba35aafe34" title="Function templates for transforming decision diagrams.">dd_backward_transform</a>(navi.elseBranch(), init, newNode,
<a name="l00189"></a>00189 terminate) );
<a name="l00190"></a>00190 }
<a name="l00191"></a>00191 <span class="keywordflow">return</span> result;
<a name="l00192"></a>00192 }
<a name="l00193"></a>00193
<a name="l00194"></a>00194
<a name="l00196"></a>00196 <span class="keyword">template</span>< <span class="keyword">class </span>NaviType, <span class="keyword">class </span>TermType, <span class="keyword">class </span>OutIterator,
<a name="l00197"></a>00197 <span class="keyword">class </span>ThenBinaryOperator, <span class="keyword">class </span>ElseBinaryOperator,
<a name="l00198"></a>00198 <span class="keyword">class </span>TerminalOperator >
<a name="l00199"></a>00199 OutIterator
<a name="l00200"></a><a class="code" href="namespacepolybori.html#094813e9371a53ba49be73a828c5a9dd">00200</a> <a class="code" href="namespacepolybori.html#094813e9371a53ba49be73a828c5a9dd" title="Function templates for transforming decision diagrams.">dd_transform</a>( NaviType navi, TermType init, OutIterator result,
<a name="l00201"></a>00201 ThenBinaryOperator then_binop, ElseBinaryOperator else_binop,
<a name="l00202"></a>00202 TerminalOperator terminate ) {
<a name="l00203"></a>00203
<a name="l00204"></a>00204
<a name="l00205"></a>00205 <span class="keywordflow">if</span> (navi.isConstant()) { <span class="comment">// Reached end of path</span>
<a name="l00206"></a>00206 <span class="keywordflow">if</span> (navi.terminalValue()){ <span class="comment">// Case of a valid path</span>
<a name="l00207"></a>00207 *result = terminate(init);
<a name="l00208"></a>00208 ++result;
<a name="l00209"></a>00209 }
<a name="l00210"></a>00210 }
<a name="l00211"></a>00211 <span class="keywordflow">else</span> {
<a name="l00212"></a>00212 result = <a class="code" href="namespacepolybori.html#094813e9371a53ba49be73a828c5a9dd" title="Function templates for transforming decision diagrams.">dd_transform</a>(navi.thenBranch(), then_binop(init, *navi), result,
<a name="l00213"></a>00213 then_binop, else_binop, terminate);
<a name="l00214"></a>00214 result = <a class="code" href="namespacepolybori.html#094813e9371a53ba49be73a828c5a9dd" title="Function templates for transforming decision diagrams.">dd_transform</a>(navi.elseBranch(), else_binop(init, *navi), result,
<a name="l00215"></a>00215 then_binop, else_binop, terminate);
<a name="l00216"></a>00216 }
<a name="l00217"></a>00217 <span class="keywordflow">return</span> result;
<a name="l00218"></a>00218 }
<a name="l00219"></a>00219
<a name="l00222"></a>00222 <span class="keyword">template</span>< <span class="keyword">class </span>NaviType, <span class="keyword">class </span>TermType, <span class="keyword">class </span>OutIterator,
<a name="l00223"></a>00223 <span class="keyword">class </span>ThenBinaryOperator, <span class="keyword">class </span>ElseBinaryOperator,
<a name="l00224"></a>00224 <span class="keyword">class </span>TerminalOperator, <span class="keyword">class </span>FirstTermOp >
<a name="l00225"></a>00225 OutIterator
<a name="l00226"></a><a class="code" href="namespacepolybori.html#786b86aa045cae7a738a47d9918ecce9">00226</a> <a class="code" href="namespacepolybori.html#094813e9371a53ba49be73a828c5a9dd" title="Function templates for transforming decision diagrams.">dd_transform</a>( NaviType navi, TermType init, OutIterator result,
<a name="l00227"></a>00227 ThenBinaryOperator then_binop, ElseBinaryOperator else_binop,
<a name="l00228"></a>00228 TerminalOperator terminate, FirstTermOp terminate_first ) {
<a name="l00229"></a>00229
<a name="l00230"></a>00230 <span class="keywordflow">if</span> (navi.isConstant()) { <span class="comment">// Reached end of path</span>
<a name="l00231"></a>00231 <span class="keywordflow">if</span> (navi.terminalValue()){ <span class="comment">// Case of a valid path - here leading term</span>
<a name="l00232"></a>00232 *result = terminate_first(init);
<a name="l00233"></a>00233 ++result;
<a name="l00234"></a>00234 }
<a name="l00235"></a>00235 }
<a name="l00236"></a>00236 <span class="keywordflow">else</span> {
<a name="l00237"></a>00237 result = <a class="code" href="namespacepolybori.html#094813e9371a53ba49be73a828c5a9dd" title="Function templates for transforming decision diagrams.">dd_transform</a>(navi.thenBranch(), then_binop(init, *navi), result,
<a name="l00238"></a>00238 then_binop, else_binop, terminate, terminate_first);
<a name="l00239"></a>00239 result = <a class="code" href="namespacepolybori.html#094813e9371a53ba49be73a828c5a9dd" title="Function templates for transforming decision diagrams.">dd_transform</a>(navi.elseBranch(), else_binop(init, *navi), result,
<a name="l00240"></a>00240 then_binop, else_binop, terminate);
<a name="l00241"></a>00241 }
<a name="l00242"></a>00242 <span class="keywordflow">return</span> result;
<a name="l00243"></a>00243 }
<a name="l00244"></a>00244
<a name="l00246"></a>00246 <span class="keyword">template</span>< <span class="keyword">class </span>NaviType, <span class="keyword">class </span>TermType, <span class="keyword">class </span>OutIterator,
<a name="l00247"></a>00247 <span class="keyword">class </span>ThenBinaryOperator, <span class="keyword">class </span>ElseBinaryOperator >
<a name="l00248"></a>00248 <span class="keywordtype">void</span>
<a name="l00249"></a><a class="code" href="namespacepolybori.html#ec5429fd8cdb912534290d56eb5d78d5">00249</a> <a class="code" href="namespacepolybori.html#094813e9371a53ba49be73a828c5a9dd" title="Function templates for transforming decision diagrams.">dd_transform</a>( <span class="keyword">const</span> NaviType& navi, <span class="keyword">const</span> TermType& init,
<a name="l00250"></a>00250 <span class="keyword">const</span> OutIterator& result,
<a name="l00251"></a>00251 <span class="keyword">const</span> ThenBinaryOperator& then_binop,
<a name="l00252"></a>00252 <span class="keyword">const</span> ElseBinaryOperator& else_binop ) {
<a name="l00253"></a>00253
<a name="l00254"></a>00254 <a class="code" href="namespacepolybori.html#094813e9371a53ba49be73a828c5a9dd" title="Function templates for transforming decision diagrams.">dd_transform</a>(navi, init, result, then_binop, else_binop,
<a name="l00255"></a>00255 <a class="code" href="classproject__ith.html" title="Virtually does nothing with the given arguments.">project_ith<1></a>() );
<a name="l00256"></a>00256 }
<a name="l00257"></a>00257
<a name="l00259"></a>00259 <span class="keyword">template</span>< <span class="keyword">class </span>NaviType, <span class="keyword">class </span>TermType, <span class="keyword">class </span>OutIterator,
<a name="l00260"></a>00260 <span class="keyword">class </span>ThenBinaryOperator >
<a name="l00261"></a>00261 <span class="keywordtype">void</span>
<a name="l00262"></a><a class="code" href="namespacepolybori.html#eb1a56a93f04c61bc5924739c1176d05">00262</a> <a class="code" href="namespacepolybori.html#094813e9371a53ba49be73a828c5a9dd" title="Function templates for transforming decision diagrams.">dd_transform</a>( <span class="keyword">const</span> NaviType& navi, <span class="keyword">const</span> TermType& init,
<a name="l00263"></a>00263 <span class="keyword">const</span> OutIterator& result,
<a name="l00264"></a>00264 <span class="keyword">const</span> ThenBinaryOperator& then_binop ) {
<a name="l00265"></a>00265
<a name="l00266"></a>00266 <a class="code" href="namespacepolybori.html#094813e9371a53ba49be73a828c5a9dd" title="Function templates for transforming decision diagrams.">dd_transform</a>(navi, init, result, then_binop,
<a name="l00267"></a>00267 <a class="code" href="classproject__ith.html" title="Virtually does nothing with the given arguments.">project_ith<1, 2></a>(),
<a name="l00268"></a>00268 <a class="code" href="classproject__ith.html" title="Virtually does nothing with the given arguments.">project_ith<1></a>() );
<a name="l00269"></a>00269 }
<a name="l00270"></a>00270
<a name="l00271"></a>00271
<a name="l00272"></a>00272 <span class="keyword">template</span> <<span class="keyword">class </span>InputIterator, <span class="keyword">class </span>OutputIterator,
<a name="l00273"></a>00273 <span class="keyword">class </span>FirstFunction, <span class="keyword">class </span>UnaryFunction>
<a name="l00274"></a>00274 OutputIterator
<a name="l00275"></a><a class="code" href="namespacepolybori.html#623299a572ab265b87536471038a051b">00275</a> <a class="code" href="namespacepolybori.html#623299a572ab265b87536471038a051b">special_first_transform</a>(InputIterator first, InputIterator last,
<a name="l00276"></a>00276 OutputIterator result,
<a name="l00277"></a>00277 UnaryFunction op, FirstFunction firstop) {
<a name="l00278"></a>00278 InputIterator second(first);
<a name="l00279"></a>00279 <span class="keywordflow">if</span> (second != last) {
<a name="l00280"></a>00280 ++second;
<a name="l00281"></a>00281 result = std::transform(first, second, result, firstop);
<a name="l00282"></a>00282 }
<a name="l00283"></a>00283 <span class="keywordflow">return</span> std::transform(second, last, result, op);
<a name="l00284"></a>00284 }
<a name="l00285"></a>00285
<a name="l00286"></a>00286
<a name="l00288"></a>00288 <span class="keyword">template</span> <<span class="keyword">class</span> InputIterator, <span class="keyword">class</span> Intermediate, <span class="keyword">class</span> OutputIterator>
<a name="l00289"></a>00289 OutputIterator
<a name="l00290"></a><a class="code" href="namespacepolybori.html#39e393c4286cf8905dd845f004f04443">00290</a> <a class="code" href="namespacepolybori.html#39e393c4286cf8905dd845f004f04443" title="Function templates doing a reversed copy using intermediate storage.">reversed_inter_copy</a>( InputIterator start, InputIterator finish,
<a name="l00291"></a>00291 Intermediate& inter, OutputIterator output ) {
<a name="l00292"></a>00292
<a name="l00293"></a>00293 std::copy(start, finish, inter.begin());
<a name="l00294"></a>00294 <span class="comment">// force constant</span>
<a name="l00295"></a>00295 <span class="keywordflow">return</span> std::copy( const_cast<const Intermediate&>(inter).rbegin(),
<a name="l00296"></a>00296 const_cast<const Intermediate&>(inter).rend(),
<a name="l00297"></a>00297 output );
<a name="l00298"></a>00298 }
<a name="l00299"></a>00299
<a name="l00302"></a>00302 <span class="keyword">template</span> <<span class="keyword">class</span> NaviType>
<a name="l00303"></a>00303 <span class="keywordtype">bool</span>
<a name="l00304"></a><a class="code" href="namespacepolybori.html#e0f426c9c7e4e2fe4d75775a4ef99ee9">00304</a> <a class="code" href="namespacepolybori.html#e0f426c9c7e4e2fe4d75775a4ef99ee9">dd_on_path</a>(NaviType navi) {
<a name="l00305"></a>00305
<a name="l00306"></a>00306 <span class="keywordflow">if</span> (navi.isConstant())
<a name="l00307"></a>00307 <span class="keywordflow">return</span> navi.terminalValue();
<a name="l00308"></a>00308
<a name="l00309"></a>00309 <span class="keywordflow">return</span> <a class="code" href="namespacepolybori.html#e0f426c9c7e4e2fe4d75775a4ef99ee9">dd_on_path</a>(navi.thenBranch()) || <a class="code" href="namespacepolybori.html#e0f426c9c7e4e2fe4d75775a4ef99ee9">dd_on_path</a>(navi.elseBranch());
<a name="l00310"></a>00310 }
<a name="l00311"></a>00311
<a name="l00314"></a>00314 <span class="keyword">template</span> <<span class="keyword">class</span> NaviType, <span class="keyword">class</span> OrderedIterator>
<a name="l00315"></a>00315 <span class="keywordtype">bool</span>
<a name="l00316"></a><a class="code" href="namespacepolybori.html#cb6344d5ff20ba21b11d4480ee9e78e2">00316</a> <a class="code" href="namespacepolybori.html#cb6344d5ff20ba21b11d4480ee9e78e2">dd_owns_term_of_indices</a>(NaviType navi,
<a name="l00317"></a>00317 OrderedIterator start, OrderedIterator finish) {
<a name="l00318"></a>00318
<a name="l00319"></a>00319 <span class="keywordflow">if</span> (!navi.isConstant()) { <span class="comment">// Not at end of path</span>
<a name="l00320"></a>00320 <span class="keywordtype">bool</span> not_at_end;
<a name="l00321"></a>00321
<a name="l00322"></a>00322 <span class="keywordflow">while</span>( (not_at_end = (start != finish)) && (*start < *navi) )
<a name="l00323"></a>00323 ++start;
<a name="l00324"></a>00324
<a name="l00325"></a>00325 NaviType elsenode = navi.elseBranch();
<a name="l00326"></a>00326
<a name="l00327"></a>00327 <span class="keywordflow">if</span> (elsenode.isConstant() && elsenode.terminalValue())
<a name="l00328"></a>00328 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00329"></a>00329
<a name="l00330"></a>00330
<a name="l00331"></a>00331 <span class="keywordflow">if</span> (not_at_end){
<a name="l00332"></a>00332
<a name="l00333"></a>00333 <span class="keywordflow">if</span> ( (*start == *navi) &&
<a name="l00334"></a>00334 <a class="code" href="namespacepolybori.html#cb6344d5ff20ba21b11d4480ee9e78e2">dd_owns_term_of_indices</a>(navi.thenBranch(), start, finish))
<a name="l00335"></a>00335 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00336"></a>00336 <span class="keywordflow">else</span>
<a name="l00337"></a>00337 <span class="keywordflow">return</span> <a class="code" href="namespacepolybori.html#cb6344d5ff20ba21b11d4480ee9e78e2">dd_owns_term_of_indices</a>(elsenode, start, finish);
<a name="l00338"></a>00338 }
<a name="l00339"></a>00339 <span class="keywordflow">else</span> {
<a name="l00340"></a>00340
<a name="l00341"></a>00341 <span class="keywordflow">while</span>(!elsenode.isConstant())
<a name="l00342"></a>00342 elsenode.incrementElse();
<a name="l00343"></a>00343 <span class="keywordflow">return</span> elsenode.terminalValue();
<a name="l00344"></a>00344 }
<a name="l00345"></a>00345
<a name="l00346"></a>00346 }
<a name="l00347"></a>00347 <span class="keywordflow">return</span> navi.terminalValue();
<a name="l00348"></a>00348 }
<a name="l00349"></a>00349
<a name="l00353"></a>00353 <span class="keyword">template</span> <<span class="keyword">class</span> NaviType, <span class="keyword">class</span> OrderedIterator, <span class="keyword">class</span> NodeOperation>
<a name="l00354"></a>00354 NaviType
<a name="l00355"></a><a class="code" href="namespacepolybori.html#f85e7fef57412e7c2b830144c68e2509">00355</a> <a class="code" href="namespacepolybori.html#f85e7fef57412e7c2b830144c68e2509">dd_intersect_some_index</a>(NaviType navi,
<a name="l00356"></a>00356 OrderedIterator start, OrderedIterator finish,
<a name="l00357"></a>00357 NodeOperation newNode ) {
<a name="l00358"></a>00358
<a name="l00359"></a>00359 <span class="keywordflow">if</span> (!navi.isConstant()) { <span class="comment">// Not at end of path</span>
<a name="l00360"></a>00360 <span class="keywordtype">bool</span> not_at_end;
<a name="l00361"></a>00361 <span class="keywordflow">while</span>( (not_at_end = (start != finish)) && (*start < *navi) )
<a name="l00362"></a>00362 ++start;
<a name="l00363"></a>00363
<a name="l00364"></a>00364 <span class="keywordflow">if</span> (not_at_end) {
<a name="l00365"></a>00365 NaviType elseNode =
<a name="l00366"></a>00366 <a class="code" href="namespacepolybori.html#f85e7fef57412e7c2b830144c68e2509">dd_intersect_some_index</a>(navi.elseBranch(), start, finish,
<a name="l00367"></a>00367 newNode);
<a name="l00368"></a>00368
<a name="l00369"></a>00369 <span class="keywordflow">if</span> (*start == *navi) {
<a name="l00370"></a>00370
<a name="l00371"></a>00371 NaviType thenNode =
<a name="l00372"></a>00372 <a class="code" href="namespacepolybori.html#f85e7fef57412e7c2b830144c68e2509">dd_intersect_some_index</a>(navi.thenBranch(), start, finish,
<a name="l00373"></a>00373 newNode);
<a name="l00374"></a>00374
<a name="l00375"></a>00375 <span class="keywordflow">return</span> newNode(*start, navi, thenNode, elseNode);
<a name="l00376"></a>00376 }
<a name="l00377"></a>00377 <span class="keywordflow">else</span>
<a name="l00378"></a>00378 <span class="keywordflow">return</span> elseNode;
<a name="l00379"></a>00379 }
<a name="l00380"></a>00380 <span class="keywordflow">else</span> { <span class="comment">// if the start == finish, we only check </span>
<a name="l00381"></a>00381 <span class="comment">// validity of the else-only branch </span>
<a name="l00382"></a>00382 <span class="keywordflow">while</span>(!navi.isConstant())
<a name="l00383"></a>00383 navi = navi.elseBranch();
<a name="l00384"></a>00384 <span class="keywordflow">return</span> newNode(navi);
<a name="l00385"></a>00385 }
<a name="l00386"></a>00386
<a name="l00387"></a>00387 }
<a name="l00388"></a>00388
<a name="l00389"></a>00389 <span class="keywordflow">return</span> newNode(navi);
<a name="l00390"></a>00390 }
<a name="l00391"></a>00391
<a name="l00392"></a>00392
<a name="l00393"></a>00393
<a name="l00395"></a>00395 <span class="keyword">template</span> <<span class="keyword">class</span> NaviType>
<a name="l00396"></a>00396 <span class="keywordtype">void</span>
<a name="l00397"></a><a class="code" href="namespacepolybori.html#b5d7d5cc3e86f3707d30aeffc57bb685">00397</a> <a class="code" href="namespacepolybori.html#b5d7d5cc3e86f3707d30aeffc57bb685" title="Function templates for debugging, prints dd indices and reference counts.">dd_print</a>(NaviType navi) {
<a name="l00398"></a>00398
<a name="l00399"></a>00399 <span class="keywordflow">if</span> (!navi.isConstant()) { <span class="comment">// Not at end of path</span>
<a name="l00400"></a>00400
<a name="l00401"></a>00401 std::cout << std::endl<< <span class="stringliteral">"idx "</span> << *navi <<<span class="stringliteral">" addr "</span><<
<a name="l00402"></a>00402 ((DdNode*)navi)<<<span class="stringliteral">" ref "</span><<
<a name="l00403"></a>00403 int(Cudd_Regular((DdNode*)navi)->ref) << std::endl;
<a name="l00404"></a>00404
<a name="l00405"></a>00405 <a class="code" href="namespacepolybori.html#b5d7d5cc3e86f3707d30aeffc57bb685" title="Function templates for debugging, prints dd indices and reference counts.">dd_print</a>(navi.thenBranch());
<a name="l00406"></a>00406 <a class="code" href="namespacepolybori.html#b5d7d5cc3e86f3707d30aeffc57bb685" title="Function templates for debugging, prints dd indices and reference counts.">dd_print</a>(navi.elseBranch());
<a name="l00407"></a>00407
<a name="l00408"></a>00408 }
<a name="l00409"></a>00409 <span class="keywordflow">else</span> {
<a name="l00410"></a>00410 std::cout << <span class="stringliteral">"const isvalid? "</span><<navi.isValid()<<<span class="stringliteral">" addr "</span>
<a name="l00411"></a>00411 <<((DdNode*)navi)<<<span class="stringliteral">" ref "</span><<
<a name="l00412"></a>00412 int(Cudd_Regular((DdNode*)navi)->ref)<<std::endl;
<a name="l00413"></a>00413
<a name="l00414"></a>00414 }
<a name="l00415"></a>00415 }
<a name="l00416"></a>00416
<a name="l00417"></a>00417 <span class="comment">// Determinine the minimum of the distance between two iterators and limit</span>
<a name="l00418"></a>00418 <span class="keyword">template</span> <<span class="keyword">class</span> IteratorType, <span class="keyword">class</span> SizeType>
<a name="l00419"></a>00419 SizeType
<a name="l00420"></a><a class="code" href="namespacepolybori.html#b82f8384b788b0d1ace855581c13c0c4">00420</a> <a class="code" href="namespacepolybori.html#b82f8384b788b0d1ace855581c13c0c4">limited_distance</a>(IteratorType start, IteratorType finish, SizeType limit) {
<a name="l00421"></a>00421
<a name="l00422"></a>00422 SizeType result = 0;
<a name="l00423"></a>00423
<a name="l00424"></a>00424 <span class="keywordflow">while</span> ((result < limit) && (start != finish)) {
<a name="l00425"></a>00425 ++start, ++result;
<a name="l00426"></a>00426 }
<a name="l00427"></a>00427
<a name="l00428"></a>00428 <span class="keywordflow">return</span> result;
<a name="l00429"></a>00429 }
<a name="l00430"></a>00430
<a name="l00431"></a>00431 <span class="preprocessor">#if 0</span>
<a name="l00432"></a>00432 <span class="preprocessor"></span><span class="comment">// Forward declaration of CTermIter template</span>
<a name="l00433"></a>00433 <span class="keyword">template</span> <<span class="keyword">class</span>, <span class="keyword">class</span>, <span class="keyword">class</span>, <span class="keyword">class</span>, <span class="keyword">class</span>, <span class="keyword">class</span>> <span class="keyword">class </span>CTermIter;
<a name="l00434"></a>00434
<a name="l00435"></a>00435 <span class="comment">// Determinine the minimum of the number of terms and limit</span>
<a name="l00436"></a>00436 <span class="keyword">template</span> <<span class="keyword">class</span> NaviType, <span class="keyword">class</span> SizeType>
<a name="l00437"></a>00437 SizeType
<a name="l00438"></a>00438 limited_length(NaviType navi, SizeType limit) {
<a name="l00439"></a>00439
<a name="l00440"></a>00440
<a name="l00441"></a>00441 <span class="keyword">typedef</span> CTermIter<dummy_iterator, NaviType,
<a name="l00442"></a>00442 <a class="code" href="classproject__ith.html" title="Virtually does nothing with the given arguments.">project_ith<1></a>, project_ith<1>, <a class="code" href="classproject__ith.html" title="Virtually does nothing with the given arguments.">project_ith<1, 2></a>,
<a name="l00443"></a>00443 project_ith<1> >
<a name="l00444"></a>00444 iterator;
<a name="l00445"></a>00445
<a name="l00446"></a>00446 <span class="keywordflow">return</span> <a class="code" href="namespacepolybori.html#b82f8384b788b0d1ace855581c13c0c4">limited_distance</a>(iterator(navi), iterator(), limit);
<a name="l00447"></a>00447 }
<a name="l00448"></a>00448 <span class="preprocessor">#endif</span>
<a name="l00449"></a>00449 <span class="preprocessor"></span>
<a name="l00453"></a>00453 <span class="keyword">template</span> <<span class="keyword">class</span> NaviType, <span class="keyword">class</span> DDType>
<a name="l00454"></a>00454 DDType
<a name="l00455"></a><a class="code" href="namespacepolybori.html#f21584c7975eb3bde0a26902776245d9">00455</a> <a class="code" href="namespacepolybori.html#f21584c7975eb3bde0a26902776245d9">dd_minimal_elements</a>(NaviType navi, DDType dd, DDType& multiples) {
<a name="l00456"></a>00456
<a name="l00457"></a>00457
<a name="l00458"></a>00458 <span class="keywordflow">if</span> (!navi.isConstant()) { <span class="comment">// Not at end of path</span>
<a name="l00459"></a>00459
<a name="l00460"></a>00460 DDType elsedd = dd.subset0(*navi);
<a name="l00461"></a>00461
<a name="l00462"></a>00462
<a name="l00463"></a>00463 DDType elseMultiples;
<a name="l00464"></a>00464 elsedd = <a class="code" href="namespacepolybori.html#f21584c7975eb3bde0a26902776245d9">dd_minimal_elements</a>(navi.elseBranch(), elsedd, elseMultiples);
<a name="l00465"></a>00465
<a name="l00466"></a>00466 <span class="comment">// short cut if else and then branche equal or else contains 1</span>
<a name="l00467"></a>00467 <span class="keywordflow">if</span>((navi.elseBranch() == navi.thenBranch()) || elsedd.blankness()){
<a name="l00468"></a>00468 multiples = elseMultiples;
<a name="l00469"></a>00469 <span class="keywordflow">return</span> elsedd;
<a name="l00470"></a>00470 }
<a name="l00471"></a>00471
<a name="l00472"></a>00472 NaviType elseNavi = elseMultiples.navigation();
<a name="l00473"></a>00473
<a name="l00474"></a>00474 <span class="keywordtype">int</span> nmax;
<a name="l00475"></a>00475 <span class="keywordflow">if</span> (elseNavi.isConstant()){
<a name="l00476"></a>00476 <span class="keywordflow">if</span> (elseNavi.terminalValue())
<a name="l00477"></a>00477 nmax = dd.nVariables();
<a name="l00478"></a>00478 <span class="keywordflow">else</span>
<a name="l00479"></a>00479 nmax = *navi;
<a name="l00480"></a>00480 }
<a name="l00481"></a>00481 <span class="keywordflow">else</span>
<a name="l00482"></a>00482 nmax = *elseNavi;
<a name="l00483"></a>00483
<a name="l00484"></a>00484
<a name="l00485"></a>00485 <span class="keywordflow">for</span>(<span class="keywordtype">int</span> i = nmax-1; i > *navi; --i){
<a name="l00486"></a>00486 elseMultiples.uniteAssign(elseMultiples.change(i));
<a name="l00487"></a>00487 }
<a name="l00488"></a>00488
<a name="l00489"></a>00489
<a name="l00490"></a>00490 DDType thendd = dd.subset1(*navi);
<a name="l00491"></a>00491 thendd = thendd.diff(elseMultiples);
<a name="l00492"></a>00492
<a name="l00493"></a>00493 DDType thenMultiples;
<a name="l00494"></a>00494 thendd = <a class="code" href="namespacepolybori.html#f21584c7975eb3bde0a26902776245d9">dd_minimal_elements</a>(navi.thenBranch(), thendd, thenMultiples);
<a name="l00495"></a>00495
<a name="l00496"></a>00496 NaviType thenNavi = thenMultiples.navigation();
<a name="l00497"></a>00497
<a name="l00498"></a>00498
<a name="l00499"></a>00499 <span class="keywordflow">if</span> (thenNavi.isConstant()){
<a name="l00500"></a>00500 <span class="keywordflow">if</span> (thenNavi.terminalValue())
<a name="l00501"></a>00501 nmax = dd.nVariables();
<a name="l00502"></a>00502 <span class="keywordflow">else</span>
<a name="l00503"></a>00503 nmax = *navi;
<a name="l00504"></a>00504 }
<a name="l00505"></a>00505 <span class="keywordflow">else</span>
<a name="l00506"></a>00506 nmax = *thenNavi;
<a name="l00507"></a>00507
<a name="l00508"></a>00508
<a name="l00509"></a>00509 <span class="keywordflow">for</span>(<span class="keywordtype">int</span> i = nmax-1; i > *navi; --i){
<a name="l00510"></a>00510 thenMultiples.uniteAssign(thenMultiples.change(i));
<a name="l00511"></a>00511 }
<a name="l00512"></a>00512
<a name="l00513"></a>00513
<a name="l00514"></a>00514 thenMultiples = thenMultiples.unite(elseMultiples);
<a name="l00515"></a>00515 thenMultiples = thenMultiples.change(*navi);
<a name="l00516"></a>00516
<a name="l00517"></a>00517
<a name="l00518"></a>00518 multiples = thenMultiples.unite(elseMultiples);
<a name="l00519"></a>00519 thendd = thendd.change(*navi);
<a name="l00520"></a>00520
<a name="l00521"></a>00521 DDType result = thendd.unite(elsedd);
<a name="l00522"></a>00522
<a name="l00523"></a>00523 <span class="keywordflow">return</span> result;
<a name="l00524"></a>00524
<a name="l00525"></a>00525 }
<a name="l00526"></a>00526
<a name="l00527"></a>00527 multiples = dd;
<a name="l00528"></a>00528 <span class="keywordflow">return</span> dd;
<a name="l00529"></a>00529 }
<a name="l00530"></a>00530
<a name="l00531"></a>00531 <span class="keyword">template</span> <<span class="keyword">class</span> MgrType>
<a name="l00532"></a>00532 <span class="keyword">inline</span> <span class="keyword">const</span> MgrType&
<a name="l00533"></a><a class="code" href="namespacepolybori.html#133ade2eba08cb872ac4355b389f2cdf">00533</a> <a class="code" href="namespacepolybori.html#133ade2eba08cb872ac4355b389f2cdf">get_mgr_core</a>(<span class="keyword">const</span> MgrType& rhs) {
<a name="l00534"></a>00534 <span class="keywordflow">return</span> rhs;
<a name="l00535"></a>00535 }
<a name="l00536"></a>00536 <span class="keyword">inline</span> Cudd*
<a name="l00537"></a><a class="code" href="namespacepolybori.html#c9ecc6f30d24c887aee5050125db8dfe">00537</a> <a class="code" href="namespacepolybori.html#133ade2eba08cb872ac4355b389f2cdf">get_mgr_core</a>(<span class="keyword">const</span> Cudd& rhs) {
<a name="l00538"></a>00538 <span class="keywordflow">return</span> &<span class="keyword">const_cast<</span>Cudd&<span class="keyword">></span>(rhs);
<a name="l00539"></a>00539 }
<a name="l00540"></a>00540
<a name="l00542"></a>00542 <span class="keyword">inline</span> CCuddInterface::mgrcore_ptr
<a name="l00543"></a><a class="code" href="namespacepolybori.html#704e9319a84420bbfed328e77d3ee460">00543</a> <a class="code" href="namespacepolybori.html#133ade2eba08cb872ac4355b389f2cdf">get_mgr_core</a>(<span class="keyword">const</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>& mgr) {
<a name="l00544"></a>00544 <span class="keywordflow">return</span> mgr.<a class="code" href="classpolybori_1_1CCuddInterface.html#faf2deee4b5b79723c8719ca14dbfda6" title="Get (shared) pointer to initialized manager.">managerCore</a>();
<a name="l00545"></a>00545 }
<a name="l00546"></a>00546
<a name="l00548"></a>00548 <span class="keyword">template</span><<span class="keyword">class</span> ManagerType, <span class="keyword">class</span> ReverseIterator, <span class="keyword">class</span> MultReverseIterator>
<a name="l00549"></a>00549 <span class="keyword">typename</span> manager_traits<ManagerType>::dd_base
<a name="l00550"></a><a class="code" href="namespacepolybori.html#9f5a4551340ca9187a30a37dbccf3f56">00550</a> <a class="code" href="namespacepolybori.html#9f5a4551340ca9187a30a37dbccf3f56" title="temporarily (needs to be more generic)">cudd_generate_multiples</a>(<span class="keyword">const</span> ManagerType& mgr,
<a name="l00551"></a>00551 ReverseIterator start, ReverseIterator finish,
<a name="l00552"></a>00552 MultReverseIterator multStart,
<a name="l00553"></a>00553 MultReverseIterator multFinish) {
<a name="l00554"></a>00554
<a name="l00555"></a>00555 DdNode* prev( (mgr.getManager())->one );
<a name="l00556"></a>00556
<a name="l00557"></a>00557 DdNode* zeroNode( (mgr.getManager())->zero );
<a name="l00558"></a>00558
<a name="l00559"></a>00559 Cudd_Ref(prev);
<a name="l00560"></a>00560 <span class="keywordflow">while</span>(start != finish) {
<a name="l00561"></a>00561
<a name="l00562"></a>00562 <span class="keywordflow">while</span>((multStart != multFinish) && (*start < *multStart)) {
<a name="l00563"></a>00563
<a name="l00564"></a>00564 DdNode* result = cuddUniqueInterZdd( mgr.getManager(), *multStart,
<a name="l00565"></a>00565 prev, prev );
<a name="l00566"></a>00566
<a name="l00567"></a>00567 Cudd_Ref(result);
<a name="l00568"></a>00568 Cudd_RecursiveDerefZdd(mgr.getManager(), prev);
<a name="l00569"></a>00569
<a name="l00570"></a>00570 prev = result;
<a name="l00571"></a>00571 ++multStart;
<a name="l00572"></a>00572
<a name="l00573"></a>00573 };
<a name="l00574"></a>00574
<a name="l00575"></a>00575 DdNode* result = cuddUniqueInterZdd( mgr.getManager(), *start,
<a name="l00576"></a>00576 prev, zeroNode );
<a name="l00577"></a>00577
<a name="l00578"></a>00578 Cudd_Ref(result);
<a name="l00579"></a>00579 Cudd_RecursiveDerefZdd(mgr.getManager(), prev);
<a name="l00580"></a>00580
<a name="l00581"></a>00581 prev = result;
<a name="l00582"></a>00582
<a name="l00583"></a>00583
<a name="l00584"></a>00584 <span class="keywordflow">if</span>((multStart != multFinish) && (*start == *multStart))
<a name="l00585"></a>00585 ++multStart;
<a name="l00586"></a>00586
<a name="l00587"></a>00587
<a name="l00588"></a>00588 ++start;
<a name="l00589"></a>00589 }
<a name="l00590"></a>00590
<a name="l00591"></a>00591 <span class="keywordflow">while</span>(multStart != multFinish) {
<a name="l00592"></a>00592
<a name="l00593"></a>00593 DdNode* result = cuddUniqueInterZdd( mgr.getManager(), *multStart,
<a name="l00594"></a>00594 prev, prev );
<a name="l00595"></a>00595
<a name="l00596"></a>00596 Cudd_Ref(result);
<a name="l00597"></a>00597 Cudd_RecursiveDerefZdd(mgr.getManager(), prev);
<a name="l00598"></a>00598
<a name="l00599"></a>00599 prev = result;
<a name="l00600"></a>00600 ++multStart;
<a name="l00601"></a>00601
<a name="l00602"></a>00602 };
<a name="l00603"></a>00603
<a name="l00604"></a>00604 Cudd_Deref(prev);
<a name="l00605"></a>00605
<a name="l00606"></a>00606 <span class="keyword">typedef</span> <span class="keyword">typename</span> <a class="code" href="structpolybori_1_1manager__traits.html">manager_traits<ManagerType>::dd_base</a> dd_base;
<a name="l00607"></a>00607 <span class="keywordflow">return</span> dd_base(<a class="code" href="namespacepolybori.html#133ade2eba08cb872ac4355b389f2cdf">get_mgr_core</a>(mgr), prev);
<a name="l00608"></a>00608 }
<a name="l00609"></a>00609
<a name="l00610"></a>00610
<a name="l00611"></a>00611
<a name="l00613"></a>00613 <span class="keyword">template</span><<span class="keyword">class</span> ManagerType, <span class="keyword">class</span> ReverseIterator>
<a name="l00614"></a>00614 <span class="keyword">typename</span> manager_traits<ManagerType>::dd_base
<a name="l00615"></a><a class="code" href="namespacepolybori.html#220b46f13d6e432df1cd40432dddbabb">00615</a> <a class="code" href="namespacepolybori.html#220b46f13d6e432df1cd40432dddbabb" title="temporarily (needs to be more generic)">cudd_generate_divisors</a>(<span class="keyword">const</span> ManagerType& mgr,
<a name="l00616"></a>00616 ReverseIterator start, ReverseIterator finish) {
<a name="l00617"></a>00617
<a name="l00618"></a>00618 <span class="keyword">typedef</span> <span class="keyword">typename</span> <a class="code" href="structpolybori_1_1manager__traits.html">manager_traits<ManagerType>::dd_base</a> dd_base;
<a name="l00619"></a>00619 DdNode* prev= (mgr.getManager())->one;
<a name="l00620"></a>00620
<a name="l00621"></a>00621 Cudd_Ref(prev);
<a name="l00622"></a>00622 <span class="keywordflow">while</span>(start != finish) {
<a name="l00623"></a>00623
<a name="l00624"></a>00624 DdNode* result = cuddUniqueInterZdd( mgr.getManager(), *start,
<a name="l00625"></a>00625 prev, prev);
<a name="l00626"></a>00626
<a name="l00627"></a>00627 Cudd_Ref(result);
<a name="l00628"></a>00628 Cudd_RecursiveDerefZdd(mgr.getManager(), prev);
<a name="l00629"></a>00629
<a name="l00630"></a>00630 prev = result;
<a name="l00631"></a>00631 ++start;
<a name="l00632"></a>00632 }
<a name="l00633"></a>00633
<a name="l00634"></a>00634 Cudd_Deref(prev);
<a name="l00636"></a>00636 <span class="keywordflow">return</span> dd_base(<a class="code" href="namespacepolybori.html#133ade2eba08cb872ac4355b389f2cdf">get_mgr_core</a>(mgr), prev);
<a name="l00637"></a>00637
<a name="l00638"></a>00638 }
<a name="l00639"></a>00639
<a name="l00640"></a>00640
<a name="l00641"></a>00641 <span class="keyword">template</span><<span class="keyword">class</span> Iterator, <span class="keyword">class</span> SizeType>
<a name="l00642"></a>00642 Iterator
<a name="l00643"></a><a class="code" href="namespacepolybori.html#56c065103475f23d2b514ebf419fa79e">00643</a> <a class="code" href="namespacepolybori.html#56c065103475f23d2b514ebf419fa79e">bounded_max_element</a>(Iterator start, Iterator finish, SizeType bound){
<a name="l00644"></a>00644
<a name="l00645"></a>00645 <span class="keywordflow">if</span> (*start >= bound)
<a name="l00646"></a>00646 <span class="keywordflow">return</span> start;
<a name="l00647"></a>00647
<a name="l00648"></a>00648 Iterator result(start);
<a name="l00649"></a>00649 <span class="keywordflow">if</span> (start != finish)
<a name="l00650"></a>00650 ++start;
<a name="l00651"></a>00651
<a name="l00652"></a>00652 <span class="keywordflow">while</span> (start != finish) {
<a name="l00653"></a>00653 <span class="keywordflow">if</span>(*start >= bound)
<a name="l00654"></a>00654 <span class="keywordflow">return</span> start;
<a name="l00655"></a>00655 <span class="keywordflow">if</span>(*start > *result)
<a name="l00656"></a>00656 result = start;
<a name="l00657"></a>00657 ++start;
<a name="l00658"></a>00658 }
<a name="l00659"></a>00659
<a name="l00660"></a>00660 <span class="keywordflow">return</span> result;
<a name="l00661"></a>00661 }
<a name="l00662"></a>00662
<a name="l00665"></a>00665 <span class="keyword">template</span> <<span class="keyword">class</span> LhsType, <span class="keyword">class</span> RhsType, <span class="keyword">class</span> BinaryPredicate>
<a name="l00666"></a>00666 CTypes::comp_type
<a name="l00667"></a><a class="code" href="namespacepolybori.html#5d5bac8b009548eb8ec17ca2f47eced8">00667</a> <a class="code" href="namespacepolybori.html#5d5bac8b009548eb8ec17ca2f47eced8" title="defines lexicographic comparison for variable indices">generic_compare_3way</a>(<span class="keyword">const</span> LhsType& lhs, <span class="keyword">const</span> RhsType& rhs, BinaryPredicate comp) {
<a name="l00668"></a>00668
<a name="l00669"></a>00669 <span class="keywordflow">if</span> (lhs == rhs)
<a name="l00670"></a>00670 <span class="keywordflow">return</span> CTypes::equality;
<a name="l00671"></a>00671
<a name="l00672"></a>00672 <span class="keywordflow">return</span> (comp(lhs, rhs)? CTypes::greater_than: CTypes::less_than);
<a name="l00673"></a>00673 }
<a name="l00674"></a>00674
<a name="l00675"></a>00675
<a name="l00676"></a>00676
<a name="l00677"></a>00677 <span class="keyword">template</span> <<span class="keyword">class</span> IteratorLike, <span class="keyword">class</span> ForwardIteratorTag>
<a name="l00678"></a>00678 IteratorLike
<a name="l00679"></a><a class="code" href="namespacepolybori.html#d7c8a70512fdf0903425cc0e4b6d7125">00679</a> <a class="code" href="namespacepolybori.html#d7c8a70512fdf0903425cc0e4b6d7125">increment_iteratorlike</a>(IteratorLike iter, ForwardIteratorTag) {
<a name="l00680"></a>00680
<a name="l00681"></a>00681 <span class="keywordflow">return</span> ++iter;
<a name="l00682"></a>00682 }
<a name="l00683"></a>00683
<a name="l00684"></a>00684 <span class="keyword">template</span> <<span class="keyword">class</span> IteratorLike>
<a name="l00685"></a>00685 IteratorLike
<a name="l00686"></a><a class="code" href="namespacepolybori.html#6e736eaf4ce650ab31ef125ebb052f5b">00686</a> <a class="code" href="namespacepolybori.html#d7c8a70512fdf0903425cc0e4b6d7125">increment_iteratorlike</a>(IteratorLike iter, <a class="code" href="structpolybori_1_1navigator__tag.html" title="for iterator_category">navigator_tag</a>) {
<a name="l00687"></a>00687
<a name="l00688"></a>00688 <span class="keywordflow">return</span> iter.thenBranch();
<a name="l00689"></a>00689 }
<a name="l00690"></a>00690
<a name="l00691"></a>00691
<a name="l00692"></a>00692 <span class="keyword">template</span> <<span class="keyword">class</span> IteratorLike>
<a name="l00693"></a>00693 IteratorLike
<a name="l00694"></a><a class="code" href="namespacepolybori.html#2032714f022961f802e7f4500ccbf8bd">00694</a> <a class="code" href="namespacepolybori.html#d7c8a70512fdf0903425cc0e4b6d7125">increment_iteratorlike</a>(IteratorLike iter) {
<a name="l00695"></a>00695
<a name="l00696"></a>00696 <span class="keyword">typedef</span> <span class="keyword">typename</span> std::iterator_traits<IteratorLike>::iterator_category
<a name="l00697"></a>00697 iterator_category;
<a name="l00698"></a>00698
<a name="l00699"></a>00699 <span class="keywordflow">return</span> <a class="code" href="namespacepolybori.html#d7c8a70512fdf0903425cc0e4b6d7125">increment_iteratorlike</a>(iter, iterator_category());
<a name="l00700"></a>00700 }
<a name="l00701"></a>00701
<a name="l00702"></a>00702 <span class="preprocessor">#ifdef PBORI_LOWLEVEL_XOR </span>
<a name="l00703"></a>00703 <span class="preprocessor"></span>
<a name="l00704"></a>00704 <span class="comment">// dummy for cuddcache (implemented in pbori_routines.cc)</span>
<a name="l00705"></a>00705 DdNode*
<a name="l00706"></a>00706 <a class="code" href="namespacepolybori.html#c8eef4822df804ee3e8a6c97ecb722ef">pboriCuddZddUnionXor__</a>(DdManager *, DdNode *, DdNode *);
<a name="l00707"></a>00707
<a name="l00708"></a>00708
<a name="l00712"></a>00712 <span class="keyword">template</span> <<span class="keyword">class</span> MgrType, <span class="keyword">class</span> NodeType>
<a name="l00713"></a>00713 NodeType
<a name="l00714"></a><a class="code" href="namespacepolybori.html#e49cee209098fb6dd51dbd9f5af13c21">00714</a> <a class="code" href="namespacepolybori.html#e49cee209098fb6dd51dbd9f5af13c21">pboriCuddZddUnionXor</a>(MgrType zdd, NodeType P, NodeType Q) {
<a name="l00715"></a>00715
<a name="l00716"></a>00716 <span class="keywordtype">int</span> p_top, q_top;
<a name="l00717"></a>00717 NodeType empty = DD_ZERO(zdd), t, e, res;
<a name="l00718"></a>00718 MgrType table = zdd;
<a name="l00719"></a>00719
<a name="l00720"></a>00720 statLine(zdd);
<a name="l00721"></a>00721
<a name="l00722"></a>00722 <span class="keywordflow">if</span> (P == empty)
<a name="l00723"></a>00723 <span class="keywordflow">return</span>(Q);
<a name="l00724"></a>00724 <span class="keywordflow">if</span> (Q == empty)
<a name="l00725"></a>00725 <span class="keywordflow">return</span>(P);
<a name="l00726"></a>00726 <span class="keywordflow">if</span> (P == Q)
<a name="l00727"></a>00727 <span class="keywordflow">return</span>(empty);
<a name="l00728"></a>00728
<a name="l00729"></a>00729 <span class="comment">/* Check cache */</span>
<a name="l00730"></a>00730 res = cuddCacheLookup2Zdd(table, <a class="code" href="namespacepolybori.html#c8eef4822df804ee3e8a6c97ecb722ef">pboriCuddZddUnionXor__</a>, P, Q);
<a name="l00731"></a>00731 <span class="keywordflow">if</span> (res != NULL)
<a name="l00732"></a>00732 <span class="keywordflow">return</span>(res);
<a name="l00733"></a>00733
<a name="l00734"></a>00734 <span class="keywordflow">if</span> (cuddIsConstant(P))
<a name="l00735"></a>00735 p_top = P->index;
<a name="l00736"></a>00736 <span class="keywordflow">else</span>
<a name="l00737"></a>00737 p_top = P->index;<span class="comment">/* zdd->permZ[P->index]; */</span>
<a name="l00738"></a>00738 <span class="keywordflow">if</span> (cuddIsConstant(Q))
<a name="l00739"></a>00739 q_top = Q->index;
<a name="l00740"></a>00740 <span class="keywordflow">else</span>
<a name="l00741"></a>00741 q_top = Q->index; <span class="comment">/* zdd->permZ[Q->index]; */</span>
<a name="l00742"></a>00742 <span class="keywordflow">if</span> (p_top < q_top) {
<a name="l00743"></a>00743 e = <a class="code" href="namespacepolybori.html#e49cee209098fb6dd51dbd9f5af13c21">pboriCuddZddUnionXor</a>(zdd, cuddE(P), Q);
<a name="l00744"></a>00744 <span class="keywordflow">if</span> (e == NULL) <span class="keywordflow">return</span> (NULL);
<a name="l00745"></a>00745 Cudd_Ref(e);
<a name="l00746"></a>00746 res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
<a name="l00747"></a>00747 <span class="keywordflow">if</span> (res == NULL) {
<a name="l00748"></a>00748 Cudd_RecursiveDerefZdd(table, e);
<a name="l00749"></a>00749 <span class="keywordflow">return</span>(NULL);
<a name="l00750"></a>00750 }
<a name="l00751"></a>00751 Cudd_Deref(e);
<a name="l00752"></a>00752 } <span class="keywordflow">else</span> <span class="keywordflow">if</span> (p_top > q_top) {
<a name="l00753"></a>00753 e = <a class="code" href="namespacepolybori.html#e49cee209098fb6dd51dbd9f5af13c21">pboriCuddZddUnionXor</a>(zdd, P, cuddE(Q));
<a name="l00754"></a>00754 <span class="keywordflow">if</span> (e == NULL) <span class="keywordflow">return</span>(NULL);
<a name="l00755"></a>00755 Cudd_Ref(e);
<a name="l00756"></a>00756 res = cuddZddGetNode(zdd, Q->index, cuddT(Q), e);
<a name="l00757"></a>00757 <span class="keywordflow">if</span> (res == NULL) {
<a name="l00758"></a>00758 Cudd_RecursiveDerefZdd(table, e);
<a name="l00759"></a>00759 <span class="keywordflow">return</span>(NULL);
<a name="l00760"></a>00760 }
<a name="l00761"></a>00761 Cudd_Deref(e);
<a name="l00762"></a>00762 } <span class="keywordflow">else</span> {
<a name="l00763"></a>00763 t = <a class="code" href="namespacepolybori.html#e49cee209098fb6dd51dbd9f5af13c21">pboriCuddZddUnionXor</a>(zdd, cuddT(P), cuddT(Q));
<a name="l00764"></a>00764 <span class="keywordflow">if</span> (t == NULL) <span class="keywordflow">return</span>(NULL);
<a name="l00765"></a>00765 Cudd_Ref(t);
<a name="l00766"></a>00766 e = <a class="code" href="namespacepolybori.html#e49cee209098fb6dd51dbd9f5af13c21">pboriCuddZddUnionXor</a>(zdd, cuddE(P), cuddE(Q));
<a name="l00767"></a>00767 <span class="keywordflow">if</span> (e == NULL) {
<a name="l00768"></a>00768 Cudd_RecursiveDerefZdd(table, t);
<a name="l00769"></a>00769 <span class="keywordflow">return</span>(NULL);
<a name="l00770"></a>00770 }
<a name="l00771"></a>00771 Cudd_Ref(e);
<a name="l00772"></a>00772 res = cuddZddGetNode(zdd, P->index, t, e);
<a name="l00773"></a>00773 <span class="keywordflow">if</span> (res == NULL) {
<a name="l00774"></a>00774 Cudd_RecursiveDerefZdd(table, t);
<a name="l00775"></a>00775 Cudd_RecursiveDerefZdd(table, e);
<a name="l00776"></a>00776 <span class="keywordflow">return</span>(NULL);
<a name="l00777"></a>00777 }
<a name="l00778"></a>00778 Cudd_Deref(t);
<a name="l00779"></a>00779 Cudd_Deref(e);
<a name="l00780"></a>00780 }
<a name="l00781"></a>00781
<a name="l00782"></a>00782 cuddCacheInsert2(table, <a class="code" href="namespacepolybori.html#c8eef4822df804ee3e8a6c97ecb722ef">pboriCuddZddUnionXor__</a>, P, Q, res);
<a name="l00783"></a>00783
<a name="l00784"></a>00784 <span class="keywordflow">return</span>(res);
<a name="l00785"></a>00785 } <span class="comment">/* end of pboriCuddZddUnionXor */</span>
<a name="l00786"></a>00786
<a name="l00787"></a>00787 <span class="keyword">template</span> <<span class="keyword">class</span> MgrType, <span class="keyword">class</span> NodeType>
<a name="l00788"></a>00788 NodeType
<a name="l00789"></a><a class="code" href="namespacepolybori.html#41700debc9ce9c13c5e1b325e4148fcc">00789</a> <a class="code" href="namespacepolybori.html#41700debc9ce9c13c5e1b325e4148fcc">pboriCudd_zddUnionXor</a>(MgrType dd, NodeType P, NodeType Q) {
<a name="l00790"></a>00790
<a name="l00791"></a>00791 NodeType res;
<a name="l00792"></a>00792 <span class="keywordflow">do</span> {
<a name="l00793"></a>00793 dd->reordered = 0;
<a name="l00794"></a>00794 res = <a class="code" href="namespacepolybori.html#e49cee209098fb6dd51dbd9f5af13c21">pboriCuddZddUnionXor</a>(dd, P, Q);
<a name="l00795"></a>00795 } <span class="keywordflow">while</span> (dd->reordered == 1);
<a name="l00796"></a>00796 <span class="keywordflow">return</span>(res);
<a name="l00797"></a>00797 }
<a name="l00798"></a>00798
<a name="l00799"></a>00799 <span class="preprocessor">#endif // PBORI_LOWLEVEL_XOR </span>
<a name="l00800"></a>00800 <span class="preprocessor"></span>
<a name="l00801"></a>00801
<a name="l00802"></a>00802 <span class="keyword">template</span> <<span class="keyword">class</span> NaviType>
<a name="l00803"></a>00803 <span class="keywordtype">bool</span>
<a name="l00804"></a><a class="code" href="namespacepolybori.html#c33297fcea6d9ca92eabacdeeb2e050e">00804</a> <a class="code" href="namespacepolybori.html#c33297fcea6d9ca92eabacdeeb2e050e">dd_is_singleton</a>(NaviType navi) {
<a name="l00805"></a>00805
<a name="l00806"></a>00806 <span class="keywordflow">while</span>(!navi.isConstant()) {
<a name="l00807"></a>00807 <span class="keywordflow">if</span> (!navi.elseBranch().isEmpty())
<a name="l00808"></a>00808 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00809"></a>00809 navi.incrementThen();
<a name="l00810"></a>00810 }
<a name="l00811"></a>00811 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00812"></a>00812 }
<a name="l00813"></a>00813
<a name="l00814"></a>00814 <span class="keyword">template</span> <<span class="keyword">class</span> NaviType, <span class="keyword">class</span> BooleConstant>
<a name="l00815"></a>00815 BooleConstant
<a name="l00816"></a><a class="code" href="namespacepolybori.html#4e8278bdd0e2fb5175daff3f3d193f9d">00816</a> <a class="code" href="namespacepolybori.html#4e8278bdd0e2fb5175daff3f3d193f9d">dd_pair_check</a>(NaviType navi, <a class="code" href="classpolybori_1_1BooleConstant.html" title="This class wraps a bool value, which was not converted to a boolean polynomial or...">BooleConstant</a> allowSingleton) {
<a name="l00817"></a>00817
<a name="l00818"></a>00818 <span class="keywordflow">while</span>(!navi.isConstant()) {
<a name="l00819"></a>00819
<a name="l00820"></a>00820 <span class="keywordflow">if</span> (!navi.elseBranch().isEmpty())
<a name="l00821"></a>00821 <span class="keywordflow">return</span> <a class="code" href="namespacepolybori.html#c33297fcea6d9ca92eabacdeeb2e050e">dd_is_singleton</a>(navi.elseBranch()) &&
<a name="l00822"></a>00822 <a class="code" href="namespacepolybori.html#c33297fcea6d9ca92eabacdeeb2e050e">dd_is_singleton</a>(navi.thenBranch());
<a name="l00823"></a>00823
<a name="l00824"></a>00824 navi.incrementThen();
<a name="l00825"></a>00825 }
<a name="l00826"></a>00826 <span class="keywordflow">return</span> allowSingleton;<span class="comment">//();</span>
<a name="l00827"></a>00827 }
<a name="l00828"></a>00828
<a name="l00829"></a>00829
<a name="l00830"></a>00830 <span class="keyword">template</span> <<span class="keyword">class</span> NaviType>
<a name="l00831"></a>00831 <span class="keywordtype">bool</span>
<a name="l00832"></a><a class="code" href="namespacepolybori.html#e0805d1b223014c55931ebb35a19b435">00832</a> <a class="code" href="namespacepolybori.html#e0805d1b223014c55931ebb35a19b435">dd_is_singleton_or_pair</a>(NaviType navi) {
<a name="l00833"></a>00833
<a name="l00834"></a>00834 <span class="keywordflow">return</span> <a class="code" href="namespacepolybori.html#4e8278bdd0e2fb5175daff3f3d193f9d">dd_pair_check</a>(navi, <span class="keyword">true</span>);
<a name="l00835"></a>00835 }
<a name="l00836"></a>00836
<a name="l00837"></a>00837 <span class="keyword">template</span> <<span class="keyword">class</span> NaviType>
<a name="l00838"></a>00838 <span class="keywordtype">bool</span>
<a name="l00839"></a><a class="code" href="namespacepolybori.html#1e37aeba5f3db38e566e81de60082baa">00839</a> <a class="code" href="namespacepolybori.html#1e37aeba5f3db38e566e81de60082baa">dd_is_pair</a>(NaviType navi) {
<a name="l00840"></a>00840
<a name="l00841"></a>00841 <span class="keywordflow">return</span> <a class="code" href="namespacepolybori.html#4e8278bdd0e2fb5175daff3f3d193f9d">dd_pair_check</a>(navi, <span class="keyword">false</span>);
<a name="l00842"></a>00842 }
<a name="l00843"></a>00843
<a name="l00844"></a>00844
<a name="l00845"></a>00845
<a name="l00846"></a>00846 <span class="keyword">template</span> <<span class="keyword">class</span> SetType>
<a name="l00847"></a><a class="code" href="namespacepolybori.html#b65c63c61dd7aad862079a7925b4e723">00847</a> <span class="keywordtype">void</span> <a class="code" href="namespacepolybori.html#b65c63c61dd7aad862079a7925b4e723">combine_sizes</a>(<span class="keyword">const</span> SetType& bset, <span class="keywordtype">double</span>& init) {
<a name="l00848"></a>00848 init += bset.sizeDouble();
<a name="l00849"></a>00849 }
<a name="l00850"></a>00850
<a name="l00851"></a>00851 <span class="keyword">template</span> <<span class="keyword">class</span> SetType>
<a name="l00852"></a><a class="code" href="namespacepolybori.html#d21dcb084f3c03e9e7b2cbaa55e1aee4">00852</a> <span class="keywordtype">void</span> <a class="code" href="namespacepolybori.html#b65c63c61dd7aad862079a7925b4e723">combine_sizes</a>(<span class="keyword">const</span> SetType& bset,
<a name="l00853"></a>00853 <span class="keyword">typename</span> SetType::size_type& init) {
<a name="l00854"></a>00854 init += bset.size();
<a name="l00855"></a>00855 }
<a name="l00856"></a>00856
<a name="l00857"></a>00857
<a name="l00858"></a>00858 <span class="keyword">template</span> <<span class="keyword">class</span> SizeType, <span class="keyword">class</span> IdxType, <span class="keyword">class</span> NaviType, <span class="keyword">class</span> SetType>
<a name="l00859"></a>00859 SizeType&
<a name="l00860"></a><a class="code" href="namespacepolybori.html#1ef23e0db31b7bdde5d643bd686f19ba">00860</a> <a class="code" href="namespacepolybori.html#1ef23e0db31b7bdde5d643bd686f19ba">count_index</a>(SizeType& size, IdxType idx, NaviType navi, <span class="keyword">const</span> SetType& init) {
<a name="l00861"></a>00861
<a name="l00862"></a>00862 <span class="keywordflow">if</span> (*navi == idx)
<a name="l00863"></a>00863 <a class="code" href="namespacepolybori.html#b65c63c61dd7aad862079a7925b4e723">combine_sizes</a>(SetType(navi.incrementThen(), init.ring()), size);
<a name="l00864"></a>00864
<a name="l00865"></a>00865 <span class="keywordflow">if</span> (*navi < idx) {
<a name="l00866"></a>00866 <a class="code" href="namespacepolybori.html#1ef23e0db31b7bdde5d643bd686f19ba">count_index</a>(size, idx, navi.thenBranch(), init);
<a name="l00867"></a>00867 <a class="code" href="namespacepolybori.html#1ef23e0db31b7bdde5d643bd686f19ba">count_index</a>(size, idx, navi.elseBranch(), init);
<a name="l00868"></a>00868 }
<a name="l00869"></a>00869 <span class="keywordflow">return</span> size;
<a name="l00870"></a>00870 }
<a name="l00871"></a>00871
<a name="l00872"></a>00872
<a name="l00873"></a>00873 <span class="keyword">template</span> <<span class="keyword">class</span> SizeType, <span class="keyword">class</span> IdxType, <span class="keyword">class</span> SetType>
<a name="l00874"></a>00874 SizeType&
<a name="l00875"></a><a class="code" href="namespacepolybori.html#d2cfa7f286fcb7edd2506ea988108d15">00875</a> <a class="code" href="namespacepolybori.html#1ef23e0db31b7bdde5d643bd686f19ba">count_index</a>(SizeType& size, IdxType idx, <span class="keyword">const</span> SetType& bset) {
<a name="l00876"></a>00876
<a name="l00877"></a>00877 <span class="keywordflow">return</span> <a class="code" href="namespacepolybori.html#1ef23e0db31b7bdde5d643bd686f19ba">count_index</a>(size, idx, bset.navigation(), SetType());
<a name="l00878"></a>00878 }
<a name="l00879"></a>00879
<a name="l00880"></a>00880 <a class="code" href="pbori__defs_8h.html#faf094fde6c1a7f1aad18bcb455f3b06" title="Finish project&#39;s namespace.">END_NAMESPACE_PBORI</a>
<a name="l00881"></a>00881
<a name="l00882"></a>00882 <span class="preprocessor">#endif</span>
</pre></div></div>
<hr size="1"><address style="text-align: right;"><small>Generated on Wed Sep 9 14:30:59 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>
distrib
>
Mandriva
>
2010.0
>
i586
>
media
>
contrib-release
>
by-pkgid
>
a24e1a39141f9b4ca49bd1e2e23a54ba
>
files
>
804
