PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00015 //***************************************************************************** 00016 00017 // load PolyBoRi settings 00018 # include "pbori_defs.h" 00019 00020 // include basic decision diagram manager interface 00021 #include "CCuddCore.h" 00022 #include "PBoRiError.h" 00023 #include "CCheckedIdx.h" 00024 #include <boost/intrusive_ptr.hpp> 00025 00026 #include <list> 00027 00028 #ifndef BoolePolyRing_h_ 00029 #define BoolePolyRing_h_ 00030 00031 00032 BEGIN_NAMESPACE_PBORI 00033 00034 00035 00041 class BoolePolyRing: 00042 public CTypes::orderenums_type, public CTypes::compenums_type, 00043 public CTypes::auxtypes_type { 00044 00046 typedef BoolePolyRing self; 00047 00048 public: 00050 typedef class BooleExponent exp_type; 00051 00053 typedef class BooleMonomial monom_type; 00054 00056 typedef class BooleVariable var_type; 00057 00059 typedef class BooleSet dd_type; 00060 00062 typedef class BoolePolynomial poly_type; 00064 00065 typedef CTypes::ordercode_type ordercode_type; 00066 typedef CTypes::vartext_type vartext_type; 00068 00070 typedef CCheckedIdx checked_idx_type; 00071 00073 typedef CCuddCore core_type; 00074 typedef core_type::const_varname_reference const_varname_reference; 00076 typedef boost::intrusive_ptr<core_type> core_ptr; 00077 00079 typedef core_type::order_type order_type; 00080 00082 typedef core_type::order_ptr order_ptr; 00083 00085 typedef order_type& order_reference; 00086 00087 typedef DdManager mgr_type; 00089 using CTypes::orderenums_type::ordercodes; 00090 00092 typedef std::vector<idx_type> block_idx_type; 00093 00095 typedef block_idx_type::const_iterator block_iterator; 00096 00097 protected: 00098 00101 BoolePolyRing(const core_ptr& rhs): p_core(rhs) {} 00102 00103 public: 00105 BoolePolyRing(); 00106 00108 explicit BoolePolyRing(size_type nvars, 00109 ordercode_type order = lp, 00110 bool_type make_active = true); 00111 00113 BoolePolyRing(size_type nvars, const order_ptr& order): 00114 p_core(new core_type(nvars, order)) {} 00115 00117 BoolePolyRing(const self& rhs): p_core(rhs.p_core) {} 00118 00120 ~BoolePolyRing() {} 00121 00123 size_type nVariables() const { return p_core->m_mgr.nVariables(); } 00124 00126 vartext_type getVariableName(checked_idx_type idx) const { 00127 return p_core->m_names[idx]; 00128 } 00129 00131 void setVariableName(checked_idx_type idx, vartext_type varname) { 00132 p_core->m_names.set(idx, varname); 00133 } 00134 00136 void clearCache() { p_core->m_mgr.cacheFlush(); } 00137 00139 ostream_type& print(ostream_type&) const; 00140 00142 hash_type hash() const { 00143 return static_cast<hash_type>(reinterpret_cast<std::ptrdiff_t 00144 >(getManager())); 00145 } 00146 00148 order_reference ordering() const { return *(p_core->pOrder); } 00149 00151 mgr_type* getManager() const { return p_core->m_mgr.getManager(); } 00152 00154 self clone() const { return self(new core_type(*p_core)); } 00155 00157 void activate(); 00158 00160 void changeOrdering(ordercode_type); 00161 00163 poly_type coerce(const poly_type& rhs) const; 00164 00166 monom_type coerce(const monom_type& rhs) const; 00167 00169 var_type coerce(const var_type& rhs) const; 00170 00172 dd_type variable(checked_idx_type nvar) const; 00173 00175 dd_type zero() const; // inlined below 00176 00178 dd_type one() const; // inlined below 00179 00181 dd_type constant(bool is_one) const; // inlined below 00182 00183 protected: 00185 core_ptr core() const {return p_core;}; 00186 00188 core_ptr p_core; 00189 }; 00190 00192 inline BoolePolyRing::ostream_type& 00193 operator<<(BoolePolyRing::ostream_type& os, const BoolePolyRing& ring) { 00194 return ring.print(os); 00195 } 00196 00197 END_NAMESPACE_PBORI 00198 00199 #include "BooleSet.h" 00200 00201 BEGIN_NAMESPACE_PBORI 00202 00204 inline BoolePolyRing::dd_type BoolePolyRing::zero() const { return dd_type(*this, p_core->m_mgr.zddZero()); } 00205 00207 inline BoolePolyRing::dd_type BoolePolyRing::one() const { return dd_type(*this, p_core->m_mgr.zddOne()); } 00208 00209 00211 inline BoolePolyRing::dd_type BoolePolyRing::constant(bool is_one) const { return (is_one? one(): zero()); } 00212 00213 inline BoolePolyRing::dd_type BoolePolyRing::variable(checked_idx_type nvar) const { 00214 return dd_type(*this, p_core->m_mgr.getVar(nvar)); 00215 } 00216 00217 END_NAMESPACE_PBORI 00218 00219 #endif // of #ifndef BoolePolyRing_h_