1 /****************************************** 2 Copyright (c) 2016, Mate Soos 3 4 Permission is hereby granted, free of charge, to any person obtaining a copy 5 of this software and associated documentation files (the "Software"), to deal 6 in the Software without restriction, including without limitation the rights 7 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell 8 copies of the Software, and to permit persons to whom the Software is 9 furnished to do so, subject to the following conditions: 10 11 The above copyright notice and this permission notice shall be included in 12 all copies or substantial portions of the Software. 13 14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR 15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, 16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE 17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER 18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, 19 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN 20 THE SOFTWARE. 21 ***********************************************/ 22 23 #ifndef WATCHED_H 24 #define WATCHED_H 25 26 //#define DEBUG_WATCHED 27 28 #include "clabstraction.h" 29 #include "constants.h" 30 #include "cloffset.h" 31 #include "solvertypes.h" 32 33 #include <limits> 34 #include <string.h> 35 36 37 namespace CMSat { 38 39 enum WatchType { 40 watch_clause_t = 0 41 , watch_binary_t = 1 42 , watch_idx_t = 3 43 }; 44 45 /** 46 @brief An element in the watchlist. Natively contains 2- and 3-long clauses, others are referenced by pointer 47 48 This class contains two 32-bit datapieces. They are either used as: 49 \li One literal, in the case of binary clauses 50 \li Two literals, in the case of tertiary clauses 51 \li One blocking literal (i.e. an example literal from the clause) and a clause 52 offset (as per ClauseAllocator ), in the case of long clauses 53 */ 54 class Watched { 55 public: 56 Watched(Watched const&) = default; 57 58 /** 59 @brief Constructor for a long (>3) clause 60 */ Watched(const ClOffset offset,Lit blockedLit)61 Watched(const ClOffset offset, Lit blockedLit) : 62 data1(blockedLit.toInt()) 63 , type(watch_clause_t) 64 , data2(offset) 65 { 66 } 67 68 /** 69 @brief Constructor for a long (>3) clause 70 */ Watched(const ClOffset offset,cl_abst_type abst)71 Watched(const ClOffset offset, cl_abst_type abst) : 72 data1(abst) 73 , type(watch_clause_t) 74 , data2(offset) 75 { 76 } 77 Watched()78 Watched() : 79 data1 (std::numeric_limits<uint32_t>::max()) 80 , type(watch_clause_t) // initialize type with most generic type of clause 81 , data2(std::numeric_limits<uint32_t>::max() >> 2) 82 {} 83 84 /** 85 @brief Constructor for a binary clause 86 */ Watched(const Lit lit,const bool red)87 Watched(const Lit lit, const bool red) : 88 data1(lit.toInt()) 89 , type(watch_binary_t) 90 , data2(red) 91 { 92 } 93 94 /** 95 @brief Constructor for an Index value 96 */ Watched(const uint32_t idx)97 explicit Watched(const uint32_t idx) : 98 data1(idx) 99 , type(watch_idx_t) 100 { 101 } 102 103 /** 104 @brief To update the blocked literal of a >3-long normal clause 105 */ setBlockedLit(const Lit blockedLit)106 void setBlockedLit(const Lit blockedLit) 107 { 108 #ifdef DEBUG_WATCHED 109 assert(type == watch_clause_t); 110 #endif 111 data1 = blockedLit.toInt(); 112 } 113 getType()114 WatchType getType() const 115 { 116 // we rely that WatchType enum is in [0-3] range and fits into type field two bits 117 return static_cast<WatchType>(type); 118 } 119 isBin()120 bool isBin() const 121 { 122 return (type == watch_binary_t); 123 } 124 isClause()125 bool isClause() const 126 { 127 return (type == watch_clause_t); 128 } 129 isIdx()130 bool isIdx() const 131 { 132 return (type == watch_idx_t); 133 } 134 get_idx()135 uint32_t get_idx() const 136 { 137 #ifdef DEBUG_WATCHED 138 assert(type == watch_idx_t); 139 #endif 140 return data1; 141 } 142 143 /** 144 @brief Get the sole other lit of the binary clause, or get lit2 of the tertiary clause 145 */ lit2()146 Lit lit2() const 147 { 148 #ifdef DEBUG_WATCHED 149 assert(isBin()); 150 #endif 151 return Lit::toLit(data1); 152 } 153 154 /** 155 @brief Set the sole other lit of the binary clause 156 */ setLit2(const Lit lit)157 void setLit2(const Lit lit) 158 { 159 #ifdef DEBUG_WATCHED 160 assert(isBin()); 161 #endif 162 data1 = lit.toInt(); 163 } 164 red()165 bool red() const 166 { 167 #ifdef DEBUG_WATCHED 168 assert(isBin()); 169 #endif 170 return data2 & 1; 171 } 172 setRed(const bool toSet)173 void setRed(const bool toSet) 174 { 175 #ifdef DEBUG_WATCHED 176 assert(isBin()); 177 assert(red()); 178 #endif 179 assert(toSet == false); 180 data2 &= (~(1U)); 181 } 182 mark_bin_cl()183 void mark_bin_cl() 184 { 185 #ifdef DEBUG_WATCHED 186 assert(isBin()); 187 #endif 188 data2 |= 2; 189 } 190 unmark_bin_cl()191 void unmark_bin_cl() 192 { 193 #ifdef DEBUG_WATCHED 194 assert(isBin()); 195 #endif 196 data2 &= 1; 197 } 198 bin_cl_marked()199 bool bin_cl_marked() const 200 { 201 #ifdef DEBUG_WATCHED 202 assert(isBin()); 203 #endif 204 return data2&2; 205 } 206 207 /** 208 @brief Get example literal (blocked lit) of a normal >3-long clause 209 */ getBlockedLit()210 Lit getBlockedLit() const 211 { 212 #ifdef DEBUG_WATCHED 213 assert(isClause()); 214 #endif 215 return Lit::toLit(data1); 216 } 217 getAbst()218 cl_abst_type getAbst() const 219 { 220 #ifdef DEBUG_WATCHED 221 assert(isClause()); 222 #endif 223 return data1; 224 } 225 226 /** 227 @brief Get offset of a >3-long normal clause or of an xor clause (which may be 3-long) 228 */ get_offset()229 ClOffset get_offset() const 230 { 231 #ifdef DEBUG_WATCHED 232 assert(isClause()); 233 #endif 234 return data2; 235 } 236 237 bool operator==(const Watched& other) const 238 { 239 return data1 == other.data1 && data2 == other.data2 && type == other.type; 240 } 241 242 bool operator!=(const Watched& other) const 243 { 244 return !(*this == other); 245 } 246 247 private: 248 uint32_t data1; 249 // binary, tertiary or long, as per WatchType 250 // currently WatchType is enum with range [0..3] and fits in type 251 // in case if WatchType extended type size won't be enough. 252 ClOffset type:2; 253 ClOffset data2:EFFECTIVELY_USEABLE_BITS; 254 }; 255 256 inline std::ostream& operator<<(std::ostream& os, const Watched& ws) 257 { 258 259 if (ws.isClause()) { 260 os << "Clause offset " << ws.get_offset(); 261 } 262 263 if (ws.isBin()) { 264 os << "Bin lit " << ws.lit2() << " (red: " << ws.red() << " )"; 265 } 266 267 return os; 268 } 269 270 struct OccurClause { OccurClauseOccurClause271 OccurClause(const Lit _lit, const Watched _ws) : 272 lit(_lit) 273 , ws(_ws) 274 {} 275 OccurClauseOccurClause276 OccurClause() : 277 lit(lit_Undef) 278 {} 279 280 bool operator==(const OccurClause& other) const 281 { 282 return lit == other.lit && ws == other.ws; 283 } 284 285 Lit lit; 286 Watched ws; 287 }; 288 289 struct WatchSorterBinTriLong { operatorWatchSorterBinTriLong290 bool operator()(const Watched& a, const Watched& b) 291 { 292 assert(!a.isIdx()); 293 assert(!b.isIdx()); 294 295 //Anything but clause! 296 if (a.isClause()) { 297 //A is definitely not better than B 298 return false; 299 } 300 if (b.isClause()) { 301 //B is clause, A is NOT a clause. So A is better than B. 302 return true; 303 } 304 305 //Both are BIN 306 assert(a.isBin()); 307 assert(b.isBin()); 308 309 if (a.lit2() != b.lit2()) { 310 return a.lit2() < b.lit2(); 311 } 312 313 if (a.red() != b.red()) { 314 return !a.red(); 315 } 316 return false; 317 } 318 }; 319 320 321 } //end namespace 322 323 #endif //WATCHED_H 324