<!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_int.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_int.h</h1><a href="pbori__algo__int_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="l00055"></a>00055 <span class="comment"></span><span class="comment">//*****************************************************************************</span>
<a name="l00056"></a>00056
<a name="l00057"></a>00057 <span class="comment">// include polybori's definitions</span>
<a name="l00058"></a>00058 <span class="preprocessor">#include "<a class="code" href="pbori__defs_8h.html">pbori_defs.h</a>"</span>
<a name="l00059"></a>00059
<a name="l00060"></a>00060 <span class="comment">// get polybori's functionals</span>
<a name="l00061"></a>00061 <span class="preprocessor">#include "<a class="code" href="pbori__func_8h.html">pbori_func.h</a>"</span>
<a name="l00062"></a>00062 <span class="preprocessor">#include "<a class="code" href="CCuddNavigator_8h.html">CCuddNavigator.h</a>"</span>
<a name="l00063"></a>00063 <span class="preprocessor">#ifndef pbori_algo_int_h_</span>
<a name="l00064"></a>00064 <span class="preprocessor"></span><span class="preprocessor">#define pbori_algo_int_h_</span>
<a name="l00065"></a>00065 <span class="preprocessor"></span>
<a name="l00066"></a>00066 <a class="code" href="pbori__defs_8h.html#6ae360a591580558f31b6157ee792a10" title="Start project&#39;s namespace.">BEGIN_NAMESPACE_PBORI</a>
<a name="l00067"></a>00067
<a name="l00068"></a>00068
<a name="l00069"></a>00069
<a name="l00070"></a>00070 <span class="keyword">inline</span> <span class="keywordtype">void</span>
<a name="l00071"></a><a class="code" href="namespacepolybori.html#4d98e6d55edb29688b0d24fae3a349b9">00071</a> <a class="code" href="namespacepolybori.html#4d98e6d55edb29688b0d24fae3a349b9">inc_ref</a>(DdNode* node) {
<a name="l00072"></a>00072 Cudd_Ref(node);
<a name="l00073"></a>00073 }
<a name="l00074"></a>00074
<a name="l00075"></a>00075 <span class="keyword">template</span><<span class="keyword">class</span> NaviType>
<a name="l00076"></a>00076 <span class="keyword">inline</span> <span class="keywordtype">void</span>
<a name="l00077"></a><a class="code" href="namespacepolybori.html#d9cf47005b6fd44ae7fb33b491fcf176">00077</a> <a class="code" href="namespacepolybori.html#4d98e6d55edb29688b0d24fae3a349b9">inc_ref</a>(<span class="keyword">const</span> NaviType & navi) {
<a name="l00078"></a>00078 navi.incRef();
<a name="l00079"></a>00079 }
<a name="l00080"></a>00080
<a name="l00081"></a>00081 <span class="keyword">inline</span> <span class="keywordtype">void</span>
<a name="l00082"></a><a class="code" href="namespacepolybori.html#95f4ae2c996c9c5f3a7579b2b4c9b4df">00082</a> <a class="code" href="namespacepolybori.html#95f4ae2c996c9c5f3a7579b2b4c9b4df">dec_ref</a>(DdNode* node) {
<a name="l00083"></a>00083 Cudd_Deref(node);
<a name="l00084"></a>00084 }
<a name="l00085"></a>00085
<a name="l00086"></a>00086 <span class="keyword">template</span><<span class="keyword">class</span> NaviType>
<a name="l00087"></a>00087 <span class="keyword">inline</span> <span class="keywordtype">void</span>
<a name="l00088"></a><a class="code" href="namespacepolybori.html#db112a81d1c472d9dc767e336a6fccb9">00088</a> <a class="code" href="namespacepolybori.html#95f4ae2c996c9c5f3a7579b2b4c9b4df">dec_ref</a>(<span class="keyword">const</span> NaviType & navi) {
<a name="l00089"></a>00089 navi.decRef();
<a name="l00090"></a>00090 }
<a name="l00091"></a>00091
<a name="l00092"></a>00092 <span class="keyword">inline</span> DdNode*
<a name="l00093"></a><a class="code" href="namespacepolybori.html#e65aa84dbe2bba343ca9c10a5b87e05e">00093</a> <a class="code" href="namespacepolybori.html#e65aa84dbe2bba343ca9c10a5b87e05e">do_get_node</a>(DdNode* node) {
<a name="l00094"></a>00094 <span class="keywordflow">return</span> node;
<a name="l00095"></a>00095 }
<a name="l00096"></a>00096
<a name="l00097"></a>00097 <span class="keyword">template</span><<span class="keyword">class</span> NaviType>
<a name="l00098"></a>00098 <span class="keyword">inline</span> DdNode*
<a name="l00099"></a><a class="code" href="namespacepolybori.html#5a939c4b24f55c0b39e010f07d94cbce">00099</a> <a class="code" href="namespacepolybori.html#e65aa84dbe2bba343ca9c10a5b87e05e">do_get_node</a>(<span class="keyword">const</span> NaviType & navi) {
<a name="l00100"></a>00100 <span class="keywordflow">return</span> navi.getNode();
<a name="l00101"></a>00101 }
<a name="l00102"></a>00102
<a name="l00103"></a>00103 <span class="keyword">template</span> <<span class="keyword">class</span> MgrType>
<a name="l00104"></a>00104 <span class="keyword">inline</span> <span class="keywordtype">void</span>
<a name="l00105"></a><a class="code" href="namespacepolybori.html#2cd2b80c1a060d8530bf5e38b81081c6">00105</a> <a class="code" href="namespacepolybori.html#2cd2b80c1a060d8530bf5e38b81081c6">recursive_dec_ref</a>(<span class="keyword">const</span> MgrType& mgr, DdNode* node) {
<a name="l00106"></a>00106 Cudd_RecursiveDerefZdd(mgr, node);
<a name="l00107"></a>00107 }
<a name="l00108"></a>00108
<a name="l00109"></a>00109 <span class="keyword">template</span> <<span class="keyword">class</span> MgrType, <span class="keyword">class</span> NaviType>
<a name="l00110"></a>00110 <span class="keyword">inline</span> <span class="keywordtype">void</span>
<a name="l00111"></a><a class="code" href="namespacepolybori.html#2fc573a9e125f0b0a850ea157c8c9ec8">00111</a> <a class="code" href="namespacepolybori.html#2cd2b80c1a060d8530bf5e38b81081c6">recursive_dec_ref</a>(<span class="keyword">const</span> MgrType& mgr, <span class="keyword">const</span> NaviType & navi) {
<a name="l00112"></a>00112 navi.recursiveDecRef(mgr);
<a name="l00113"></a>00113 }
<a name="l00114"></a>00114
<a name="l00115"></a>00115 <span class="comment">// template<class NaviType, class SizeType, class ManagerType></span>
<a name="l00116"></a>00116 <span class="comment">// NaviType</span>
<a name="l00117"></a>00117 <span class="comment">// multiples_of_one_term(NaviType navi, SizeType nmax, ManagerType& man){</span>
<a name="l00118"></a>00118
<a name="l00119"></a>00119
<a name="l00120"></a>00120 <span class="comment">// std::vector<int> indices (Cudd_SupportSize(man,navi));</span>
<a name="l00121"></a>00121 <span class="comment">// std::vector<int>::iterator iter(indices.begin());</span>
<a name="l00122"></a>00122
<a name="l00123"></a>00123 <span class="comment">// NaviType multiples = navi;</span>
<a name="l00124"></a>00124
<a name="l00125"></a>00125 <span class="comment">// while(!multiples.isConstant()) {</span>
<a name="l00126"></a>00126 <span class="comment">// *iter = *multiples;</span>
<a name="l00127"></a>00127 <span class="comment">// multiples.incrementThen();</span>
<a name="l00128"></a>00128 <span class="comment">// ++iter;</span>
<a name="l00129"></a>00129 <span class="comment">// }</span>
<a name="l00130"></a>00130
<a name="l00131"></a>00131 <span class="comment">// std::vector<int>::const_reverse_iterator start(indices.rbegin()),</span>
<a name="l00132"></a>00132 <span class="comment">// finish(indices.rend());</span>
<a name="l00133"></a>00133
<a name="l00134"></a>00134 <span class="comment">// // int nmax = dd.nVariables();</span>
<a name="l00135"></a>00135
<a name="l00136"></a>00136 <span class="comment">// Cudd_Ref(multiples);</span>
<a name="l00137"></a>00137 <span class="comment">// NaviType emptyset = navi.elseBranch();</span>
<a name="l00138"></a>00138
<a name="l00139"></a>00139 <span class="comment">// NaviType tmp;</span>
<a name="l00140"></a>00140 <span class="comment">// SizeType i = nmax-1;</span>
<a name="l00141"></a>00141
<a name="l00142"></a>00142 <span class="comment">// while(start != finish){</span>
<a name="l00143"></a>00143
<a name="l00144"></a>00144 <span class="comment">// while ((idxStart != idxFinish) && (*idxStart > *start))</span>
<a name="l00145"></a>00145 <span class="comment">// // while(i > *start) {</span>
<a name="l00146"></a>00146
<a name="l00147"></a>00147 <span class="comment">// tmp = cuddZddGetNode(man, i, multiples, multiples);</span>
<a name="l00148"></a>00148 <span class="comment">// Cudd_Ref(tmp);</span>
<a name="l00149"></a>00149 <span class="comment">// Cudd_Deref(multiples);</span>
<a name="l00150"></a>00150 <span class="comment">// multiples = tmp;</span>
<a name="l00151"></a>00151 <span class="comment">// --i;</span>
<a name="l00152"></a>00152 <span class="comment">// }</span>
<a name="l00153"></a>00153 <span class="comment">// tmp = cuddZddGetNode(man, i, multiples, emptyset);</span>
<a name="l00154"></a>00154 <span class="comment">// Cudd_Ref(tmp);</span>
<a name="l00155"></a>00155 <span class="comment">// Cudd_Deref(multiples);</span>
<a name="l00156"></a>00156 <span class="comment">// multiples = tmp;</span>
<a name="l00157"></a>00157 <span class="comment">// --i;</span>
<a name="l00158"></a>00158 <span class="comment">// ++start;</span>
<a name="l00159"></a>00159 <span class="comment">// }</span>
<a name="l00160"></a>00160
<a name="l00161"></a>00161 <span class="comment">// return multiples;</span>
<a name="l00162"></a>00162 <span class="comment">// }</span>
<a name="l00163"></a>00163
<a name="l00164"></a>00164
<a name="l00165"></a>00165 <span class="keyword">template</span><<span class="keyword">class</span> NaviType, <span class="keyword">class</span> ReverseIterator, <span class="keyword">class</span> DDOperations>
<a name="l00166"></a>00166 NaviType
<a name="l00167"></a><a class="code" href="namespacepolybori.html#85cef6454769d8c9ae1e235782e4b8be">00167</a> <a class="code" href="namespacepolybori.html#85cef6454769d8c9ae1e235782e4b8be">indexed_term_multiples</a>(NaviType navi,
<a name="l00168"></a>00168 ReverseIterator idxStart, ReverseIterator idxFinish,
<a name="l00169"></a>00169 <span class="keyword">const</span> DDOperations& apply){
<a name="l00170"></a>00170
<a name="l00171"></a>00171 <span class="keyword">typedef</span> <span class="keyword">typename</span> NaviType::value_type <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a>;
<a name="l00172"></a>00172 <span class="keyword">typedef</span> <span class="keyword">typename</span> std::vector<idx_type> vector_type;
<a name="l00173"></a>00173 <span class="keyword">typedef</span> <span class="keyword">typename</span> vector_type::iterator iterator;
<a name="l00174"></a>00174 <span class="keyword">typedef</span> <span class="keyword">typename</span> vector_type::const_reverse_iterator const_reverse_iterator;
<a name="l00175"></a>00175
<a name="l00176"></a>00176 vector_type indices(apply.nSupport(navi));
<a name="l00177"></a>00177 iterator iter(indices.begin());
<a name="l00178"></a>00178
<a name="l00179"></a>00179 NaviType multiples = navi;
<a name="l00180"></a>00180
<a name="l00181"></a>00181 <span class="keywordflow">while</span>(!multiples.isConstant()) {
<a name="l00182"></a>00182 *iter = *multiples;
<a name="l00183"></a>00183 multiples.incrementThen();
<a name="l00184"></a>00184 ++iter;
<a name="l00185"></a>00185 }
<a name="l00186"></a>00186
<a name="l00187"></a>00187 const_reverse_iterator start(indices.rbegin()),
<a name="l00188"></a>00188 finish(indices.rend());
<a name="l00189"></a>00189
<a name="l00190"></a>00190
<a name="l00191"></a>00191 <a class="code" href="namespacepolybori.html#4d98e6d55edb29688b0d24fae3a349b9">inc_ref</a>(multiples);
<a name="l00192"></a>00192
<a name="l00193"></a>00193 <span class="keywordflow">while</span>(start != finish){
<a name="l00194"></a>00194
<a name="l00195"></a>00195 <span class="keywordflow">while</span>( (idxStart != idxFinish) && (*idxStart > *start) ) {
<a name="l00196"></a>00196 apply.multiplesAssign(multiples, *idxStart);
<a name="l00197"></a>00197 ++idxStart;
<a name="l00198"></a>00198 }
<a name="l00199"></a>00199 apply.productAssign(multiples, *start);
<a name="l00200"></a>00200 <span class="keywordflow">if</span>(idxStart != idxFinish)
<a name="l00201"></a>00201 ++idxStart;
<a name="l00202"></a>00202
<a name="l00203"></a>00203 ++start;
<a name="l00204"></a>00204 }
<a name="l00205"></a>00205
<a name="l00206"></a>00206 <span class="keywordflow">return</span> multiples;
<a name="l00207"></a>00207 }
<a name="l00208"></a>00208
<a name="l00209"></a>00209
<a name="l00210"></a>00210 <span class="keyword">template</span> <<span class="keyword">class</span> NaviType>
<a name="l00211"></a>00211 <span class="keywordtype">bool</span>
<a name="l00212"></a><a class="code" href="namespacepolybori.html#642441efa10dc73fe2ca9e6250b86fc8">00212</a> <a class="code" href="namespacepolybori.html#642441efa10dc73fe2ca9e6250b86fc8">is_reducible_by</a>(NaviType first, NaviType second){
<a name="l00213"></a>00213
<a name="l00214"></a>00214 <span class="keywordflow">while</span>(!second.isConstant()){
<a name="l00215"></a>00215 <span class="keywordflow">while</span>( (!first.isConstant()) && (*first < *second))
<a name="l00216"></a>00216 first.incrementThen();
<a name="l00217"></a>00217 <span class="keywordflow">if</span>(*first != *second)
<a name="l00218"></a>00218 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00219"></a>00219 second.incrementThen();
<a name="l00220"></a>00220 }
<a name="l00221"></a>00221 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00222"></a>00222 }
<a name="l00223"></a>00223
<a name="l00224"></a>00224 <span class="keyword">template</span><<span class="keyword">class</span> NaviType, <span class="keyword">class</span> ReverseIterator, <span class="keyword">class</span> DDOperations>
<a name="l00225"></a>00225 NaviType
<a name="l00226"></a><a class="code" href="namespacepolybori.html#cbdb4b217bcd090cafbb697ff07ba44a">00226</a> <a class="code" href="namespacepolybori.html#cbdb4b217bcd090cafbb697ff07ba44a">minimal_of_two_terms</a>(NaviType navi, NaviType& multiples,
<a name="l00227"></a>00227 ReverseIterator idxStart, ReverseIterator idxFinish,
<a name="l00228"></a>00228 <span class="keyword">const</span> DDOperations& apply){
<a name="l00229"></a>00229
<a name="l00230"></a>00230 <span class="keyword">typedef</span> <span class="keyword">typename</span> NaviType::value_type <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a>;
<a name="l00231"></a>00231 <span class="keyword">typedef</span> <span class="keyword">typename</span> std::vector<idx_type> vector_type;
<a name="l00232"></a>00232 <span class="keyword">typedef</span> <span class="keyword">typename</span> vector_type::iterator iterator;
<a name="l00233"></a>00233 <span class="keyword">typedef</span> <span class="keyword">typename</span> vector_type::size_type size_type;
<a name="l00234"></a>00234 <span class="keyword">typedef</span> <span class="keyword">typename</span> vector_type::const_reverse_iterator const_reverse_iterator;
<a name="l00235"></a>00235
<a name="l00236"></a>00236 <span class="comment">// std::cout <<"2s ";</span>
<a name="l00237"></a>00237
<a name="l00238"></a>00238
<a name="l00239"></a>00239 size_type nmax = apply.nSupport(navi);
<a name="l00240"></a>00240 vector_type thenIdx(nmax), elseIdx(nmax);
<a name="l00241"></a>00241
<a name="l00242"></a>00242 thenIdx.resize(0);
<a name="l00243"></a>00243 elseIdx.resize(0);
<a name="l00244"></a>00244
<a name="l00245"></a>00245 NaviType thenNavi = navi;
<a name="l00246"></a>00246 NaviType elseNavi = navi;
<a name="l00247"></a>00247
<a name="l00248"></a>00248 <span class="comment">// See CCuddLastIterator</span>
<a name="l00249"></a>00249 NaviType tmp(elseNavi);
<a name="l00250"></a>00250 elseNavi.incrementElse();
<a name="l00251"></a>00251
<a name="l00252"></a>00252 <span class="keywordflow">while</span>(!elseNavi.isConstant()){
<a name="l00253"></a>00253 tmp = elseNavi;
<a name="l00254"></a>00254 elseNavi.incrementElse();
<a name="l00255"></a>00255 }
<a name="l00256"></a>00256 <span class="keywordflow">if</span>(elseNavi.isEmpty())
<a name="l00257"></a>00257 elseNavi = tmp;
<a name="l00258"></a>00258
<a name="l00259"></a>00259 <span class="comment">// std::cout <<"TH "<<*thenNavi <<" "<<*elseNavi<< ":";</span>
<a name="l00260"></a>00260
<a name="l00261"></a>00261 <span class="keywordtype">bool</span> isReducible = <span class="keyword">true</span>;
<a name="l00262"></a>00262 <span class="keywordflow">while</span> (isReducible && !thenNavi.isConstant() && !elseNavi.isConstant()){
<a name="l00263"></a>00263
<a name="l00264"></a>00264 <span class="keywordflow">while</span>( !thenNavi.isConstant() && (*thenNavi < *elseNavi)) {
<a name="l00265"></a>00265 <span class="comment">// std::cout <<"th "<<*thenNavi <<" "<<*elseNavi<< ":";</span>
<a name="l00266"></a>00266
<a name="l00267"></a>00267 <span class="comment">// apply.print(thenNavi);</span>
<a name="l00268"></a>00268 <span class="comment">// apply.print(elseNavi);</span>
<a name="l00269"></a>00269 thenIdx.push_back(*thenNavi);
<a name="l00270"></a>00270 thenNavi.incrementThen();
<a name="l00271"></a>00271 }
<a name="l00272"></a>00272
<a name="l00273"></a>00273 <span class="keywordflow">if</span>(!thenNavi.isConstant() && (*thenNavi == *elseNavi) ){
<a name="l00274"></a>00274 thenIdx.push_back(*thenNavi);
<a name="l00275"></a>00275 thenNavi.incrementThen();
<a name="l00276"></a>00276 }
<a name="l00277"></a>00277 <span class="keywordflow">else</span>
<a name="l00278"></a>00278 isReducible = <span class="keyword">false</span>;
<a name="l00279"></a>00279 <span class="comment">// std::cout <<""<<isReducible << thenNavi.isConstant()<<std::endl;</span>
<a name="l00280"></a>00280
<a name="l00281"></a>00281 elseIdx.push_back(*elseNavi);
<a name="l00282"></a>00282
<a name="l00283"></a>00283 <span class="comment">// next on last path</span>
<a name="l00284"></a>00284 elseNavi.incrementThen();
<a name="l00285"></a>00285 <span class="keywordflow">if</span>( !elseNavi.isConstant() ) { <span class="comment">// if still in interior of a path</span>
<a name="l00286"></a>00286
<a name="l00287"></a>00287 tmp = elseNavi; <span class="comment">// store copy of *this</span>
<a name="l00288"></a>00288 elseNavi.incrementElse(); <span class="comment">// go in direction of last term, if possible</span>
<a name="l00289"></a>00289
<a name="l00290"></a>00290 <span class="comment">// restore previous value, of else branch was invalid</span>
<a name="l00291"></a>00291 <span class="keywordflow">if</span>( elseNavi.isEmpty() )
<a name="l00292"></a>00292 elseNavi = tmp;
<a name="l00293"></a>00293
<a name="l00294"></a>00294 }
<a name="l00295"></a>00295 }
<a name="l00296"></a>00296
<a name="l00297"></a>00297
<a name="l00298"></a>00298 NaviType elseTail, elseMult;
<a name="l00299"></a>00299 apply.assign(elseTail, elseNavi);
<a name="l00300"></a>00300
<a name="l00301"></a>00301
<a name="l00302"></a>00302 <span class="comment">// int initref = ((DdNode*)elseNavi)->ref;</span>
<a name="l00303"></a>00303 <span class="comment">// std::cout << ((DdNode*)elseNavi)->ref <<std::endl;</span>
<a name="l00304"></a>00304 <span class="keywordflow">if</span> (!elseNavi.isConstant()) {
<a name="l00305"></a>00305 isReducible = <span class="keyword">false</span>;
<a name="l00306"></a>00306 elseMult =
<a name="l00307"></a>00307 <a class="code" href="namespacepolybori.html#85cef6454769d8c9ae1e235782e4b8be">indexed_term_multiples</a>(elseTail, idxStart, idxFinish, apply);
<a name="l00308"></a>00308 <span class="comment">// if(elseMult==elseTail)</span>
<a name="l00309"></a>00309 <span class="comment">// Cudd_Deref(elseMult);</span>
<a name="l00310"></a>00310 }
<a name="l00311"></a>00311 <span class="keywordflow">else</span> {
<a name="l00314"></a>00314 apply.assign(elseMult, elseTail);
<a name="l00315"></a>00315 }
<a name="l00316"></a>00316
<a name="l00317"></a>00317 NaviType tmp2 = <a class="code" href="namespacepolybori.html#ab0655446e6aaf46050e2d4e143588d6">prepend_multiples_wrt_indices</a>(elseMult, *navi,
<a name="l00318"></a>00318 idxStart, idxFinish, apply);
<a name="l00319"></a>00319
<a name="l00320"></a>00320 tmp2.incRef();
<a name="l00321"></a>00321 elseMult.decRef();
<a name="l00322"></a>00322 elseMult = tmp2;
<a name="l00323"></a>00323 <span class="comment">// std::cerr<< "h1"<<std::endl;</span>
<a name="l00324"></a>00324
<a name="l00325"></a>00325 NaviType thenTail, thenMult;
<a name="l00326"></a>00326
<a name="l00327"></a>00327 <span class="keywordflow">if</span>(!isReducible){
<a name="l00328"></a>00328
<a name="l00329"></a>00329 <span class="comment">// if(!thenNavi.isConstant())</span>
<a name="l00330"></a>00330 <span class="comment">// std::cout << " "<<(*thenNavi)<< " "<< *idxStart<<std::endl;</span>
<a name="l00331"></a>00331 apply.assign(thenTail, thenNavi);
<a name="l00333"></a>00333
<a name="l00334"></a>00334 <span class="keywordflow">if</span> (!thenNavi.isConstant()){
<a name="l00335"></a>00335
<a name="l00336"></a>00336 thenMult =
<a name="l00337"></a>00337 <a class="code" href="namespacepolybori.html#85cef6454769d8c9ae1e235782e4b8be">indexed_term_multiples</a>(thenTail, idxStart, idxFinish, apply);
<a name="l00338"></a>00338 <span class="comment">// if(thenMult==thenTail)</span>
<a name="l00339"></a>00339 <span class="comment">// Cudd_Deref(thenMult);</span>
<a name="l00340"></a>00340 <span class="comment">//Cudd_Deref(thenTail);///</span>
<a name="l00342"></a>00342 <span class="comment"></span> }
<a name="l00343"></a>00343 <span class="keywordflow">else</span>{
<a name="l00345"></a>00345 apply.assign(thenMult, thenTail);
<a name="l00346"></a>00346 }
<a name="l00347"></a>00347 }
<a name="l00348"></a>00348 <span class="comment">// std::cerr<< "h2"<<std::endl;</span>
<a name="l00349"></a>00349 <span class="comment">// generating elsePath and multiples</span>
<a name="l00350"></a>00350 ReverseIterator idxIter = idxStart;
<a name="l00351"></a>00351 const_reverse_iterator start(elseIdx.rbegin()), finish(elseIdx.rend());
<a name="l00352"></a>00352
<a name="l00353"></a>00353 <span class="comment">// Cudd_Ref(elseMult);</span>
<a name="l00354"></a>00354 <span class="comment">// std::cout << "isRed"<< isReducible <<std::endl;</span>
<a name="l00355"></a>00355
<a name="l00356"></a>00356 <span class="keywordflow">if</span>(!elseMult.isConstant())
<a name="l00357"></a>00357 <span class="keywordflow">while</span>((idxIter != idxFinish) && (*idxIter >= *elseMult) )
<a name="l00358"></a>00358 ++idxIter;
<a name="l00359"></a>00359
<a name="l00360"></a>00360 <span class="keywordflow">while</span>(start != finish){
<a name="l00361"></a>00361
<a name="l00362"></a>00362 <span class="keywordflow">while</span>((idxIter != idxFinish) && (*idxIter > *start) ) {
<a name="l00363"></a>00363
<a name="l00364"></a>00364 apply.multiplesAssign(elseMult, *idxIter);
<a name="l00365"></a>00365 ++idxIter;
<a name="l00366"></a>00366 }
<a name="l00367"></a>00367 apply.productAssign(elseMult, *start);
<a name="l00368"></a>00368
<a name="l00369"></a>00369 <span class="keywordflow">if</span> (isReducible)
<a name="l00370"></a>00370 apply.productAssign(elseTail, *start);
<a name="l00371"></a>00371
<a name="l00372"></a>00372 <span class="keywordflow">if</span>(idxIter != idxFinish)
<a name="l00373"></a>00373 ++idxIter;
<a name="l00374"></a>00374 ++start;
<a name="l00375"></a>00375 }
<a name="l00376"></a>00376 <span class="comment">// std::cerr<< "h3"<<std::endl;</span>
<a name="l00377"></a>00377 <span class="keywordflow">if</span> (isReducible){
<a name="l00378"></a>00378 multiples = elseMult;
<a name="l00379"></a>00379
<a name="l00380"></a>00380
<a name="l00382"></a>00382 <span class="comment">// Cudd_Ref(elseTail); </span>
<a name="l00383"></a>00383 <span class="comment">//Cudd_Deref(thenTail); </span>
<a name="l00384"></a>00384 <span class="comment">//Cudd_Deref(thenMult); </span>
<a name="l00385"></a>00385
<a name="l00386"></a>00386 <span class="comment">// std::cerr<< "h4"<<std::endl;</span>
<a name="l00387"></a>00387 <span class="keywordflow">return</span> elseTail;
<a name="l00388"></a>00388 }
<a name="l00389"></a>00389 <span class="keywordflow">else</span> {
<a name="l00390"></a>00390
<a name="l00391"></a>00391 <span class="comment">// std::cerr<< "h5"<<std::endl;</span>
<a name="l00392"></a>00392 const_reverse_iterator start2(thenIdx.rbegin()), finish2(thenIdx.rend());
<a name="l00393"></a>00393 ReverseIterator idxIter = idxStart;
<a name="l00394"></a>00394
<a name="l00395"></a>00395 <span class="comment">// Cudd_Ref(thenMult);</span>
<a name="l00396"></a>00396 <span class="comment">// NaviType printer = thenMult; std::cout<< "thenMult"<<std::endl;</span>
<a name="l00397"></a>00397 <span class="comment">// while(!printer.isConstant()){</span>
<a name="l00398"></a>00398 <span class="comment">// std::cout<< *printer <<" & ";</span>
<a name="l00399"></a>00399 <span class="comment">// printer.incrementThen();</span>
<a name="l00400"></a>00400 <span class="comment">// }</span>
<a name="l00401"></a>00401 <span class="keywordflow">if</span>(!thenMult.isConstant())
<a name="l00402"></a>00402 <span class="keywordflow">while</span>((idxIter != idxFinish) && (*idxIter >= *thenMult) )
<a name="l00403"></a>00403 ++idxIter;
<a name="l00404"></a>00404
<a name="l00405"></a>00405
<a name="l00406"></a>00406 <span class="comment">// std::cerr<< "h6"<<std::endl;</span>
<a name="l00407"></a>00407
<a name="l00408"></a>00408
<a name="l00409"></a>00409 <span class="keywordflow">while</span>(start2 != finish2){
<a name="l00410"></a>00410
<a name="l00411"></a>00411 <span class="keywordflow">while</span>((idxIter != idxFinish) && (*idxIter > *start2) ) {
<a name="l00412"></a>00412 <span class="comment">// std::cout<< *idxIter <<" ? ";</span>
<a name="l00413"></a>00413 apply.multiplesAssign(thenMult, *idxIter);
<a name="l00414"></a>00414 ++idxIter;
<a name="l00415"></a>00415 }
<a name="l00416"></a>00416 apply.productAssign(thenMult, *start2);
<a name="l00417"></a>00417 <span class="comment">// apply.productAssign(thenTail, *start); </span>
<a name="l00418"></a>00418 <span class="keywordflow">if</span>(idxIter != idxFinish)
<a name="l00419"></a>00419 ++idxIter;
<a name="l00420"></a>00420 ++start2;
<a name="l00421"></a>00421 }
<a name="l00422"></a>00422
<a name="l00423"></a>00423
<a name="l00424"></a>00424 apply.replacingUnite(multiples, elseMult, thenMult);
<a name="l00425"></a>00425
<a name="l00426"></a>00426
<a name="l00427"></a>00427
<a name="l00428"></a>00428 <span class="comment">// std::cerr<< "h7"<<std::endl;</span>
<a name="l00429"></a>00429 <span class="comment">// printer = multiples; std::cout<< "mu"<<std::endl;</span>
<a name="l00430"></a>00430 <span class="comment">// while(!printer.isConstant()){</span>
<a name="l00431"></a>00431 <span class="comment">// // std::cout<< *printer <<" & ";</span>
<a name="l00432"></a>00432 <span class="comment">// printer.incrementThen();</span>
<a name="l00433"></a>00433 <span class="comment">// }</span>
<a name="l00434"></a>00434 <span class="comment">// std::cout<< std::endl;</span>
<a name="l00436"></a>00436 <span class="comment"></span> <span class="comment">// return apply.newNode(navi);</span>
<a name="l00437"></a>00437 <span class="comment">// std::cout << " "<<((DdNode*)thenTail)->ref<<std::endl;</span>
<a name="l00438"></a>00438 <span class="comment">// std::cerr<< "h8"<<std::endl;</span>
<a name="l00439"></a>00439
<a name="l00440"></a>00440 apply.kill(elseTail);
<a name="l00441"></a>00441 apply.kill(thenTail);
<a name="l00442"></a>00442
<a name="l00443"></a>00443
<a name="l00444"></a>00444 <span class="keywordflow">return</span> apply.newNode(navi);
<a name="l00445"></a>00445 }
<a name="l00446"></a>00446
<a name="l00447"></a>00447
<a name="l00448"></a>00448
<a name="l00449"></a>00449 <span class="comment">// // remainder of first term</span>
<a name="l00450"></a>00450 <span class="comment">// while (!thenNavi.isConstant() ){</span>
<a name="l00451"></a>00451 <span class="comment">// thenIdx.push_back(*thenNavi);</span>
<a name="l00452"></a>00452 <span class="comment">// thenIdx.incrementThen();</span>
<a name="l00453"></a>00453 <span class="comment">// }</span>
<a name="l00454"></a>00454
<a name="l00455"></a>00455 <span class="comment">// // remainder of last term</span>
<a name="l00456"></a>00456 <span class="comment">// while (!elseNavi.isConstant()){</span>
<a name="l00457"></a>00457 <span class="comment">// elseIdx.push_back(*elseNavi);</span>
<a name="l00458"></a>00458
<a name="l00459"></a>00459 <span class="comment">// elseIdx.incrementThen();</span>
<a name="l00460"></a>00460 <span class="comment">// if( !elseIdx.isConstant() ) { // if still in interior of a path</span>
<a name="l00461"></a>00461
<a name="l00462"></a>00462 <span class="comment">// tmp = elseNavi; // store copy of *this</span>
<a name="l00463"></a>00463 <span class="comment">// elseNavi.incrementElse(); // go in direction of last term, if possible</span>
<a name="l00464"></a>00464
<a name="l00465"></a>00465 <span class="comment">// // restore previous value, of else branch was invalid</span>
<a name="l00466"></a>00466 <span class="comment">// if( elseNavi.isEmpty() )</span>
<a name="l00467"></a>00467 <span class="comment">// elseNavi = tmp;</span>
<a name="l00468"></a>00468 <span class="comment">// }</span>
<a name="l00469"></a>00469 <span class="comment">// isReducible = false;</span>
<a name="l00470"></a>00470 <span class="comment">// }</span>
<a name="l00471"></a>00471
<a name="l00472"></a>00472
<a name="l00473"></a>00473
<a name="l00474"></a>00474 }
<a name="l00475"></a>00475
<a name="l00476"></a>00476
<a name="l00477"></a>00477 <span class="keyword">template</span> <<span class="keyword">class </span>NaviType, <span class="keyword">class </span>SizeType, <span class="keyword">class </span>ReverseIterator,
<a name="l00478"></a>00478 <span class="keyword">class </span>DDOperations>
<a name="l00479"></a>00479 NaviType
<a name="l00480"></a><a class="code" href="namespacepolybori.html#ab0655446e6aaf46050e2d4e143588d6">00480</a> <a class="code" href="namespacepolybori.html#ab0655446e6aaf46050e2d4e143588d6">prepend_multiples_wrt_indices</a>(NaviType navi, SizeType minIdx,
<a name="l00481"></a>00481 ReverseIterator start, ReverseIterator finish,
<a name="l00482"></a>00482 <span class="keyword">const</span> DDOperations& apply) {
<a name="l00483"></a>00483
<a name="l00484"></a>00484 <span class="keywordflow">if</span> (navi.isConstant()){
<a name="l00485"></a>00485 <span class="keywordflow">if</span> (!navi.terminalValue())
<a name="l00486"></a>00486 <span class="keywordflow">return</span> navi;
<a name="l00487"></a>00487 }
<a name="l00488"></a>00488 <span class="keywordflow">else</span>
<a name="l00489"></a>00489 <span class="keywordflow">while</span> ( (start != finish) && (*start >= *navi) )
<a name="l00490"></a>00490 ++start;
<a name="l00491"></a>00491
<a name="l00492"></a>00492 <span class="keywordflow">while</span>( (start != finish) && (*start > minIdx) ){
<a name="l00493"></a>00493 apply.multiplesAssign(navi, *start);
<a name="l00494"></a>00494 ++start;
<a name="l00495"></a>00495 }
<a name="l00496"></a>00496 <span class="keywordflow">return</span> navi;
<a name="l00497"></a>00497 }
<a name="l00498"></a>00498
<a name="l00499"></a>00499 <span class="keyword">template</span><<span class="keyword">class</span> FunctionType, <span class="keyword">class</span> ManagerType, <span class="keyword">class</span> NodeType>
<a name="l00500"></a><a class="code" href="namespacepolybori.html#3ae33491fa91b97ee75b4b7eab8f3f8f">00500</a> <span class="keywordtype">void</span> <a class="code" href="namespacepolybori.html#3ae33491fa91b97ee75b4b7eab8f3f8f">apply_assign_cudd_function</a>(FunctionType func, ManagerType& mgr,
<a name="l00501"></a>00501 NodeType& first, <span class="keyword">const</span> NodeType& second) {
<a name="l00502"></a>00502
<a name="l00503"></a>00503 NodeType newNode(func(mgr, <a class="code" href="namespacepolybori.html#e65aa84dbe2bba343ca9c10a5b87e05e">do_get_node</a>(first), <a class="code" href="namespacepolybori.html#e65aa84dbe2bba343ca9c10a5b87e05e">do_get_node</a>(second)));
<a name="l00504"></a>00504 <a class="code" href="namespacepolybori.html#4d98e6d55edb29688b0d24fae3a349b9">inc_ref</a>(newNode);
<a name="l00505"></a>00505 <a class="code" href="namespacepolybori.html#2cd2b80c1a060d8530bf5e38b81081c6">recursive_dec_ref</a>(mgr, first);
<a name="l00506"></a>00506 first = newNode;
<a name="l00507"></a>00507 }
<a name="l00508"></a>00508
<a name="l00509"></a>00509
<a name="l00510"></a>00510
<a name="l00511"></a>00511 <span class="keyword">template</span><<span class="keyword">class </span>FunctionType, <span class="keyword">class </span>ManagerType, <span class="keyword">class </span>ResultType,
<a name="l00512"></a>00512 <span class="keyword">class </span>NodeType>
<a name="l00513"></a><a class="code" href="namespacepolybori.html#fc0c31909c2746cc0cff6d463f6cf4ef">00513</a> <span class="keywordtype">void</span> <a class="code" href="namespacepolybori.html#fc0c31909c2746cc0cff6d463f6cf4ef">apply_replacing_cudd_function</a>(FunctionType func, ManagerType& mgr,
<a name="l00514"></a>00514 ResultType& newNode,
<a name="l00515"></a>00515 <span class="keyword">const</span> NodeType& first,
<a name="l00516"></a>00516 <span class="keyword">const</span> NodeType& second) {
<a name="l00517"></a>00517
<a name="l00518"></a>00518 newNode = NodeType(func(mgr, <a class="code" href="namespacepolybori.html#e65aa84dbe2bba343ca9c10a5b87e05e">do_get_node</a>(first), <a class="code" href="namespacepolybori.html#e65aa84dbe2bba343ca9c10a5b87e05e">do_get_node</a>(second)));
<a name="l00519"></a>00519 <a class="code" href="namespacepolybori.html#4d98e6d55edb29688b0d24fae3a349b9">inc_ref</a>(newNode);
<a name="l00520"></a>00520 <a class="code" href="namespacepolybori.html#2cd2b80c1a060d8530bf5e38b81081c6">recursive_dec_ref</a>(mgr, first);
<a name="l00521"></a>00521 <a class="code" href="namespacepolybori.html#2cd2b80c1a060d8530bf5e38b81081c6">recursive_dec_ref</a>(mgr, second);
<a name="l00522"></a>00522 }
<a name="l00523"></a>00523
<a name="l00524"></a>00524 <span class="keyword">template</span><<span class="keyword">class</span> FunctionType, <span class="keyword">class</span> ManagerType, <span class="keyword">class</span> NodeType>
<a name="l00525"></a><a class="code" href="namespacepolybori.html#65583cfb652f6bb456fd4df488d0c1b4">00525</a> NodeType <a class="code" href="namespacepolybori.html#65583cfb652f6bb456fd4df488d0c1b4">apply_cudd_function</a>(FunctionType func, ManagerType& mgr,
<a name="l00526"></a>00526 <span class="keyword">const</span> NodeType& first, <span class="keyword">const</span> NodeType& second) {
<a name="l00527"></a>00527
<a name="l00528"></a>00528 NodeType newNode;
<a name="l00529"></a>00529 newNode = NodeType(func(mgr, <a class="code" href="namespacepolybori.html#e65aa84dbe2bba343ca9c10a5b87e05e">do_get_node</a>(first), <a class="code" href="namespacepolybori.html#e65aa84dbe2bba343ca9c10a5b87e05e">do_get_node</a>(second)));
<a name="l00530"></a>00530 <a class="code" href="namespacepolybori.html#4d98e6d55edb29688b0d24fae3a349b9">inc_ref</a>(newNode);
<a name="l00531"></a>00531 <span class="keywordflow">return</span> newNode;
<a name="l00532"></a>00532 }
<a name="l00533"></a>00533
<a name="l00534"></a>00534 <span class="keyword">template</span> <<span class="keyword">class</span> DDType>
<a name="l00535"></a>00535 <span class="keyword">class </span>dd_operations;
<a name="l00536"></a>00536
<a name="l00537"></a>00537 <span class="keyword">template</span><>
<a name="l00538"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html">00538</a> <span class="keyword">class </span>dd_operations<<a class="code" href="structpolybori_1_1CTypes.html" title="This struct contains type definitions to be used in library classes.">CTypes</a>::<a class="code" href="classpolybori_1_1CDDInterface.html">dd_type</a>::<a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>> {
<a name="l00539"></a>00539 <span class="keyword">public</span>:
<a name="l00540"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#84fd0199b8e107a5a13eaee756f02a96">00540</a> <span class="keyword">typedef</span> DdManager* manager_type;
<a name="l00541"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#2d20d54db970ebd7db7d798fef8d35ac">00541</a> <span class="keyword">typedef</span> <a class="code" href="classpolybori_1_1CDDInterface.html">CTypes::dd_type</a> <a class="code" href="classpolybori_1_1CDDInterface.html">dd_type</a>;
<a name="l00542"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#b15241ff708646664877c38a109e8bbf">00542</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...">dd_type::navigator</a> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>;
<a name="l00543"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#c1328563048384b01282c3b0a87d2f8f">00543</a> <span class="keyword">typedef</span> <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">dd_type::idx_type</a> <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a>;
<a name="l00544"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#6e1e0b132354ce7d3065d8165cd40f5f">00544</a> <span class="keyword">typedef</span> dd_type::size_type size_type;
<a name="l00545"></a>00545
<a name="l00546"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#cf653b2b767ed69426ffac0355effcdf">00546</a> <a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#cf653b2b767ed69426ffac0355effcdf">dd_operations</a>(manager_type man): mgr(man) {}
<a name="l00547"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#eb6a284a4c77f270f101d1aac3c7c6ce">00547</a> <span class="keywordtype">void</span> replacingUnite(<a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& newNode,
<a name="l00548"></a>00548 <span class="keyword">const</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& first, <span class="keyword">const</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& second)<span class="keyword"> const </span>{
<a name="l00549"></a>00549
<a name="l00550"></a>00550 <a class="code" href="namespacepolybori.html#fc0c31909c2746cc0cff6d463f6cf4ef">apply_replacing_cudd_function</a>(Cudd_zddUnion, mgr, newNode, first, second);
<a name="l00551"></a>00551 }
<a name="l00552"></a>00552
<a name="l00553"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#2fc459e94ef76b12644e4e3cec21b9ca">00553</a> <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#2fc459e94ef76b12644e4e3cec21b9ca">uniteAssign</a>(<a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& first, <span class="keyword">const</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& second)<span class="keyword"> const </span>{
<a name="l00554"></a>00554 <a class="code" href="namespacepolybori.html#3ae33491fa91b97ee75b4b7eab8f3f8f">apply_assign_cudd_function</a>(Cudd_zddUnion, mgr, first, second);
<a name="l00555"></a>00555 }
<a name="l00556"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#4f65e0f58365b7d663b612b160516890">00556</a> <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#4f65e0f58365b7d663b612b160516890">diffAssign</a>(<a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& first, <span class="keyword">const</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& second)<span class="keyword"> const </span>{
<a name="l00557"></a>00557 <a class="code" href="namespacepolybori.html#3ae33491fa91b97ee75b4b7eab8f3f8f">apply_assign_cudd_function</a>(Cudd_zddDiff, mgr, first, second);
<a name="l00558"></a>00558 }
<a name="l00559"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#f77b19c0459095f2ccafc6a538f584f4">00559</a> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a> <a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#f77b19c0459095f2ccafc6a538f584f4">diff</a>(<span class="keyword">const</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& first, <span class="keyword">const</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& second)<span class="keyword"> const </span>{
<a name="l00560"></a>00560 <span class="keywordflow">return</span> <a class="code" href="namespacepolybori.html#65583cfb652f6bb456fd4df488d0c1b4">apply_cudd_function</a>(Cudd_zddDiff, mgr, first, second);
<a name="l00561"></a>00561 }
<a name="l00562"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#2302bfad8dfb1c10cc68f8fe0e1b4797">00562</a> <span class="keywordtype">void</span> replacingNode(<a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& newNode, <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> idx,
<a name="l00563"></a>00563 <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& first, <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& second)<span class="keyword"> const </span>{
<a name="l00564"></a>00564
<a name="l00565"></a>00565 newNode = <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>(cuddZddGetNode(mgr, idx, first.<a class="code" href="classpolybori_1_1CCuddNavigator.html#0244a90132338327589f7447edadfe56" title="Constant pointer access operator.">getNode</a>(),
<a name="l00566"></a>00566 second.<a class="code" href="classpolybori_1_1CCuddNavigator.html#0244a90132338327589f7447edadfe56" title="Constant pointer access operator.">getNode</a>()));
<a name="l00567"></a>00567 newNode.<a class="code" href="classpolybori_1_1CCuddNavigator.html#ab995a3941060c3745506044c8a91da7" title="Force incrementation of reference count.">incRef</a>();
<a name="l00568"></a>00568 <a class="code" href="namespacepolybori.html#2cd2b80c1a060d8530bf5e38b81081c6">recursive_dec_ref</a>(mgr, first);
<a name="l00569"></a>00569 <a class="code" href="namespacepolybori.html#2cd2b80c1a060d8530bf5e38b81081c6">recursive_dec_ref</a>(mgr, second);
<a name="l00570"></a>00570 }
<a name="l00571"></a>00571
<a name="l00572"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#973524b464a9c18eb5d99706aeb17d79">00572</a> <span class="keywordtype">void</span> newNodeAssign(<a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> idx,
<a name="l00573"></a>00573 <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& thenNode, <span class="keyword">const</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& elseNode)<span class="keyword"> const </span>{
<a name="l00574"></a>00574 <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a> newNode = <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>(cuddZddGetNode(mgr, idx,
<a name="l00575"></a>00575 thenNode.<a class="code" href="classpolybori_1_1CCuddNavigator.html#0244a90132338327589f7447edadfe56" title="Constant pointer access operator.">getNode</a>(),
<a name="l00576"></a>00576 elseNode.<a class="code" href="classpolybori_1_1CCuddNavigator.html#0244a90132338327589f7447edadfe56" title="Constant pointer access operator.">getNode</a>()));
<a name="l00577"></a>00577 newNode.<a class="code" href="classpolybori_1_1CCuddNavigator.html#ab995a3941060c3745506044c8a91da7" title="Force incrementation of reference count.">incRef</a>();
<a name="l00578"></a>00578 <span class="comment">//Cudd_Deref(thenNode); </span>
<a name="l00579"></a>00579 <a class="code" href="namespacepolybori.html#2cd2b80c1a060d8530bf5e38b81081c6">recursive_dec_ref</a>(mgr, thenNode);
<a name="l00580"></a>00580 thenNode = newNode;
<a name="l00581"></a>00581 }
<a name="l00582"></a>00582
<a name="l00583"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#31d3ab3e8b78204f92e42844c6337681">00583</a> <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#31d3ab3e8b78204f92e42844c6337681">multiplesAssign</a>(<a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& node, <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> idx)<span class="keyword"> const </span>{
<a name="l00584"></a>00584 newNodeAssign(idx, node, node);
<a name="l00585"></a>00585 }
<a name="l00586"></a>00586
<a name="l00587"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#7d5ffe1045696cf6db9da9d78393b4bb">00587</a> <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#7d5ffe1045696cf6db9da9d78393b4bb">productAssign</a>(<a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& node, <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> idx)<span class="keyword"> const </span>{
<a name="l00588"></a>00588 <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a> emptyset = <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>(Cudd_ReadZero(mgr));
<a name="l00589"></a>00589 newNodeAssign(idx, node, emptyset);
<a name="l00590"></a>00590 }
<a name="l00591"></a>00591
<a name="l00592"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#cf5b263986b150e78d2313eb60b05d2e">00592</a> <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#cf5b263986b150e78d2313eb60b05d2e">assign</a>(<a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& first, <span class="keyword">const</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& second)<span class="keyword"> const </span>{
<a name="l00593"></a>00593
<a name="l00594"></a>00594 first = second;
<a name="l00595"></a>00595 first.<a class="code" href="classpolybori_1_1CCuddNavigator.html#ab995a3941060c3745506044c8a91da7" title="Force incrementation of reference count.">incRef</a>();
<a name="l00596"></a>00596 }
<a name="l00597"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#f85fa713cc26ee1fdd4e0340bda88420">00597</a> <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#f85fa713cc26ee1fdd4e0340bda88420">replace</a>(<a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& first, <span class="keyword">const</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& second)<span class="keyword"> const </span>{
<a name="l00598"></a>00598 <a class="code" href="namespacepolybori.html#2cd2b80c1a060d8530bf5e38b81081c6">recursive_dec_ref</a>(mgr, first);
<a name="l00599"></a>00599 first = second;
<a name="l00600"></a>00600 }
<a name="l00601"></a>00601
<a name="l00602"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#06fdcba61127648627583c3374f3701c">00602</a> size_type <a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#06fdcba61127648627583c3374f3701c">nSupport</a>(<span class="keyword">const</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& node)<span class="keyword"> const </span>{
<a name="l00603"></a>00603 <span class="keywordflow">return</span> Cudd_SupportSize(mgr, node.<a class="code" href="classpolybori_1_1CCuddNavigator.html#0244a90132338327589f7447edadfe56" title="Constant pointer access operator.">getNode</a>());
<a name="l00604"></a>00604 }
<a name="l00605"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#d2718ca72a09ead5f9ed9abfd34c3c4d">00605</a> size_type <a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#d2718ca72a09ead5f9ed9abfd34c3c4d">length</a>(<span class="keyword">const</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& node)<span class="keyword"> const </span>{
<a name="l00606"></a>00606 <span class="keywordflow">return</span> Cudd_zddCount(mgr, node.<a class="code" href="classpolybori_1_1CCuddNavigator.html#0244a90132338327589f7447edadfe56" title="Constant pointer access operator.">getNode</a>());
<a name="l00607"></a>00607 }
<a name="l00608"></a>00608
<a name="l00609"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#fe3b27fa849443ee92b3f7f15b17c75e">00609</a> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& <a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#fe3b27fa849443ee92b3f7f15b17c75e">newNode</a>(<a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& node)<span class="keyword"> const </span>{
<a name="l00610"></a>00610 node.<a class="code" href="classpolybori_1_1CCuddNavigator.html#ab995a3941060c3745506044c8a91da7" title="Force incrementation of reference count.">incRef</a>();
<a name="l00611"></a>00611 <span class="keywordflow">return</span> node;
<a name="l00612"></a>00612 }
<a name="l00613"></a>00613
<a name="l00614"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#ebbd5bef9b1eb962cc878284fb6d894c">00614</a> <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#ebbd5bef9b1eb962cc878284fb6d894c">kill</a>(<a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>& node)<span class="keyword"> const </span>{
<a name="l00615"></a>00615 <a class="code" href="namespacepolybori.html#2cd2b80c1a060d8530bf5e38b81081c6">recursive_dec_ref</a>(mgr, node);
<a name="l00616"></a>00616 }
<a name="l00617"></a>00617 <span class="keyword">protected</span>:
<a name="l00618"></a><a class="code" href="classpolybori_1_1dd__operations_3_01CTypes_1_1dd__type_1_1navigator_01_4.html#1d08da04f2a9f9e1e453956ee58b7662">00618</a> manager_type mgr;
<a name="l00619"></a>00619 };
<a name="l00620"></a>00620
<a name="l00624"></a>00624 <span class="keyword">template</span> <<span class="keyword">class </span>NaviType, <span class="keyword">class </span>DDType2, <span class="keyword">class </span>ReverseIterator,
<a name="l00625"></a>00625 <span class="keyword">class </span>DDOperations>
<a name="l00626"></a>00626 <span class="comment">//DDType</span>
<a name="l00627"></a>00627 NaviType
<a name="l00628"></a><a class="code" href="namespacepolybori.html#2b040ac0677e9b8a9c4a070cec208cb6">00628</a> <a class="code" href="namespacepolybori.html#f21584c7975eb3bde0a26902776245d9">dd_minimal_elements</a>(NaviType navi,DDType2& multiples,
<a name="l00629"></a>00629 ReverseIterator idxStart, ReverseIterator idxEnd,
<a name="l00630"></a>00630 <span class="keyword">const</span> DDOperations& apply) {
<a name="l00631"></a>00631
<a name="l00632"></a>00632
<a name="l00633"></a>00633
<a name="l00634"></a>00634 <span class="keywordflow">if</span> (!navi.isConstant()) { <span class="comment">// Not at end of path</span>
<a name="l00635"></a>00635
<a name="l00636"></a>00636 <span class="keywordtype">int</span> nlen = apply.length(navi);
<a name="l00637"></a>00637
<a name="l00638"></a>00638 <span class="keywordflow">if</span>(<span class="keyword">false</span>&&(nlen == 2)) {
<a name="l00639"></a>00639
<a name="l00640"></a>00640 <span class="comment">// std::cerr << "hier"<<std::endl;</span>
<a name="l00641"></a>00641 navi = <a class="code" href="namespacepolybori.html#cbdb4b217bcd090cafbb697ff07ba44a">minimal_of_two_terms</a>(navi, multiples,idxStart, idxEnd, apply);
<a name="l00642"></a>00642
<a name="l00643"></a>00643 <span class="comment">// std::cerr << "danach"<<std::endl;</span>
<a name="l00644"></a>00644 <span class="keywordflow">return</span> navi;
<a name="l00645"></a>00645
<a name="l00646"></a>00646 <span class="preprocessor">#if 0</span>
<a name="l00647"></a>00647 <span class="preprocessor"></span> multiples = navi;
<a name="l00648"></a>00648
<a name="l00649"></a>00649
<a name="l00650"></a>00650 std::vector<int> indices (apply.nSupport(navi));
<a name="l00651"></a>00651 std::vector<int>::iterator iter(indices.begin()), iend(indices.end());
<a name="l00652"></a>00652 <span class="keywordtype">bool</span> is_reducible = <span class="keyword">true</span>;
<a name="l00653"></a>00653 <span class="keywordtype">bool</span> reducible_tested = <span class="keyword">false</span>;
<a name="l00654"></a>00654
<a name="l00655"></a>00655 <span class="keywordtype">int</span> used = 0;
<a name="l00656"></a>00656 NaviType thenBr;
<a name="l00657"></a>00657 NaviType elseBr;
<a name="l00658"></a>00658 <span class="keywordflow">while</span>( is_reducible&&(!multiples.isConstant())) {
<a name="l00659"></a>00659 *iter = *multiples;
<a name="l00660"></a>00660 used++;
<a name="l00661"></a>00661
<a name="l00662"></a>00662 thenBr = multiples.thenBranch();
<a name="l00663"></a>00663 elseBr = multiples.elseBranch();
<a name="l00664"></a>00664
<a name="l00665"></a>00665 <span class="keywordflow">if</span>((elseBr.isConstant() && elseBr.terminalValue())) {
<a name="l00666"></a>00666 --iter;
<a name="l00667"></a>00667 --used;
<a name="l00668"></a>00668 multiples = elseBr;
<a name="l00669"></a>00669 }
<a name="l00670"></a>00670 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (elseBr.isConstant() && !elseBr.terminalValue())
<a name="l00671"></a>00671 multiples = thenBr;
<a name="l00672"></a>00672 <span class="keywordflow">else</span> {
<a name="l00673"></a>00673 <span class="keywordflow">if</span> (!reducible_tested){
<a name="l00674"></a>00674 reducible_tested == <span class="keyword">true</span>;
<a name="l00675"></a>00675 is_reducible = <a class="code" href="namespacepolybori.html#642441efa10dc73fe2ca9e6250b86fc8">is_reducible_by</a>(thenBr, elseBr);
<a name="l00676"></a>00676 }
<a name="l00677"></a>00677 <span class="keywordflow">if</span>(is_reducible){
<a name="l00678"></a>00678 --iter;
<a name="l00679"></a>00679 --used;
<a name="l00680"></a>00680 }
<a name="l00681"></a>00681
<a name="l00682"></a>00682 multiples = elseBr;
<a name="l00683"></a>00683 }
<a name="l00684"></a>00684
<a name="l00685"></a>00685
<a name="l00686"></a>00686 ++iter;
<a name="l00687"></a>00687
<a name="l00688"></a>00688 }
<a name="l00689"></a>00689
<a name="l00690"></a>00690
<a name="l00691"></a>00691
<a name="l00692"></a>00692 indices.resize(used);
<a name="l00693"></a>00693
<a name="l00694"></a>00694 <span class="keywordflow">if</span> (is_reducible) {
<a name="l00695"></a>00695
<a name="l00696"></a>00696 std::vector<int>::const_reverse_iterator start(indices.rbegin()),
<a name="l00697"></a>00697 finish(indices.rend());
<a name="l00698"></a>00698
<a name="l00699"></a>00699 <span class="comment">// int nmax = dd.nVariables();</span>
<a name="l00700"></a>00700
<a name="l00701"></a>00701 <a class="code" href="namespacepolybori.html#4d98e6d55edb29688b0d24fae3a349b9">inc_ref</a>(multiples);
<a name="l00702"></a>00702
<a name="l00703"></a>00703
<a name="l00704"></a>00704 NaviType tmp,tmpnavi;
<a name="l00705"></a>00705
<a name="l00706"></a>00706 apply.assign(tmpnavi, multiples);
<a name="l00707"></a>00707
<a name="l00708"></a>00708 ReverseIterator idxIter = idxStart;
<a name="l00709"></a>00709 <span class="keywordflow">while</span>(start != finish){
<a name="l00710"></a>00710
<a name="l00711"></a>00711 <span class="keywordflow">while</span>((idxIter != idxEnd) && (*idxIter > *start) ) {
<a name="l00712"></a>00712
<a name="l00713"></a>00713 apply.multiplesAssign(multiples, *idxIter);
<a name="l00714"></a>00714 ++idxIter;
<a name="l00715"></a>00715 }
<a name="l00716"></a>00716 apply.productAssign(multiples, *start);
<a name="l00717"></a>00717 apply.productAssign(tmpnavi, *start);
<a name="l00718"></a>00718 <span class="keywordflow">if</span>(idxIter != idxEnd)
<a name="l00719"></a>00719 ++idxIter;
<a name="l00720"></a>00720 ++start;
<a name="l00721"></a>00721 }
<a name="l00722"></a>00722
<a name="l00723"></a>00723 navi = tmpnavi;
<a name="l00724"></a>00724 <span class="keywordflow">return</span> navi;
<a name="l00725"></a>00725 }
<a name="l00726"></a>00726 <span class="comment">// else { // Subcase: two proper terms</span>
<a name="l00727"></a>00727
<a name="l00728"></a>00728 <span class="comment">// thenBr = indexed_term_multiples(thenBr, idxStart, idxEnd, apply);</span>
<a name="l00729"></a>00729 <span class="comment">// elseBr = indexed_term_multiples(elseBr, idxStart, idxEnd, apply);</span>
<a name="l00730"></a>00730
<a name="l00731"></a>00731 <span class="comment">// }</span>
<a name="l00732"></a>00732 <span class="preprocessor">#endif</span>
<a name="l00733"></a>00733 <span class="preprocessor"></span> }
<a name="l00734"></a>00734
<a name="l00735"></a>00735
<a name="l00736"></a>00736
<a name="l00737"></a>00737 <span class="keywordflow">if</span>(nlen == 1) { <span class="comment">// Special case of only one term</span>
<a name="l00738"></a>00738 <span class="comment">// Cudd_Ref(navi);</span>
<a name="l00739"></a>00739 multiples = <a class="code" href="namespacepolybori.html#85cef6454769d8c9ae1e235782e4b8be">indexed_term_multiples</a>(navi, idxStart, idxEnd, apply);
<a name="l00740"></a>00740 <span class="keywordflow">return</span> apply.newNode(navi);
<a name="l00741"></a>00741 }
<a name="l00742"></a>00742
<a name="l00743"></a>00743
<a name="l00744"></a>00744 <span class="comment">// treat else branch</span>
<a name="l00745"></a>00745 NaviType elseMult;
<a name="l00746"></a>00746 NaviType elsedd = <a class="code" href="namespacepolybori.html#f21584c7975eb3bde0a26902776245d9">dd_minimal_elements</a>(navi.elseBranch(),
<a name="l00747"></a>00747 elseMult, idxStart, idxEnd, apply);
<a name="l00748"></a>00748 elseMult = <a class="code" href="namespacepolybori.html#ab0655446e6aaf46050e2d4e143588d6">prepend_multiples_wrt_indices</a>(elseMult, *navi,
<a name="l00749"></a>00749 idxStart, idxEnd, apply);
<a name="l00750"></a>00750
<a name="l00751"></a>00751 <span class="comment">// short cut for obvious inclusion</span>
<a name="l00752"></a>00752 <span class="keywordflow">if</span>( (navi.elseBranch() == navi.thenBranch()) ||
<a name="l00753"></a>00753 (elsedd.isConstant() && elsedd.terminalValue()) ){
<a name="l00754"></a>00754 multiples = elseMult;
<a name="l00755"></a>00755 <span class="keywordflow">return</span> elsedd;
<a name="l00756"></a>00756 }
<a name="l00757"></a>00757
<a name="l00758"></a>00758 <span class="comment">// remove already treated branches</span>
<a name="l00759"></a>00759 NaviType thenNavi(apply.diff(navi.thenBranch(), elseMult));
<a name="l00760"></a>00760
<a name="l00761"></a>00761 <span class="comment">// treat remaining parts of then branch</span>
<a name="l00762"></a>00762 NaviType thenMult;
<a name="l00763"></a>00763 apply.replace(thenNavi, <a class="code" href="namespacepolybori.html#f21584c7975eb3bde0a26902776245d9">dd_minimal_elements</a>(thenNavi, thenMult,
<a name="l00764"></a>00764 idxStart, idxEnd, apply));
<a name="l00765"></a>00765 thenMult = <a class="code" href="namespacepolybori.html#ab0655446e6aaf46050e2d4e143588d6">prepend_multiples_wrt_indices</a>(thenMult, *navi,
<a name="l00766"></a>00766 idxStart, idxEnd, apply);
<a name="l00767"></a>00767
<a name="l00768"></a>00768 <span class="comment">// generate node consisting of all multiples</span>
<a name="l00769"></a>00769 apply.uniteAssign(thenMult, elseMult);
<a name="l00770"></a>00770 apply.replacingNode(multiples, *navi, thenMult, elseMult);
<a name="l00771"></a>00771
<a name="l00772"></a>00772 <span class="comment">// generate result from minimal elements of then and else brach</span>
<a name="l00773"></a>00773 NaviType result;
<a name="l00774"></a>00774 apply.replacingNode(result, *navi, thenNavi, elsedd);
<a name="l00775"></a>00775
<a name="l00776"></a>00776 <span class="keywordflow">return</span> result;
<a name="l00777"></a>00777
<a name="l00778"></a>00778 }
<a name="l00779"></a>00779
<a name="l00780"></a>00780 apply.assign(multiples, navi);
<a name="l00781"></a>00781
<a name="l00782"></a>00782 <span class="keywordflow">return</span> apply.newNode(navi);
<a name="l00783"></a>00783 }
<a name="l00784"></a>00784
<a name="l00785"></a>00785 <a class="code" href="pbori__defs_8h.html#faf094fde6c1a7f1aad18bcb455f3b06" title="Finish project&#39;s namespace.">END_NAMESPACE_PBORI</a>
<a name="l00786"></a>00786
<a name="l00787"></a>00787 <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
>
806
