00001 // -*- c++ -*- 00002 //***************************************************************************** 00089 //***************************************************************************** 00090 00091 #ifndef BooleVariable_h_ 00092 #define BooleVariable_h_ 00093 00094 // include basic definitions 00095 #include "pbori_defs.h" 00096 00097 // get BoolePolynomial's definition 00098 #include "BooleEnv.h" 00099 #include "BoolePolynomial.h" 00100 00101 BEGIN_NAMESPACE_PBORI 00102 00111 class BooleVariable { 00112 00113 public: 00114 //------------------------------------------------------------------------- 00115 // types definitions 00116 //------------------------------------------------------------------------- 00117 00119 00120 typedef CTypes::dd_type dd_type; 00121 typedef CTypes::size_type size_type; 00122 typedef CTypes::idx_type idx_type; 00123 typedef CTypes::hash_type hash_type; 00125 00127 typedef BooleVariable self; 00128 00130 typedef BooleSet set_type; 00131 00133 typedef BooleRing ring_type; 00134 00136 explicit BooleVariable(idx_type idx = 0): 00137 m_poly( BooleEnv::persistentVariable(idx) ) {} 00138 00140 BooleVariable(idx_type idx, const ring_type& ring): 00141 m_poly( ring.persistentVariable(idx) ) {} 00142 00143 00145 BooleVariable(const self& rhs): 00146 m_poly(rhs.m_poly) {} 00147 00149 operator const BoolePolynomial&() const { return m_poly; } 00150 00152 idx_type index() const { return *m_poly.firstBegin(); } 00153 00155 bool operator== (const self& other) const{ 00156 return m_poly==other.m_poly; 00157 } 00158 00159 // Nonequality check 00160 bool operator!= (const self& other) const{ 00161 return m_poly!=other.m_poly; 00162 } 00163 00165 hash_type stableHash() const{ return m_poly.stableHash(); } 00166 00168 hash_type hash() const { return m_poly.hash(); } 00169 00171 set_type set() const { return m_poly.set(); } 00172 00174 ring_type ring() const { return m_poly.ring(); } 00175 00176 private: 00177 BoolePolynomial m_poly; 00178 }; 00179 00180 00181 00182 inline BoolePolynomial 00183 operator/(const BooleVariable& lhs, const BooleVariable& rhs) { 00184 return BoolePolynomial(BooleConstant(lhs == rhs), lhs.ring()); 00185 } 00186 00187 00188 00189 END_NAMESPACE_PBORI 00190 00191 #endif // of BooleVariable_h_