PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00114 //***************************************************************************** 00115 00116 // include basic definitions 00117 #include "pbori_defs.h" 00118 00119 // get decision diagram manager interface 00120 #include "CDDManager.h" 00121 00122 #include "BoolePolynomial.h" 00123 00124 #include "BooleMonomial.h" 00125 00126 #include "BooleExponent.h" 00127 00128 #include "COrderProperties.h" 00129 #include "CVariableNames.h" 00130 00131 #include "CGenericIter.h" 00132 00133 //#include "CIndirectIter.h" 00134 00135 00136 00137 00138 #include <vector> 00139 #ifndef OrderedManager_h_ 00140 #define OrderedManager_h_ 00141 #include "COrderedIter.h" 00142 BEGIN_NAMESPACE_PBORI 00143 00144 template <class IdxType, class OrderType> 00145 bool 00146 lie_in_same_block(IdxType, IdxType, const OrderType&, 00147 invalid_tag) { // not a block order 00148 return true; 00149 } 00150 00151 00152 template <class IdxType, class OrderType> 00153 bool 00154 lie_in_same_block(IdxType first, IdxType second, const OrderType& order, 00155 valid_tag) { // is block order 00156 if (second < first) 00157 std::swap(first, second); 00158 00159 typename OrderType::block_iterator upper(order.blockBegin()); 00160 while (first >= *upper) // Note: convention, last element is max_idx 00161 ++upper; 00162 return (second < *upper); 00163 } 00164 00170 // template <class ManType> 00171 // class CNamedManager: 00172 // public CDDManager<ManType> { 00173 00174 // public: 00175 00176 // /// Variable manager type 00177 // typedef ManType manager_type; 00178 00179 // /// Variable manager interface (base type) 00180 // typedef CDDManager<manager_type> base; 00181 00182 // /// Type of *this 00183 // typedef CNamedManager<manager_type> self; 00184 00185 // /// @name adopt global type definitions 00186 // //@{ 00187 // typedef CTypes::bool_type bool_type; 00188 // typedef CTypes::dd_type dd_type; 00189 // typedef CTypes::size_type size_type; 00190 // typedef CTypes::idx_type idx_type; 00191 // typedef CTypes::comp_type comp_type; 00192 // typedef CTypes::ordercode_type ordercode_type; 00193 // typedef BooleMonomial monom_type; 00194 // typedef BoolePolynomial poly_type; 00195 // typedef BoolePolynomial::navigator navigator; 00196 // typedef BooleExponent exp_type; 00197 // //@} 00198 00199 // /// Define type for storing names of variables 00200 // typedef CVariableNames variable_names_type; 00201 00202 // /// Define type for getting names of variables 00203 // typedef variable_names_type::const_reference const_varname_reference; 00204 00205 // /// Construct new decision diagramm manager 00206 // CNamedManager(size_type nvars = 0): 00207 // base(nvars) { } 00208 00209 // /// Construct old decision diagramm manager 00210 // CNamedManager(const base& rhs): 00211 // base(rhs) { } 00212 00213 00214 // /// Construct new decision diagramm manager 00215 // CNamedManager(const self& rhs): 00216 // base(rhs) { } 00217 00218 // // Destructor 00219 // ~CNamedManager() { } 00220 00221 // /// Set name of variable with index idx 00222 // void setVariableName(idx_type idx, const_varname_reference varname) { 00223 // base::manager().names().set(idx, varname); 00224 // } 00225 00226 // /// Get name of variable with index idx 00227 // const_varname_reference getVariableName(idx_type idx) const { 00228 // return base::manager().names()[idx]; 00229 // } 00230 00231 // private: 00232 // /// Stores names of variables 00233 // //variable_names_type m_names; 00234 // }; 00235 00236 00243 class CDynamicOrderBase { 00244 00245 public: 00246 00248 typedef CDynamicOrderBase self; 00249 00251 00252 typedef CTypes::bool_type bool_type; 00253 typedef CTypes::size_type size_type; 00254 typedef CTypes::idx_type idx_type; 00255 typedef CTypes::comp_type comp_type; 00256 typedef CTypes::ordercode_type ordercode_type; 00257 typedef BoolePolynomial poly_type; 00258 typedef poly_type::monom_type monom_type; 00259 typedef poly_type::navigator navigator; 00260 typedef poly_type::exp_type exp_type; 00261 00262 00263 typedef COrderedIter<navigator, monom_type> ordered_iterator; 00264 typedef COrderedIter<navigator, exp_type> ordered_exp_iterator; 00266 00268 typedef std::vector<idx_type> block_idx_type; 00269 00271 typedef block_idx_type::const_iterator block_iterator; 00272 00273 00275 CDynamicOrderBase() { } 00276 00277 // Destructor 00278 virtual ~CDynamicOrderBase() { } 00279 00281 virtual comp_type compare(idx_type, idx_type) const = 0; 00282 00283 virtual comp_type compare(const monom_type&, const monom_type&) const = 0; 00284 00285 virtual comp_type compare(const exp_type&, const exp_type&) const = 0; 00286 00288 virtual monom_type lead(const poly_type&) const = 0; 00289 00291 virtual monom_type lead(const poly_type&, size_type) const = 0; 00292 00294 virtual exp_type leadExp(const poly_type&) const = 0; 00295 00297 virtual exp_type leadExp(const poly_type&, size_type) const = 0; 00298 00300 virtual poly_type leadFirst(const poly_type&) const = 0; 00301 00303 virtual bool_type isLexicographical() const = 0; 00304 00306 virtual bool_type orderedStandardIteration() const = 0; 00307 00309 virtual bool_type isSymmetric() const = 0; 00310 00312 virtual bool_type isDegreeOrder() const = 0; 00313 00315 virtual bool_type isBlockOrder() const = 0; 00316 00318 virtual bool_type isTotalDegreeOrder() const = 0; 00319 00321 virtual bool_type ascendingVariables() const = 0; 00322 00324 virtual bool_type descendingVariables() const = 0; 00325 00327 virtual bool_type isDegreeReverseLexicograpical() const = 0; 00328 00330 virtual ordered_iterator leadIteratorBegin(const poly_type&) const = 0; 00331 00332 virtual ordered_iterator leadIteratorEnd() const = 0; 00333 virtual ordered_exp_iterator leadExpIteratorBegin(const poly_type&) const = 0; 00334 00335 virtual ordered_exp_iterator leadExpIteratorEnd() const = 0; 00336 00338 virtual ordercode_type getOrderCode() const = 0; 00339 00341 virtual ordercode_type getBaseOrderCode() const = 0 ; 00342 00344 00345 virtual block_iterator blockBegin() const = 0; 00346 virtual block_iterator blockEnd() const = 0; 00347 virtual void appendBlock(idx_type) = 0; 00348 virtual void clearBlocks() = 0; 00350 00353 virtual bool_type lieInSameBlock(idx_type, idx_type) const = 0; 00354 00355 }; 00356 00363 template <class OrderType> 00364 class CDynamicOrder: 00365 public CDynamicOrderBase { 00366 00367 public: 00368 00369 00371 typedef OrderType order_type; 00372 00374 typedef CDynamicOrderBase base; 00375 00377 typedef CDynamicOrder<order_type> self; 00378 00380 typedef COrderProperties<order_type> properties_type; 00381 00383 00384 typedef typename base::bool_type bool_type; 00385 typedef typename base::size_type size_type; 00386 typedef typename base::idx_type idx_type; 00387 typedef typename base::comp_type comp_type; 00388 typedef typename base::monom_type monom_type; 00389 typedef typename base::poly_type poly_type; 00390 typedef typename base::exp_type exp_type; 00391 typedef typename base::ordered_iterator ordered_iterator; 00392 typedef typename base::ordered_exp_iterator ordered_exp_iterator; 00393 typedef typename base::ordercode_type ordercode_type; 00394 typedef typename base::block_iterator block_iterator; 00396 00398 CDynamicOrder( const order_type& theOrder = order_type() ): 00399 ordering(theOrder) { } 00400 00402 CDynamicOrder(const self& rhs): 00403 ordering(rhs.ordering) { } 00404 00405 // Destructor 00406 ~CDynamicOrder() { } 00407 00409 comp_type compare(idx_type lhs, idx_type rhs) const { 00410 return ordering.compare(lhs, rhs); 00411 } 00412 00414 comp_type compare(const monom_type& lhs, const monom_type& rhs) const { 00415 return ordering.compare(lhs, rhs); 00416 } 00417 00418 comp_type compare(const exp_type& lhs, const exp_type& rhs) const { 00419 return ordering.compare(lhs, rhs); 00420 } 00421 00423 monom_type lead(const poly_type& rhs) const { 00424 00425 return ordering.lead(rhs); 00426 } 00428 monom_type lead(const poly_type& rhs, size_type bound) const { 00429 00430 return ordering.lead(rhs, bound); 00431 } 00432 00434 exp_type leadExp(const poly_type& rhs) const { 00435 00436 return ordering.leadExp(rhs); 00437 } 00438 00440 exp_type leadExp(const poly_type& rhs, size_type bound) const { 00441 00442 return ordering.leadExp(rhs, bound); 00443 } 00444 00446 poly_type leadFirst(const poly_type& poly) const { 00447 00448 if(orderedStandardIteration()) 00449 return poly; 00450 else 00451 return lead(poly); 00452 } 00453 00455 bool_type isLexicographical() const { 00456 return properties_type().isLexicographical(); 00457 } 00458 00460 bool_type orderedStandardIteration() const { 00461 return properties_type().orderedStandardIteration(); 00462 } 00463 00465 bool_type isSymmetric() const { 00466 return properties_type().isSymmetric(); 00467 } 00468 00470 bool_type isDegreeOrder() const { 00471 return properties_type().isDegreeOrder(); 00472 } 00473 00475 bool_type isBlockOrder() const { 00476 return properties_type().isBlockOrder(); 00477 } 00478 00480 bool_type isTotalDegreeOrder() const { 00481 return properties_type().isTotalDegreeOrder(); 00482 } 00483 00485 bool_type isDegreeReverseLexicograpical() const { 00486 return properties_type().isDegreeReverseLexicograpical(); 00487 } 00488 00490 bool_type ascendingVariables() const { 00491 return properties_type().ascendingVariables(); 00492 } 00493 00495 bool_type descendingVariables() const { 00496 return properties_type().descendingVariables(); 00497 } 00498 00500 // iterator leadIterator(const poly_type& poly) const { 00501 // return ordering.leadIterator(poly); 00502 // } 00504 ordered_iterator leadIteratorBegin(const poly_type& poly) const { 00505 return ordering.leadIteratorBegin(poly); 00506 } 00507 00508 ordered_iterator leadIteratorEnd() const { 00509 return ordering.leadIteratorEnd(); 00510 } 00512 ordered_exp_iterator leadExpIteratorBegin(const poly_type& poly) const { 00513 return ordering.leadExpIteratorBegin(poly); 00514 } 00515 00516 ordered_exp_iterator leadExpIteratorEnd() const { 00517 return ordering.leadExpIteratorEnd(); 00518 } 00519 00521 ordercode_type getOrderCode() const { 00522 return order_type::order_code; 00523 } 00524 00526 ordercode_type getBaseOrderCode() const { 00527 return order_type::baseorder_code; 00528 } 00529 00531 00532 block_iterator blockBegin() const { return ordering.blockBegin(); } 00533 block_iterator blockEnd() const { return ordering.blockEnd(); } 00534 void appendBlock(idx_type idx) { ordering.appendBlock(idx); } 00535 void clearBlocks() { ordering.clearBlocks(); } 00537 00540 bool_type lieInSameBlock(idx_type first, idx_type second) const { 00541 return lie_in_same_block(first, second, *this, 00542 typename properties_type::blockorder_property()); 00543 } 00544 00545 protected: 00546 order_type ordering; 00547 }; 00548 00549 END_NAMESPACE_PBORI 00550 00551 #endif