PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00014 //***************************************************************************** 00015 00016 // include basic definitions 00017 #include "pbori_defs.h" 00018 00019 #include "BooleEnv.h" 00020 00021 #include "CCacheManagement.h" 00022 00023 #ifndef CDegreeCache_h_ 00024 #define CDegreeCache_h_ 00025 00026 BEGIN_NAMESPACE_PBORI 00027 //class BoolePolyRing; 00034 template <class NaviType> 00035 class CIndexHandle { 00036 public: 00037 00038 enum { invalid = CTypes::max_idx }; 00039 00041 typedef NaviType navigator; 00042 00044 typedef navigator base; 00045 00047 typedef typename navigator::bool_type bool_type; 00048 00050 typedef typename CTypes::idx_type idx_type; 00051 00053 typedef typename CTypes::size_type size_type; 00054 00056 typedef BoolePolyRing manager_type; 00057 00059 CIndexHandle(idx_type idx): m_idx(idx) {} 00060 00062 explicit CIndexHandle(navigator navi, const manager_type& mgr): 00063 m_idx(fromNode(navi, mgr)) {} 00064 00066 idx_type operator*() const { 00067 return m_idx; 00068 } 00069 00070 bool isValid() const { 00071 return (m_idx != invalid); 00072 } 00073 protected: 00075 idx_type fromNode(navigator navi, const manager_type& mgr) const { 00076 00077 if (!navi.isValid()) 00078 return invalid; 00079 00080 if UNLIKELY(navi.isConstant()) 00081 return mgr.nVariables(); 00082 else 00083 return *navi; 00084 } 00085 00086 00087 00088 idx_type m_idx; 00089 }; 00090 00091 00092 template <class NaviType> 00093 class CIndexCacheHandle { 00094 public: 00095 00097 typedef NaviType navigator; 00098 00100 // typedef navigator base; 00101 00103 typedef typename navigator::bool_type bool_type; 00104 00106 typedef typename navigator::value_type idx_type; 00107 00109 typedef typename navigator::size_type size_type; 00110 00112 typedef BoolePolyRing manager_type; 00113 00115 CIndexCacheHandle(idx_type idx, const manager_type& mgr): 00116 m_navi( toNode(idx, mgr) ) {} 00117 00119 explicit CIndexCacheHandle(navigator navi): 00120 m_navi(navi) {} 00121 00122 operator navigator() const { return m_navi; } 00123 00124 protected: 00126 navigator toNode(idx_type idx, const manager_type& mgr) const { 00127 00128 if LIKELY((size_type)idx < mgr.nVariables()) 00129 return mgr.variable(idx).navigation(); 00130 00131 return mgr.zero().navigation(); 00132 } 00133 00135 navigator m_navi; 00136 }; 00137 00138 template <class DDType> 00139 class CDegreeCache: 00140 public CCacheManagement<BoolePolyRing, typename CCacheTypes::degree, 1> { 00141 typedef CDegreeCache self; 00142 public: 00144 00145 typedef DDType dd_type; 00146 typedef typename CCacheTypes::degree tag_type; 00147 typedef CCacheManagement<BoolePolyRing, tag_type, 1> base; 00149 00151 00152 typedef typename base::node_type input_node_type; 00153 typedef typename base::manager_type manager_type; 00154 typedef typename dd_type::navigator navi_type; 00155 typedef CIndexHandle<navi_type> node_type; 00156 typedef CIndexCacheHandle<navi_type> node_cache_type; 00158 00160 CDegreeCache(const manager_type& mgr): base(mgr) {} 00161 00163 CDegreeCache(const self& rhs): base(rhs) {} 00164 00166 ~CDegreeCache() {} 00167 00169 node_type find(input_node_type navi) const{ 00170 return node_type(base::find(navi), base::manager()); } 00171 00172 node_type find(navi_type navi) const{ 00173 return node_type(base::find(navi), base::manager()); } 00174 00176 void insert(input_node_type navi, deg_type deg) const { 00177 base::insert(navi, node_cache_type(deg, base::manager())); 00178 } 00179 00181 void insert(navi_type navi, deg_type deg) const { 00182 base::insert(navi, node_cache_type(deg, base::manager())); 00183 } 00185 node_type find(input_node_type navi, deg_type) const { return self::find(navi); } 00186 00187 node_type find(navi_type navi, deg_type) const{ return self::find(navi); } 00188 00190 void insert(input_node_type navi, deg_type, deg_type deg) const { 00191 self::insert(navi, deg); 00192 } 00193 00195 void insert(navi_type navi, deg_type, deg_type deg) const { 00196 self::insert(navi, deg); 00197 } 00198 00199 }; 00200 00201 template <class DDType> 00202 class CBoundedDegreeCache: 00203 public CCacheManagement<BoolePolyRing, typename CCacheTypes::degree, 2> { 00204 typedef CBoundedDegreeCache self; 00205 public: 00207 00208 typedef DDType dd_type; 00209 typedef typename CCacheTypes::degree tag_type; 00210 typedef CCacheManagement<BoolePolyRing, tag_type, 2> base; 00212 00214 00215 typedef typename base::node_type input_node_type; 00216 typedef typename base::manager_type manager_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 CBoundedDegreeCache(const manager_type& mgr): base(mgr) {} 00224 00226 CBoundedDegreeCache(const self& rhs): base(rhs) {} 00227 00229 ~CBoundedDegreeCache() {} 00230 00232 node_type find(input_node_type navi, deg_type upper_bound) const{ 00233 return node_type(base::find(navi, 00234 node_cache_type(upper_bound, base::manager())), 00235 base::manager()); 00236 } 00237 00238 node_type find(navi_type navi, deg_type upper_bound) const{ 00239 return node_type(base::find(navi, 00240 node_cache_type(upper_bound, base::manager())), 00241 base::manager()); 00242 } 00243 00245 void insert(input_node_type navi, deg_type upper_bound, deg_type deg) const { 00246 base::insert(navi, node_cache_type(upper_bound, base::manager()), 00247 node_cache_type(deg, base::manager())); 00248 } 00249 00251 void insert(navi_type navi, deg_type upper_bound, deg_type deg) const { 00252 base::insert(navi, node_cache_type(upper_bound, base::manager()), 00253 node_cache_type(deg, base::manager())); 00254 } 00255 00256 }; 00257 00258 00259 template <class DDType> 00260 class CBlockDegreeCache: 00261 public CCacheManagement<BoolePolyRing, 00262 typename CCacheTypes::block_degree, 2> { 00263 00264 public: 00266 00267 typedef DDType dd_type; 00268 typedef typename CCacheTypes::block_degree tag_type; 00269 typedef CCacheManagement<BoolePolyRing, tag_type, 2> base; 00270 typedef CBlockDegreeCache<dd_type> self; 00272 00274 00275 typedef typename base::node_type input_node_type; 00276 typedef typename base::manager_type manager_type; 00277 typedef typename dd_type::navigator navi_type; 00278 typedef CIndexHandle<navi_type> node_type; 00279 typedef CIndexCacheHandle<navi_type> node_cache_type; 00281 00283 CBlockDegreeCache(const manager_type& mgr): base(mgr) {} 00284 00286 CBlockDegreeCache(const self& rhs): base(rhs) {} 00287 00289 ~CBlockDegreeCache() {} 00290 00292 node_type find(input_node_type navi, idx_type idx) const{ 00293 return node_type(base::find(navi, node_cache_type(idx, base::manager())), 00294 base::manager()); } 00295 00296 node_type find(navi_type navi, idx_type idx) const{ 00297 return node_type(base::find(navi, node_cache_type(idx, base::manager())), 00298 base::manager()); } 00299 00301 void insert(input_node_type navi, idx_type idx, size_type deg) const { 00302 base::insert(navi, node_cache_type(idx, base::manager()), 00303 node_cache_type(deg, base::manager())); 00304 } 00305 00307 void insert(navi_type navi, idx_type idx, size_type deg) const { 00308 base::insert(navi, node_cache_type(idx, base::manager()), 00309 node_cache_type(deg, base::manager())); 00310 } 00311 }; 00312 00313 template <class TagType, 00314 class DDType> 00315 class CDegreeArgumentCache: 00316 public CCacheManagement<BoolePolyRing, TagType, 2>, 00317 public CAuxTypes { 00318 00319 public: 00321 00322 typedef DDType dd_type; 00323 typedef TagType tag_type; 00324 typedef CCacheManagement<BoolePolyRing, tag_type, 2> base; 00325 typedef CDegreeArgumentCache<tag_type, dd_type> self; 00327 00329 00330 typedef typename base::node_type node_type; 00331 typedef typename base::manager_type manager_type; 00332 typedef typename dd_type::navigator navi_type; 00333 typedef CIndexCacheHandle<navi_type> degree_node_type; 00335 00337 CDegreeArgumentCache(const manager_type& mgr): base(mgr) {} 00338 00340 CDegreeArgumentCache(const self& rhs): base(rhs) {} 00341 00343 ~CDegreeArgumentCache() {} 00344 00346 navi_type find(navi_type navi, size_type deg) const{ 00347 return base::find(navi, degree_node_type(deg, base::manager())); 00348 } 00349 00351 void insert(navi_type navi, size_type deg, navi_type result) const { 00352 base::insert(navi, degree_node_type(deg, base::manager()), result); 00353 } 00354 00355 }; 00356 00357 00358 END_NAMESPACE_PBORI 00359 00360 #endif