PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00153 //***************************************************************************** 00154 00155 // get polybori definitions 00156 #include "pbori_defs.h" 00157 00158 // get polybori properties 00159 #include "pbori_traits.h" 00160 00161 // get standard string and string stream functionality 00162 #include <string> 00163 #include <sstream> 00164 00165 00166 // get map/hash_map functionality from stl/stl-ext 00167 #define HAVE_HASH_MAP 1 00168 #ifdef HAVE_HASH_MAP 00169 # include <ext/hash_map> 00170 #else 00171 # include <map> 00172 #endif 00173 00174 #ifndef pbori_func_h_ 00175 #define pbori_func_h_ 00176 00177 BEGIN_NAMESPACE_PBORI 00178 00181 template <class ListType, class ValueType = typename ListType::value_type > 00182 class push_back { 00183 public: 00184 00185 ListType 00186 operator()(ListType theList, const ValueType& elt) const { 00187 theList.push_back(elt); 00188 return theList; 00189 } 00190 }; 00191 00194 template <class RhsType, class LhsType = typename RhsType::idx_type > 00195 class change_idx { 00196 public: 00197 00198 RhsType operator() (const RhsType& rhs, const LhsType& lhs) const { 00199 return (rhs.change(lhs)); 00200 } 00201 00202 }; 00203 00206 template <class RhsType = void, 00207 class LhsType = typename pbori_traits<RhsType>::idx_type > 00208 class change_assign; 00209 00210 // default variant 00211 template <class RhsType, class LhsType> 00212 class change_assign { 00213 public: 00214 00215 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00216 return (rhs.changeAssign(lhs)); 00217 } 00218 00219 }; 00220 00221 // template specialization 00222 template<> 00223 class change_assign<void, pbori_traits<void>::idx_type> { 00224 public: 00225 00226 template <class RhsType, class LhsType> 00227 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00228 return (rhs.changeAssign(lhs)); 00229 } 00230 00231 }; 00232 00235 template <class RhsType, class LhsType = typename RhsType::idx_type> 00236 class subset1_assign { 00237 public: 00238 00239 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00240 (rhs.subset1Assign(lhs)); 00241 return rhs; 00242 } 00243 }; 00244 00247 template <class RhsType, class LhsType> 00248 class subset0_assign { 00249 public: 00250 00251 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00252 return (rhs.subset0Assign(lhs)); 00253 } 00254 }; 00257 template <class RhsType, 00258 class LhsType = typename pbori_traits<RhsType>::idx_type > 00259 class unite_assign: 00260 public std::binary_function<RhsType&, const LhsType&, RhsType&> { 00261 00262 public: 00263 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00264 return (rhs.uniteAssign(lhs)); 00265 } 00266 }; 00267 00268 00269 // @class project_ith 00275 00276 template <unsigned int ITH, unsigned int NLEN = ITH> 00277 class project_ith; 00278 00281 template <unsigned int NLEN> 00282 class project_ith<0, NLEN> { 00283 00284 public: 00286 template <class ValueType> 00287 void operator() (const ValueType&, ...) const { } 00288 }; 00289 00292 template <unsigned int NLEN> 00293 class project_ith<1, NLEN> { 00294 00295 public: 00297 template <class ValueType> 00298 const ValueType& operator() (const ValueType& value, ...) const { 00299 return value; 00300 } 00301 00303 template <class ValueType> 00304 ValueType& operator() (ValueType& value, ...) const { 00305 return value; 00306 } 00307 }; 00308 00309 00312 template <unsigned int NLEN> 00313 class project_ith<2, NLEN> { 00314 00315 public: 00317 template <class FirstType, class ValueType> 00318 const ValueType& 00319 operator() (const FirstType&, const ValueType& value, ...) const { 00320 return value; 00321 } 00322 00324 template <class FirstType, class ValueType> 00325 ValueType& operator() (const FirstType&, ValueType& value, ...) const { 00326 return value; 00327 } 00328 }; 00329 00330 00333 template <unsigned int NLEN> 00334 class project_ith<3, NLEN> { 00335 00336 public: 00338 template <class FirstType, class SecondType, class ValueType> 00339 const ValueType& 00340 operator() (const FirstType&, const SecondType&, 00341 const ValueType& value, ...) const { 00342 return value; 00343 } 00344 00346 template <class FirstType, class SecondType, class ValueType> 00347 ValueType& operator() (const FirstType&, const SecondType&, 00348 ValueType& value, ...) const { 00349 return value; 00350 } 00351 }; 00352 00353 /* 00354 class print_all { 00355 public: 00356 00357 print_all(std::ostream& os_):os(os_){} 00358 00359 template<class Type> 00360 Type& operator()(Type& val){ 00361 std::copy(val.begin(), val.end(), 00362 std::ostream_iterator<typename Type::value_type>(os, ", ")); 00363 return val; 00364 } 00365 std::ostream& os; 00366 }; 00367 */ 00368 00371 class dummy_iterator { 00372 public: 00373 00375 typedef dummy_iterator self; 00376 00377 template <class Type> 00378 const self& operator=(const Type&) const { return *this;} 00379 00380 const self& operator*() const { return *this;} 00381 const self& operator++() const { return *this;} 00382 const self& operator++(int) const { return *this;} 00383 }; 00384 00385 template <> 00386 class pbori_traits<dummy_iterator>: 00387 public CTypes { 00388 }; 00389 00395 template <class IntType, IntType INTCONST, class ResultType = IntType> 00396 struct integral_constant { 00397 00398 typedef ResultType result_type; 00399 result_type operator()(...) const { return INTCONST; } 00400 }; 00401 00405 template <class BinaryOp, class FirstOp, class SecondOp> 00406 class binary_composition: 00407 public BinaryOp { 00408 00409 public: 00410 00412 00413 typedef BinaryOp base; 00414 typedef FirstOp first_op_type; 00415 typedef SecondOp second_op_type; 00417 00418 // Constructor 00419 binary_composition(const base& binop = base(), 00420 const first_op_type& unop1 = first_op_type(), 00421 const second_op_type& unop2 = second_op_type() ): 00422 base(binop), first_op(unop1), second_op(unop2) {} 00423 00425 typedef typename base::result_type result_type; 00426 00428 template <class FirstType, class SecondType> 00429 result_type operator()(const FirstType& first, 00430 const SecondType& second) const { 00431 return base::operator()(first_op(first), second_op(second)); 00432 } 00433 00435 template <class FirstType, class SecondType> 00436 result_type operator()(FirstType& first, 00437 const SecondType& second) const { 00438 return base::operator()(first_op(first), second_op(second)); 00439 } 00440 00442 template <class FirstType, class SecondType> 00443 result_type operator()(const FirstType& first, 00444 SecondType& second) const { 00445 return base::operator()(first_op(first), second_op(second)); 00446 } 00447 00448 protected: 00449 first_op_type first_op; 00450 second_op_type second_op; 00451 }; 00452 00456 template <class BinaryOp, class UnaryOperation> 00457 class symmetric_composition: 00458 public binary_composition<BinaryOp, UnaryOperation, UnaryOperation> { 00459 00460 public: 00461 00463 00464 typedef BinaryOp binary_op_type; 00465 typedef UnaryOperation unary_op_type; 00466 typedef binary_composition<binary_op_type, unary_op_type, unary_op_type> 00467 base; 00469 00470 // Constructor 00471 symmetric_composition(const binary_op_type& binop = binary_op_type(), 00472 const unary_op_type& unop = unary_op_type() ): 00473 base(binop, unop, unop) {} 00474 }; 00475 00478 template<class ValueType> 00479 class maximum_iteration { 00480 public: 00481 maximum_iteration(ValueType & init) : max(init){} 00482 00483 ValueType& operator()(const ValueType& val) const { 00484 return max = std::max(max, val); 00485 } 00486 00487 private: 00488 ValueType & max; 00489 }; 00490 00493 template <class DDType> 00494 class dd_add_assign { 00495 public: 00496 00497 DDType& operator()(DDType& lhs, const DDType& rhs) const { 00498 // several possible implementations 00499 return 00500 #ifdef PBORI_ADD_BY_ITE 00501 lhs.iteAssign(lhs.diff(rhs), rhs); 00502 00503 # elif defined(PBORI_ADD_BY_OR) 00504 (lhs = (lhs.diff(rhs)).unite(rhs.diff(lhs))); 00505 00506 # elif defined(PBORI_ADD_BY_UNION) 00507 (lhs = lhs.unite(rhs).diff( lhs.intersect(rhs) ) ); 00508 # elif defined(PBORI_ADD_BY_EXTRA_XOR) || defined(PBORI_ADD_BY_XOR) 00509 (lhs = lhs.Xor(rhs)); 00510 #endif 00511 } 00512 }; 00513 00516 template <class DDType, class IdxType = typename DDType::idx_type> 00517 class times_indexed_var { 00518 public: 00519 00520 DDType& operator()(DDType& lhs, IdxType idx) const { 00521 00522 // get all terms not containing the variable with index idx 00523 DDType tmp( lhs.subset0(idx) ); 00524 00525 // get the complementary terms 00526 lhs.diffAssign(tmp); 00527 00528 // construct polynomial terms 00529 dd_add_assign<DDType>()(lhs, tmp.change(idx)); 00530 00531 return lhs; 00532 } 00533 00534 }; 00535 00538 template <class DDType, class IdxType = typename DDType::idx_type> 00539 class append_indexed_divisor { 00540 public: 00541 00542 DDType& operator()(DDType& lhs, IdxType idx) const { 00543 00544 lhs.uniteAssign( lhs.change(idx) ); 00545 return lhs; 00546 } 00547 00548 }; 00549 00552 // template <class RhsType = void, 00553 // class LhsType = typename RhsType::value_type > 00554 // class inserts: 00555 // public std::binary_function<RhsType&, const LhsType&, RhsType&> { 00556 // public: 00557 00558 // RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00559 // rhs.insert(lhs); 00560 // return rhs; 00561 // } 00562 00563 // }; 00564 00565 00568 template <class RhsType = void, 00569 class LhsType = typename pbori_traits<RhsType>::idx_type > 00570 class inserts; 00571 00572 template <class RhsType, class LhsType> 00573 class inserts: 00574 public std::binary_function<RhsType&, const LhsType&, RhsType&> { 00575 public: 00576 00577 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00578 rhs.insert(lhs); 00579 return rhs; 00580 } 00581 }; 00582 00583 template <> 00584 class inserts<void, pbori_traits<void>::idx_type> { 00585 public: 00586 template <class RhsType, class LhsType> 00587 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00588 rhs.insert(lhs); 00589 return rhs; 00590 } 00591 }; 00592 00593 00596 template <class RhsType = void, 00597 class LhsType = typename pbori_traits<RhsType>::idx_type > 00598 class insert_assign; 00599 00600 template <class RhsType, class LhsType> 00601 class insert_assign: 00602 public std::binary_function<RhsType&, const LhsType&, RhsType&> { 00603 public: 00604 00605 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00606 rhs.insertAssign(lhs); 00607 return rhs; 00608 } 00609 }; 00610 00611 template <> 00612 class insert_assign<void, pbori_traits<void>::idx_type> { 00613 public: 00614 template <class RhsType, class LhsType> 00615 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00616 rhs.insertAssign(lhs); 00617 return rhs; 00618 } 00619 }; 00620 00621 00622 00625 template <class RhsType = void, 00626 class LhsType = typename pbori_traits<RhsType>::idx_type > 00627 class removes; 00628 00629 00630 template <class RhsType, class LhsType> 00631 class removes: 00632 public std::binary_function<RhsType&, const LhsType&, RhsType&> { 00633 public: 00634 00635 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00636 rhs.remove(lhs); 00637 return rhs; 00638 } 00639 }; 00640 00641 00642 template <> 00643 class removes<void, pbori_traits<void>::idx_type> { 00644 public: 00645 00646 template <class RhsType, class LhsType> 00647 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00648 rhs.remove(lhs); 00649 return rhs; 00650 } 00651 }; 00652 00655 template <class RhsType = void, 00656 class LhsType = typename pbori_traits<RhsType>::idx_type > 00657 class remove_assign; 00658 00659 00660 template <class RhsType, class LhsType> 00661 class remove_assign: 00662 public std::binary_function<RhsType&, const LhsType&, RhsType&> { 00663 public: 00664 00665 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00666 rhs.removeAssign(lhs); 00667 return rhs; 00668 } 00669 }; 00670 00671 00672 template <> 00673 class remove_assign<void, pbori_traits<void>::idx_type> { 00674 public: 00675 00676 template <class RhsType, class LhsType> 00677 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00678 rhs.removeAssign(lhs); 00679 return rhs; 00680 } 00681 }; 00682 00685 template <class ListType, class RhsType, class LhsType> 00686 class insert_second_to_list { 00687 public: 00688 00689 insert_second_to_list(ListType& theList__): 00690 theList(theList__) {}; 00691 00692 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00693 theList.insert(lhs); 00694 return rhs; 00695 } 00696 00697 private: 00698 ListType& theList; 00699 }; 00700 00701 00705 template <class Type1, class Type2> 00706 class is_same_type; 00707 00708 template <class Type> 00709 class is_same_type<Type, Type>: 00710 public integral_constant<CTypes::bool_type, true> {}; 00711 00712 template <class Type1, class Type2> 00713 class is_same_type: 00714 public integral_constant<CTypes::bool_type, false> {}; 00715 00716 00720 template <class Type1, class Type2, class ThenType, class ElseType> 00721 class on_same_type; 00722 00723 template <class Type, class ThenType, class ElseType> 00724 class on_same_type<Type, Type, ThenType, ElseType> { 00725 public: 00726 typedef ThenType type; 00727 }; 00728 00729 template <class Type1, class Type2, class ThenType, class ElseType> 00730 class on_same_type { 00731 public: 00732 typedef ElseType type; 00733 }; 00734 00735 00739 struct internal_tag {}; 00740 00744 template<class Type> 00745 struct type_tag {}; 00746 00747 template <class Type> 00748 class hashes { 00749 public: 00750 00751 typedef typename Type::hash_type hash_type; 00752 00753 hash_type operator() (const Type& rhs) const{ 00754 return rhs.hash(); 00755 } 00756 }; 00757 00758 template <class Type> 00759 class lm_hashes { 00760 public: 00761 00762 typedef typename Type::hash_type hash_type; 00763 00764 hash_type operator() (const Type& rhs) const{ 00765 return rhs.lmHash(); 00766 } 00767 }; 00768 00769 template <class Type> 00770 class generate_index_map { 00771 00772 typedef typename Type::idx_type idx_type; 00773 public: 00775 #ifdef HAVE_HASH_MAP 00776 typedef __gnu_cxx::hash_map<Type, idx_type, hashes<Type> > type; 00777 #else 00778 typedef std::map<Type, idx_type> type; 00779 #endif 00780 }; 00781 00785 template <class ListType> 00786 class sizes_less: 00787 public std::binary_function<const ListType&, const ListType&, bool> { 00788 00789 public: 00790 bool operator()(const ListType& lhs, const ListType& rhs) const { 00791 return (lhs.size() < rhs.size()); 00792 } 00793 }; 00794 00798 template <class BiIterator> 00799 class reversed_iteration_adaptor { 00800 public: 00801 00803 typedef BiIterator iterator; 00804 00806 typedef reversed_iteration_adaptor<iterator> self; 00808 00809 typedef std::bidirectional_iterator_tag iterator_category; 00810 typedef typename std::iterator_traits<iterator>::difference_type 00811 difference_type; 00812 typedef typename std::iterator_traits<iterator>::pointer pointer; 00813 typedef typename std::iterator_traits<iterator>::reference reference; 00814 typedef typename std::iterator_traits<iterator>::value_type value_type; 00816 00818 reversed_iteration_adaptor(const iterator& iter): 00819 m_iter(iter) {} 00820 00822 00823 reference operator*() const { 00824 return *m_iter; 00825 } 00826 00828 self& operator++() { 00829 --m_iter; 00830 return *this; 00831 } 00832 00834 self& operator--() { 00835 ++m_iter; 00836 return *this; 00837 } 00838 00839 bool operator==(const self& rhs) const { 00840 return m_iter == rhs.m_iter; 00841 } 00842 00843 bool operator!=(const self& rhs) const { 00844 return m_iter != rhs.m_iter; 00845 } 00846 iterator get() const { 00847 return m_iter; 00848 } 00849 00850 protected: 00851 iterator m_iter; 00852 }; 00853 00854 00855 template <class DDType> 00856 class navigates: 00857 public std::unary_function<DDType, typename DDType::navigator> { 00858 public: 00860 typedef DDType dd_type; 00861 00863 typedef typename DDType::navigator navigator; 00864 00866 typedef std::unary_function<dd_type, navigator> base; 00867 00869 typename base::result_type operator()(const dd_type& rhs) const{ 00870 return rhs.navigation(); 00871 } 00872 00873 }; 00874 00875 00876 template <class ValueType> 00877 class default_value { 00878 public: 00879 typedef ValueType value_type; 00880 00881 value_type operator()(...) const{ 00882 return value_type(); 00883 } 00884 00885 }; 00886 00887 template <template<class> class BindType, class BinaryFunction, 00888 class ValueType, class ConstantOp> 00889 class constant_binder_base : 00890 public BindType<BinaryFunction>{ 00891 public: 00892 typedef BinaryFunction bin_op; 00893 typedef ConstantOp const_type; 00894 typedef BindType<bin_op> base; 00895 00896 typedef ValueType value_type; 00897 00898 constant_binder_base(const bin_op& op = bin_op()): base(op, const_type()()) {} 00899 }; 00900 00901 template <class BinaryFunction, class ConstantOp> 00902 class constant_binder2nd : 00903 public constant_binder_base<std::binder2nd, BinaryFunction, 00904 typename BinaryFunction::second_argument_type, 00905 ConstantOp> { 00906 }; 00907 00908 00909 template <class BinaryFunction, class ConstantOp> 00910 class constant_binder1st : 00911 public constant_binder_base<std::binder1st, BinaryFunction, 00912 typename BinaryFunction::first_argument_type, 00913 ConstantOp> { 00914 }; 00915 00916 template <template<class> class BindType, 00917 class BinaryFunction, class ValueType> 00918 class default_binder_base : 00919 public BindType<BinaryFunction>{ 00920 public: 00921 typedef BinaryFunction bin_op; 00922 typedef BindType<bin_op> base; 00923 00924 typedef ValueType value_type; 00925 00926 default_binder_base(const value_type& val): base(bin_op(), val) {} 00927 }; 00928 00929 template <class BinaryFunction> 00930 class default_binder2nd : 00931 public default_binder_base<std::binder2nd, BinaryFunction, 00932 typename BinaryFunction::second_argument_type> { 00933 public: 00934 typedef default_binder_base<std::binder2nd, BinaryFunction, 00935 typename BinaryFunction::second_argument_type> 00936 base; 00937 00938 default_binder2nd(const typename base::value_type& val): base(val) {} 00939 }; 00940 00941 00942 template <class BinaryFunction> 00943 class default_binder1st : 00944 public default_binder_base<std::binder1st, BinaryFunction, 00945 typename BinaryFunction::first_argument_type> { 00946 }; 00947 00948 // /** @class property_owner 00949 // * @brief defines generic base for properties 00950 // **/ 00951 // template <class ValidityTag> 00952 // class property_owner { 00953 // public: 00954 00955 // /// Set marker for validity 00956 // typedef typename 00957 // on_same_type<ValidityTag, valid_tag, valid_tag, invalid_tag>::type property; 00958 00959 // /// Generate Boolean member function 00960 // is_same_type<property, valid_tag> hasProperty; 00961 // }; 00962 00966 template <class ManagerType, 00967 class IdxType = typename ManagerType::idx_type, 00968 class VarNameType = typename ManagerType::const_varname_reference> 00969 class variable_name { 00970 public: 00971 typedef ManagerType manager_type; 00972 typedef IdxType idx_type; 00973 typedef VarNameType varname_type; 00974 00976 variable_name(const manager_type& mgr): m_mgr(mgr) {} 00977 00979 varname_type operator()(idx_type idx) const{ 00980 return m_mgr.getName(idx); 00981 } 00982 00983 protected: 00985 const manager_type& m_mgr; 00986 }; 00987 00988 template <class MapType, class VariableType, class TermType, class NodeType> 00989 class mapped_new_node { 00990 public: 00991 typedef MapType map_type; 00992 typedef NodeType node_type; 00993 00994 typedef typename node_type::idx_type idx_type; 00995 00996 mapped_new_node(const map_type& the_map): m_map(the_map) {} 00997 00998 NodeType operator()(idx_type idx, 00999 const node_type& first, const node_type& second) const{ 01000 return ((TermType)VariableType(m_map[idx]))*first + second; 01001 } 01002 01003 01004 01005 private: 01006 const map_type& m_map; 01007 }; 01008 01009 01014 template <class NewType> 01015 struct pbori_base; 01016 01017 01018 01019 template <class DDType> 01020 class get_node { 01021 01022 public: 01023 typename DDType::node_type operator()(const DDType& rhs) const { 01024 return rhs.getNode(); 01025 } 01026 }; 01027 01028 template<unsigned ErrorNumber = CUDD_INTERNAL_ERROR> 01029 struct handle_error { 01030 typedef mgrcore_traits<Cudd>::errorfunc_type errorfunc_type; 01031 01032 handle_error(errorfunc_type errfunc): m_errfunc(errfunc) {} 01033 01034 bool found(unsigned err) const { 01035 if UNLIKELY(err == ErrorNumber) { 01036 m_errfunc(cudd_error_traits<ErrorNumber>()()); 01037 return true; 01038 } 01039 return false; 01040 } 01041 01042 void operator()(unsigned err) const { 01043 if UNLIKELY(err == ErrorNumber) 01044 m_errfunc(cudd_error_traits<ErrorNumber>()()); 01045 else 01046 reinterpret_cast<const handle_error<ErrorNumber - 1>&>(*this)(err); 01047 } 01048 01049 protected: 01050 const errorfunc_type m_errfunc; 01051 }; 01052 01053 01054 template<> 01055 struct handle_error<0> { 01056 typedef mgrcore_traits<Cudd>::errorfunc_type errorfunc_type; 01057 01058 handle_error(errorfunc_type errfunc): m_errfunc(errfunc) {} 01059 01060 void operator()(unsigned err) const { 01061 if LIKELY(err == 0) 01062 m_errfunc(cudd_error_traits<0>()()); 01063 } 01064 protected: 01065 errorfunc_type m_errfunc; 01066 }; 01067 01068 01069 END_NAMESPACE_PBORI 01070 01071 #endif