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