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 35 namespace CMSat { 36 37 enum WatchType { 38 watch_clause_t = 0 39 , watch_binary_t = 1 40 , watch_idx_t = 3 41 }; 42 43 /** 44 @brief An element in the watchlist. Natively contains 2- and 3-long clauses, others are referenced by pointer 45 46 This class contains two 32-bit datapieces. They are either used as: 47 \li One literal, in the case of binary clauses 48 \li Two literals, in the case of tertiary clauses 49 \li One blocking literal (i.e. an example literal from the clause) and a clause 50 offset (as per ClauseAllocator ), in the case of long clauses 51 */ 52 class Watched { 53 public: 54 /** 55 @brief Constructor for a long (>3) clause 56 */ Watched(const ClOffset offset,Lit blockedLit)57 Watched(const ClOffset offset, Lit blockedLit) : 58 data1(blockedLit.toInt()) 59 , data2(offset) 60 , type(watch_clause_t) 61 { 62 } 63 64 /** 65 @brief Constructor for a long (>3) clause 66 */ Watched(const ClOffset offset,cl_abst_type abst)67 Watched(const ClOffset offset, cl_abst_type abst) : 68 data1(abst) 69 , data2(offset) 70 , type(watch_clause_t) 71 { 72 } 73 Watched()74 Watched(){} 75 76 /** 77 @brief Constructor for a binary clause 78 */ Watched(const Lit lit,const bool red)79 Watched(const Lit lit, const bool red) : 80 data1(lit.toInt()) 81 , type(watch_binary_t) 82 , _red(red) 83 { 84 } 85 86 /** 87 @brief Constructor for an Index value 88 */ Watched(const uint32_t idx)89 Watched(const uint32_t idx) : 90 data1(idx) 91 , type(watch_idx_t) 92 { 93 } 94 95 /** 96 @brief To update the blocked literal of a >3-long normal clause 97 */ setBlockedLit(const Lit blockedLit)98 void setBlockedLit(const Lit blockedLit) 99 { 100 #ifdef DEBUG_WATCHED 101 assert(type == watch_clause_t); 102 #endif 103 data1 = blockedLit.toInt(); 104 } 105 getType()106 WatchType getType() const 107 { 108 // we rely that WatchType enum is in [0-3] range and fits into type field two bits 109 return static_cast<WatchType>(type); 110 } 111 isBin()112 bool isBin() const 113 { 114 return (type == watch_binary_t); 115 } 116 isClause()117 bool isClause() const 118 { 119 return (type == watch_clause_t); 120 } 121 isIdx()122 bool isIdx() const 123 { 124 return (type == watch_idx_t); 125 } 126 get_idx()127 uint32_t get_idx() const 128 { 129 #ifdef DEBUG_WATCHED 130 assert(type == watch_idx_t); 131 #endif 132 return data1; 133 } 134 135 /** 136 @brief Get the sole other lit of the binary clause, or get lit2 of the tertiary clause 137 */ lit2()138 Lit lit2() const 139 { 140 #ifdef DEBUG_WATCHED 141 assert(isBin()); 142 #endif 143 return Lit::toLit(data1); 144 } 145 146 /** 147 @brief Set the sole other lit of the binary clause 148 */ setLit2(const Lit lit)149 void setLit2(const Lit lit) 150 { 151 #ifdef DEBUG_WATCHED 152 assert(isBin()); 153 #endif 154 data1 = lit.toInt(); 155 } 156 red()157 bool red() const 158 { 159 #ifdef DEBUG_WATCHED 160 assert(isBin()); 161 #endif 162 return _red; 163 } 164 setRed(const bool toSet)165 void setRed(const bool 166 #ifdef DEBUG_WATCHED 167 toSet 168 #endif 169 ) 170 { 171 #ifdef DEBUG_WATCHED 172 assert(isBin()); 173 assert(red()); 174 assert(toSet == false); 175 #endif 176 _red = true; 177 } 178 mark_bin_cl()179 void mark_bin_cl() 180 { 181 #ifdef DEBUG_WATCHED 182 assert(isBin()); 183 #endif 184 marked = 1; 185 } 186 unmark_bin_cl()187 void unmark_bin_cl() 188 { 189 #ifdef DEBUG_WATCHED 190 assert(isBin()); 191 #endif 192 marked= 0; 193 } 194 bin_cl_marked()195 bool bin_cl_marked() const 196 { 197 #ifdef DEBUG_WATCHED 198 assert(isBin()); 199 #endif 200 return marked; 201 } 202 203 /** 204 @brief Get example literal (blocked lit) of a normal >3-long clause 205 */ getBlockedLit()206 Lit getBlockedLit() const 207 { 208 #ifdef DEBUG_WATCHED 209 assert(isClause()); 210 #endif 211 return Lit::toLit(data1); 212 } 213 getAbst()214 cl_abst_type getAbst() const 215 { 216 #ifdef DEBUG_WATCHED 217 assert(isClause()); 218 #endif 219 return data1; 220 } 221 222 /** 223 @brief Get offset of a >3-long normal clause or of an xor clause (which may be 3-long) 224 */ get_offset()225 ClOffset get_offset() const 226 { 227 #ifdef DEBUG_WATCHED 228 assert(isClause()); 229 #endif 230 return data2; 231 } 232 233 bool operator==(const Watched& other) const 234 { 235 return data1 == other.data1 && data2 == other.data2 && type == other.type 236 && _red == other._red; 237 } 238 239 bool operator!=(const Watched& other) const 240 { 241 return !(*this == other); 242 } 243 Watched(Watched && o)244 Watched(Watched&& o) noexcept { 245 data1 = o.data1; 246 data2 = o.data2; 247 type = o.type; 248 _red = o._red; 249 marked = o.marked; 250 } 251 Watched(const Watched & o)252 Watched(const Watched& o) noexcept { 253 data1 = o.data1; 254 data2 = o.data2; 255 type = o.type; 256 _red = o._red; 257 marked = o.marked; 258 } 259 260 Watched& operator=(const Watched& o) noexcept { 261 data1 = o.data1; 262 data2 = o.data2; 263 type = o.type; 264 _red = o._red; 265 marked = o.marked; 266 return *this; 267 } 268 269 private: 270 uint32_t data1; 271 // binary, tertiary or long, as per WatchType 272 // currently WatchType is enum with range [0..3] and fits in type 273 // in case if WatchType extended type size won't be enough. 274 uint32_t data2; 275 char type; 276 char _red; 277 char marked; 278 }; 279 280 inline std::ostream& operator<<(std::ostream& os, const Watched& ws) 281 { 282 283 if (ws.isClause()) { 284 os << "Clause offset " << ws.get_offset(); 285 } 286 287 if (ws.isBin()) { 288 os << "Bin lit " << ws.lit2() << " (red: " << ws.red() << " )"; 289 } 290 291 return os; 292 } 293 294 struct OccurClause { OccurClauseOccurClause295 OccurClause(const Lit _lit, const Watched _ws) : 296 lit(_lit) 297 , ws(_ws) 298 {} 299 OccurClauseOccurClause300 OccurClause() : 301 lit(lit_Undef) 302 {} 303 304 bool operator==(const OccurClause& other) const 305 { 306 return lit == other.lit && ws == other.ws; 307 } 308 309 Lit lit; 310 Watched ws; 311 }; 312 313 struct WatchSorterBinTriLong { operatorWatchSorterBinTriLong314 bool operator()(const Watched& a, const Watched& b) 315 { 316 assert(!a.isIdx()); 317 assert(!b.isIdx()); 318 319 //Anything but clause! 320 if (a.isClause()) { 321 //A is definitely not better than B 322 return false; 323 } 324 if (b.isClause()) { 325 //B is clause, A is NOT a clause. So A is better than B. 326 return true; 327 } 328 329 //Both are BIN 330 assert(a.isBin()); 331 assert(b.isBin()); 332 333 if (a.lit2() != b.lit2()) { 334 return a.lit2() < b.lit2(); 335 } 336 337 if (a.red() != b.red()) { 338 return !a.red(); 339 } 340 return false; 341 } 342 }; 343 344 345 } //end namespace 346 347 #endif //WATCHED_H 348