[9] | 1 | // Class automatically generated by Dev-C++ New Class wizard |
---|
| 2 | |
---|
| 3 | #ifndef ATOMSANDNODES_H |
---|
| 4 | #define ATOMSANDNODES_H |
---|
| 5 | |
---|
| 6 | #include <vector> |
---|
| 7 | |
---|
| 8 | #include <iostream> |
---|
| 9 | |
---|
| 10 | #include "../../Basics.h" |
---|
| 11 | #include <SomeTime.h> |
---|
| 12 | |
---|
| 13 | using namespace std; |
---|
| 14 | |
---|
| 15 | #define INVALID_DL -1 |
---|
| 16 | |
---|
| 17 | class CClauseVertex; |
---|
| 18 | typedef CClauseVertex *PCLV; |
---|
| 19 | |
---|
| 20 | class CVariableVertex; |
---|
| 21 | typedef CVariableVertex *PVARV; |
---|
| 22 | |
---|
| 23 | typedef unsigned int indexTypeVARS; |
---|
| 24 | typedef unsigned int indexTypeCLS; |
---|
| 25 | |
---|
| 26 | typedef indexTypeVARS VarIdT; |
---|
| 27 | typedef indexTypeCLS ClauseIdT; |
---|
| 28 | |
---|
| 29 | class LiteralIdT |
---|
| 30 | { |
---|
| 31 | indexTypeVARS val; |
---|
| 32 | public: |
---|
| 33 | |
---|
| 34 | LiteralIdT() |
---|
| 35 | { |
---|
| 36 | val = 0; |
---|
| 37 | } |
---|
| 38 | LiteralIdT(int iLitIdx) |
---|
| 39 | { |
---|
| 40 | val = (abs(iLitIdx)<<1) + (unsigned int)(iLitIdx > 0); |
---|
| 41 | } |
---|
| 42 | |
---|
| 43 | LiteralIdT(VarIdT iVarIdx, bool polarity) |
---|
| 44 | { |
---|
| 45 | val = (iVarIdx<<1) + (unsigned int)polarity; |
---|
| 46 | } |
---|
| 47 | |
---|
| 48 | VarIdT toVarIdx() const |
---|
| 49 | { |
---|
| 50 | return (val >> 1); |
---|
| 51 | } |
---|
| 52 | |
---|
| 53 | unsigned int toUInt() const |
---|
| 54 | { |
---|
| 55 | return val; |
---|
| 56 | } |
---|
| 57 | |
---|
| 58 | void makeFromUInt(unsigned int v) |
---|
| 59 | { |
---|
| 60 | val = v; |
---|
| 61 | } |
---|
| 62 | |
---|
| 63 | bool polarity() const |
---|
| 64 | { |
---|
| 65 | return (bool)(val & 0x01); |
---|
| 66 | } |
---|
| 67 | |
---|
| 68 | TriValue polarityTriVal() const |
---|
| 69 | { |
---|
| 70 | return (TriValue)(val & 0x01); |
---|
| 71 | } |
---|
| 72 | |
---|
| 73 | bool operator!=(const LiteralIdT &rL2) const |
---|
| 74 | { |
---|
| 75 | return val != rL2.val; |
---|
| 76 | } |
---|
| 77 | |
---|
| 78 | bool operator==(const LiteralIdT &rL2) const |
---|
| 79 | { |
---|
| 80 | return val == rL2.val; |
---|
| 81 | } |
---|
| 82 | |
---|
| 83 | const LiteralIdT oppositeLit() const |
---|
| 84 | { |
---|
| 85 | return LiteralIdT(toVarIdx(),!polarity()); |
---|
| 86 | } |
---|
| 87 | |
---|
| 88 | void print() const |
---|
| 89 | { |
---|
| 90 | toSTDOUT((polarity()?" ":"-")<< toVarIdx()<<" "); |
---|
| 91 | } |
---|
| 92 | }; |
---|
| 93 | |
---|
| 94 | |
---|
| 95 | static const ClauseIdT NOT_A_CLAUSE(0); |
---|
| 96 | static const LiteralIdT NOT_A_LIT(0,false); |
---|
| 97 | |
---|
| 98 | #define SENTINEL_CL NOT_A_CLAUSE |
---|
| 99 | #define SENTINEL_LIT NOT_A_LIT |
---|
| 100 | |
---|
| 101 | |
---|
| 102 | class CClauseVertex |
---|
| 103 | { |
---|
| 104 | /// the offset of the first literal of this clause in theLitVector of |
---|
| 105 | /// the main CInstanceGraph |
---|
| 106 | unsigned int litPoolOfs; |
---|
| 107 | |
---|
| 108 | LiteralIdT litA, litB; |
---|
| 109 | |
---|
| 110 | unsigned int numLits; |
---|
| 111 | int lastTouchTime; |
---|
| 112 | |
---|
| 113 | public: |
---|
| 114 | |
---|
| 115 | bool hasWatchLitA() { return litA != NOT_A_LIT;} |
---|
| 116 | bool hasWatchLitB() { return litB != NOT_A_LIT;} |
---|
| 117 | |
---|
| 118 | void setLitA(const LiteralIdT & lit) { litA = lit;} |
---|
| 119 | void setLitB(const LiteralIdT & lit) { litB = lit;} |
---|
| 120 | |
---|
| 121 | const LiteralIdT &idLitA() const {return litA;} |
---|
| 122 | const LiteralIdT &idLitB() const {return litB;} |
---|
| 123 | |
---|
| 124 | int getLastTouchTime() const |
---|
| 125 | { |
---|
| 126 | return lastTouchTime; |
---|
| 127 | } |
---|
| 128 | |
---|
| 129 | void setTouched() |
---|
| 130 | { |
---|
| 131 | lastTouchTime = CStepTime::getTime(); |
---|
| 132 | } |
---|
| 133 | |
---|
| 134 | void setLength(unsigned int nlen) |
---|
| 135 | { |
---|
| 136 | numLits = nlen; |
---|
| 137 | } |
---|
| 138 | unsigned int length() const |
---|
| 139 | { |
---|
| 140 | return numLits; |
---|
| 141 | } |
---|
| 142 | |
---|
| 143 | bool isDeleted() const |
---|
| 144 | { |
---|
| 145 | return numLits == 0; |
---|
| 146 | } |
---|
| 147 | |
---|
| 148 | void setDeleted() |
---|
| 149 | { |
---|
| 150 | numLits = 0; |
---|
| 151 | } |
---|
| 152 | |
---|
| 153 | |
---|
| 154 | void setLitOfs(unsigned int ofs) {litPoolOfs = ofs;} |
---|
| 155 | unsigned int getLitOfs() const {return litPoolOfs;} |
---|
| 156 | |
---|
| 157 | |
---|
| 158 | // class constructor |
---|
| 159 | CClauseVertex() |
---|
| 160 | { |
---|
| 161 | litA = litB = NOT_A_LIT; |
---|
| 162 | numLits = 0; |
---|
| 163 | litPoolOfs = 0; |
---|
| 164 | lastTouchTime =0; |
---|
| 165 | } |
---|
| 166 | |
---|
| 167 | void reset() |
---|
| 168 | { |
---|
| 169 | |
---|
| 170 | lastTouchTime = 0; |
---|
| 171 | } |
---|
| 172 | |
---|
| 173 | ~CClauseVertex(){} |
---|
| 174 | |
---|
| 175 | bool watches(const VarIdT &theVar) const |
---|
| 176 | { |
---|
| 177 | return (idLitA().toVarIdx() == theVar || idLitB().toVarIdx() == theVar); |
---|
| 178 | } |
---|
| 179 | |
---|
| 180 | }; |
---|
| 181 | |
---|
| 182 | |
---|
| 183 | |
---|
| 184 | |
---|
| 185 | |
---|
| 186 | template <typename _T> |
---|
| 187 | class extd_vector : public vector<_T> |
---|
| 188 | { |
---|
| 189 | |
---|
| 190 | |
---|
| 191 | public: |
---|
| 192 | void quickErase(int iOfs) |
---|
| 193 | { |
---|
| 194 | (*this)[iOfs] = vector<_T>::back(); |
---|
| 195 | vector<_T>::pop_back(); |
---|
| 196 | } |
---|
| 197 | |
---|
| 198 | //typename vector<_T>::iterator |
---|
| 199 | void quickErase(typename vector<_T>::iterator &it) |
---|
| 200 | { |
---|
| 201 | *it = vector<_T>::back(); |
---|
| 202 | vector<_T>::pop_back(); |
---|
| 203 | } |
---|
| 204 | |
---|
| 205 | }; |
---|
| 206 | |
---|
| 207 | |
---|
| 208 | |
---|
| 209 | class AntecedentT |
---|
| 210 | { |
---|
| 211 | unsigned int val; |
---|
| 212 | |
---|
| 213 | public: |
---|
| 214 | AntecedentT() { val = 1;} |
---|
| 215 | AntecedentT(const ClauseIdT idCl) |
---|
| 216 | { |
---|
| 217 | val = (idCl << 1) | 1; |
---|
| 218 | } |
---|
| 219 | AntecedentT(const LiteralIdT idLit) |
---|
| 220 | { |
---|
| 221 | val = (idLit.toUInt() << 1) ; |
---|
| 222 | } |
---|
| 223 | |
---|
| 224 | bool isAClause() {return val & 0x01;} |
---|
| 225 | |
---|
| 226 | ClauseIdT toCl() |
---|
| 227 | { |
---|
| 228 | return val>>1; |
---|
| 229 | } |
---|
| 230 | LiteralIdT toLit() |
---|
| 231 | { |
---|
| 232 | LiteralIdT idLit; |
---|
| 233 | idLit.makeFromUInt(val>>1); |
---|
| 234 | return idLit; |
---|
| 235 | } |
---|
| 236 | bool isAnt() { return (isAClause() && !(toCl() == NOT_A_CLAUSE)) |
---|
| 237 | || (!isAClause() && (toLit() != NOT_A_LIT));} |
---|
| 238 | |
---|
| 239 | }; |
---|
| 240 | |
---|
| 241 | class AntAndLit |
---|
| 242 | //structure saving a Lit and the antecedent implying it |
---|
| 243 | // antecedents may be clauses or literals |
---|
| 244 | { |
---|
| 245 | public: |
---|
| 246 | AntecedentT theAnt; |
---|
| 247 | LiteralIdT theLit; |
---|
| 248 | |
---|
| 249 | AntAndLit(const AntecedentT ant,const LiteralIdT pL) |
---|
| 250 | { |
---|
| 251 | theAnt = ant; |
---|
| 252 | theLit = pL; |
---|
| 253 | } |
---|
| 254 | |
---|
| 255 | AntAndLit(const LiteralIdT idAntLit,const LiteralIdT pL) |
---|
| 256 | { |
---|
| 257 | theAnt = AntecedentT(idAntLit); |
---|
| 258 | theLit = pL; |
---|
| 259 | } |
---|
| 260 | |
---|
| 261 | AntAndLit(const ClauseIdT idCl = NOT_A_CLAUSE,const LiteralIdT pL = 0) |
---|
| 262 | { |
---|
| 263 | theAnt = AntecedentT(idCl); |
---|
| 264 | theLit = pL; |
---|
| 265 | } |
---|
| 266 | |
---|
| 267 | AntecedentT &getAnt(){return theAnt;} |
---|
| 268 | LiteralIdT& getLit() {return theLit;} |
---|
| 269 | }; |
---|
| 270 | |
---|
| 271 | |
---|
| 272 | class CVariableVertex |
---|
| 273 | { |
---|
| 274 | /// INVARIANT : SENTINEL clclcl ... |
---|
| 275 | /// this is due to the watchCls being passed in reverse by BCP |
---|
| 276 | extd_vector<ClauseIdT> watchCls[2]; |
---|
| 277 | |
---|
| 278 | TriValue theVal; |
---|
| 279 | |
---|
| 280 | VarIdT itecIndex; |
---|
| 281 | |
---|
| 282 | AntecedentT myAntecedent; |
---|
| 283 | int DecLevelOfDeactivation; |
---|
| 284 | |
---|
| 285 | /// INVARIANT: array content: llll SENTINEL xxxxx SENTINEL |
---|
| 286 | /// x: conflict binary link |
---|
| 287 | vector<LiteralIdT> binClLinks[2]; // where the variable occurrs in pos/neg |
---|
| 288 | |
---|
| 289 | unsigned int inClsVecOfs[2]; // the offset in the theInClsVector |
---|
| 290 | unsigned int iVarNum; // the number the variable had in the input file |
---|
| 291 | |
---|
| 292 | |
---|
| 293 | public: |
---|
| 294 | |
---|
| 295 | void setInClsVecOfs(bool pol, unsigned int ofs) |
---|
| 296 | { |
---|
| 297 | inClsVecOfs[pol] = ofs; |
---|
| 298 | } |
---|
| 299 | |
---|
| 300 | void setInClsVecOfs(unsigned int ofs) |
---|
| 301 | { |
---|
| 302 | unsigned int diff = inClsVecOfs[true] - inClsVecOfs[false]; |
---|
| 303 | inClsVecOfs[false] = ofs; |
---|
| 304 | inClsVecOfs[true] = ofs + diff; |
---|
| 305 | } |
---|
| 306 | |
---|
| 307 | unsigned int getInClsVecOfs(bool pol) const |
---|
| 308 | { |
---|
| 309 | return inClsVecOfs[pol]; |
---|
| 310 | } |
---|
| 311 | |
---|
| 312 | |
---|
| 313 | int scoreDLIS[2]; |
---|
| 314 | int scoreVSIDS[2]; |
---|
| 315 | |
---|
| 316 | void eraseAllEdges() |
---|
| 317 | { |
---|
| 318 | inClsVecOfs[0] = 1; |
---|
| 319 | inClsVecOfs[1] = 1; |
---|
| 320 | |
---|
| 321 | watchCls[0].clear(); |
---|
| 322 | watchCls[0].push_back(SENTINEL_CL); |
---|
| 323 | watchCls[1].clear(); |
---|
| 324 | watchCls[1].push_back(SENTINEL_CL); |
---|
| 325 | |
---|
| 326 | binClLinks[0].clear(); |
---|
| 327 | binClLinks[0].push_back(SENTINEL_LIT); |
---|
| 328 | binClLinks[0].push_back(SENTINEL_LIT); |
---|
| 329 | binClLinks[1].clear(); |
---|
| 330 | binClLinks[1].push_back(SENTINEL_LIT); |
---|
| 331 | binClLinks[1].push_back(SENTINEL_LIT); |
---|
| 332 | } |
---|
| 333 | |
---|
| 334 | |
---|
| 335 | CVariableVertex(unsigned int numofVar = 0, VarIdT index = 0): itecIndex(index), iVarNum(numofVar) |
---|
| 336 | { |
---|
| 337 | DecLevelOfDeactivation = INVALID_DL; |
---|
| 338 | theVal=X; |
---|
| 339 | |
---|
| 340 | scoreDLIS[0] = scoreDLIS[1] = 0; |
---|
| 341 | scoreVSIDS[0] = scoreVSIDS[1] = 0; |
---|
| 342 | |
---|
| 343 | eraseAllEdges(); |
---|
| 344 | } |
---|
| 345 | |
---|
| 346 | bool isolated() {return (inClsVecOfs[0] <= 1) && (inClsVecOfs[1] <= 1) |
---|
| 347 | && (binClLinks[0].size()<=2) && (binClLinks[1].size()<=2);} |
---|
| 348 | |
---|
| 349 | LiteralIdT getLitIdT(bool polarity) {return LiteralIdT(getVarIdT(),polarity);} |
---|
| 350 | |
---|
| 351 | void newtecIndex(VarIdT iIdx) {itecIndex = iIdx;} |
---|
| 352 | |
---|
| 353 | int getDLCSScore() const {return scoreDLIS[0] + scoreDLIS[1];} |
---|
| 354 | |
---|
| 355 | int getVSIDSScore(){return scoreVSIDS[0] + scoreVSIDS[1];} |
---|
| 356 | |
---|
| 357 | inline const unsigned int getVarNum() const {return iVarNum;} |
---|
| 358 | |
---|
| 359 | inline const unsigned int getVarIdT() const {return itecIndex;} |
---|
| 360 | |
---|
| 361 | int getDLOD() const {return DecLevelOfDeactivation;} |
---|
| 362 | |
---|
| 363 | bool setVal(bool aVal,unsigned int atDL, AntecedentT ant = AntecedentT(NOT_A_CLAUSE)) |
---|
| 364 | { |
---|
| 365 | if(!isActive()) return false; |
---|
| 366 | DecLevelOfDeactivation = atDL; |
---|
| 367 | |
---|
| 368 | myAntecedent = ant; |
---|
| 369 | theVal = (TriValue) aVal; |
---|
| 370 | return true; |
---|
| 371 | } |
---|
| 372 | |
---|
| 373 | void unsetVal() |
---|
| 374 | { |
---|
| 375 | myAntecedent = AntecedentT(NOT_A_CLAUSE); |
---|
| 376 | DecLevelOfDeactivation = INVALID_DL; |
---|
| 377 | theVal = X; |
---|
| 378 | } |
---|
| 379 | |
---|
| 380 | bool isImpliedBy(const ClauseIdT idCl) |
---|
| 381 | { |
---|
| 382 | if(isActive() || !myAntecedent.isAClause()) return false; |
---|
| 383 | if(myAntecedent.toCl() == idCl) return true; |
---|
| 384 | return false; |
---|
| 385 | } |
---|
| 386 | void adjustAntecedent(AntecedentT ant) {myAntecedent=ant;} |
---|
| 387 | bool isActive() const {return theVal == X;} |
---|
| 388 | |
---|
| 389 | bool flipVal() |
---|
| 390 | { |
---|
| 391 | if(theVal == W) theVal =F; |
---|
| 392 | else if(theVal == F) theVal =W; |
---|
| 393 | |
---|
| 394 | return true; |
---|
| 395 | } |
---|
| 396 | |
---|
| 397 | AntecedentT getAntecedent() {return myAntecedent;} |
---|
| 398 | |
---|
| 399 | bool getboolVal() const {return theVal==W;} |
---|
| 400 | |
---|
| 401 | TriValue getVal() const {return theVal;} |
---|
| 402 | |
---|
| 403 | unsigned int countBinLinks() const {return binClLinks[0].size() + binClLinks[1].size() - 4;} |
---|
| 404 | unsigned int countBinLinks(bool pol) const {return binClLinks[pol].size() - 2;} |
---|
| 405 | |
---|
| 406 | |
---|
| 407 | extd_vector<ClauseIdT> &getWatchClauses(bool polarity) |
---|
| 408 | { |
---|
| 409 | return watchCls[polarity]; |
---|
| 410 | } |
---|
| 411 | |
---|
| 412 | const extd_vector<ClauseIdT> &getWatchClauses(bool polarity) const |
---|
| 413 | { |
---|
| 414 | return watchCls[polarity]; |
---|
| 415 | } |
---|
| 416 | |
---|
| 417 | void addWatchClause(ClauseIdT idCl,bool polarity) |
---|
| 418 | { |
---|
| 419 | watchCls[polarity].push_back(idCl); |
---|
| 420 | } |
---|
| 421 | |
---|
| 422 | void addBinLink(bool polarity, LiteralIdT &lit) |
---|
| 423 | { |
---|
| 424 | *(binClLinks[polarity].end()-2) = lit; |
---|
| 425 | binClLinks[polarity].push_back(SENTINEL_LIT); |
---|
| 426 | } |
---|
| 427 | |
---|
| 428 | void addBinLinkCCl(bool polarity, LiteralIdT &lit) |
---|
| 429 | { |
---|
| 430 | *(binClLinks[polarity].end()-1) = lit; |
---|
| 431 | binClLinks[polarity].push_back(SENTINEL_LIT); |
---|
| 432 | } |
---|
| 433 | |
---|
| 434 | bool eraseBinLinkTo(LiteralIdT idLit, bool Linkpolarity); |
---|
| 435 | bool hasBinLinkTo(LiteralIdT idLit,bool pol) const; |
---|
| 436 | |
---|
| 437 | const vector<LiteralIdT> & getBinLinks(bool polarity) const |
---|
| 438 | { |
---|
| 439 | return binClLinks[polarity]; |
---|
| 440 | } |
---|
| 441 | vector<LiteralIdT> & getBinLinks(bool polarity) |
---|
| 442 | { |
---|
| 443 | return binClLinks[polarity]; |
---|
| 444 | } |
---|
| 445 | |
---|
| 446 | bool eraseWatchClause(ClauseIdT idCl, bool polarity); |
---|
| 447 | |
---|
| 448 | bool substituteWatchCl(bool polarity, const ClauseIdT & oldId, const ClauseIdT &newId); |
---|
| 449 | |
---|
| 450 | bool substituteBinLink(bool polarity, const LiteralIdT& oldLit, const LiteralIdT& newLit); |
---|
| 451 | |
---|
| 452 | // class destructor |
---|
| 453 | ~CVariableVertex(); |
---|
| 454 | }; |
---|
| 455 | |
---|
| 456 | #endif |
---|
| 457 | |
---|