PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00070 //***************************************************************************** 00071 00072 // include basic definitions 00073 #include "pbori_defs.h" 00074 00075 #include "BooleEnv.h" 00076 00077 #include "CCacheManagement.h" 00078 00079 #ifndef CDegreeCache_h_ 00080 #define CDegreeCache_h_ 00081 00082 BEGIN_NAMESPACE_PBORI 00083 //class BoolePolyRing; 00090 template <class NaviType> 00091 class CIndexHandle { 00092 public: 00093 00094 enum { invalid = CTypes::max_idx }; 00095 00097 typedef NaviType navigator; 00098 00100 typedef navigator base; 00101 00103 typedef typename navigator::bool_type bool_type; 00104 00106 typedef typename CTypes::idx_type idx_type; 00107 00109 typedef typename CTypes::size_type size_type; 00110 00112 typedef typename CTypes::manager_base manager_type; 00113 00115 CIndexHandle(idx_type idx): m_idx(idx) {} 00116 00118 explicit CIndexHandle(navigator navi, const manager_type& mgr): 00119 m_idx(fromNode(navi, mgr)) {} 00120 00122 idx_type operator*() const { 00123 return m_idx; 00124 } 00125 00126 bool isValid() const { 00127 return (m_idx != invalid); 00128 } 00129 protected: 00131 idx_type fromNode(navigator navi, const manager_type& mgr) const { 00132 00133 if (!navi.isValid()) 00134 return invalid; 00135 00136 if UNLIKELY(navi.isConstant()) 00137 return mgr.nVariables(); 00138 else 00139 return *navi; 00140 } 00141 00142 00143 00144 idx_type m_idx; 00145 }; 00146 00147 00148 template <class NaviType> 00149 class CIndexCacheHandle { 00150 public: 00151 00153 typedef NaviType navigator; 00154 00156 // typedef navigator base; 00157 00159 typedef typename navigator::bool_type bool_type; 00160 00162 typedef typename navigator::value_type idx_type; 00163 00165 typedef typename navigator::size_type size_type; 00166 00168 typedef typename CTypes::manager_base manager_type; 00169 00171 CIndexCacheHandle(idx_type idx, const manager_type& mgr): 00172 m_navi( toNode(idx, mgr) ) {} 00173 00175 explicit CIndexCacheHandle(navigator navi): 00176 m_navi(navi) {} 00177 00178 operator navigator() const { return m_navi; } 00179 00180 protected: 00182 navigator toNode(idx_type idx, const manager_type& mgr) const { 00183 00184 if LIKELY((size_type)idx < mgr.nVariables()) 00185 return navigator(mgr.getVar(idx)); 00186 00187 return navigator(mgr.zddZero()); 00188 } 00189 00191 navigator m_navi; 00192 }; 00193 00194 template <class TagType = typename CCacheTypes::degree, 00195 class DDType = typename CTypes::dd_type> 00196 class CDegreeCache: 00197 public CCacheManagement<TagType, 1> { 00198 00199 public: 00201 00202 typedef DDType dd_type; 00203 typedef TagType tag_type; 00204 typedef CCacheManagement<tag_type, 1> base; 00205 typedef CDegreeCache<tag_type, dd_type> self; 00207 00209 00210 typedef typename base::node_type input_node_type; 00211 typedef typename base::manager_type manager_type; 00212 typedef typename dd_type::size_type size_type; 00213 typedef typename dd_type::navigator navi_type; 00214 typedef CIndexHandle<navi_type> node_type; 00215 typedef CIndexCacheHandle<navi_type> node_cache_type; 00217 00219 CDegreeCache(const manager_type& mgr): base(mgr) {} 00220 00222 CDegreeCache(const self& rhs): base(rhs) {} 00223 00225 ~CDegreeCache() {} 00226 00228 node_type find(input_node_type navi) const{ 00229 return node_type(base::find(navi), base::manager()); } 00230 00231 node_type find(navi_type navi) const{ 00232 return node_type(base::find(navi), base::manager()); } 00233 00235 void insert(input_node_type navi, size_type deg) const { 00236 base::insert(navi, node_cache_type(deg, base::manager())); 00237 } 00238 00240 void insert(navi_type navi, size_type deg) const { 00241 base::insert(navi, node_cache_type(deg, base::manager())); 00242 } 00243 00244 }; 00245 00246 00247 00248 00249 template <class TagType = typename CCacheTypes::block_degree, 00250 class DDType = typename CTypes::dd_type> 00251 class CBlockDegreeCache: 00252 public CCacheManagement<TagType, 2> { 00253 00254 public: 00256 00257 typedef DDType dd_type; 00258 typedef TagType tag_type; 00259 typedef CCacheManagement<tag_type, 2> base; 00260 typedef CBlockDegreeCache<tag_type, dd_type> self; 00262 00264 00265 typedef typename base::node_type input_node_type; 00266 typedef typename base::manager_type manager_type; 00267 typedef typename dd_type::idx_type idx_type; 00268 typedef typename dd_type::size_type size_type; 00269 typedef typename dd_type::navigator navi_type; 00270 typedef CIndexHandle<navi_type> node_type; 00271 typedef CIndexCacheHandle<navi_type> node_cache_type; 00273 00275 CBlockDegreeCache(const manager_type& mgr): base(mgr) {} 00276 00278 CBlockDegreeCache(const self& rhs): base(rhs) {} 00279 00281 ~CBlockDegreeCache() {} 00282 00284 node_type find(input_node_type navi, idx_type idx) const{ 00285 return node_type(base::find(navi, node_cache_type(idx, base::manager())), 00286 base::manager()); } 00287 00288 node_type find(navi_type navi, idx_type idx) const{ 00289 return node_type(base::find(navi, node_cache_type(idx, base::manager())), 00290 base::manager()); } 00291 00293 void insert(input_node_type navi, idx_type idx, size_type deg) const { 00294 base::insert(navi, node_cache_type(idx, base::manager()), 00295 node_cache_type(deg, base::manager())); 00296 } 00297 00299 void insert(navi_type navi, idx_type idx, size_type deg) const { 00300 base::insert(navi, node_cache_type(idx, base::manager()), 00301 node_cache_type(deg, base::manager())); 00302 } 00303 }; 00304 00305 template <class TagType, 00306 class DDType = typename CTypes::dd_type> 00307 class CDegreeArgumentCache: 00308 public CCacheManagement<TagType, 2> { 00309 00310 public: 00312 00313 typedef DDType dd_type; 00314 typedef TagType tag_type; 00315 typedef CCacheManagement<tag_type, 2> base; 00316 typedef CDegreeArgumentCache<tag_type, dd_type> self; 00318 00320 00321 typedef typename base::node_type node_type; 00322 typedef typename base::manager_type manager_type; 00323 typedef typename dd_type::size_type size_type; 00324 typedef typename dd_type::navigator navi_type; 00325 typedef CIndexCacheHandle<navi_type> degree_node_type; 00327 00329 CDegreeArgumentCache(const manager_type& mgr): base(mgr) {} 00330 00332 CDegreeArgumentCache(const self& rhs): base(rhs) {} 00333 00335 ~CDegreeArgumentCache() {} 00336 00338 navi_type find(navi_type navi, size_type deg) const{ 00339 return base::find(navi, degree_node_type(deg, base::manager())); 00340 } 00341 00343 void insert(navi_type navi, size_type deg, navi_type result) const { 00344 base::insert(navi, degree_node_type(deg, base::manager()), result); 00345 } 00346 00347 }; 00348 00349 00350 END_NAMESPACE_PBORI 00351 00352 #endif