PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00073 //***************************************************************************** 00074 00075 // include basic definitions 00076 #include "pbori_defs.h" 00077 00078 #include "BooleEnv.h" 00079 00080 #include "CCacheManagement.h" 00081 00082 #ifndef CDegreeCache_h_ 00083 #define CDegreeCache_h_ 00084 00085 BEGIN_NAMESPACE_PBORI 00086 //class BoolePolyRing; 00093 template <class NaviType> 00094 class CIndexHandle { 00095 public: 00096 00097 enum { invalid = CTypes::max_idx }; 00098 00100 typedef NaviType navigator; 00101 00103 typedef navigator base; 00104 00106 typedef typename navigator::bool_type bool_type; 00107 00109 typedef typename CTypes::idx_type idx_type; 00110 00112 typedef typename CTypes::size_type size_type; 00113 00115 typedef typename CTypes::manager_base manager_type; 00116 00118 CIndexHandle(idx_type idx): m_idx(idx) {} 00119 00121 explicit CIndexHandle(navigator navi, const manager_type& mgr): 00122 m_idx(fromNode(navi, mgr)) {} 00123 00125 idx_type operator*() const { 00126 return m_idx; 00127 } 00128 00129 bool isValid() const { 00130 return (m_idx != invalid); 00131 } 00132 protected: 00134 idx_type fromNode(navigator navi, const manager_type& mgr) const { 00135 00136 if (!navi.isValid()) 00137 return invalid; 00138 00139 if UNLIKELY(navi.isConstant()) 00140 return mgr.nVariables(); 00141 else 00142 return *navi; 00143 } 00144 00145 00146 00147 idx_type m_idx; 00148 }; 00149 00150 00151 template <class NaviType> 00152 class CIndexCacheHandle { 00153 public: 00154 00156 typedef NaviType navigator; 00157 00159 // typedef navigator base; 00160 00162 typedef typename navigator::bool_type bool_type; 00163 00165 typedef typename navigator::value_type idx_type; 00166 00168 typedef typename navigator::size_type size_type; 00169 00171 typedef typename CTypes::manager_base manager_type; 00172 00174 CIndexCacheHandle(idx_type idx, const manager_type& mgr): 00175 m_navi( toNode(idx, mgr) ) {} 00176 00178 explicit CIndexCacheHandle(navigator navi): 00179 m_navi(navi) {} 00180 00181 operator navigator() const { return m_navi; } 00182 00183 protected: 00185 navigator toNode(idx_type idx, const manager_type& mgr) const { 00186 00187 if LIKELY((size_type)idx < mgr.nVariables()) 00188 return navigator(mgr.getVar(idx)); 00189 00190 return navigator(mgr.zddZero()); 00191 } 00192 00194 navigator m_navi; 00195 }; 00196 00197 template <class TagType = typename CCacheTypes::degree, 00198 class DDType = typename CTypes::dd_type> 00199 class CDegreeCache: 00200 public CCacheManagement<TagType, 1> { 00201 00202 public: 00204 00205 typedef DDType dd_type; 00206 typedef TagType tag_type; 00207 typedef CCacheManagement<tag_type, 1> base; 00208 typedef CDegreeCache<tag_type, dd_type> self; 00210 00212 00213 typedef typename base::node_type input_node_type; 00214 typedef typename base::manager_type manager_type; 00215 typedef typename dd_type::size_type size_type; 00216 typedef typename dd_type::deg_type deg_type; 00217 typedef typename dd_type::navigator navi_type; 00218 typedef CIndexHandle<navi_type> node_type; 00219 typedef CIndexCacheHandle<navi_type> node_cache_type; 00221 00223 CDegreeCache(const manager_type& mgr): base(mgr) {} 00224 00226 CDegreeCache(const self& rhs): base(rhs) {} 00227 00229 ~CDegreeCache() {} 00230 00232 node_type find(input_node_type navi) const{ 00233 return node_type(base::find(navi), base::manager()); } 00234 00235 node_type find(navi_type navi) const{ 00236 return node_type(base::find(navi), base::manager()); } 00237 00239 void insert(input_node_type navi, deg_type deg) const { 00240 base::insert(navi, node_cache_type(deg, base::manager())); 00241 } 00242 00244 void insert(navi_type navi, deg_type deg) const { 00245 base::insert(navi, node_cache_type(deg, base::manager())); 00246 } 00247 00248 }; 00249 00250 00251 00252 00253 template <class TagType = typename CCacheTypes::block_degree, 00254 class DDType = typename CTypes::dd_type> 00255 class CBlockDegreeCache: 00256 public CCacheManagement<TagType, 2> { 00257 00258 public: 00260 00261 typedef DDType dd_type; 00262 typedef TagType tag_type; 00263 typedef CCacheManagement<tag_type, 2> base; 00264 typedef CBlockDegreeCache<tag_type, dd_type> self; 00266 00268 00269 typedef typename base::node_type input_node_type; 00270 typedef typename base::manager_type manager_type; 00271 typedef typename dd_type::idx_type idx_type; 00272 typedef typename dd_type::size_type size_type; 00273 typedef typename dd_type::navigator navi_type; 00274 typedef CIndexHandle<navi_type> node_type; 00275 typedef CIndexCacheHandle<navi_type> node_cache_type; 00277 00279 CBlockDegreeCache(const manager_type& mgr): base(mgr) {} 00280 00282 CBlockDegreeCache(const self& rhs): base(rhs) {} 00283 00285 ~CBlockDegreeCache() {} 00286 00288 node_type find(input_node_type navi, idx_type idx) const{ 00289 return node_type(base::find(navi, node_cache_type(idx, base::manager())), 00290 base::manager()); } 00291 00292 node_type find(navi_type navi, idx_type idx) const{ 00293 return node_type(base::find(navi, node_cache_type(idx, base::manager())), 00294 base::manager()); } 00295 00297 void insert(input_node_type navi, idx_type idx, size_type deg) const { 00298 base::insert(navi, node_cache_type(idx, base::manager()), 00299 node_cache_type(deg, base::manager())); 00300 } 00301 00303 void insert(navi_type navi, idx_type idx, size_type deg) const { 00304 base::insert(navi, node_cache_type(idx, base::manager()), 00305 node_cache_type(deg, base::manager())); 00306 } 00307 }; 00308 00309 template <class TagType, 00310 class DDType = typename CTypes::dd_type> 00311 class CDegreeArgumentCache: 00312 public CCacheManagement<TagType, 2> { 00313 00314 public: 00316 00317 typedef DDType dd_type; 00318 typedef TagType tag_type; 00319 typedef CCacheManagement<tag_type, 2> base; 00320 typedef CDegreeArgumentCache<tag_type, dd_type> self; 00322 00324 00325 typedef typename base::node_type node_type; 00326 typedef typename base::manager_type manager_type; 00327 typedef typename dd_type::size_type size_type; 00328 typedef typename dd_type::navigator navi_type; 00329 typedef CIndexCacheHandle<navi_type> degree_node_type; 00331 00333 CDegreeArgumentCache(const manager_type& mgr): base(mgr) {} 00334 00336 CDegreeArgumentCache(const self& rhs): base(rhs) {} 00337 00339 ~CDegreeArgumentCache() {} 00340 00342 navi_type find(navi_type navi, size_type deg) const{ 00343 return base::find(navi, degree_node_type(deg, base::manager())); 00344 } 00345 00347 void insert(navi_type navi, size_type deg, navi_type result) const { 00348 base::insert(navi, degree_node_type(deg, base::manager()), result); 00349 } 00350 00351 }; 00352 00353 00354 END_NAMESPACE_PBORI 00355 00356 #endif