PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00057 //***************************************************************************** 00058 00059 #include <set> 00060 #include <vector> 00061 00062 // include basic definitions 00063 #include "pbori_defs.h" 00064 #include "pbori_tags.h" 00065 // #include "CCuddInterface.h" 00066 00067 #include <boost/preprocessor/cat.hpp> 00068 #include <boost/preprocessor/seq/for_each.hpp> 00069 #include <boost/preprocessor/facilities/expand.hpp> 00070 #include <boost/preprocessor/stringize.hpp> 00071 00072 #ifndef pbori_traits_h_ 00073 #define pbori_traits_h_ 00074 00075 BEGIN_NAMESPACE_PBORI 00076 00082 template <class ValueType> 00083 class pbori_traits { 00084 00085 public: 00086 //------------------------------------------------------------------------- 00087 // types for treatment of decision diagrams 00088 //------------------------------------------------------------------------- 00089 typedef ValueType value_type; 00090 00092 typedef typename value_type::dd_type dd_type; 00093 00094 // /// Manage variables to be used by polynomials over Boolean ring 00095 // typedef typename value_type::manager_type manager_type; 00096 00097 // /// Reference to decision diagramm manager 00098 // typedef typename value_type::manager_reference manager_reference; 00099 00100 // /// Define shared pointer to decision diagram manager 00101 // typedef typename value_type::manager_ptr manager_ptr; 00102 00103 //------------------------------------------------------------------------- 00104 // types for several purposes 00105 //------------------------------------------------------------------------- 00106 00108 typedef typename value_type::bool_type bool_type; 00109 00111 typedef typename value_type::size_type size_type; 00112 00114 typedef typename value_type::integer_type integer_type; 00115 00117 typedef typename value_type::idx_type idx_type; 00118 00120 typedef typename value_type::comp_type comp_type; 00121 00123 typedef typename value_type::hash_type hash_type; 00124 00126 typedef typename value_type::ostream_type ostream_type; 00127 00129 typedef typename value_type::easy_equality_property easy_equality_property; 00130 }; 00131 00132 // Built-in types inherit global definitions 00133 template <> 00134 class pbori_traits<void>: 00135 public CTypes, public equality_property<valid_tag> { 00136 }; 00137 00138 template <> 00139 class pbori_traits<int>: 00140 public CTypes, public equality_property<valid_tag> { 00141 }; 00142 00143 template <> 00144 class pbori_traits<unsigned int>: 00145 public CTypes, public equality_property<valid_tag> { 00146 }; 00147 00148 template <> 00149 class pbori_traits<long int>: 00150 public CTypes, public equality_property<valid_tag> { 00151 }; 00152 00153 00154 template <class ValueType> 00155 class pbori_traits< std::set<ValueType> >: 00156 public CTypes, public equality_property<invalid_tag> { 00157 }; 00158 00159 template <class ValueType> 00160 class pbori_traits< std::vector<ValueType> >: 00161 public CTypes, public equality_property<invalid_tag> { 00162 }; 00163 00164 00170 template <class FirstType, class SecondType> 00171 class pbori_binary_traits; 00172 00173 template <class OnlyType> 00174 class pbori_binary_traits<OnlyType, OnlyType> { 00175 public: 00176 typedef typename OnlyType::easy_equality_property easy_equality_property; 00177 }; 00178 00179 template <class FirstType, class SecondType> 00180 class pbori_binary_traits: 00181 public equality_property<invalid_tag>{ 00182 }; 00183 00184 00185 00186 00187 template <class MgrType> 00188 struct manager_traits; 00189 00190 template <> 00191 struct manager_traits<Cudd> { 00192 typedef ZDD dd_base; 00193 typedef Cudd* core_type; 00194 typedef Cudd& tmp_ref; 00195 }; 00196 00197 template <> 00198 struct manager_traits<Cudd*> : 00199 public manager_traits<Cudd> { 00200 }; 00201 00202 template <> 00203 struct manager_traits<DdManager*> : 00204 public manager_traits<Cudd> { 00205 }; 00206 00207 template <class CuddLike> 00208 struct manager_traits { 00209 typedef typename CuddLike::dd_type dd_base; 00210 typedef typename CuddLike::mgrcore_ptr core_type; 00211 typedef typename CuddLike::tmp_ref tmp_ref; 00212 00213 typedef unsigned long large_size_type; 00214 typedef long int refcount_type; 00215 00216 typedef CTypes::idx_type idx_type; 00217 typedef CTypes::size_type size_type; 00218 00219 typedef DdNode* node_type; 00220 typedef DdManager* mgrcore_type; 00221 00222 typedef PFC errorfunc_type; 00223 typedef node_type (*unary_int_function)(mgrcore_type, int); 00224 typedef node_type (*void_function)(mgrcore_type); 00225 00226 typedef DD_CTFP binary_function; 00227 typedef node_type (*binary_int_function)(mgrcore_type, node_type, int); 00228 typedef 00229 node_type (*ternary_function)(mgrcore_type, node_type, node_type, node_type); 00230 00231 typedef int (*int_unary_function)(mgrcore_type, node_type); 00232 }; 00233 00234 template <class CuddLike> 00235 struct mgrcore_traits; 00236 00237 template<> 00238 struct mgrcore_traits<Cudd> { 00239 00240 typedef unsigned long large_size_type; 00241 typedef long int refcount_type; 00242 00243 typedef CTypes::idx_type idx_type; 00244 typedef CTypes::size_type size_type; 00245 00246 typedef DdNode* node_type; 00247 typedef DdManager* mgrcore_type; 00248 00249 typedef PFC errorfunc_type; 00250 typedef node_type (*unary_int_function)(mgrcore_type, int); 00251 typedef node_type (*void_function)(mgrcore_type); 00252 00253 typedef DD_CTFP binary_function; 00254 typedef node_type (*binary_int_function)(mgrcore_type, node_type, int); 00255 typedef 00256 node_type (*ternary_function)(mgrcore_type, node_type, node_type, node_type); 00257 00258 typedef int (*int_unary_function)(mgrcore_type, node_type); 00259 }; 00260 00261 #define PB_DECLARE_CUDD_TYPES(fromspace) \ 00262 typedef fromspace::errorfunc_type errorfunc_type; \ 00263 typedef fromspace::large_size_type large_size_type; \ 00264 typedef fromspace::refcount_type refcount_type; \ 00265 typedef fromspace::node_type node_type; \ 00266 typedef fromspace::mgrcore_type mgrcore_type; \ 00267 typedef fromspace::unary_int_function unary_int_function; \ 00268 typedef fromspace::void_function void_function; \ 00269 typedef fromspace::binary_function binary_function; \ 00270 typedef fromspace::binary_int_function binary_int_function; \ 00271 typedef fromspace::ternary_function ternary_function; \ 00272 typedef fromspace::int_unary_function int_unary_function; \ 00273 typedef fromspace::size_type size_type;\ 00274 typedef fromspace::idx_type idx_type; 00275 00276 // template <> 00277 // struct manager_traits<CCuddInterface::mgrcore_ptr> : 00278 // public manager_traits<CCuddInterface> { 00279 // }; 00280 00281 00282 template <class ZDDType> 00283 struct zdd_traits; 00284 00285 template <> 00286 struct zdd_traits<ZDD> { 00287 typedef Cudd manager_base; 00288 }; 00289 00290 template <> 00291 struct zdd_traits<CCuddZDD> { 00292 typedef CCuddInterface manager_base; 00293 }; 00294 00295 00296 #define PB_BINARY_FUNC_CALL(count, funcname, arg_pair) \ 00297 BOOST_PP_EXPAND(funcname(BOOST_PP_SEQ_HEAD(arg_pair), \ 00298 BOOST_PP_SEQ_HEAD(BOOST_PP_SEQ_TAIL(arg_pair)))) 00299 00300 template<unsigned ErrorNumber> 00301 struct cudd_error_traits { 00302 typedef const char* result_type; 00303 00304 result_type operator()() const; 00305 }; 00306 00307 00308 00309 00310 #define PB_CUDD_ERROR_TRAITS(errcode, errstr) \ 00311 template<> inline cudd_error_traits<errcode>::result_type \ 00312 cudd_error_traits<errcode>::operator()() const { \ 00313 return BOOST_PP_STRINGIZE(errstr); } 00314 00315 BOOST_PP_SEQ_FOR_EACH( PB_BINARY_FUNC_CALL, PB_CUDD_ERROR_TRAITS, 00316 ((CUDD_MEMORY_OUT)(Out of memory.)) 00317 ((CUDD_TOO_MANY_NODES)(Too many nodes.)) 00318 ((CUDD_MAX_MEM_EXCEEDED)(Maximum memory exceeded.)) 00319 ((CUDD_INVALID_ARG)(Invalid argument.)) 00320 ((CUDD_INTERNAL_ERROR)(Internal error.)) 00321 ((CUDD_NO_ERROR)(Unexpected error.)) 00322 ) 00323 00324 #undef PB_CUDD_ERROR_TRAITS 00325 00326 END_NAMESPACE_PBORI 00327 00328 #endif