<!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: CDDInterface.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>CDDInterface.h</h1><a href="CDDInterface_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="l00220"></a>00220 <span class="comment"></span><span class="comment">//*****************************************************************************</span>
<a name="l00221"></a>00221
<a name="l00222"></a>00222 <span class="preprocessor">#ifndef CDDInterface_h_</span>
<a name="l00223"></a>00223 <span class="preprocessor"></span><span class="preprocessor">#define CDDInterface_h_</span>
<a name="l00224"></a>00224 <span class="preprocessor"></span>
<a name="l00225"></a>00225 <span class="preprocessor">#include "<a class="code" href="extrafwd_8h.html">extrafwd.h</a>"</span>
<a name="l00226"></a>00226 <span class="comment">// load basic definitions</span>
<a name="l00227"></a>00227 <span class="preprocessor">#include "<a class="code" href="pbori__defs_8h.html">pbori_defs.h</a>"</span>
<a name="l00228"></a>00228
<a name="l00229"></a>00229
<a name="l00230"></a>00230
<a name="l00231"></a>00231 <span class="comment">// Getting iterator type for navigating through Cudd's ZDDs structure</span>
<a name="l00232"></a>00232 <span class="preprocessor">#include "<a class="code" href="CCuddNavigator_8h.html">CCuddNavigator.h</a>"</span>
<a name="l00233"></a>00233
<a name="l00234"></a>00234 <span class="comment">// Getting iterator type for retrieving first term from Cudd's ZDDs</span>
<a name="l00235"></a>00235 <span class="preprocessor">#include "<a class="code" href="CCuddFirstIter_8h.html">CCuddFirstIter.h</a>"</span>
<a name="l00236"></a>00236
<a name="l00237"></a>00237 <span class="comment">// Getting iterator type for retrieving last term from Cudd's ZDDs</span>
<a name="l00238"></a>00238 <span class="preprocessor">#include "<a class="code" href="CCuddLastIter_8h.html">CCuddLastIter.h</a>"</span>
<a name="l00239"></a>00239
<a name="l00240"></a>00240 <span class="comment">// Getting functional for generating new Cudd's ZDD nodes</span>
<a name="l00241"></a>00241 <span class="preprocessor">#include "<a class="code" href="CCuddGetNode_8h.html">CCuddGetNode.h</a>"</span>
<a name="l00242"></a>00242
<a name="l00243"></a>00243 <span class="comment">// Getting output iterator functionality</span>
<a name="l00244"></a>00244 <span class="preprocessor">#include "<a class="code" href="PBoRiOutIter_8h.html">PBoRiOutIter.h</a>"</span>
<a name="l00245"></a>00245
<a name="l00246"></a>00246 <span class="comment">// Getting error coe functionality</span>
<a name="l00247"></a>00247 <span class="preprocessor">#include "<a class="code" href="PBoRiGenericError_8h.html">PBoRiGenericError.h</a>"</span>
<a name="l00248"></a>00248
<a name="l00249"></a>00249 <span class="comment">// Cudd's internal definitions</span>
<a name="l00250"></a>00250 <span class="preprocessor">#include "cuddInt.h"</span>
<a name="l00251"></a>00251
<a name="l00252"></a>00252 <span class="preprocessor">#include "<a class="code" href="pbori__algo_8h.html">pbori_algo.h</a>"</span>
<a name="l00253"></a>00253
<a name="l00254"></a>00254 <span class="preprocessor">#include "<a class="code" href="pbori__tags_8h.html">pbori_tags.h</a>"</span>
<a name="l00255"></a>00255 <span class="preprocessor">#include "<a class="code" href="pbori__routines__hash_8h.html">pbori_routines_hash.h</a>"</span>
<a name="l00256"></a>00256
<a name="l00257"></a>00257 <span class="comment">// Using stl's vector</span>
<a name="l00258"></a>00258 <span class="preprocessor">#include <vector></span>
<a name="l00259"></a>00259 <span class="preprocessor">#include <numeric></span>
<a name="l00260"></a>00260
<a name="l00261"></a>00261 <span class="preprocessor">#include "<a class="code" href="CCuddInterface_8h.html">CCuddInterface.h</a>"</span>
<a name="l00262"></a>00262 <span class="preprocessor">#include "<a class="code" href="pbori__traits_8h.html">pbori_traits.h</a>"</span>
<a name="l00263"></a>00263
<a name="l00264"></a>00264 <a class="code" href="pbori__defs_8h.html#6ae360a591580558f31b6157ee792a10" title="Start project&#39;s namespace.">BEGIN_NAMESPACE_PBORI</a>
<a name="l00265"></a>00265
<a name="l00266"></a>00266
<a name="l00267"></a>00267 <span class="keyword">inline</span> Cudd*
<a name="l00268"></a><a class="code" href="namespacepolybori.html#383fd66e3fa464a887facf198284030d">00268</a> <a class="code" href="namespacepolybori.html#383fd66e3fa464a887facf198284030d">extract_manager</a>(<span class="keyword">const</span> Cudd& mgr) {
<a name="l00269"></a>00269 <span class="keywordflow">return</span> &<span class="keyword">const_cast<</span>Cudd&<span class="keyword">></span>(mgr);
<a name="l00270"></a>00270 }
<a name="l00271"></a>00271
<a name="l00272"></a>00272 <span class="keyword">inline</span> CCuddInterface::mgrcore_ptr
<a name="l00273"></a><a class="code" href="namespacepolybori.html#d76a66ba19b2d62f3cc1502ecba0db90">00273</a> <a class="code" href="namespacepolybori.html#383fd66e3fa464a887facf198284030d">extract_manager</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="l00274"></a>00274 <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="l00275"></a>00275 }
<a name="l00276"></a>00276
<a name="l00277"></a>00277 <span class="keyword">template</span> <<span class="keyword">class</span> MgrType>
<a name="l00278"></a>00278 <span class="keyword">inline</span> <span class="keyword">const</span> MgrType&
<a name="l00279"></a><a class="code" href="namespacepolybori.html#370ec3934514854e817d3fc25b94cc7c">00279</a> <a class="code" href="namespacepolybori.html#383fd66e3fa464a887facf198284030d">extract_manager</a>(<span class="keyword">const</span> MgrType& mgr) {
<a name="l00280"></a>00280 <span class="keywordflow">return</span> mgr;
<a name="l00281"></a>00281 }
<a name="l00282"></a>00282
<a name="l00283"></a>00283 <span class="keyword">inline</span> Cudd&
<a name="l00284"></a><a class="code" href="namespacepolybori.html#a8924f3c16bad2c0c02e5fc9048717f6">00284</a> <a class="code" href="namespacepolybori.html#a8924f3c16bad2c0c02e5fc9048717f6">get_manager</a>(Cudd* mgr) {
<a name="l00285"></a>00285 <span class="keywordflow">return</span> *mgr;
<a name="l00286"></a>00286 }
<a name="l00287"></a>00287
<a name="l00288"></a>00288 <span class="keyword">template</span> <<span class="keyword">class</span> MgrType>
<a name="l00289"></a>00289 <span class="keyword">inline</span> <span class="keyword">const</span> MgrType&
<a name="l00290"></a><a class="code" href="namespacepolybori.html#ef13ebcd1a58d0da6a72f7bbe82b71a3">00290</a> <a class="code" href="namespacepolybori.html#a8924f3c16bad2c0c02e5fc9048717f6">get_manager</a>(<span class="keyword">const</span> MgrType& mgr) {
<a name="l00291"></a>00291 <span class="keywordflow">return</span> mgr;
<a name="l00292"></a>00292 }
<a name="l00300"></a>00300 <span class="keyword">template</span><<span class="keyword">class</span> DDType>
<a name="l00301"></a><a class="code" href="classpolybori_1_1CDDInterfaceBase.html">00301</a> <span class="keyword">class </span><a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">CDDInterfaceBase</a> {
<a name="l00302"></a>00302
<a name="l00303"></a>00303 <span class="keyword">public</span>:
<a name="l00304"></a>00304
<a name="l00306"></a><a class="code" href="classpolybori_1_1CDDInterfaceBase.html#3a6affc8f40899b5e9db4bdb5e90767b">00306</a> <span class="keyword">typedef</span> DDType interfaced_type;
<a name="l00307"></a>00307
<a name="l00309"></a><a class="code" href="classpolybori_1_1CDDInterfaceBase.html#5143706233c92624d9f6ac6413fc5d46">00309</a> <span class="keyword">typedef</span> <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">CDDInterfaceBase<interfaced_type></a> <span class="keyword">self</span>;
<a name="l00310"></a>00310
<a name="l00312"></a><a class="code" href="classpolybori_1_1CDDInterfaceBase.html#3bb4019e5d0afd01531df79b81ec385b">00312</a> <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">CDDInterfaceBase</a>() :
<a name="l00313"></a>00313 m_interfaced() {}
<a name="l00314"></a>00314
<a name="l00316"></a><a class="code" href="classpolybori_1_1CDDInterfaceBase.html#5ab4416394b77ed103ede6b4d472441c">00316</a> <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">CDDInterfaceBase</a>(<span class="keyword">const</span> interfaced_type& interfaced) :
<a name="l00317"></a>00317 m_interfaced(interfaced) {}
<a name="l00318"></a>00318
<a name="l00320"></a><a class="code" href="classpolybori_1_1CDDInterfaceBase.html#5bc1a37d7cd8d19ae4f78dbfdb049a57">00320</a> <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">CDDInterfaceBase</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs) :
<a name="l00321"></a>00321 m_interfaced(rhs.m_interfaced) {}
<a name="l00322"></a>00322
<a name="l00324"></a><a class="code" href="classpolybori_1_1CDDInterfaceBase.html#f620a68ad264f9eeb92e8a0c60ffcda1">00324</a> <a class="code" href="classpolybori_1_1CDDInterfaceBase.html#f620a68ad264f9eeb92e8a0c60ffcda1" title="Destructor.">~CDDInterfaceBase</a>() {}
<a name="l00325"></a>00325
<a name="l00327"></a><a class="code" href="classpolybori_1_1CDDInterfaceBase.html#19a26ad8e92dc96c16de0f22097b8fe2">00327</a> operator const interfaced_type&()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> m_interfaced; }
<a name="l00328"></a>00328
<a name="l00329"></a>00329 <span class="keyword">protected</span>:
<a name="l00330"></a><a class="code" href="classpolybori_1_1CDDInterfaceBase.html#14f2443eb33566a0295c95575cf66ffb">00330</a> interfaced_type m_interfaced;
<a name="l00331"></a>00331 };
<a name="l00332"></a>00332
<a name="l00335"></a>00335 <span class="keyword">template</span><<span class="keyword">class</span> CuddLikeZDD>
<a name="l00336"></a><a class="code" href="classpolybori_1_1CDDInterface.html">00336</a> <span class="keyword">class </span><a class="code" href="classpolybori_1_1CDDInterface.html">CDDInterface</a>:
<a name="l00337"></a>00337 <span class="keyword">public</span> <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">CDDInterfaceBase</a><CuddLikeZDD> {
<a name="l00338"></a>00338 <span class="keyword">public</span>:
<a name="l00339"></a>00339
<a name="l00341"></a><a class="code" href="classpolybori_1_1CDDInterface.html#581c47be759552f70d15a029a8a680eb">00341</a> <span class="keyword">typedef</span> CuddLikeZDD interfaced_type;
<a name="l00342"></a>00342
<a name="l00344"></a><a class="code" href="classpolybori_1_1CDDInterface.html#4e4c86152f9a10374e963b2d86a3be07">00344</a> <span class="keyword">typedef</span> <span class="keyword">typename</span> zdd_traits<interfaced_type>::manager_base manager_base;
<a name="l00345"></a>00345
<a name="l00347"></a><a class="code" href="classpolybori_1_1CDDInterface.html#1c9678fad8a854ddfc0a8a0a072c45ae">00347</a> <span class="keyword">typedef</span> <span class="keyword">typename</span> <a class="code" href="structpolybori_1_1manager__traits.html">manager_traits<manager_base>::tmp_ref</a> mgr_ref;
<a name="l00348"></a>00348
<a name="l00350"></a><a class="code" href="classpolybori_1_1CDDInterface.html#f04a1aa611802efb65282d2ad405c45b">00350</a> <span class="keyword">typedef</span> <span class="keyword">typename</span> <a class="code" href="structpolybori_1_1manager__traits.html">manager_traits<manager_base>::core_type</a> core_type;
<a name="l00351"></a>00351
<a name="l00353"></a><a class="code" href="classpolybori_1_1CDDInterface.html#1e8c2de7230560be3790d79a56f8c1cc">00353</a> <span class="keyword">typedef</span> <a class="code" href="classpolybori_1_1CDDManager_3_01CCuddInterface_01_4.html">CDDManager<CCuddInterface></a> <a class="code" href="classpolybori_1_1CDDManager_3_01CCuddInterface_01_4.html">manager_type</a>;
<a name="l00354"></a>00354
<a name="l00356"></a><a class="code" href="classpolybori_1_1CDDInterface.html#53b2bc361a08dfb9e74c5bfac213fd8a">00356</a> <span class="keyword">typedef</span> <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">CDDInterfaceBase<interfaced_type></a> <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">base_type</a>;
<a name="l00357"></a><a class="code" href="classpolybori_1_1CDDInterface.html#2d1a043a28136d98a53e329339402143">00357</a> <span class="keyword">typedef</span> <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">base_type</a> <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">base</a>;
<a name="l00358"></a>00358 <span class="keyword">using</span> base::m_interfaced;
<a name="l00359"></a>00359
<a name="l00361"></a><a class="code" href="classpolybori_1_1CDDInterface.html#23e68104e0e176953fa85b401674582b">00361</a> <span class="keyword">typedef</span> <a class="code" href="classpolybori_1_1CDDInterface.html">CDDInterface<interfaced_type></a> <span class="keyword">self</span>;
<a name="l00362"></a>00362
<a name="l00364"></a><a class="code" href="classpolybori_1_1CDDInterface.html#3c5302a498f41b02a778f65c720c3441">00364</a> <span class="keyword">typedef</span> CTypes::size_type size_type;
<a name="l00365"></a>00365
<a name="l00367"></a><a class="code" href="classpolybori_1_1CDDInterface.html#a0c138660bde4b5b935243c2bfd8c6aa">00367</a> <span class="keyword">typedef</span> <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">CTypes::idx_type</a> <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a>;
<a name="l00368"></a>00368
<a name="l00370"></a><a class="code" href="classpolybori_1_1CDDInterface.html#9b21d36a78a7e9cb12486a4a0ae1c1c0">00370</a> <span class="keyword">typedef</span> CTypes::ostream_type ostream_type;
<a name="l00371"></a>00371
<a name="l00373"></a><a class="code" href="classpolybori_1_1CDDInterface.html#0e3bacf8cde66c20f7b9b3094c928fea">00373</a> <span class="keyword">typedef</span> CTypes::bool_type bool_type;
<a name="l00374"></a>00374
<a name="l00376"></a><a class="code" href="classpolybori_1_1CDDInterface.html#ebd02aee609d3195f736e1b0b1de6c86">00376</a> <span class="keyword">typedef</span> CTypes::hash_type hash_type;
<a name="l00377"></a>00377
<a name="l00379"></a><a class="code" href="classpolybori_1_1CDDInterface.html#60ef5f70cb4b40242442c6d224778065">00379</a> <span class="keyword">typedef</span> <a class="code" href="classpolybori_1_1CCuddFirstIter.html" title="This class defines an iterator over the first minimal term of a given ZDD node.">CCuddFirstIter</a> <a class="code" href="classpolybori_1_1CCuddFirstIter.html" title="This class defines an iterator over the first minimal term of a given ZDD node.">first_iterator</a>;
<a name="l00380"></a>00380
<a name="l00382"></a><a class="code" href="classpolybori_1_1CDDInterface.html#7c1dde2debf409f4836bf55ab32b50e4">00382</a> <span class="keyword">typedef</span> <a class="code" href="classpolybori_1_1CCuddLastIter.html" title="This class defines an iterator over the last minimal term of a given ZDD node.">CCuddLastIter</a> <a class="code" href="classpolybori_1_1CCuddLastIter.html" title="This class defines an iterator over the last minimal term of a given ZDD node.">last_iterator</a>;
<a name="l00383"></a>00383
<a name="l00385"></a><a class="code" href="classpolybori_1_1CDDInterface.html#2728afd1f0dbf503a94915b79f4502bf">00385</a> <span class="keyword">typedef</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">CCuddNavigator</a> <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="l00386"></a>00386
<a name="l00388"></a><a class="code" href="classpolybori_1_1CDDInterface.html#f8429917ee2c4fe2e1430d29b54da631">00388</a> <span class="keyword">typedef</span> FILE* pretty_out_type;
<a name="l00389"></a>00389
<a name="l00391"></a><a class="code" href="classpolybori_1_1CDDInterface.html#6da7252e8579b44c832b6d1c343063ae">00391</a> <span class="keyword">typedef</span> <span class="keyword">const</span> <span class="keywordtype">char</span>* filename_type;
<a name="l00392"></a>00392
<a name="l00394"></a><a class="code" href="classpolybori_1_1CDDInterface.html#db2dc64a5d34769db45898acb35216eb">00394</a> <span class="keyword">typedef</span> <a class="code" href="structpolybori_1_1valid__tag.html" title="This class shows, whether a property of an order is valid.">valid_tag</a> <a class="code" href="structpolybori_1_1valid__tag.html" title="This class shows, whether a property of an order is valid.">easy_equality_property</a>;
<a name="l00395"></a>00395
<a name="l00397"></a><a class="code" href="classpolybori_1_1CDDInterface.html#354a3712b7b5a1dedf62e06305f68c5f">00397</a> <a class="code" href="classpolybori_1_1CDDInterface.html#354a3712b7b5a1dedf62e06305f68c5f" title="Default constructor.">CDDInterface</a>(): <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">base_type</a>() {}
<a name="l00398"></a>00398
<a name="l00400"></a><a class="code" href="classpolybori_1_1CDDInterface.html#60115341bdca29943aa76a48c008cb9c">00400</a> <a class="code" href="classpolybori_1_1CDDInterface.html#60115341bdca29943aa76a48c008cb9c" title="Copy constructor.">CDDInterface</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs): <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">base_type</a>(rhs) {}
<a name="l00401"></a>00401
<a name="l00403"></a><a class="code" href="classpolybori_1_1CDDInterface.html#de06225812d49717b61c7aad1677a67b">00403</a> <a class="code" href="classpolybori_1_1CDDInterface.html#de06225812d49717b61c7aad1677a67b" title="Construct from interfaced type.">CDDInterface</a>(<span class="keyword">const</span> interfaced_type& rhs): <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">base_type</a>(rhs) {}
<a name="l00404"></a>00404
<a name="l00406"></a><a class="code" href="classpolybori_1_1CDDInterface.html#339df63fbb684e88c2e96e53eac1de73">00406</a> <a class="code" href="classpolybori_1_1CDDInterface.html">CDDInterface</a>(<span class="keyword">const</span> manager_base& mgr, <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>& navi):
<a name="l00407"></a>00407 <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">base_type</a>(<a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">self</a>::newDiagram(mgr, navi)) {}
<a name="l00408"></a>00408
<a name="l00410"></a><a class="code" href="classpolybori_1_1CDDInterface.html#c1ca0fbb65d676d11ca17be36ac43c28">00410</a> <a class="code" href="classpolybori_1_1CDDInterface.html">CDDInterface</a>(<span class="keyword">const</span> manager_base& mgr,
<a name="l00411"></a>00411 <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> idx, <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> thenNavi, <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> elseNavi):
<a name="l00412"></a>00412 <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">base_type</a>( <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">self</a>::newNodeDiagram(mgr, idx, thenNavi, elseNavi) ) {
<a name="l00413"></a>00413 }
<a name="l00414"></a>00414
<a name="l00417"></a><a class="code" href="classpolybori_1_1CDDInterface.html#3b9f5a3be7d0b35ec2d4bcb3bde5a7d3">00417</a> <a class="code" href="classpolybori_1_1CDDInterface.html">CDDInterface</a>(<span class="keyword">const</span> manager_base& mgr,
<a name="l00418"></a>00418 <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> idx, <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> navi):
<a name="l00419"></a>00419 <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">base_type</a>( <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">self</a>::newNodeDiagram(mgr, idx, navi, navi) ) {
<a name="l00420"></a>00420 }
<a name="l00421"></a>00421
<a name="l00423"></a><a class="code" href="classpolybori_1_1CDDInterface.html#2f217b9da073c38f75d7cd5eedfbe107">00423</a> <a class="code" href="classpolybori_1_1CDDInterface.html">CDDInterface</a>(<a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> idx, <span class="keyword">const</span> <span class="keyword">self</span>& thenDD, <span class="keyword">const</span> <span class="keyword">self</span>& elseDD):
<a name="l00424"></a>00424 <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">base_type</a>( <a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">self</a>::newNodeDiagram(thenDD.manager(), idx,
<a name="l00425"></a>00425 thenDD.navigation(),
<a name="l00426"></a>00426 elseDD.navigation()) ) {
<a name="l00427"></a>00427 }
<a name="l00428"></a>00428
<a name="l00430"></a><a class="code" href="classpolybori_1_1CDDInterface.html#98a94fecbdcdaa23f156124686685483">00430</a> <a class="code" href="classpolybori_1_1CDDInterface.html#98a94fecbdcdaa23f156124686685483" title="Destructor.">~CDDInterface</a>() {}
<a name="l00431"></a>00431
<a name="l00433"></a><a class="code" href="classpolybori_1_1CDDInterface.html#db6548a66c3999d86dcadf0009836b03">00433</a> hash_type <a class="code" href="classpolybori_1_1CDDInterface.html#db6548a66c3999d86dcadf0009836b03" title="Get unique hash value (valid only per runtime).">hash</a>()<span class="keyword"> const </span>{
<a name="l00434"></a>00434 <span class="keywordflow">return</span> <span class="keyword">static_cast<</span>hash_type<span class="keyword">></span>(<span class="keyword">reinterpret_cast<</span>std::ptrdiff_t<span class="keyword">></span>(m_interfaced
<a name="l00435"></a>00435 .getNode()));
<a name="l00436"></a>00436 }
<a name="l00437"></a>00437
<a name="l00439"></a><a class="code" href="classpolybori_1_1CDDInterface.html#02bea25795fd5fd691eeea688e0b86d1">00439</a> hash_type <a class="code" href="classpolybori_1_1CDDInterface.html#02bea25795fd5fd691eeea688e0b86d1" title="Get stable hash value, which is reproducible.">stableHash</a>()<span class="keyword"> const </span>{
<a name="l00440"></a>00440 <span class="keywordflow">return</span> <a class="code" href="namespacepolybori.html#f3ca38c9ee70d41e5c065fbaa14d903d">stable_hash_range</a>(navigation());
<a name="l00441"></a>00441 }
<a name="l00442"></a>00442
<a name="l00444"></a><a class="code" href="classpolybori_1_1CDDInterface.html#c2d7c3cab926aa4d332f52610b194f5a">00444</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#c2d7c3cab926aa4d332f52610b194f5a" title="Set union.">unite</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{
<a name="l00445"></a>00445 <span class="keywordflow">return</span> <span class="keyword">self</span>(<a class="code" href="classpolybori_1_1CDDInterfaceBase.html" title="This is the common base for the specialized template class CDDInterface.">base_type</a>(m_interfaced.Union(rhs.m_interfaced)));
<a name="l00446"></a>00446 };
<a name="l00447"></a>00447
<a name="l00449"></a><a class="code" href="classpolybori_1_1CDDInterface.html#9790974bdc39f5abaa46e3882876ab7b">00449</a> <span class="keyword">self</span>& <a class="code" href="classpolybori_1_1CDDInterface.html#9790974bdc39f5abaa46e3882876ab7b" title="Set union with assignment.">uniteAssign</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs) {
<a name="l00450"></a>00450 m_interfaced = m_interfaced.Union(rhs.m_interfaced);
<a name="l00451"></a>00451 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00452"></a>00452 };
<a name="l00454"></a><a class="code" href="classpolybori_1_1CDDInterface.html#c602d283181aac6dd85a16dcf0d45d15">00454</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#c602d283181aac6dd85a16dcf0d45d15" title="If-Then-Else operation.">ite</a>(<span class="keyword">const</span> <span class="keyword">self</span>& then_dd, <span class="keyword">const</span> <span class="keyword">self</span>& else_dd)<span class="keyword"> const </span>{
<a name="l00455"></a>00455 <span class="keywordflow">return</span> <span class="keyword">self</span>(m_interfaced.Ite(then_dd, else_dd));
<a name="l00456"></a>00456 };
<a name="l00457"></a>00457
<a name="l00459"></a><a class="code" href="classpolybori_1_1CDDInterface.html#ec13c049c043d3c352d94c9133c045fd">00459</a> <span class="keyword">self</span>& <a class="code" href="classpolybori_1_1CDDInterface.html#ec13c049c043d3c352d94c9133c045fd" title="If-Then-Else operation with assignment.">iteAssign</a>(<span class="keyword">const</span> <span class="keyword">self</span>& then_dd, <span class="keyword">const</span> <span class="keyword">self</span>& else_dd) {
<a name="l00460"></a>00460 m_interfaced = m_interfaced.Ite(then_dd, else_dd);
<a name="l00461"></a>00461 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00462"></a>00462 };
<a name="l00463"></a>00463
<a name="l00465"></a><a class="code" href="classpolybori_1_1CDDInterface.html#952b93666cbf3de6a97d2b69b829976b">00465</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#952b93666cbf3de6a97d2b69b829976b" title="Set difference.">diff</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{
<a name="l00466"></a>00466 <span class="keywordflow">return</span> m_interfaced.Diff(rhs.m_interfaced);
<a name="l00467"></a>00467 };
<a name="l00468"></a>00468
<a name="l00470"></a><a class="code" href="classpolybori_1_1CDDInterface.html#516c040ff1856555dc542027374890cd">00470</a> <span class="keyword">self</span>& <a class="code" href="classpolybori_1_1CDDInterface.html#516c040ff1856555dc542027374890cd" title="Set difference with assignment.">diffAssign</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs) {
<a name="l00471"></a>00471 m_interfaced = m_interfaced.Diff(rhs.m_interfaced);
<a name="l00472"></a>00472 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00473"></a>00473 };
<a name="l00474"></a>00474
<a name="l00476"></a><a class="code" href="classpolybori_1_1CDDInterface.html#f18fc26811026e902132504fadbbedba">00476</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#f18fc26811026e902132504fadbbedba" title="Set difference.">diffConst</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{
<a name="l00477"></a>00477 <span class="keywordflow">return</span> m_interfaced.DiffConst(rhs.m_interfaced);
<a name="l00478"></a>00478 };
<a name="l00479"></a>00479
<a name="l00481"></a><a class="code" href="classpolybori_1_1CDDInterface.html#652fde32f9304bfdc00c972d215177fb">00481</a> <span class="keyword">self</span>& <a class="code" href="classpolybori_1_1CDDInterface.html#652fde32f9304bfdc00c972d215177fb" title="Set difference with assignment.">diffConstAssign</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs) {
<a name="l00482"></a>00482 m_interfaced = m_interfaced.DiffConst(rhs.m_interfaced);
<a name="l00483"></a>00483 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00484"></a>00484 };
<a name="l00485"></a>00485
<a name="l00487"></a><a class="code" href="classpolybori_1_1CDDInterface.html#f9c3271ea6861e604bdc000684683c73">00487</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#f9c3271ea6861e604bdc000684683c73" title="Set intersection.">intersect</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{
<a name="l00488"></a>00488 <span class="keywordflow">return</span> m_interfaced.Intersect(rhs.m_interfaced);
<a name="l00489"></a>00489 };
<a name="l00490"></a>00490
<a name="l00492"></a><a class="code" href="classpolybori_1_1CDDInterface.html#10e485df94875c45ecbe42d0bbca72bf">00492</a> <span class="keyword">self</span>& <a class="code" href="classpolybori_1_1CDDInterface.html#10e485df94875c45ecbe42d0bbca72bf" title="Set intersection with assignment.">intersectAssign</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs) {
<a name="l00493"></a>00493 m_interfaced = m_interfaced.Intersect(rhs.m_interfaced);
<a name="l00494"></a>00494 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00495"></a>00495 };
<a name="l00496"></a>00496
<a name="l00498"></a><a class="code" href="classpolybori_1_1CDDInterface.html#48c207e7da8cfdf9457749cf19f17e32">00498</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#48c207e7da8cfdf9457749cf19f17e32" title="Product.">product</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{
<a name="l00499"></a>00499 <span class="keywordflow">return</span> m_interfaced.Product(rhs.m_interfaced);
<a name="l00500"></a>00500 };
<a name="l00501"></a>00501
<a name="l00503"></a><a class="code" href="classpolybori_1_1CDDInterface.html#d503e4affae5e573b656709e0a20b986">00503</a> <span class="keyword">self</span>& <a class="code" href="classpolybori_1_1CDDInterface.html#d503e4affae5e573b656709e0a20b986" title="Product with assignment.">productAssign</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs) {
<a name="l00504"></a>00504 m_interfaced = m_interfaced.Product(rhs.m_interfaced);
<a name="l00505"></a>00505 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00506"></a>00506 };
<a name="l00507"></a>00507
<a name="l00509"></a><a class="code" href="classpolybori_1_1CDDInterface.html#f6f84bbc8dc3e94a5ba03499af89c107">00509</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#f6f84bbc8dc3e94a5ba03499af89c107" title="Unate product.">unateProduct</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{
<a name="l00510"></a>00510 <span class="keywordflow">return</span> m_interfaced.UnateProduct(rhs.m_interfaced);
<a name="l00511"></a>00511 };
<a name="l00512"></a>00512
<a name="l00513"></a>00513
<a name="l00514"></a>00514
<a name="l00516"></a><a class="code" href="classpolybori_1_1CDDInterface.html#4f3aa67f921cb7e5b7035891854d2be6">00516</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#4f3aa67f921cb7e5b7035891854d2be6" title="Returns dot Product.">dotProduct</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{
<a name="l00517"></a>00517 <span class="keywordflow">return</span> interfaced_type(m_interfaced.manager(),
<a name="l00518"></a>00518 <a class="code" href="extrafwd_8h.html#1192f3df8e54281288caf283245de4d5">Extra_zddDotProduct</a>(
<a name="l00519"></a>00519 manager().getManager(),
<a name="l00520"></a>00520 m_interfaced.getNode(),
<a name="l00521"></a>00521 rhs.m_interfaced.getNode()));
<a name="l00522"></a>00522 }
<a name="l00523"></a>00523
<a name="l00524"></a><a class="code" href="classpolybori_1_1CDDInterface.html#6253bb18dc397f271a08c7595f4acd58">00524</a> <span class="keyword">self</span>& <a class="code" href="classpolybori_1_1CDDInterface.html#6253bb18dc397f271a08c7595f4acd58">dotProductAssign</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs){
<a name="l00525"></a>00525 m_interfaced=interfaced_type(m_interfaced.manager(),
<a name="l00526"></a>00526 <a class="code" href="extrafwd_8h.html#1192f3df8e54281288caf283245de4d5">Extra_zddDotProduct</a>(
<a name="l00527"></a>00527 manager().getManager(),
<a name="l00528"></a>00528 m_interfaced.getNode(),
<a name="l00529"></a>00529 rhs.m_interfaced.getNode()));
<a name="l00530"></a>00530 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00531"></a>00531 }
<a name="l00532"></a>00532
<a name="l00533"></a><a class="code" href="classpolybori_1_1CDDInterface.html#17ff3bbba87ecd58056ca6334863a8d9">00533</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#17ff3bbba87ecd58056ca6334863a8d9">Xor</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{
<a name="l00534"></a>00534 <span class="keywordflow">if</span> (rhs.emptiness())
<a name="l00535"></a>00535 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00536"></a>00536 <span class="preprocessor">#ifdef PBORI_LOWLEVEL_XOR</span>
<a name="l00537"></a>00537 <span class="preprocessor"></span> <span class="keywordflow">return</span> interfaced_type(m_interfaced.manager(),
<a name="l00538"></a>00538 <a class="code" href="namespacepolybori.html#41700debc9ce9c13c5e1b325e4148fcc">pboriCudd_zddUnionXor</a>(
<a name="l00539"></a>00539 manager().getManager(),
<a name="l00540"></a>00540 m_interfaced.getNode(),
<a name="l00541"></a>00541 rhs.m_interfaced.getNode()));
<a name="l00542"></a>00542 <span class="preprocessor">#else</span>
<a name="l00543"></a>00543 <span class="preprocessor"></span> <span class="keywordflow">return</span> interfaced_type(m_interfaced.manager(),
<a name="l00544"></a>00544 <a class="code" href="extrafwd_8h.html#b3e9d664e7fbbb038b0427a031d883ca">Extra_zddUnionExor</a>(
<a name="l00545"></a>00545 manager().getManager(),
<a name="l00546"></a>00546 m_interfaced.getNode(),
<a name="l00547"></a>00547 rhs.m_interfaced.getNode()));
<a name="l00548"></a>00548 <span class="preprocessor">#endif</span>
<a name="l00549"></a>00549 <span class="preprocessor"></span> }
<a name="l00550"></a>00550
<a name="l00551"></a>00551
<a name="l00553"></a><a class="code" href="classpolybori_1_1CDDInterface.html#5a3d124510ee060e88cfe30a41e3a730">00553</a> <span class="keyword">self</span>& <a class="code" href="classpolybori_1_1CDDInterface.html#5a3d124510ee060e88cfe30a41e3a730" title="Unate product with assignment.">unateProductAssign</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs) {
<a name="l00554"></a>00554 m_interfaced = m_interfaced.UnateProduct(rhs.m_interfaced);
<a name="l00555"></a>00555 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00556"></a>00556 };
<a name="l00557"></a>00557
<a name="l00559"></a><a class="code" href="classpolybori_1_1CDDInterface.html#1f187bf7bfc67573af3bd982961cfa69">00559</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#1f187bf7bfc67573af3bd982961cfa69" title="Generate subset, where decision diagram manager variable idx is false.">subset0</a>(<a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> idx)<span class="keyword"> const </span>{
<a name="l00560"></a>00560 <span class="keywordflow">return</span> m_interfaced.Subset0(idx);
<a name="l00561"></a>00561 };
<a name="l00562"></a>00562
<a name="l00564"></a><a class="code" href="classpolybori_1_1CDDInterface.html#588867d4ef9bbce684a0814ee284185a">00564</a> <span class="keyword">self</span>& <a class="code" href="classpolybori_1_1CDDInterface.html#588867d4ef9bbce684a0814ee284185a" title="subset0 with assignment">subset0Assign</a>(<a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> idx) {
<a name="l00565"></a>00565 m_interfaced = m_interfaced.Subset0(idx);
<a name="l00566"></a>00566 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00567"></a>00567 };
<a name="l00568"></a>00568
<a name="l00570"></a><a class="code" href="classpolybori_1_1CDDInterface.html#674bdebf1957e9d8c053d72e5e6ef5bb">00570</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#674bdebf1957e9d8c053d72e5e6ef5bb" title="Generate subset, where decision diagram manager variable idx is asserted.">subset1</a>(<a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> idx)<span class="keyword"> const </span>{
<a name="l00571"></a>00571 <span class="keywordflow">return</span> m_interfaced.Subset1(idx);
<a name="l00572"></a>00572 };
<a name="l00573"></a>00573
<a name="l00575"></a><a class="code" href="classpolybori_1_1CDDInterface.html#6348b342a055af6144dcda0a63e3dabb">00575</a> <span class="keyword">self</span>& <a class="code" href="classpolybori_1_1CDDInterface.html#6348b342a055af6144dcda0a63e3dabb" title="subset1 with assignment">subset1Assign</a>(<a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> idx) {
<a name="l00576"></a>00576 m_interfaced = m_interfaced.Subset1(idx);
<a name="l00577"></a>00577 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00578"></a>00578 };
<a name="l00579"></a>00579
<a name="l00581"></a><a class="code" href="classpolybori_1_1CDDInterface.html#5bd0851844c6b6bc4d65dd51465990a4">00581</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#5bd0851844c6b6bc4d65dd51465990a4" title="Substitute variable with index idx by its complement.">change</a>(<a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> idx)<span class="keyword"> const </span>{
<a name="l00582"></a>00582
<a name="l00583"></a>00583 <span class="keywordflow">return</span> m_interfaced.Change(idx);
<a name="l00584"></a>00584 };
<a name="l00585"></a>00585
<a name="l00587"></a><a class="code" href="classpolybori_1_1CDDInterface.html#184ebb28e1cf6e6642506f7d9837b0a6">00587</a> <span class="keyword">self</span>& <a class="code" href="classpolybori_1_1CDDInterface.html#184ebb28e1cf6e6642506f7d9837b0a6" title="Change with assignment.">changeAssign</a>(<a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> idx) {
<a name="l00588"></a>00588 m_interfaced = m_interfaced.Change(idx);
<a name="l00589"></a>00589 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00590"></a>00590 };
<a name="l00591"></a>00591
<a name="l00593"></a><a class="code" href="classpolybori_1_1CDDInterface.html#8bb7332bea41eec1b3e9012e49b4ed01">00593</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#8bb7332bea41eec1b3e9012e49b4ed01" title="Division.">ddDivide</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{
<a name="l00594"></a>00594 <span class="keywordflow">return</span> m_interfaced.Divide(rhs);
<a name="l00595"></a>00595 };
<a name="l00596"></a>00596
<a name="l00598"></a><a class="code" href="classpolybori_1_1CDDInterface.html#bee0b4c2ea9e3aec2756eb55b2c7c22f">00598</a> <span class="keyword">self</span>& <a class="code" href="classpolybori_1_1CDDInterface.html#bee0b4c2ea9e3aec2756eb55b2c7c22f" title="Division with assignment.">ddDivideAssign</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs) {
<a name="l00599"></a>00599 m_interfaced = m_interfaced.Divide(rhs);
<a name="l00600"></a>00600 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00601"></a>00601 };
<a name="l00603"></a><a class="code" href="classpolybori_1_1CDDInterface.html#634fdc163c3446d95e6c23ea9a6cc64f">00603</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#634fdc163c3446d95e6c23ea9a6cc64f" title="Weak division.">weakDivide</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{
<a name="l00604"></a>00604 <span class="keywordflow">return</span> m_interfaced.WeakDiv(rhs);
<a name="l00605"></a>00605 };
<a name="l00606"></a>00606
<a name="l00608"></a><a class="code" href="classpolybori_1_1CDDInterface.html#cea5039d309b02dce68a1abed99b46d9">00608</a> <span class="keyword">self</span>& <a class="code" href="classpolybori_1_1CDDInterface.html#cea5039d309b02dce68a1abed99b46d9" title="Weak division with assignment.">weakDivideAssign</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs) {
<a name="l00609"></a>00609 m_interfaced = m_interfaced.WeakDiv(rhs);
<a name="l00610"></a>00610 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00611"></a>00611 };
<a name="l00612"></a>00612
<a name="l00614"></a><a class="code" href="classpolybori_1_1CDDInterface.html#6d7f05fdd2e54f5b8c1ced24ac8ece7a">00614</a> <span class="keyword">self</span>& <a class="code" href="classpolybori_1_1CDDInterface.html#6d7f05fdd2e54f5b8c1ced24ac8ece7a" title="Division with first term of right-hand side and assignment.">divideFirstAssign</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs) {
<a name="l00615"></a>00615
<a name="l00616"></a>00616 <a class="code" href="classpolybori_1_1PBoRiOutIter.html" title="This template class defines an output iterator which interprets assignments of indices...">PBoRiOutIter<self, idx_type, subset1_assign<self></a> > outiter(*<span class="keyword">this</span>);
<a name="l00617"></a>00617 std::copy(rhs.firstBegin(), rhs.firstEnd(), outiter);
<a name="l00618"></a>00618
<a name="l00619"></a>00619 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00620"></a>00620 }
<a name="l00621"></a>00621
<a name="l00623"></a><a class="code" href="classpolybori_1_1CDDInterface.html#2df42bc62e42a1afe527098a1c862ad4">00623</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#2df42bc62e42a1afe527098a1c862ad4" title="Division with first term of right-hand side.">divideFirst</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{
<a name="l00624"></a>00624
<a name="l00625"></a>00625 <span class="keyword">self</span> result(*<span class="keyword">this</span>);
<a name="l00626"></a>00626 result.divideFirstAssign(rhs);
<a name="l00627"></a>00627
<a name="l00628"></a>00628 <span class="keywordflow">return</span> result;
<a name="l00629"></a>00629 }
<a name="l00630"></a>00630
<a name="l00631"></a>00631
<a name="l00633"></a><a class="code" href="classpolybori_1_1CDDInterface.html#f13a6ae0bf2ab99c2b17f631829fa78f">00633</a> size_type <a class="code" href="classpolybori_1_1CDDInterface.html#f13a6ae0bf2ab99c2b17f631829fa78f" title="Get number of nodes in decision diagram.">nNodes</a>()<span class="keyword"> const </span>{
<a name="l00634"></a>00634 <span class="keywordflow">return</span> Cudd_zddDagSize(m_interfaced.getNode());
<a name="l00635"></a>00635 }
<a name="l00636"></a>00636
<a name="l00638"></a><a class="code" href="classpolybori_1_1CDDInterface.html#2b3f1d292626e0baae5979e72352dd64">00638</a> ostream_type& <a class="code" href="classpolybori_1_1CDDInterface.html#2b3f1d292626e0baae5979e72352dd64" title="Get number of nodes in decision diagram.">print</a>(ostream_type& os)<span class="keyword"> const </span>{
<a name="l00639"></a>00639
<a name="l00640"></a>00640 FILE* oldstdout = manager().ReadStdout();
<a name="l00641"></a>00641
<a name="l00643"></a>00643 <span class="keywordflow">if</span> (os == std::cout)
<a name="l00644"></a>00644 manager().SetStdout(stdout);
<a name="l00645"></a>00645 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (os == std::cerr)
<a name="l00646"></a>00646 manager().SetStdout(stderr);
<a name="l00647"></a>00647
<a name="l00648"></a>00648 m_interfaced.print( Cudd_ReadZddSize(manager().getManager()) );
<a name="l00649"></a>00649 m_interfaced.PrintMinterm();
<a name="l00650"></a>00650
<a name="l00651"></a>00651 manager().SetStdout(oldstdout);
<a name="l00652"></a>00652 <span class="keywordflow">return</span> os;
<a name="l00653"></a>00653 }
<a name="l00654"></a>00654
<a name="l00656"></a><a class="code" href="classpolybori_1_1CDDInterface.html#9f03d240edf9220ace28654cf21143be">00656</a> <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1CDDInterface.html#9f03d240edf9220ace28654cf21143be" title="Print Dot-output to file given by file handle.">prettyPrint</a>(pretty_out_type filehandle = stdout)<span class="keyword"> const </span>{
<a name="l00657"></a>00657 DdNode* tmp = m_interfaced.getNode();
<a name="l00658"></a>00658 Cudd_zddDumpDot(m_interfaced.getManager(), 1, &tmp,
<a name="l00659"></a>00659 NULL, NULL, filehandle);
<a name="l00660"></a>00660 };
<a name="l00661"></a>00661
<a name="l00663"></a><a class="code" href="classpolybori_1_1CDDInterface.html#f0936c6d8261b45f4b9d8d87f6364623">00663</a> bool_type <a class="code" href="classpolybori_1_1CDDInterface.html#f0936c6d8261b45f4b9d8d87f6364623" title="Print Dot-output to file given by file name.">prettyPrint</a>(filename_type filename)<span class="keyword"> const </span>{
<a name="l00664"></a>00664
<a name="l00665"></a>00665 FILE* theFile = fopen( filename, <span class="stringliteral">"w"</span>);
<a name="l00666"></a>00666 <span class="keywordflow">if</span> (theFile == NULL)
<a name="l00667"></a>00667 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00668"></a>00668
<a name="l00669"></a>00669 prettyPrint(theFile);
<a name="l00670"></a>00670 fclose(theFile);
<a name="l00671"></a>00671
<a name="l00672"></a>00672 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00673"></a>00673 };
<a name="l00674"></a>00674
<a name="l00676"></a><a class="code" href="classpolybori_1_1CDDInterface.html#050d1bd7a007d90aef802f1f4cbabd3c">00676</a> bool_type <a class="code" href="classpolybori_1_1CDDInterface.html#050d1bd7a007d90aef802f1f4cbabd3c" title="Equality check.">operator==</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{
<a name="l00677"></a>00677 <span class="keywordflow">return</span> (m_interfaced == rhs.m_interfaced);
<a name="l00678"></a>00678 }
<a name="l00679"></a>00679
<a name="l00681"></a><a class="code" href="classpolybori_1_1CDDInterface.html#9f44fa6d8bf28213ab63d9601f814a3f">00681</a> bool_type <a class="code" href="classpolybori_1_1CDDInterface.html#9f44fa6d8bf28213ab63d9601f814a3f" title="Nonequality check.">operator!=</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{
<a name="l00682"></a>00682 <span class="keywordflow">return</span> (m_interfaced != rhs.m_interfaced);
<a name="l00683"></a>00683 }
<a name="l00684"></a>00684
<a name="l00686"></a><a class="code" href="classpolybori_1_1CDDInterface.html#41134aa1cc96606701528ccc5856c51f">00686</a> mgr_ref <a class="code" href="classpolybori_1_1CDDInterface.html#41134aa1cc96606701528ccc5856c51f" title="Get reference to actual decision diagram manager.">manager</a>()<span class="keyword"> const </span>{
<a name="l00687"></a>00687 <span class="keywordflow">return</span> <a class="code" href="namespacepolybori.html#a8924f3c16bad2c0c02e5fc9048717f6">get_manager</a>(m_interfaced.manager());
<a name="l00688"></a>00688 }
<a name="l00689"></a><a class="code" href="classpolybori_1_1CDDInterface.html#65cf8fbce2b06128d83b86f49670e33a">00689</a> core_type <a class="code" href="classpolybori_1_1CDDInterface.html#65cf8fbce2b06128d83b86f49670e33a">managerCore</a>()<span class="keyword"> const</span>{
<a name="l00690"></a>00690 <span class="keywordflow">return</span> m_interfaced.manager();
<a name="l00691"></a>00691 }
<a name="l00693"></a><a class="code" href="classpolybori_1_1CDDInterface.html#101d1f478212b83bdcb5de8cda227c6c">00693</a> size_type <a class="code" href="classpolybori_1_1CDDInterface.html#101d1f478212b83bdcb5de8cda227c6c" title="Get numbers of used variables.">nSupport</a>()<span class="keyword"> const </span>{
<a name="l00694"></a>00694 <span class="keywordflow">return</span> Cudd_SupportSize(manager().getManager(), m_interfaced.getNode());
<a name="l00695"></a>00695 }
<a name="l00696"></a>00696
<a name="l00697"></a>00697 <span class="preprocessor">#if 1</span>
<a name="l00699"></a><a class="code" href="classpolybori_1_1CDDInterface.html#6aba64d24b0795670dda592a0ec1330f">00699</a> <span class="preprocessor"> self support() const {</span>
<a name="l00700"></a>00700 <span class="preprocessor"></span>
<a name="l00701"></a>00701 <span class="comment">// BDD supp( &manager(), </span>
<a name="l00702"></a>00702 DdNode* tmp = Cudd_Support(manager().getManager(), m_interfaced.getNode());
<a name="l00703"></a>00703 Cudd_Ref(tmp);
<a name="l00704"></a>00704
<a name="l00705"></a>00705 <span class="keyword">self</span> result = interfaced_type(m_interfaced.manager(),
<a name="l00706"></a>00706 Cudd_zddPortFromBdd(manager().getManager(), tmp));
<a name="l00707"></a>00707 Cudd_RecursiveDeref(manager().getManager(), tmp);
<a name="l00708"></a>00708 <span class="comment">// return supp.PortToZdd();</span>
<a name="l00709"></a>00709
<a name="l00710"></a>00710 <span class="comment">// assert(false);</span>
<a name="l00711"></a>00711 <span class="keywordflow">return</span> result;
<a name="l00712"></a>00712 }
<a name="l00713"></a>00713 <span class="preprocessor">#endif</span>
<a name="l00714"></a>00714 <span class="preprocessor"></span>
<a name="l00716"></a>00716 <span class="keyword">template</span><<span class="keyword">class</span> VectorLikeType>
<a name="l00717"></a><a class="code" href="classpolybori_1_1CDDInterface.html#74cf302d21f752cacd41581ba4e0de0a">00717</a> <span class="keywordtype">void</span> <a class="code" href="classpolybori_1_1CDDInterface.html#74cf302d21f752cacd41581ba4e0de0a" title="Get used variables (assuming indices of zero length).">usedIndices</a>(VectorLikeType& indices)<span class="keyword"> const </span>{
<a name="l00718"></a>00718
<a name="l00719"></a>00719 <span class="keywordtype">int</span>* pIdx = Cudd_SupportIndex( manager().getManager(),
<a name="l00720"></a>00720 m_interfaced.getNode() );
<a name="l00721"></a>00721
<a name="l00722"></a>00722
<a name="l00723"></a>00723
<a name="l00724"></a>00724 size_type nlen(nVariables());
<a name="l00725"></a>00725
<a name="l00726"></a>00726 indices.reserve(std::accumulate(pIdx, pIdx + nlen, size_type()));
<a name="l00727"></a>00727
<a name="l00728"></a>00728 <span class="keywordflow">for</span>(size_type idx = 0; idx < nlen; ++idx)
<a name="l00729"></a>00729 <span class="keywordflow">if</span> (pIdx[idx] == 1){
<a name="l00730"></a>00730 indices.push_back(idx);
<a name="l00731"></a>00731 }
<a name="l00732"></a>00732 FREE(pIdx);
<a name="l00733"></a>00733 }
<a name="l00734"></a>00734
<a name="l00736"></a><a class="code" href="classpolybori_1_1CDDInterface.html#9c8ba5faa7c153f0b0b75ceaec06d15a">00736</a> <span class="keywordtype">int</span>* <a class="code" href="classpolybori_1_1CDDInterface.html#9c8ba5faa7c153f0b0b75ceaec06d15a" title="Get used variables (assuming indices of length nSupport()).">usedIndices</a>()<span class="keyword"> const </span>{
<a name="l00737"></a>00737
<a name="l00738"></a>00738 <span class="keywordflow">return</span> Cudd_SupportIndex( manager().getManager(),
<a name="l00739"></a>00739 m_interfaced.getNode() );
<a name="l00740"></a>00740
<a name="l00741"></a>00741
<a name="l00742"></a>00742 }
<a name="l00743"></a>00743
<a name="l00744"></a>00744
<a name="l00746"></a><a class="code" href="classpolybori_1_1CDDInterface.html#47cac92b3401359385b60abf760db61d">00746</a> <a class="code" href="classpolybori_1_1CCuddFirstIter.html" title="This class defines an iterator over the first minimal term of a given ZDD node.">first_iterator</a> <a class="code" href="classpolybori_1_1CDDInterface.html#47cac92b3401359385b60abf760db61d" title="Start of first term.">firstBegin</a>()<span class="keyword"> const </span>{
<a name="l00747"></a>00747 <span class="keywordflow">return</span> <a class="code" href="classpolybori_1_1CCuddFirstIter.html" title="This class defines an iterator over the first minimal term of a given ZDD node.">first_iterator</a>(navigation());
<a name="l00748"></a>00748 }
<a name="l00749"></a>00749
<a name="l00751"></a><a class="code" href="classpolybori_1_1CDDInterface.html#2ca7110e74d98e0419b1e8aaba2c7b99">00751</a> <a class="code" href="classpolybori_1_1CCuddFirstIter.html" title="This class defines an iterator over the first minimal term of a given ZDD node.">first_iterator</a> <a class="code" href="classpolybori_1_1CDDInterface.html#2ca7110e74d98e0419b1e8aaba2c7b99" title="Finish of first term.">firstEnd</a>()<span class="keyword"> const </span>{
<a name="l00752"></a>00752 <span class="keywordflow">return</span> <a class="code" href="classpolybori_1_1CCuddFirstIter.html" title="This class defines an iterator over the first minimal term of a given ZDD node.">first_iterator</a>();
<a name="l00753"></a>00753 }
<a name="l00754"></a>00754
<a name="l00756"></a><a class="code" href="classpolybori_1_1CDDInterface.html#c06da94bf4cbf86a0e98cbd7a3bd21a5">00756</a> <a class="code" href="classpolybori_1_1CCuddLastIter.html" title="This class defines an iterator over the last minimal term of a given ZDD node.">last_iterator</a> <a class="code" href="classpolybori_1_1CDDInterface.html#c06da94bf4cbf86a0e98cbd7a3bd21a5" title="Start of first term.">lastBegin</a>()<span class="keyword"> const </span>{
<a name="l00757"></a>00757 <span class="keywordflow">return</span> <a class="code" href="classpolybori_1_1CCuddLastIter.html" title="This class defines an iterator over the last minimal term of a given ZDD node.">last_iterator</a>(m_interfaced.getNode());
<a name="l00758"></a>00758 }
<a name="l00759"></a>00759
<a name="l00761"></a><a class="code" href="classpolybori_1_1CDDInterface.html#0581557146dd62840da4cee301c09e2e">00761</a> <a class="code" href="classpolybori_1_1CCuddLastIter.html" title="This class defines an iterator over the last minimal term of a given ZDD node.">last_iterator</a> <a class="code" href="classpolybori_1_1CDDInterface.html#0581557146dd62840da4cee301c09e2e" title="Finish of first term.">lastEnd</a>()<span class="keyword"> const </span>{
<a name="l00762"></a>00762 <span class="keywordflow">return</span> <a class="code" href="classpolybori_1_1CCuddLastIter.html" title="This class defines an iterator over the last minimal term of a given ZDD node.">last_iterator</a>();
<a name="l00763"></a>00763 }
<a name="l00764"></a>00764
<a name="l00766"></a><a class="code" href="classpolybori_1_1CDDInterface.html#6b139678e062c727bd419556978b8139">00766</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#6b139678e062c727bd419556978b8139" title="Get decison diagram representing the multiples of the first term.">firstMultiples</a>(<span class="keyword">const</span> std::vector<idx_type>& multipliers)<span class="keyword"> const </span>{
<a name="l00767"></a>00767
<a name="l00768"></a>00768 std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
<a name="l00769"></a>00769
<a name="l00770"></a>00770 std::copy( firstBegin(), firstEnd(), indices.begin() );
<a name="l00771"></a>00771
<a name="l00772"></a>00772 <span class="keywordflow">return</span> <a class="code" href="namespacepolybori.html#9f5a4551340ca9187a30a37dbccf3f56" title="temporarily (needs to be more generic)">cudd_generate_multiples</a>( manager(),
<a name="l00773"></a>00773 indices.rbegin(), indices.rend(),
<a name="l00774"></a>00774 multipliers.rbegin(),
<a name="l00775"></a>00775 multipliers.rend() );
<a name="l00776"></a>00776 }
<a name="l00777"></a>00777
<a name="l00778"></a>00778
<a name="l00779"></a>00779
<a name="l00780"></a><a class="code" href="classpolybori_1_1CDDInterface.html#2b3fc32266bd01a4358fcd2acb6acb26">00780</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#2b3fc32266bd01a4358fcd2acb6acb26">subSet</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{
<a name="l00781"></a>00781
<a name="l00782"></a>00782 <span class="keywordflow">return</span> interfaced_type(m_interfaced.manager(),
<a name="l00783"></a>00783 <a class="code" href="extrafwd_8h.html#e71887adf63ff82b71f5752b931c2b42">Extra_zddSubSet</a>(manager().getManager(),
<a name="l00784"></a>00784 m_interfaced.getNode(),
<a name="l00785"></a>00785 rhs.m_interfaced.getNode()) );
<a name="l00786"></a>00786 }
<a name="l00787"></a>00787
<a name="l00788"></a><a class="code" href="classpolybori_1_1CDDInterface.html#f199d6c33745d60e668ba8ec7362382f">00788</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#f199d6c33745d60e668ba8ec7362382f">supSet</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{
<a name="l00789"></a>00789
<a name="l00790"></a>00790 <span class="keywordflow">return</span> interfaced_type(m_interfaced.manager(),
<a name="l00791"></a>00791 <a class="code" href="extrafwd_8h.html#4d7756c43cdee777ac3b3c97974a991a">Extra_zddSupSet</a>(manager().getManager(),
<a name="l00792"></a>00792 m_interfaced.getNode(),
<a name="l00793"></a>00793 rhs.m_interfaced.getNode()) );
<a name="l00794"></a>00794 }
<a name="l00796"></a><a class="code" href="classpolybori_1_1CDDInterface.html#c3d85737b7c5146e2204655a1c967d25">00796</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#c3d85737b7c5146e2204655a1c967d25" title="Get decison diagram representing the divisors of the first term.">firstDivisors</a>()<span class="keyword"> const </span>{
<a name="l00797"></a>00797
<a name="l00798"></a>00798 std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
<a name="l00799"></a>00799
<a name="l00800"></a>00800 std::copy( firstBegin(), firstEnd(), indices.begin() );
<a name="l00801"></a>00801
<a name="l00802"></a>00802 <span class="keywordflow">return</span> <a class="code" href="namespacepolybori.html#220b46f13d6e432df1cd40432dddbabb" title="temporarily (needs to be more generic)">cudd_generate_divisors</a>(manager(), indices.rbegin(), indices.rend());
<a name="l00803"></a>00803 }
<a name="l00804"></a>00804
<a name="l00806"></a><a class="code" href="classpolybori_1_1CDDInterface.html#7dde88b9d522c7faae213f8e75ba4b12">00806</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_1CDDInterface.html#7dde88b9d522c7faae213f8e75ba4b12" title="Navigate through ZDD by incrementThen(), incrementElse(), and terminated().">navigation</a>()<span class="keyword"> const </span>{
<a name="l00807"></a>00807 <span class="keywordflow">return</span> <a class="code" href="classpolybori_1_1CCuddNavigator.html" title="This class defines an iterator for navigating through then and else branches of ZDDs...">navigator</a>(m_interfaced.getNode());
<a name="l00808"></a>00808 }
<a name="l00809"></a>00809
<a name="l00811"></a><a class="code" href="classpolybori_1_1CDDInterface.html#78e9bcc6af406137eb48c822ced16536">00811</a> bool_type <a class="code" href="classpolybori_1_1CDDInterface.html#78e9bcc6af406137eb48c822ced16536" title="Checks whether the decision diagram is empty.">emptiness</a>()<span class="keyword"> const </span>{
<a name="l00812"></a>00812 <span class="keywordflow">return</span> ( m_interfaced.getNode() == manager().zddZero().getNode() );
<a name="l00813"></a>00813 }
<a name="l00814"></a>00814
<a name="l00816"></a><a class="code" href="classpolybori_1_1CDDInterface.html#5c7a7c14791679e372b12f677022899b">00816</a> bool_type <a class="code" href="classpolybori_1_1CDDInterface.html#5c7a7c14791679e372b12f677022899b" title="Checks whether the decision diagram has every variable negated.">blankness</a>()<span class="keyword"> const </span>{
<a name="l00817"></a>00817
<a name="l00818"></a>00818 <span class="keywordflow">return</span> ( m_interfaced.getNode() ==
<a name="l00819"></a>00819 manager().zddOne( nVariables() ).getNode() );
<a name="l00820"></a>00820
<a name="l00821"></a>00821 }
<a name="l00822"></a>00822
<a name="l00823"></a><a class="code" href="classpolybori_1_1CDDInterface.html#a55c1c7e1e42383c8ef5064654ddc4d0">00823</a> bool_type <a class="code" href="classpolybori_1_1CDDInterface.html#a55c1c7e1e42383c8ef5064654ddc4d0">isConstant</a>()<span class="keyword"> const </span>{
<a name="l00824"></a>00824 <span class="keywordflow">return</span> (m_interfaced.getNode()) && Cudd_IsConstant(m_interfaced.getNode());
<a name="l00825"></a>00825 }
<a name="l00826"></a>00826
<a name="l00828"></a><a class="code" href="classpolybori_1_1CDDInterface.html#5128cab0f470b0dec943f7c33d6e2f17">00828</a> size_type <a class="code" href="classpolybori_1_1CDDInterface.html#5128cab0f470b0dec943f7c33d6e2f17" title="Returns number of terms.">size</a>()<span class="keyword"> const </span>{
<a name="l00829"></a>00829 <span class="keywordflow">return</span> m_interfaced.Count();
<a name="l00830"></a>00830 }
<a name="l00831"></a>00831
<a name="l00833"></a><a class="code" href="classpolybori_1_1CDDInterface.html#92b6e64c08f1013e123b7e6ca65da885">00833</a> size_type <a class="code" href="classpolybori_1_1CDDInterface.html#92b6e64c08f1013e123b7e6ca65da885" title="Returns number of terms (deprecated).">length</a>()<span class="keyword"> const </span>{
<a name="l00834"></a>00834 <span class="keywordflow">return</span> size();
<a name="l00835"></a>00835 }
<a name="l00836"></a>00836
<a name="l00838"></a><a class="code" href="classpolybori_1_1CDDInterface.html#977112822d6abc67de39dd7712cd56a9">00838</a> size_type <a class="code" href="classpolybori_1_1CDDInterface.html#977112822d6abc67de39dd7712cd56a9" title="Returns number of variables in manager.">nVariables</a>()<span class="keyword"> const </span>{
<a name="l00839"></a>00839 <span class="keywordflow">return</span> Cudd_ReadZddSize(manager().getManager() );
<a name="l00840"></a>00840 }
<a name="l00841"></a>00841
<a name="l00843"></a><a class="code" href="classpolybori_1_1CDDInterface.html#477a0f68a5528de0d6a74c28b1fc54b4">00843</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#477a0f68a5528de0d6a74c28b1fc54b4" title="Returns minimal factors of all minimal terms.">minimalElements</a>()<span class="keyword"> const </span>{
<a name="l00844"></a>00844 <span class="keywordflow">return</span> interfaced_type(m_interfaced.manager(),
<a name="l00845"></a>00845 <a class="code" href="extrafwd_8h.html#30e18eedb4e5f94ebac27795208cbb8f">Extra_zddMinimal</a>(manager().getManager(),m_interfaced.getNode()));
<a name="l00846"></a>00846 }
<a name="l00847"></a>00847
<a name="l00848"></a><a class="code" href="classpolybori_1_1CDDInterface.html#c7518f2f73758c6423b6af17d9c68b93">00848</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#c7518f2f73758c6423b6af17d9c68b93">cofactor0</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs)<span class="keyword"> const </span>{
<a name="l00849"></a>00849
<a name="l00850"></a>00850 <span class="keywordflow">return</span> interfaced_type(m_interfaced.manager(),
<a name="l00851"></a>00851 <a class="code" href="extrafwd_8h.html#3e3db6af3a432fb67d2d5f0299184c38">Extra_zddCofactor0</a>(manager().getManager(),
<a name="l00852"></a>00852 m_interfaced.getNode(),
<a name="l00853"></a>00853 rhs.m_interfaced.getNode()) );
<a name="l00854"></a>00854 }
<a name="l00855"></a>00855
<a name="l00856"></a><a class="code" href="classpolybori_1_1CDDInterface.html#8daa15844f10c83831b8230e1a732fd9">00856</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#8daa15844f10c83831b8230e1a732fd9">cofactor1</a>(<span class="keyword">const</span> <span class="keyword">self</span>& rhs, <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> includeVars)<span class="keyword"> const </span>{
<a name="l00857"></a>00857
<a name="l00858"></a>00858 <span class="keywordflow">return</span> interfaced_type(m_interfaced.manager(),
<a name="l00859"></a>00859 <a class="code" href="extrafwd_8h.html#1255f7b399f9366e1f83bbf6a206b627">Extra_zddCofactor1</a>(manager().getManager(),
<a name="l00860"></a>00860 m_interfaced.getNode(),
<a name="l00861"></a>00861 rhs.m_interfaced.getNode(),
<a name="l00862"></a>00862 includeVars) );
<a name="l00863"></a>00863 }
<a name="l00864"></a>00864
<a name="l00866"></a><a class="code" href="classpolybori_1_1CDDInterface.html#a4bc116bf1554d0fcf77766319db54e3">00866</a> bool_type <a class="code" href="classpolybori_1_1CDDInterface.html#a4bc116bf1554d0fcf77766319db54e3" title="Test whether the empty set is included.">ownsOne</a>()<span class="keyword"> const </span>{
<a name="l00867"></a>00867 <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> navi(navigation());
<a name="l00868"></a>00868
<a name="l00869"></a>00869 <span class="keywordflow">while</span> (!navi.<a class="code" href="classpolybori_1_1CCuddNavigator.html#565297a790f653c7c68bbe329f20061e" title="Check whether constant node was reached.">isConstant</a>() )
<a name="l00870"></a>00870 navi.<a class="code" href="classpolybori_1_1CCuddNavigator.html#347269fc9b99ffec1b93bbd6f44bcf27" title="Increment in else direction.">incrementElse</a>();
<a name="l00871"></a>00871
<a name="l00872"></a>00872 <span class="keywordflow">return</span> navi.<a class="code" href="classpolybori_1_1CCuddNavigator.html#5a22617f92b0d88e461d922efec2c93c" title="Check whether terminal node marks end of path.">terminalValue</a>();
<a name="l00873"></a>00873 }
<a name="l00874"></a><a class="code" href="classpolybori_1_1CDDInterface.html#530176a8be3693d2aa36d003fb25ee94">00874</a> <span class="keywordtype">double</span> <a class="code" href="classpolybori_1_1CDDInterface.html#530176a8be3693d2aa36d003fb25ee94">sizeDouble</a>()<span class="keyword"> const </span>{
<a name="l00875"></a>00875 <span class="keywordflow">return</span> m_interfaced.CountDouble();
<a name="l00876"></a>00876 }
<a name="l00877"></a>00877
<a name="l00879"></a><a class="code" href="classpolybori_1_1CDDInterface.html#09d34bf71e57be76b873a6c6c3395b11">00879</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#09d34bf71e57be76b873a6c6c3395b11" title="Get corresponding zero element.">emptyElement</a>()<span class="keyword"> const </span>{
<a name="l00880"></a>00880 <span class="keywordflow">return</span> manager().zddZero();
<a name="l00881"></a>00881 }
<a name="l00882"></a>00882
<a name="l00884"></a><a class="code" href="classpolybori_1_1CDDInterface.html#cc78842c9cae8ca22690819442802a33">00884</a> <span class="keyword">self</span> <a class="code" href="classpolybori_1_1CDDInterface.html#cc78842c9cae8ca22690819442802a33" title="Get corresponding one element.">blankElement</a>()<span class="keyword"> const </span>{
<a name="l00885"></a>00885 <span class="keywordflow">return</span> manager().zddOne();
<a name="l00886"></a>00886 }
<a name="l00887"></a>00887
<a name="l00888"></a>00888 <span class="keyword">private</span>:
<a name="l00889"></a>00889 navigator newNode(<span class="keyword">const</span> manager_base& mgr, <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> idx,
<a name="l00890"></a>00890 navigator thenNavi, navigator elseNavi)<span class="keyword"> const </span>{
<a name="l00891"></a>00891 assert(idx < *thenNavi);
<a name="l00892"></a>00892 assert(idx < *elseNavi);
<a name="l00893"></a>00893 <span class="keywordflow">return</span> navigator(cuddZddGetNode(mgr.getManager(), idx,
<a name="l00894"></a>00894 thenNavi.getNode(), elseNavi.getNode()));
<a name="l00895"></a>00895 }
<a name="l00896"></a>00896
<a name="l00897"></a>00897 interfaced_type newDiagram(<span class="keyword">const</span> manager_base& mgr, navigator navi)<span class="keyword"> const </span>{
<a name="l00898"></a>00898 <span class="keywordflow">return</span> interfaced_type(<a class="code" href="namespacepolybori.html#383fd66e3fa464a887facf198284030d">extract_manager</a>(mgr), navi.getNode());
<a name="l00899"></a>00899 }
<a name="l00900"></a>00900
<a name="l00901"></a>00901 <span class="keyword">self</span> fromTemporaryNode(<span class="keyword">const</span> navigator& navi)<span class="keyword"> const </span>{
<a name="l00902"></a>00902 navi.decRef();
<a name="l00903"></a>00903 <span class="keywordflow">return</span> <span class="keyword">self</span>(manager(), navi.getNode());
<a name="l00904"></a>00904 }
<a name="l00905"></a>00905
<a name="l00906"></a>00906
<a name="l00907"></a>00907 interfaced_type newNodeDiagram(<span class="keyword">const</span> manager_base& mgr, <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> idx,
<a name="l00908"></a>00908 navigator thenNavi,
<a name="l00909"></a>00909 navigator elseNavi)<span class="keyword"> const </span>{
<a name="l00910"></a>00910 <span class="keywordflow">if</span> ((idx >= *thenNavi) || (idx >= *elseNavi))
<a name="l00911"></a>00911 <span class="keywordflow">throw</span> PBoRiGenericError<CTypes::invalid_ite>();
<a name="l00912"></a>00912
<a name="l00913"></a>00913 <span class="keywordflow">return</span> newDiagram(mgr, newNode(mgr, idx, thenNavi, elseNavi) );
<a name="l00914"></a>00914 }
<a name="l00915"></a>00915
<a name="l00916"></a>00916 interfaced_type newNodeDiagram(<span class="keyword">const</span> manager_base& mgr,
<a name="l00917"></a>00917 <a class="code" href="namespacepolybori_1_1groebner.html#ef37a95e97afbd561cc4c5f84d660765">idx_type</a> idx, navigator navi)<span class="keyword"> const </span>{
<a name="l00918"></a>00918 <span class="keywordflow">if</span> (idx >= *navi)
<a name="l00919"></a>00919 <span class="keywordflow">throw</span> PBoRiGenericError<CTypes::invalid_ite>();
<a name="l00920"></a>00920
<a name="l00921"></a>00921 navi.incRef();
<a name="l00922"></a>00922 interfaced_type result =
<a name="l00923"></a>00923 newDiagram(mgr, newNode(mgr, idx, navi, navi) );
<a name="l00924"></a>00924 navi.decRef();
<a name="l00925"></a>00925 <span class="keywordflow">return</span> result;
<a name="l00926"></a>00926 }
<a name="l00927"></a>00927
<a name="l00928"></a>00928
<a name="l00929"></a>00929
<a name="l00930"></a>00930 };
<a name="l00931"></a>00931
<a name="l00932"></a>00932
<a name="l00933"></a>00933
<a name="l00934"></a>00934
<a name="l00935"></a>00935
<a name="l00937"></a>00937 <span class="keyword">template</span> <<span class="keyword">class</span> DDType>
<a name="l00938"></a>00938 <span class="keyword">typename</span> CDDInterface<DDType>::ostream_type&
<a name="l00939"></a><a class="code" href="namespacepolybori.html#4fc76f65a24beda9dfe4c6cbe5197c24">00939</a> operator<<( typename CDDInterface<DDType>::ostream_type& os,
<a name="l00940"></a>00940 <span class="keyword">const</span> <a class="code" href="classpolybori_1_1CDDInterface.html">CDDInterface<DDType></a>& dd ) {
<a name="l00941"></a>00941 <span class="keywordflow">return</span> dd.print(os);
<a name="l00942"></a>00942 }
<a name="l00943"></a>00943
<a name="l00944"></a>00944 <a class="code" href="pbori__defs_8h.html#faf094fde6c1a7f1aad18bcb455f3b06" title="Finish project&#39;s namespace.">END_NAMESPACE_PBORI</a>
<a name="l00945"></a>00945
<a name="l00946"></a>00946 <span class="preprocessor">#endif // of #ifndef CDDInterface_h_</span>
</pre></div></div>
<hr size="1"><address style="text-align: right;"><small>Generated on Wed Sep 9 14:30:54 2009 for PolyBoRi by
<a href="http://www.doxygen.org/index.html">
<img src="doxygen.png" alt="doxygen" align="middle" border="0"></a> 1.5.9 </small></address>
</body>
</html>
distrib
>
Mandriva
>
2010.0
>
i586
>
media
>
contrib-release
>
by-pkgid
>
a24e1a39141f9b4ca49bd1e2e23a54ba
>
files
>
57
