PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00013 //***************************************************************************** 00014 00015 // get polybori definitions 00016 #include "pbori_defs.h" 00017 00018 // get polybori properties 00019 #include "pbori_traits.h" 00020 00021 // get standard string and string stream functionality 00022 #include <string> 00023 #include <sstream> 00024 00025 00026 00027 #ifdef HAVE_TR1_UNORDERED_MAP 00028 # include <tr1/unordered_map> 00029 #else 00030 # ifdef HAVE_UNORDERED_MAP 00031 # include <unordered_map> 00032 # else 00033 # ifdef HAVE_HASH_MAP 00034 # include <ext/hash_map> 00035 # else 00036 # include <map> 00037 # endif 00038 # endif 00039 #endif 00040 00041 #ifndef pbori_func_h_ 00042 #define pbori_func_h_ 00043 00044 BEGIN_NAMESPACE_PBORI 00045 00048 template <class ListType, class ValueType = typename ListType::value_type > 00049 class push_back { 00050 public: 00051 00052 ListType 00053 operator()(ListType theList, const ValueType& elt) const { 00054 theList.push_back(elt); 00055 return theList; 00056 } 00057 }; 00058 00061 template <class RhsType, class LhsType = typename RhsType::idx_type > 00062 class change_idx { 00063 public: 00064 00065 RhsType operator() (const RhsType& rhs, const LhsType& lhs) const { 00066 return (rhs.change(lhs)); 00067 } 00068 00069 }; 00070 00073 template <class RhsType = void, 00074 class LhsType = typename pbori_traits<RhsType>::idx_type > 00075 class change_assign; 00076 00077 // default variant 00078 template <class RhsType, class LhsType> 00079 class change_assign { 00080 public: 00081 00082 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00083 return (rhs = rhs.change(lhs)); 00084 } 00085 00086 }; 00087 00088 // template specialization 00089 template<> 00090 class change_assign<void, pbori_traits<void>::idx_type> { 00091 public: 00092 00093 template <class RhsType, class LhsType> 00094 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00095 return (rhs = rhs.change(lhs)); 00096 } 00097 00098 }; 00099 00102 template <class RhsType, class LhsType = typename RhsType::idx_type> 00103 class subset1_assign { 00104 public: 00105 00106 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00107 00108 rhs = rhs.subset1(lhs); 00109 return rhs; 00110 } 00111 }; 00112 00115 template <class RhsType, class LhsType> 00116 class subset0_assign { 00117 public: 00118 00119 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00120 return (rhs = rhs.subset0(lhs)); 00121 } 00122 }; 00125 template <class RhsType, 00126 class LhsType = typename pbori_traits<RhsType>::idx_type > 00127 class unite_assign: 00128 public std::binary_function<RhsType&, const LhsType&, RhsType&> { 00129 00130 public: 00131 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00132 return (rhs = rhs.unite(lhs)); 00133 } 00134 }; 00135 00136 00137 // @class project_ith 00143 00144 template <unsigned int ITH, unsigned int NLEN = ITH> 00145 class project_ith; 00146 00149 template <unsigned int NLEN> 00150 class project_ith<0, NLEN> { 00151 00152 public: 00154 template <class ValueType> 00155 void operator() (const ValueType&, ...) const { } 00156 }; 00157 00160 template <unsigned int NLEN> 00161 class project_ith<1, NLEN> { 00162 00163 public: 00165 template <class ValueType> 00166 const ValueType& operator() (const ValueType& value, ...) const { 00167 return value; 00168 } 00169 00171 template <class ValueType> 00172 ValueType& operator() (ValueType& value, ...) const { 00173 return value; 00174 } 00175 }; 00176 00177 00180 template <unsigned int NLEN> 00181 class project_ith<2, NLEN> { 00182 00183 public: 00185 template <class FirstType, class ValueType> 00186 const ValueType& 00187 operator() (const FirstType&, const ValueType& value, ...) const { 00188 return value; 00189 } 00190 00192 template <class FirstType, class ValueType> 00193 ValueType& operator() (const FirstType&, ValueType& value, ...) const { 00194 return value; 00195 } 00196 }; 00197 00198 00201 template <unsigned int NLEN> 00202 class project_ith<3, NLEN> { 00203 00204 public: 00206 template <class FirstType, class SecondType, class ValueType> 00207 const ValueType& 00208 operator() (const FirstType&, const SecondType&, 00209 const ValueType& value, ...) const { 00210 return value; 00211 } 00212 00214 template <class FirstType, class SecondType, class ValueType> 00215 ValueType& operator() (const FirstType&, const SecondType&, 00216 ValueType& value, ...) const { 00217 return value; 00218 } 00219 }; 00220 00221 /* 00222 class print_all { 00223 public: 00224 00225 print_all(std::ostream& os_):os(os_){} 00226 00227 template<class Type> 00228 Type& operator()(Type& val){ 00229 std::copy(val.begin(), val.end(), 00230 std::ostream_iterator<typename Type::value_type>(os, ", ")); 00231 return val; 00232 } 00233 std::ostream& os; 00234 }; 00235 */ 00236 00239 class dummy_iterator { 00240 public: 00241 00243 typedef dummy_iterator self; 00244 00245 template <class Type> 00246 const self& operator=(const Type&) const { return *this;} 00247 00248 const self& operator*() const { return *this;} 00249 const self& operator++() const { return *this;} 00250 const self& operator++(int) const { return *this;} 00251 }; 00252 00253 template <> 00254 class pbori_traits<dummy_iterator>: 00255 public CTypes { 00256 }; 00257 00263 template <class IntType, IntType INTCONST, class ResultType = IntType> 00264 struct integral_constant { 00265 00266 typedef ResultType result_type; 00267 enum { result = INTCONST }; 00268 result_type operator()(...) const { return result; } 00269 }; 00270 00274 template <class BinaryOp, class FirstOp, class SecondOp> 00275 class binary_composition: 00276 public BinaryOp { 00277 00278 public: 00279 00281 00282 typedef BinaryOp base; 00283 typedef FirstOp first_op_type; 00284 typedef SecondOp second_op_type; 00286 00287 // Constructor 00288 binary_composition(const base& binop = base(), 00289 const first_op_type& unop1 = first_op_type(), 00290 const second_op_type& unop2 = second_op_type() ): 00291 base(binop), first_op(unop1), second_op(unop2) {} 00292 00294 typedef typename base::result_type result_type; 00295 00297 template <class FirstType, class SecondType> 00298 result_type operator()(const FirstType& first, 00299 const SecondType& second) const { 00300 return base::operator()(first_op(first), second_op(second)); 00301 } 00302 00304 template <class FirstType, class SecondType> 00305 result_type operator()(FirstType& first, 00306 const SecondType& second) const { 00307 return base::operator()(first_op(first), second_op(second)); 00308 } 00309 00311 template <class FirstType, class SecondType> 00312 result_type operator()(const FirstType& first, 00313 SecondType& second) const { 00314 return base::operator()(first_op(first), second_op(second)); 00315 } 00316 00317 protected: 00318 first_op_type first_op; 00319 second_op_type second_op; 00320 }; 00321 00325 template <class BinaryOp, class UnaryOperation> 00326 class symmetric_composition: 00327 public binary_composition<BinaryOp, UnaryOperation, UnaryOperation> { 00328 00329 public: 00330 00332 00333 typedef BinaryOp binary_op_type; 00334 typedef UnaryOperation unary_op_type; 00335 typedef binary_composition<binary_op_type, unary_op_type, unary_op_type> 00336 base; 00338 00339 // Constructor 00340 symmetric_composition(const binary_op_type& binop = binary_op_type(), 00341 const unary_op_type& unop = unary_op_type() ): 00342 base(binop, unop, unop) {} 00343 }; 00344 00347 template<class ValueType> 00348 class maximum_iteration { 00349 public: 00350 maximum_iteration(ValueType & init) : max(init){} 00351 00352 ValueType& operator()(const ValueType& val) const { 00353 return max = std::max(max, val); 00354 } 00355 00356 private: 00357 ValueType & max; 00358 }; 00359 00362 template <class DDType> 00363 class dd_add_assign { 00364 public: 00365 00366 DDType& operator()(DDType& lhs, const DDType& rhs) const { 00367 // several possible implementations 00368 return 00369 #if defined(PBORI_ADD_BY_OR) 00370 (lhs = (lhs.diff(rhs)).unite(rhs.diff(lhs))); 00371 00372 # elif defined(PBORI_ADD_BY_UNION) 00373 (lhs = lhs.unite(rhs).diff( lhs.intersect(rhs) ) ); 00374 # elif defined(PBORI_ADD_BY_EXTRA_XOR) || defined(PBORI_ADD_BY_XOR) 00375 (lhs = lhs.Xor(rhs)); 00376 #endif 00377 } 00378 }; 00379 00382 template <class DDType, class IdxType = typename DDType::idx_type> 00383 class times_indexed_var { 00384 public: 00385 00386 DDType& operator()(DDType& lhs, IdxType idx) const { 00387 00388 // get all terms not containing the variable with index idx 00389 DDType tmp( lhs.subset0(idx) ); 00390 00391 // get the complementary terms 00392 lhs = lhs.diff(tmp); 00393 00394 // construct polynomial terms 00395 dd_add_assign<DDType>()(lhs, tmp.change(idx)); 00396 00397 return lhs; 00398 } 00399 00400 }; 00401 00404 template <class DDType, class IdxType = typename DDType::idx_type> 00405 class append_indexed_divisor { 00406 public: 00407 00408 DDType& operator()(DDType& lhs, IdxType idx) const { 00409 00410 lhs = lhs.unite( lhs.change(idx) ); 00411 return lhs; 00412 } 00413 00414 }; 00415 00418 // template <class RhsType = void, 00419 // class LhsType = typename RhsType::value_type > 00420 // class inserts: 00421 // public std::binary_function<RhsType&, const LhsType&, RhsType&> { 00422 // public: 00423 00424 // RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00425 // rhs.insert(lhs); 00426 // return rhs; 00427 // } 00428 00429 // }; 00430 00431 00434 template <class RhsType = void, 00435 class LhsType = typename pbori_traits<RhsType>::idx_type > 00436 class inserts; 00437 00438 template <class RhsType, class LhsType> 00439 class inserts: 00440 public std::binary_function<RhsType&, const LhsType&, RhsType&> { 00441 public: 00442 00443 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00444 rhs.insert(lhs); 00445 return rhs; 00446 } 00447 }; 00448 00449 template <> 00450 class inserts<void, pbori_traits<void>::idx_type> { 00451 public: 00452 template <class RhsType, class LhsType> 00453 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00454 rhs.insert(lhs); 00455 return rhs; 00456 } 00457 }; 00458 00459 00462 template <class RhsType = void, 00463 class LhsType = typename pbori_traits<RhsType>::idx_type > 00464 class insert_assign; 00465 00466 template <class RhsType, class LhsType> 00467 class insert_assign: 00468 public std::binary_function<RhsType&, const LhsType&, RhsType&> { 00469 public: 00470 00471 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00472 rhs.insertAssign(lhs); 00473 return rhs; 00474 } 00475 }; 00476 00477 template <> 00478 class insert_assign<void, pbori_traits<void>::idx_type> { 00479 public: 00480 template <class RhsType, class LhsType> 00481 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00482 rhs.insertAssign(lhs); 00483 return rhs; 00484 } 00485 }; 00486 00487 00488 00491 template <class RhsType = void, 00492 class LhsType = typename pbori_traits<RhsType>::idx_type > 00493 class removes; 00494 00495 00496 template <class RhsType, class LhsType> 00497 class removes: 00498 public std::binary_function<RhsType&, const LhsType&, RhsType&> { 00499 public: 00500 00501 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00502 rhs.remove(lhs); 00503 return rhs; 00504 } 00505 }; 00506 00507 00508 template <> 00509 class removes<void, pbori_traits<void>::idx_type> { 00510 public: 00511 00512 template <class RhsType, class LhsType> 00513 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00514 rhs.remove(lhs); 00515 return rhs; 00516 } 00517 }; 00518 00521 template <class RhsType = void, 00522 class LhsType = typename pbori_traits<RhsType>::idx_type > 00523 class remove_assign; 00524 00525 00526 template <class RhsType, class LhsType> 00527 class remove_assign: 00528 public std::binary_function<RhsType&, const LhsType&, RhsType&> { 00529 public: 00530 00531 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00532 rhs.removeAssign(lhs); 00533 return rhs; 00534 } 00535 }; 00536 00537 00538 template <> 00539 class remove_assign<void, pbori_traits<void>::idx_type> { 00540 public: 00541 00542 template <class RhsType, class LhsType> 00543 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00544 rhs.removeAssign(lhs); 00545 return rhs; 00546 } 00547 }; 00548 00551 template <class ListType, class RhsType, class LhsType> 00552 class insert_second_to_list { 00553 public: 00554 00555 insert_second_to_list(ListType& theList__): 00556 theList(theList__) {}; 00557 00558 RhsType& operator() (RhsType& rhs, const LhsType& lhs) const { 00559 theList.insert(lhs); 00560 return rhs; 00561 } 00562 00563 private: 00564 ListType& theList; 00565 }; 00566 00567 00571 template <class Type1, class Type2> 00572 class is_same_type; 00573 00574 template <class Type> 00575 class is_same_type<Type, Type>: 00576 public integral_constant<CTypes::bool_type, true> {}; 00577 00578 template <class Type1, class Type2> 00579 class is_same_type: 00580 public integral_constant<CTypes::bool_type, false> {}; 00581 00582 template <class Type> 00583 class is_valid: 00584 public is_same_type<Type, valid_tag> {}; 00585 00589 template <class Type1, class Type2, class ThenType, class ElseType> 00590 class on_same_type; 00591 00592 template <class Type, class ThenType, class ElseType> 00593 class on_same_type<Type, Type, ThenType, ElseType> { 00594 public: 00595 typedef ThenType type; 00596 }; 00597 00598 template <class Type1, class Type2, class ThenType, class ElseType> 00599 class on_same_type { 00600 public: 00601 typedef ElseType type; 00602 }; 00603 00604 00608 struct internal_tag {}; 00609 00613 template<class Type> 00614 struct type_tag {}; 00615 00616 template <class Type> 00617 class hashes { 00618 public: 00619 00620 typedef typename Type::hash_type hash_type; 00621 00622 hash_type operator() (const Type& rhs) const{ 00623 return rhs.hash(); 00624 } 00625 }; 00626 00627 template <class Type> 00628 class generate_index_map { 00629 00630 typedef typename Type::idx_type idx_type; 00631 public: 00633 00634 #ifdef HAVE_TR1_UNORDERED_MAP 00635 typedef std::tr1::unordered_map<Type, idx_type, hashes<Type> > type; 00636 #else 00637 # ifdef HAVE_UNORDERED_MAP 00638 typedef std::unordered_map<Type, idx_type, hashes<Type> > type; 00639 # else 00640 # ifdef HAVE_HASH_MAP 00641 typedef __gnu_cxx::hash_map<Type, idx_type, hashes<Type> > type; 00642 # else 00643 typedef std::map<Type, idx_type> type; 00644 # endif 00645 # endif 00646 #endif 00647 }; 00648 00652 template <class ListType> 00653 class sizes_less: 00654 public std::binary_function<const ListType&, const ListType&, bool> { 00655 00656 public: 00657 bool operator()(const ListType& lhs, const ListType& rhs) const { 00658 return (lhs.size() < rhs.size()); 00659 } 00660 }; 00661 00665 template <class BiIterator> 00666 class reversed_iteration_adaptor { 00667 public: 00668 00670 typedef BiIterator iterator; 00671 00673 typedef reversed_iteration_adaptor<iterator> self; 00675 00676 typedef std::bidirectional_iterator_tag iterator_category; 00677 typedef typename std::iterator_traits<iterator>::difference_type 00678 difference_type; 00679 typedef typename std::iterator_traits<iterator>::pointer pointer; 00680 typedef typename std::iterator_traits<iterator>::reference reference; 00681 typedef typename std::iterator_traits<iterator>::value_type value_type; 00683 00685 reversed_iteration_adaptor(const iterator& iter): 00686 m_iter(iter) {} 00687 00689 00690 reference operator*() const { 00691 return *m_iter; 00692 } 00693 00695 self& operator++() { 00696 --m_iter; 00697 return *this; 00698 } 00699 00701 self& operator--() { 00702 ++m_iter; 00703 return *this; 00704 } 00705 00706 bool operator==(const self& rhs) const { 00707 return m_iter == rhs.m_iter; 00708 } 00709 00710 bool operator!=(const self& rhs) const { 00711 return m_iter != rhs.m_iter; 00712 } 00713 iterator get() const { 00714 return m_iter; 00715 } 00716 00717 protected: 00718 iterator m_iter; 00719 }; 00720 00721 00722 template <class DDType> 00723 class navigates: 00724 public std::unary_function<DDType, typename DDType::navigator> { 00725 public: 00727 typedef DDType dd_type; 00728 00730 typedef typename DDType::navigator navigator; 00731 00733 typedef std::unary_function<dd_type, navigator> base; 00734 00736 typename base::result_type operator()(const dd_type& rhs) const{ 00737 return rhs.navigation(); 00738 } 00739 00740 }; 00741 00742 00743 template <class ValueType> 00744 class default_value { 00745 public: 00746 typedef ValueType value_type; 00747 00748 value_type operator()(...) const{ 00749 return value_type(); 00750 } 00751 00752 }; 00753 00754 template <template<class> class BindType, class BinaryFunction, 00755 class ValueType, class ConstantOp> 00756 class constant_binder_base : 00757 public BindType<BinaryFunction>{ 00758 public: 00759 typedef BinaryFunction bin_op; 00760 typedef ConstantOp const_type; 00761 typedef BindType<bin_op> base; 00762 00763 typedef ValueType value_type; 00764 00765 constant_binder_base(const bin_op& op = bin_op()): base(op, const_type()()) {} 00766 }; 00767 00768 template <class BinaryFunction, class ConstantOp> 00769 class constant_binder2nd : 00770 public constant_binder_base<std::binder2nd, BinaryFunction, 00771 typename BinaryFunction::second_argument_type, 00772 ConstantOp> { 00773 }; 00774 00775 00776 template <class BinaryFunction, class ConstantOp> 00777 class constant_binder1st : 00778 public constant_binder_base<std::binder1st, BinaryFunction, 00779 typename BinaryFunction::first_argument_type, 00780 ConstantOp> { 00781 }; 00782 00783 template <template<class> class BindType, 00784 class BinaryFunction, class ValueType> 00785 class default_binder_base : 00786 public BindType<BinaryFunction>{ 00787 public: 00788 typedef BinaryFunction bin_op; 00789 typedef BindType<bin_op> base; 00790 00791 typedef ValueType value_type; 00792 00793 default_binder_base(const value_type& val): base(bin_op(), val) {} 00794 }; 00795 00796 template <class BinaryFunction> 00797 class default_binder2nd : 00798 public default_binder_base<std::binder2nd, BinaryFunction, 00799 typename BinaryFunction::second_argument_type> { 00800 public: 00801 typedef default_binder_base<std::binder2nd, BinaryFunction, 00802 typename BinaryFunction::second_argument_type> 00803 base; 00804 00805 default_binder2nd(const typename base::value_type& val): base(val) {} 00806 }; 00807 00808 00809 template <class BinaryFunction> 00810 class default_binder1st : 00811 public default_binder_base<std::binder1st, BinaryFunction, 00812 typename BinaryFunction::first_argument_type> { 00813 }; 00814 00815 // /** @class property_owner 00816 // * @brief defines generic base for properties 00817 // **/ 00818 // template <class ValidityTag> 00819 // class property_owner { 00820 // public: 00821 00822 // /// Set marker for validity 00823 // typedef typename 00824 // on_same_type<ValidityTag, valid_tag, valid_tag, invalid_tag>::type property; 00825 00826 // /// Generate Boolean member function 00827 // is_same_type<property, valid_tag> hasProperty; 00828 // }; 00829 00833 template <class ManagerType, 00834 class IdxType = typename ManagerType::idx_type, 00835 class VarNameType = typename ManagerType::const_varname_reference> 00836 class variable_name { 00837 public: 00838 typedef ManagerType manager_type; 00839 typedef IdxType idx_type; 00840 typedef VarNameType varname_type; 00841 00843 variable_name(const manager_type& mgr): m_mgr(mgr) {} 00844 00846 varname_type operator()(idx_type idx) const{ 00847 return m_mgr.getVariableName(idx); 00848 } 00849 00850 protected: 00852 const manager_type& m_mgr; 00853 }; 00854 00855 template <class MapType, class VariableType, class TermType, class NodeType> 00856 class mapped_new_node { 00857 public: 00858 typedef MapType map_type; 00859 typedef NodeType node_type; 00860 00861 typedef typename node_type::idx_type idx_type; 00862 00863 mapped_new_node(const map_type& the_map): m_map(the_map) {} 00864 00865 NodeType operator()(idx_type idx, 00866 const node_type& first, const node_type& second) const{ 00867 return ((TermType)VariableType(m_map[idx]))*first + second; 00868 } 00869 00870 00871 00872 private: 00873 const map_type& m_map; 00874 }; 00875 00876 00881 template <class NewType> 00882 struct pbori_base; 00883 00884 00885 00886 template <class DDType> 00887 class get_node { 00888 00889 public: 00890 typename DDType::node_type operator()(const DDType& rhs) const { 00891 return rhs.getNode(); 00892 } 00893 }; 00894 00895 // template<unsigned ErrorNumber = CUDD_INTERNAL_ERROR> 00896 // struct handle_error { 00897 // typedef mgrcore_traits<Cudd>::errorfunc_type errorfunc_type; 00898 00899 // handle_error(errorfunc_type errfunc): m_errfunc(errfunc) {} 00900 00901 // bool found(unsigned err) const { 00902 // if UNLIKELY(err == ErrorNumber) { 00903 // m_errfunc(cudd_error_traits<ErrorNumber>()()); 00904 // return true; 00905 // } 00906 // return false; 00907 // } 00908 00909 // void operator()(unsigned err) const { 00910 // if UNLIKELY(err == ErrorNumber) 00911 // m_errfunc(cudd_error_traits<ErrorNumber>()()); 00912 // else 00913 // reinterpret_cast<const handle_error<ErrorNumber - 1>&>(*this)(err); 00914 // } 00915 00916 // protected: 00917 // const errorfunc_type m_errfunc; 00918 // }; 00919 00920 00921 // template<> 00922 // struct handle_error<0> { 00923 // typedef mgrcore_traits<Cudd>::errorfunc_type errorfunc_type; 00924 00925 // handle_error(errorfunc_type errfunc): m_errfunc(errfunc) {} 00926 00927 // void operator()(unsigned err) const { 00928 // if LIKELY(err == 0) 00929 // m_errfunc(cudd_error_traits<0>()()); 00930 // } 00931 // protected: 00932 // errorfunc_type m_errfunc; 00933 // }; 00934 00935 00936 END_NAMESPACE_PBORI 00937 00938 #endif