[9] | 1 | #include "InstanceGraph.h" |
---|
| 2 | #include <math.h> |
---|
| 3 | #include<fstream> |
---|
| 4 | #include<stdio.h> |
---|
| 5 | |
---|
| 6 | CRunAnalyzer theRunAn; |
---|
| 7 | |
---|
| 8 | |
---|
| 9 | // class constructor |
---|
| 10 | CInstanceGraph::CInstanceGraph() |
---|
| 11 | { |
---|
| 12 | |
---|
| 13 | } |
---|
| 14 | |
---|
| 15 | // class destructor |
---|
| 16 | CInstanceGraph::~CInstanceGraph() |
---|
| 17 | { |
---|
| 18 | toDEBUGOUT("lv sz:"<< theLitVector.size() << endl); |
---|
| 19 | toDEBUGOUT("nUcls:"<< theUnitClauses.size() << endl); |
---|
| 20 | } |
---|
| 21 | |
---|
| 22 | |
---|
| 23 | //////////////////////////////////////////////////////////////////////// |
---|
| 24 | // |
---|
| 25 | // BEGIN Methods for Clauses |
---|
| 26 | // |
---|
| 27 | /////////////////////////////////////////////////////////////////////// |
---|
| 28 | |
---|
| 29 | bool CInstanceGraph::substituteLitsOf(CClauseVertex &rCl,const LiteralIdT &oldLit, const LiteralIdT &newLit) |
---|
| 30 | { |
---|
| 31 | vector<LiteralIdT>::iterator it; |
---|
| 32 | |
---|
| 33 | if(oldLit == rCl.idLitA()) rCl.setLitA(newLit); |
---|
| 34 | else if(oldLit == rCl.idLitB()) rCl.setLitB(newLit); |
---|
| 35 | |
---|
| 36 | if(oldLit.oppositeLit() == rCl.idLitA()) rCl.setLitA(newLit.oppositeLit()); |
---|
| 37 | else if(oldLit.oppositeLit() == rCl.idLitB()) rCl.setLitB(newLit.oppositeLit()); |
---|
| 38 | |
---|
| 39 | for(it = begin(rCl); *it != ClauseEnd();it++) |
---|
| 40 | { |
---|
| 41 | if(*it == oldLit) |
---|
| 42 | { |
---|
| 43 | *it = newLit; |
---|
| 44 | return true; |
---|
| 45 | } |
---|
| 46 | else if(*it == oldLit.oppositeLit()) |
---|
| 47 | { |
---|
| 48 | *it = newLit.oppositeLit(); |
---|
| 49 | return true; |
---|
| 50 | } |
---|
| 51 | } |
---|
| 52 | return false; |
---|
| 53 | } |
---|
| 54 | |
---|
| 55 | bool CInstanceGraph::containsVar(const CClauseVertex &rCl, const VarIdT &theVar) const |
---|
| 56 | { |
---|
| 57 | vector<LiteralIdT>::const_iterator it; |
---|
| 58 | |
---|
| 59 | for(it = begin(rCl); *it != ClauseEnd();it++) |
---|
| 60 | { |
---|
| 61 | if(it->toVarIdx() == theVar) return true; |
---|
| 62 | } |
---|
| 63 | return false; |
---|
| 64 | } |
---|
| 65 | |
---|
| 66 | bool CInstanceGraph::containsLit(const CClauseVertex &rCl, const LiteralIdT &theLit) const |
---|
| 67 | { |
---|
| 68 | vector<LiteralIdT>::const_iterator it; |
---|
| 69 | |
---|
| 70 | for(it = begin(rCl); *it != ClauseEnd();it++) |
---|
| 71 | { |
---|
| 72 | if(*it == theLit) return true; |
---|
| 73 | } |
---|
| 74 | return false; |
---|
| 75 | } |
---|
| 76 | |
---|
| 77 | |
---|
| 78 | |
---|
| 79 | void CInstanceGraph::printCl(const CClauseVertex &rCl) const |
---|
| 80 | { |
---|
| 81 | vector<LiteralIdT>::const_iterator it; |
---|
| 82 | |
---|
| 83 | for(it = begin(rCl); *it != ClauseEnd();it++) |
---|
| 84 | { |
---|
| 85 | if(!(it)->polarity()) toSTDOUT("-"); |
---|
| 86 | toSTDOUT(it->toVarIdx()+1 << " "); |
---|
| 87 | } |
---|
| 88 | toSTDOUT(" 0\n"); |
---|
| 89 | } |
---|
| 90 | |
---|
| 91 | bool CInstanceGraph::createConflictClause(const vector<LiteralIdT> &theCClause) |
---|
| 92 | { |
---|
| 93 | ClauseIdT cclId; |
---|
| 94 | vector<LiteralIdT>::const_iterator it; |
---|
| 95 | |
---|
| 96 | #ifdef DEBUG |
---|
| 97 | assert(theCClause.size() > 0); |
---|
| 98 | #endif |
---|
| 99 | |
---|
| 100 | if(theCClause.size() == 1) |
---|
| 101 | { |
---|
| 102 | createUnitCl(theCClause.front()); |
---|
| 103 | if(theUnitClauses.size() == 1 || theUnitClauses.size() % 5 == 0) |
---|
| 104 | printCClstats(); |
---|
| 105 | getVar(theCClause.front()).scoreVSIDS[theCClause.front().polarity()]++; |
---|
| 106 | getVar(theCClause.front()).scoreVSIDS[theCClause.front().oppositeLit().polarity()]++; |
---|
| 107 | theRunAn.addClause(); |
---|
| 108 | return true; |
---|
| 109 | } |
---|
| 110 | |
---|
| 111 | |
---|
| 112 | if(theCClause.size() == 2) |
---|
| 113 | { |
---|
| 114 | if(!createBinCCl(theCClause[0],theCClause[1])) return false; |
---|
| 115 | |
---|
| 116 | getVar(theCClause[0]).scoreVSIDS[theCClause[0].polarity()]++; |
---|
| 117 | getVar(theCClause[1]).scoreVSIDS[theCClause[1].polarity()]++; |
---|
| 118 | getVar(theCClause[0]).scoreVSIDS[theCClause[0].oppositeLit().polarity()]++; |
---|
| 119 | getVar(theCClause[1]).scoreVSIDS[theCClause[1].oppositeLit().polarity()]++; |
---|
| 120 | |
---|
| 121 | if(numBinCCls % 100 == 0) printCClstats(); |
---|
| 122 | theRunAn.addClause(); |
---|
| 123 | return true; |
---|
| 124 | } |
---|
| 125 | |
---|
| 126 | // create the ClauseVertex |
---|
| 127 | |
---|
| 128 | cclId = makeConflictClause(); |
---|
| 129 | |
---|
| 130 | CClauseVertex *pCCl = &getClause(cclId); |
---|
| 131 | |
---|
| 132 | pCCl->setLitOfs(theLitVector.size()); |
---|
| 133 | pCCl->setLength(theCClause.size()); |
---|
| 134 | |
---|
| 135 | int score = 0; |
---|
| 136 | LiteralIdT aLit = NOT_A_LIT; |
---|
| 137 | LiteralIdT bLit = NOT_A_LIT; |
---|
| 138 | |
---|
| 139 | theLitVector.reserve(theLitVector.size() + theCClause.size()); |
---|
| 140 | for(it = theCClause.begin(); it != theCClause.end(); it++) |
---|
| 141 | { |
---|
| 142 | // add literal *it to the litvector |
---|
| 143 | theLitVector.push_back(*it); |
---|
| 144 | |
---|
| 145 | if(getVar(*it).getDLOD() >= score) |
---|
| 146 | // determine the most recently set literals to become watched |
---|
| 147 | { |
---|
| 148 | bLit = aLit; |
---|
| 149 | aLit = *it; |
---|
| 150 | score = getVar(*it).getDLOD(); |
---|
| 151 | } |
---|
| 152 | getVar(*it).scoreVSIDS[it->polarity()]++; |
---|
| 153 | getVar(*it).scoreVSIDS[it->oppositeLit().polarity()]++; |
---|
| 154 | } |
---|
| 155 | score = 0; |
---|
| 156 | if(bLit == NOT_A_LIT) |
---|
| 157 | for(it = theCClause.begin(); it != theCClause.end(); it++) |
---|
| 158 | { |
---|
| 159 | if(*it != aLit && getVar(*it).getDLOD() >= score) |
---|
| 160 | // determine the most recently set literals to become watched |
---|
| 161 | { |
---|
| 162 | bLit = *it; |
---|
| 163 | score = getVar(*it).getDLOD(); |
---|
| 164 | } |
---|
| 165 | } |
---|
| 166 | |
---|
| 167 | #ifdef DEBUG |
---|
| 168 | assert(aLit != NOT_A_LIT); |
---|
| 169 | assert(bLit != NOT_A_LIT); |
---|
| 170 | #endif |
---|
| 171 | |
---|
| 172 | // close the clause with a SENTINEL_LIT |
---|
| 173 | theLitVector.push_back(SENTINEL_LIT); |
---|
| 174 | |
---|
| 175 | // set watch for litA |
---|
| 176 | if(aLit != NOT_A_LIT) |
---|
| 177 | { |
---|
| 178 | pCCl->setLitA(aLit); |
---|
| 179 | getVar(aLit).addWatchClause(cclId,aLit.polarity()); |
---|
| 180 | } |
---|
| 181 | // set watch for litB |
---|
| 182 | if(bLit != NOT_A_LIT) |
---|
| 183 | { |
---|
| 184 | pCCl->setLitB(bLit); |
---|
| 185 | getVar(bLit).addWatchClause(cclId,bLit.polarity()); |
---|
| 186 | } |
---|
| 187 | |
---|
| 188 | if(countCCls() % 10000 == 0) printCClstats(); |
---|
| 189 | theRunAn.addClause(); |
---|
| 190 | return true; |
---|
| 191 | } |
---|
| 192 | |
---|
| 193 | bool CInstanceGraph::setCClImplyingLit(ClauseIdT idCl, const LiteralIdT &theLit) |
---|
| 194 | { |
---|
| 195 | CClauseVertex &rCV = getClause(idCl); |
---|
| 196 | vector<LiteralIdT>::const_iterator it; |
---|
| 197 | |
---|
| 198 | getVar(rCV.idLitA()).eraseWatchClause(idCl, rCV.idLitA().polarity()); |
---|
| 199 | getVar(rCV.idLitB()).eraseWatchClause(idCl, rCV.idLitB().polarity()); |
---|
| 200 | |
---|
| 201 | int score = -1; |
---|
| 202 | LiteralIdT aLit = NOT_A_LIT; |
---|
| 203 | |
---|
| 204 | |
---|
| 205 | |
---|
| 206 | #ifdef DEBUG |
---|
| 207 | bool ex = false; |
---|
| 208 | for(it = begin(rCV); *it != ClauseEnd(); it++) |
---|
| 209 | if(*it == theLit) |
---|
| 210 | { |
---|
| 211 | ex = true; |
---|
| 212 | break; |
---|
| 213 | } |
---|
| 214 | assert(ex); |
---|
| 215 | #endif |
---|
| 216 | |
---|
| 217 | rCV.setLitA(theLit); |
---|
| 218 | getVar(rCV.idLitA()).addWatchClause(idCl,rCV.idLitA().polarity()); |
---|
| 219 | // set watch for litB |
---|
| 220 | |
---|
| 221 | aLit = NOT_A_LIT; |
---|
| 222 | score = -1; |
---|
| 223 | |
---|
| 224 | for(it = begin(rCV); *it != ClauseEnd(); it++) |
---|
| 225 | if(getVar(*it).getDLOD() > score) |
---|
| 226 | { |
---|
| 227 | if(*it == theLit) continue; |
---|
| 228 | aLit = *it; |
---|
| 229 | score = getVar(*it).getDLOD(); |
---|
| 230 | } |
---|
| 231 | |
---|
| 232 | if(aLit != NOT_A_LIT) |
---|
| 233 | { |
---|
| 234 | rCV.setLitB(aLit); |
---|
| 235 | getVar(aLit).addWatchClause(idCl,aLit.polarity()); |
---|
| 236 | } |
---|
| 237 | |
---|
| 238 | return true; |
---|
| 239 | } |
---|
| 240 | |
---|
| 241 | bool CInstanceGraph::cleanUp_deletedCCls() |
---|
| 242 | { |
---|
| 243 | DepositOfClauses::iterator ct; |
---|
| 244 | |
---|
| 245 | /////////////////// |
---|
| 246 | // clean up LitVector |
---|
| 247 | /////////////////// |
---|
| 248 | |
---|
| 249 | vector<LiteralIdT>::iterator writeLit = theLitVector.begin() + (beginOfCCls())->getLitOfs(); |
---|
| 250 | ct = beginOfCCls(); |
---|
| 251 | |
---|
| 252 | for(vector<LiteralIdT>::iterator xt = writeLit;xt != theLitVector.end();xt++) |
---|
| 253 | if(*xt != NOT_A_LIT) |
---|
| 254 | { |
---|
| 255 | if(!ct->isDeleted()) |
---|
| 256 | { |
---|
| 257 | ct->setLitOfs((unsigned int)(writeLit - theLitVector.begin())); |
---|
| 258 | |
---|
| 259 | while(*xt != NOT_A_LIT) |
---|
| 260 | { |
---|
| 261 | if(writeLit != xt) *writeLit = *xt; |
---|
| 262 | xt++; |
---|
| 263 | writeLit++; |
---|
| 264 | } |
---|
| 265 | *(writeLit++) = NOT_A_LIT; |
---|
| 266 | } |
---|
| 267 | else { // *ct is deleted, hence, omit all its literals from consideration |
---|
| 268 | while(*xt != NOT_A_LIT) xt++;//*(xt++) = NOT_A_LIT; |
---|
| 269 | } |
---|
| 270 | ct++; |
---|
| 271 | } |
---|
| 272 | |
---|
| 273 | theLitVector.resize((unsigned int)(writeLit - theLitVector.begin())); |
---|
| 274 | |
---|
| 275 | DepositOfClauses::iterator itWrite = beginOfCCls(); |
---|
| 276 | /////////////////// |
---|
| 277 | // clean up clauses |
---|
| 278 | /////////////////// |
---|
| 279 | ClauseIdT oldId,newId; |
---|
| 280 | |
---|
| 281 | for(ct = beginOfCCls(); ct != endOfCCls();ct++) |
---|
| 282 | if(!ct->isDeleted()) |
---|
| 283 | { |
---|
| 284 | if(itWrite != ct) |
---|
| 285 | { |
---|
| 286 | *itWrite = *ct; |
---|
| 287 | //BEGIN substitute CCLs |
---|
| 288 | |
---|
| 289 | oldId = toClauseIdT(ct); |
---|
| 290 | newId = toClauseIdT(itWrite); |
---|
| 291 | |
---|
| 292 | if(getVar(itWrite->idLitB()).isImpliedBy(oldId)) |
---|
| 293 | getVar(itWrite->idLitB()).adjustAntecedent(AntecedentT(newId)); |
---|
| 294 | if(getVar(itWrite->idLitA()).isImpliedBy(oldId)) |
---|
| 295 | getVar(itWrite->idLitA()).adjustAntecedent(AntecedentT(newId)); |
---|
| 296 | |
---|
| 297 | getVar(itWrite->idLitA()).substituteWatchCl(itWrite->idLitA().polarity(),oldId,newId); |
---|
| 298 | getVar(itWrite->idLitB()).substituteWatchCl(itWrite->idLitB().polarity(),oldId,newId); |
---|
| 299 | //END substitute CCLs |
---|
| 300 | |
---|
| 301 | ct->setDeleted(); |
---|
| 302 | } |
---|
| 303 | itWrite++; |
---|
| 304 | } |
---|
| 305 | |
---|
| 306 | theClauses.erase(itWrite,endOfCCls()); |
---|
| 307 | |
---|
| 308 | return true; |
---|
| 309 | } |
---|
| 310 | |
---|
| 311 | |
---|
| 312 | bool CInstanceGraph::deleteConflictCls() |
---|
| 313 | { |
---|
| 314 | DepositOfClauses::iterator it; |
---|
| 315 | |
---|
| 316 | double vgl = 0; |
---|
| 317 | |
---|
| 318 | for(it = beginOfCCls(); it != endOfCCls(); it++) |
---|
| 319 | { |
---|
| 320 | vgl = 11000.0; |
---|
| 321 | if(it->length() != 0) vgl /= pow((double)it->length(),3); |
---|
| 322 | |
---|
| 323 | if(CStepTime::getTime() - it->getLastTouchTime() > vgl) |
---|
| 324 | { |
---|
| 325 | markCClDeleted(toClauseIdT(it)); |
---|
| 326 | } |
---|
| 327 | } |
---|
| 328 | return true; |
---|
| 329 | } |
---|
| 330 | |
---|
| 331 | bool CInstanceGraph::markCClDeleted(ClauseIdT idCl) |
---|
| 332 | { |
---|
| 333 | CClauseVertex & rCV = getClause(idCl); |
---|
| 334 | if(rCV.isDeleted()) return false; |
---|
| 335 | ///// |
---|
| 336 | // a clause may not be deleted if it causes an implication: |
---|
| 337 | /// |
---|
| 338 | if(getVar(rCV.idLitB()).isImpliedBy(idCl) |
---|
| 339 | ||getVar(rCV.idLitA()).isImpliedBy(idCl)) |
---|
| 340 | { |
---|
| 341 | return false; |
---|
| 342 | } |
---|
| 343 | |
---|
| 344 | getVar(rCV.idLitB()).eraseWatchClause(idCl, rCV.idLitB().polarity()); |
---|
| 345 | getVar(rCV.idLitA()).eraseWatchClause(idCl, rCV.idLitA().polarity()); |
---|
| 346 | rCV.setDeleted(); |
---|
| 347 | return true; |
---|
| 348 | } |
---|
| 349 | |
---|
| 350 | //////////////////////////////////////////////////////////////////////// |
---|
| 351 | // |
---|
| 352 | // END Methods for Clauses |
---|
| 353 | // |
---|
| 354 | /////////////////////////////////////////////////////////////////////// |
---|
| 355 | |
---|
| 356 | bool CInstanceGraph::prep_substituteClauses(unsigned int oldIdx, unsigned int newIdx) |
---|
| 357 | { |
---|
| 358 | CClauseVertex &rCl = getClause(newIdx); |
---|
| 359 | vector<LiteralIdT>::const_iterator it; |
---|
| 360 | vector<ClauseIdT>::iterator jt; |
---|
| 361 | ClauseIdT oldId(oldIdx),newId(newIdx); |
---|
| 362 | |
---|
| 363 | |
---|
| 364 | if(getVar(rCl.idLitB()).isImpliedBy(oldId)) |
---|
| 365 | getVar(rCl.idLitB()).adjustAntecedent(AntecedentT(newId)); |
---|
| 366 | |
---|
| 367 | if(getVar(rCl.idLitA()).isImpliedBy(oldId)) |
---|
| 368 | getVar(rCl.idLitA()).adjustAntecedent(AntecedentT(newId)); |
---|
| 369 | |
---|
| 370 | |
---|
| 371 | getVar(rCl.idLitA()).substituteWatchCl(rCl.idLitA().polarity(),oldId,newId); |
---|
| 372 | getVar(rCl.idLitB()).substituteWatchCl(rCl.idLitB().polarity(),oldId,newId); |
---|
| 373 | |
---|
| 374 | for(it = begin(rCl); *it != ClauseEnd(); it++) |
---|
| 375 | { |
---|
| 376 | // substitute ClEdges in theInClsVector |
---|
| 377 | for(vector<ClauseIdT>::iterator jt = var_InClsBegin(it->toVarIdx(),false);*jt != SENTINEL_CL; jt++) |
---|
| 378 | { |
---|
| 379 | if(*jt == oldId) *jt = newId; |
---|
| 380 | } |
---|
| 381 | // |
---|
| 382 | } |
---|
| 383 | |
---|
| 384 | return true; |
---|
| 385 | } |
---|
| 386 | |
---|
| 387 | |
---|
| 388 | bool CInstanceGraph::prep_substituteVars(CVariableVertex &rV, unsigned int newIdx) |
---|
| 389 | // only valid if no conflict clauses are present |
---|
| 390 | { |
---|
| 391 | vector<ClauseIdT>::const_iterator it; |
---|
| 392 | vector<LiteralIdT>::iterator kt,vt; |
---|
| 393 | |
---|
| 394 | vector<LiteralIdT>::iterator jt; |
---|
| 395 | unsigned int oldIdx = rV.getVarIdT(); |
---|
| 396 | rV.newtecIndex(newIdx); |
---|
| 397 | |
---|
| 398 | LiteralIdT oldLit, newLit; |
---|
| 399 | |
---|
| 400 | oldLit = LiteralIdT(oldIdx,true); |
---|
| 401 | newLit = LiteralIdT(newIdx,true); |
---|
| 402 | |
---|
| 403 | for(it = var_InClsBegin(rV.getVarIdT(),true); *it != SENTINEL_CL; it++) |
---|
| 404 | { |
---|
| 405 | substituteLitsOf(getClause(*it),oldLit,newLit); |
---|
| 406 | } |
---|
| 407 | |
---|
| 408 | for(kt = rV.getBinLinks(true).begin(); *kt != SENTINEL_LIT; kt++) |
---|
| 409 | { |
---|
| 410 | getVar(*kt).substituteBinLink(kt->polarity(),oldLit,newLit); |
---|
| 411 | } |
---|
| 412 | |
---|
| 413 | oldLit = LiteralIdT(oldIdx,false); |
---|
| 414 | newLit = LiteralIdT(newIdx,false); |
---|
| 415 | |
---|
| 416 | for(it = var_InClsBegin(rV.getVarIdT(),true)-1; *it != SENTINEL_CL; it--) |
---|
| 417 | { |
---|
| 418 | substituteLitsOf(getClause(*it),oldLit,newLit); |
---|
| 419 | } |
---|
| 420 | |
---|
| 421 | for(kt = rV.getBinLinks(false).begin(); *kt != SENTINEL_LIT; kt++) |
---|
| 422 | { |
---|
| 423 | getVar(*kt).substituteBinLink(kt->polarity(),oldLit,newLit); |
---|
| 424 | } |
---|
| 425 | return true; |
---|
| 426 | } |
---|
| 427 | |
---|
| 428 | |
---|
| 429 | bool CInstanceGraph::eraseLiteralFromCl(ClauseIdT idCl,LiteralIdT theLit) |
---|
| 430 | { |
---|
| 431 | bool retV = false; |
---|
| 432 | CClauseVertex & rCV = getClause(idCl); |
---|
| 433 | vector<LiteralIdT>::iterator it; |
---|
| 434 | vector<LiteralIdT>::iterator endCl = begin(rCV) + rCV.length(); |
---|
| 435 | if(rCV.isDeleted()) return false; |
---|
| 436 | |
---|
| 437 | if(getVar(rCV.idLitA()).isImpliedBy(idCl) |
---|
| 438 | || getVar(rCV.idLitB()).isImpliedBy(idCl)) return false; |
---|
| 439 | |
---|
| 440 | getVar(rCV.idLitA()).eraseWatchClause(idCl, rCV.idLitA().polarity()); |
---|
| 441 | if(rCV.length() >= 2) |
---|
| 442 | getVar(rCV.idLitB()).eraseWatchClause(idCl, rCV.idLitB().polarity()); |
---|
| 443 | |
---|
| 444 | for(it = begin(rCV); *it != ClauseEnd();it++) |
---|
| 445 | { |
---|
| 446 | if((*it) == theLit) |
---|
| 447 | { |
---|
| 448 | if(it != endCl-1) *it = *(endCl-1); |
---|
| 449 | *(endCl-1) = NOT_A_LIT; |
---|
| 450 | rCV.setLength(rCV.length()-1); |
---|
| 451 | retV = true; |
---|
| 452 | break; |
---|
| 453 | } |
---|
| 454 | } |
---|
| 455 | |
---|
| 456 | rCV.setLitA(NOT_A_LIT); |
---|
| 457 | rCV.setLitB(NOT_A_LIT); |
---|
| 458 | |
---|
| 459 | if(rCV.length() >= 1) |
---|
| 460 | { |
---|
| 461 | rCV.setLitA(*begin(rCV)); |
---|
| 462 | getVar(rCV.idLitA()).addWatchClause(idCl, rCV.idLitA().polarity()); |
---|
| 463 | } |
---|
| 464 | if(rCV.length() >= 2) |
---|
| 465 | { |
---|
| 466 | rCV.setLitB(*(begin(rCV)+1)); |
---|
| 467 | getVar(rCV.idLitB()).addWatchClause(idCl, rCV.idLitB().polarity()); |
---|
| 468 | } |
---|
| 469 | |
---|
| 470 | return retV; |
---|
| 471 | } |
---|
| 472 | |
---|
| 473 | bool CInstanceGraph::prep_CleanUpPool() |
---|
| 474 | { |
---|
| 475 | /////////////////// |
---|
| 476 | // clean up clauses |
---|
| 477 | /////////////////// |
---|
| 478 | DepositOfClauses::iterator ct, ctWrite = theClauses.begin()+1; |
---|
| 479 | |
---|
| 480 | for(ct = theClauses.begin()+1; ct != theClauses.end();ct++) |
---|
| 481 | if(!ct->isDeleted()) |
---|
| 482 | { |
---|
| 483 | if(ctWrite != ct) |
---|
| 484 | { |
---|
| 485 | *ctWrite = *ct; |
---|
| 486 | prep_substituteClauses((unsigned int)(ct - theClauses.begin()), (unsigned int)(ctWrite - theClauses.begin())); |
---|
| 487 | } |
---|
| 488 | ctWrite++; |
---|
| 489 | } |
---|
| 490 | |
---|
| 491 | theClauses.erase(ctWrite,theClauses.end()); |
---|
| 492 | iOfsBeginConflictClauses = theClauses.size(); |
---|
| 493 | /////////////////// |
---|
| 494 | // clean up LitVector |
---|
| 495 | /////////////////// |
---|
| 496 | |
---|
| 497 | vector<LiteralIdT>::iterator writeLit = theLitVector.begin(); |
---|
| 498 | |
---|
| 499 | ct = theClauses.begin()+1; |
---|
| 500 | |
---|
| 501 | for(vector<LiteralIdT>::iterator xt = writeLit;xt != theLitVector.end();xt++) |
---|
| 502 | if(*xt != SENTINEL_LIT) // start of the next clause found |
---|
| 503 | { |
---|
| 504 | ct->setLitOfs((unsigned int) (writeLit - theLitVector.begin())); |
---|
| 505 | ct++; |
---|
| 506 | while(*xt != SENTINEL_LIT) |
---|
| 507 | { |
---|
| 508 | if(writeLit != xt) *writeLit = *xt; |
---|
| 509 | xt++; writeLit++; |
---|
| 510 | } |
---|
| 511 | *writeLit = NOT_A_LIT; |
---|
| 512 | writeLit++; |
---|
| 513 | } |
---|
| 514 | |
---|
| 515 | theLitVector.resize((unsigned int) (writeLit - theLitVector.begin())); |
---|
| 516 | |
---|
| 517 | |
---|
| 518 | /////////////////// |
---|
| 519 | // clean up vars |
---|
| 520 | /////////////////// |
---|
| 521 | |
---|
| 522 | DepositOfVars::iterator it, itWriteVar = theVars.begin()+1; |
---|
| 523 | |
---|
| 524 | for(it = theVars.begin()+1; it != theVars.end();it++) |
---|
| 525 | { |
---|
| 526 | if(!it->isolated() || it->isActive()) |
---|
| 527 | { |
---|
| 528 | if(itWriteVar != it) |
---|
| 529 | { |
---|
| 530 | *itWriteVar = *it; |
---|
| 531 | prep_substituteVars(*itWriteVar, itWriteVar - theVars.begin()); |
---|
| 532 | } |
---|
| 533 | itWriteVar++; |
---|
| 534 | } |
---|
| 535 | } |
---|
| 536 | |
---|
| 537 | theVars.erase(itWriteVar,theVars.end()); |
---|
| 538 | |
---|
| 539 | |
---|
| 540 | it = theVars.begin()+1; |
---|
| 541 | /////////////////// |
---|
| 542 | // clean up inCls |
---|
| 543 | ////////////////// |
---|
| 544 | |
---|
| 545 | vector<ClauseIdT>::iterator clt, cltWrite = theInClsVector.begin()+2; |
---|
| 546 | for(clt = theInClsVector.begin()+2;clt != theInClsVector.end();clt++) |
---|
| 547 | if(*clt != SENTINEL_CL) |
---|
| 548 | { |
---|
| 549 | while(theInClsVector[it->getInClsVecOfs(false)] == SENTINEL_CL |
---|
| 550 | && theInClsVector[it->getInClsVecOfs(true)] == SENTINEL_CL) |
---|
| 551 | { |
---|
| 552 | it->setInClsVecOfs(false,0); |
---|
| 553 | it->setInClsVecOfs(true,1); |
---|
| 554 | it++; |
---|
| 555 | } |
---|
| 556 | |
---|
| 557 | { |
---|
| 558 | it->setInClsVecOfs((unsigned int)(cltWrite - theInClsVector.begin())); |
---|
| 559 | |
---|
| 560 | while(*clt != SENTINEL_CL) |
---|
| 561 | { |
---|
| 562 | if(cltWrite != clt) *cltWrite = *clt; |
---|
| 563 | clt++; |
---|
| 564 | cltWrite++; |
---|
| 565 | } |
---|
| 566 | *(cltWrite++) = SENTINEL_CL; |
---|
| 567 | } |
---|
| 568 | it++; |
---|
| 569 | } |
---|
| 570 | |
---|
| 571 | theInClsVector.resize((unsigned int) (cltWrite - theInClsVector.begin())); |
---|
| 572 | |
---|
| 573 | theUnitClauses.clear(); |
---|
| 574 | theUClLookUp.clear(); |
---|
| 575 | theUClLookUp.resize(theVars.size(),X); |
---|
| 576 | |
---|
| 577 | unsigned int countBinCl= 0; |
---|
| 578 | // as the number of binary clauses might have changed, |
---|
| 579 | // we have to update the numBinClauses, which keeps track of the # of bin Clauses |
---|
| 580 | for(it = theVars.begin(); it != theVars.end();it++) |
---|
| 581 | { |
---|
| 582 | countBinCl += it->countBinLinks(); |
---|
| 583 | } |
---|
| 584 | numBinClauses = countBinCl>>1; |
---|
| 585 | |
---|
| 586 | toDEBUGOUT("inCls sz:"<<theInClsVector.size()*sizeof(ClauseIdT)<<" "<<endl); |
---|
| 587 | return true; |
---|
| 588 | } |
---|
| 589 | |
---|
| 590 | bool CInstanceGraph::createfromFile(const char* lpstrFileName) |
---|
| 591 | { |
---|
| 592 | |
---|
| 593 | const int BUF_SZ = 65536; |
---|
| 594 | const int TOK_SZ = 255; |
---|
| 595 | |
---|
| 596 | char buf[BUF_SZ]; |
---|
| 597 | char token[TOK_SZ]; |
---|
| 598 | unsigned int line = 0; |
---|
| 599 | unsigned int nVars, nCls; |
---|
| 600 | int lit; |
---|
| 601 | vector<int> litVec; |
---|
| 602 | vector<TriValue> seenV; |
---|
| 603 | int clauseLen = 0; |
---|
| 604 | TriValue pol; |
---|
| 605 | |
---|
| 606 | vector<int> varPosMap; |
---|
| 607 | |
---|
| 608 | // BEGIN INIT |
---|
| 609 | reset(); // clear everything |
---|
| 610 | // END INIT |
---|
| 611 | |
---|
| 612 | ///BEGIN File input |
---|
| 613 | FILE *filedesc; |
---|
| 614 | filedesc = fopen(lpstrFileName,"r"); |
---|
| 615 | if(filedesc == NULL){toERROUT(" Error opening file "<< lpstrFileName<<endl); exit(3);} |
---|
| 616 | fclose(filedesc); |
---|
| 617 | |
---|
| 618 | ifstream inFile(lpstrFileName,ios::in); //TODO change this: check if file exists |
---|
| 619 | |
---|
| 620 | // read the preamble of the cnf file |
---|
| 621 | while(inFile.getline(buf,BUF_SZ)) |
---|
| 622 | { |
---|
| 623 | line++; |
---|
| 624 | if(buf[0] == 'c') continue; |
---|
| 625 | if(buf[0] == 'p') |
---|
| 626 | { |
---|
| 627 | if(sscanf (buf, "p cnf %d %d", &nVars, &nCls) < 2) |
---|
| 628 | { |
---|
| 629 | toERROUT("line "<<line<<": failed reading problem line \n"); |
---|
| 630 | exit(3); |
---|
| 631 | } |
---|
| 632 | break; |
---|
| 633 | } |
---|
| 634 | else |
---|
| 635 | { |
---|
| 636 | toERROUT("line"<<line<<": problem line expected "<<endl); |
---|
| 637 | } |
---|
| 638 | } |
---|
| 639 | int i,j; |
---|
| 640 | // now read the data |
---|
| 641 | while(inFile.getline(buf,BUF_SZ)) |
---|
| 642 | { |
---|
| 643 | line++; |
---|
| 644 | i = 0; |
---|
| 645 | j = 0; |
---|
| 646 | if(buf[0] == 'c') continue; |
---|
| 647 | while(buf[i] != 0x0) |
---|
| 648 | { |
---|
| 649 | |
---|
| 650 | while(buf[i] != 0x0 && buf[i] != '-' &&(buf[i] < '0' || buf[i] > '9')) i++; |
---|
| 651 | while(buf[i] == '-' || buf[i] >= '0' && buf[i] <= '9') |
---|
| 652 | { |
---|
| 653 | token[j] = buf[i]; |
---|
| 654 | i++; j++; |
---|
| 655 | } |
---|
| 656 | token[j] = 0x0; |
---|
| 657 | lit = atoi(token); |
---|
| 658 | j = 0; |
---|
| 659 | if(lit == 0) // end of clause |
---|
| 660 | { |
---|
| 661 | if(clauseLen > 0) litVec.push_back(0); |
---|
| 662 | clauseLen = 0; |
---|
| 663 | } |
---|
| 664 | else { |
---|
| 665 | clauseLen++; |
---|
| 666 | litVec.push_back(lit); |
---|
| 667 | } |
---|
| 668 | } |
---|
| 669 | } |
---|
| 670 | |
---|
| 671 | |
---|
| 672 | if(!inFile.eof()){ toERROUT(" CNF input: line too long");} |
---|
| 673 | inFile.close(); |
---|
| 674 | /// END FILE input |
---|
| 675 | |
---|
| 676 | |
---|
| 677 | vector<int>::iterator it, jt, itEndCl; |
---|
| 678 | |
---|
| 679 | int actVar; |
---|
| 680 | bool istaut = true; |
---|
| 681 | int imultipleLits = 0; |
---|
| 682 | int ilitA, ilitB, lengthCl; |
---|
| 683 | LiteralIdT LitA,LitB; |
---|
| 684 | ClauseIdT idCl; |
---|
| 685 | |
---|
| 686 | seenV.resize(nVars+1,X); |
---|
| 687 | varPosMap.resize(nVars+1,-1); |
---|
| 688 | theVars.reserve(nVars+1); |
---|
| 689 | theLitVector.reserve(litVec.size()); |
---|
| 690 | theClauses.reserve(nCls + 10000); |
---|
| 691 | theRunAn.init(nVars,nCls); |
---|
| 692 | |
---|
| 693 | vector<vector<ClauseIdT> > _inClLinks[2]; |
---|
| 694 | |
---|
| 695 | _inClLinks[0].resize(nVars+1); |
---|
| 696 | _inClLinks[1].resize(nVars+1); |
---|
| 697 | |
---|
| 698 | it = litVec.begin(); |
---|
| 699 | |
---|
| 700 | |
---|
| 701 | |
---|
| 702 | while(it != litVec.end()) |
---|
| 703 | { |
---|
| 704 | jt = it; |
---|
| 705 | istaut = false; |
---|
| 706 | imultipleLits = 0; |
---|
| 707 | ilitA = 0; ilitB = 0; // we pick two literals from each clause for watch- or bin-creation |
---|
| 708 | lengthCl = 0; |
---|
| 709 | while(*jt != 0) // jt passes through the clause to determine if it is valid |
---|
| 710 | { |
---|
| 711 | actVar = abs(*jt); |
---|
| 712 | if(seenV[actVar] == X) // literal not seen |
---|
| 713 | { |
---|
| 714 | seenV[actVar] = (*jt > 0)?W:F; |
---|
| 715 | if(ilitA == 0) ilitA = *jt; |
---|
| 716 | else if(ilitB == 0) ilitB = *jt; |
---|
| 717 | jt++; |
---|
| 718 | } |
---|
| 719 | else if(seenV[actVar] == (*jt > 0)?W:F) |
---|
| 720 | { // literal occurs twice: omit it |
---|
| 721 | *jt = 0; |
---|
| 722 | imultipleLits++; |
---|
| 723 | jt++; |
---|
| 724 | } |
---|
| 725 | else |
---|
| 726 | { // literal in two opposing polarities -> don't include this clause (INVALID) |
---|
| 727 | istaut = true; |
---|
| 728 | while(*jt != 0) jt++; |
---|
| 729 | //cout <<"X"; |
---|
| 730 | break; |
---|
| 731 | } |
---|
| 732 | } |
---|
| 733 | |
---|
| 734 | itEndCl = jt; |
---|
| 735 | lengthCl = (int)(itEndCl - it) - imultipleLits; |
---|
| 736 | |
---|
| 737 | if(!istaut && lengthCl > 0) // if the clause is not tautological, add it |
---|
| 738 | { |
---|
| 739 | #ifdef DEBUG |
---|
| 740 | if(ilitA == 0){ toERROUT("ERR"); exit(3);} |
---|
| 741 | #endif |
---|
| 742 | |
---|
| 743 | actVar = abs(ilitA); |
---|
| 744 | if(varPosMap[actVar]== -1) // create new Var if not present yet |
---|
| 745 | varPosMap[actVar] = makeVariable(actVar); |
---|
| 746 | |
---|
| 747 | LitA = LiteralIdT(varPosMap[actVar],(ilitA > 0)?W:F); |
---|
| 748 | |
---|
| 749 | |
---|
| 750 | if(ilitB != 0)// determine LiteralIdT for ilitB |
---|
| 751 | { |
---|
| 752 | actVar = abs(ilitB); |
---|
| 753 | if(varPosMap[actVar]== -1) // create new Var if not present yet |
---|
| 754 | varPosMap[actVar] = makeVariable(actVar); |
---|
| 755 | |
---|
| 756 | LitB = LiteralIdT(varPosMap[actVar],(ilitB > 0)?W:F); |
---|
| 757 | } |
---|
| 758 | |
---|
| 759 | |
---|
| 760 | if(lengthCl == 1) |
---|
| 761 | { |
---|
| 762 | theUnitClauses.push_back(LitA); |
---|
| 763 | } |
---|
| 764 | else if(lengthCl == 2) |
---|
| 765 | { |
---|
| 766 | #ifdef DEBUG |
---|
| 767 | if(ilitB == 0) { toERROUT("ERR BIN CL"); exit(3);} |
---|
| 768 | #endif |
---|
| 769 | |
---|
| 770 | if(!getVar(LitA).hasBinLinkTo(LitB,LitA.polarity())) |
---|
| 771 | { |
---|
| 772 | getVar(LitA).addBinLink(LitA.polarity(),LitB); |
---|
| 773 | getVar(LitB).addBinLink(LitB.polarity(),LitA); |
---|
| 774 | numBinClauses++; |
---|
| 775 | } |
---|
| 776 | } |
---|
| 777 | else |
---|
| 778 | { |
---|
| 779 | #ifdef DEBUG |
---|
| 780 | if(ilitB == 0) { toERROUT("ERR CL"); exit(3);} |
---|
| 781 | #endif |
---|
| 782 | idCl = makeClause(); |
---|
| 783 | getClause(idCl).setLitOfs(theLitVector.size()); |
---|
| 784 | |
---|
| 785 | theLitVector.push_back(LitA); |
---|
| 786 | |
---|
| 787 | /// new |
---|
| 788 | _inClLinks[LitA.polarity()][LitA.toVarIdx()].push_back(idCl); |
---|
| 789 | getVar(LitA).scoreDLIS[LitA.polarity()]++; |
---|
| 790 | /// |
---|
| 791 | theLitVector.push_back(LitB); |
---|
| 792 | |
---|
| 793 | /// new |
---|
| 794 | _inClLinks[LitB.polarity()][LitB.toVarIdx()].push_back(idCl); |
---|
| 795 | getVar(LitB).scoreDLIS[LitB.polarity()]++; |
---|
| 796 | /// |
---|
| 797 | |
---|
| 798 | for(jt = it+2; jt != itEndCl;jt++) |
---|
| 799 | if(*jt != 0 && *jt != ilitB) // add all nonzero literals |
---|
| 800 | { |
---|
| 801 | actVar = abs(*jt); |
---|
| 802 | pol = (*jt > 0)?W:F; |
---|
| 803 | if(varPosMap[actVar]== -1) // create new Var |
---|
| 804 | varPosMap[actVar] = makeVariable(actVar); |
---|
| 805 | |
---|
| 806 | // add lit to litvector |
---|
| 807 | theLitVector.push_back(LiteralIdT(varPosMap[actVar],pol)); |
---|
| 808 | /// new |
---|
| 809 | _inClLinks[pol][varPosMap[actVar]].push_back(idCl); |
---|
| 810 | getVar(varPosMap[actVar]).scoreDLIS[pol]++; |
---|
| 811 | /// |
---|
| 812 | } |
---|
| 813 | // make an end: SENTINEL_LIT |
---|
| 814 | theLitVector.push_back(SENTINEL_LIT); |
---|
| 815 | |
---|
| 816 | getClause(idCl).setLitA(LitA); |
---|
| 817 | getClause(idCl).setLitB(LitB); |
---|
| 818 | getClause(idCl).setLength(lengthCl); |
---|
| 819 | |
---|
| 820 | getVar(LitA).addWatchClause(idCl,LitA.polarity()); |
---|
| 821 | getVar(LitB).addWatchClause(idCl,LitB.polarity()); |
---|
| 822 | } |
---|
| 823 | |
---|
| 824 | } |
---|
| 825 | |
---|
| 826 | // undo the entries in seenV |
---|
| 827 | for(jt = it; jt != itEndCl;jt++) seenV[abs(*jt)] = X; |
---|
| 828 | |
---|
| 829 | it = itEndCl; |
---|
| 830 | it++; |
---|
| 831 | } |
---|
| 832 | |
---|
| 833 | |
---|
| 834 | |
---|
| 835 | //BEGIN initialize theInClsVector |
---|
| 836 | theInClsVector.clear(); |
---|
| 837 | theInClsVector.reserve(theLitVector.size() + nVars); |
---|
| 838 | theInClsVector.push_back(SENTINEL_CL); |
---|
| 839 | vector<ClauseIdT>::iterator clt; |
---|
| 840 | for(unsigned int i = 0; i <= nVars; i++) |
---|
| 841 | { |
---|
| 842 | getVar(i).setInClsVecOfs(false,theInClsVector.size()); |
---|
| 843 | for(clt = _inClLinks[0][i].begin(); clt != _inClLinks[0][i].end(); clt++) |
---|
| 844 | { |
---|
| 845 | theInClsVector.push_back(*clt); |
---|
| 846 | } |
---|
| 847 | |
---|
| 848 | getVar(i).setInClsVecOfs(true,theInClsVector.size()); |
---|
| 849 | for(clt = _inClLinks[1][i].begin(); clt != _inClLinks[1][i].end(); clt++) |
---|
| 850 | { |
---|
| 851 | theInClsVector.push_back(*clt); |
---|
| 852 | } |
---|
| 853 | theInClsVector.push_back(SENTINEL_CL); |
---|
| 854 | } |
---|
| 855 | //END initialize theInClsVector |
---|
| 856 | |
---|
| 857 | #ifdef DEBUG |
---|
| 858 | assert(theInClsVector.size() <= theLitVector.size() + nVars + 1); |
---|
| 859 | toDEBUGOUT("inCls sz:"<<theInClsVector.size()*sizeof(ClauseIdT)<<" "<<endl); |
---|
| 860 | toDEBUGOUT("lsz: "<< theLitVector.size()*sizeof(unsigned int)<< " bytes"<<endl); |
---|
| 861 | #endif |
---|
| 862 | |
---|
| 863 | theUClLookUp.resize(theVars.size()+1,X); |
---|
| 864 | iOfsBeginConflictClauses = theClauses.size(); |
---|
| 865 | |
---|
| 866 | theRunAn.setUsedVars(countAllVars()); |
---|
| 867 | return true; |
---|
| 868 | } |
---|
| 869 | |
---|
| 870 | |
---|
| 871 | unsigned int CInstanceGraph::countActiveBinLinks(VarIdT theVar) const |
---|
| 872 | { |
---|
| 873 | unsigned int n =0; |
---|
| 874 | |
---|
| 875 | const CVariableVertex &rVar = getVar(theVar); |
---|
| 876 | vector<LiteralIdT>::const_iterator bt; |
---|
| 877 | |
---|
| 878 | for(bt = rVar.getBinLinks(true).begin(); bt != rVar.getBinLinks(true).end(); bt++) |
---|
| 879 | { |
---|
| 880 | if(*bt != SENTINEL_LIT) n+= (unsigned int)getVar(*bt).isActive(); |
---|
| 881 | } |
---|
| 882 | |
---|
| 883 | for(bt = rVar.getBinLinks(false).begin(); bt != rVar.getBinLinks(false).end(); bt++) |
---|
| 884 | { |
---|
| 885 | if(*bt != SENTINEL_LIT) n+= (unsigned int)getVar(*bt).isActive(); |
---|
| 886 | } |
---|
| 887 | |
---|
| 888 | return n; |
---|
| 889 | } |
---|
| 890 | |
---|
| 891 | void CInstanceGraph::print() |
---|
| 892 | { |
---|
| 893 | DepositOfClauses::iterator it; |
---|
| 894 | for(it = theClauses.begin()+1; it != theClauses.end();it++) |
---|
| 895 | { |
---|
| 896 | printCl(*it); |
---|
| 897 | } |
---|
| 898 | } |
---|
| 899 | |
---|
| 900 | |
---|
| 901 | void CInstanceGraph::printActiveClause(const ClauseIdT &idCl) const |
---|
| 902 | { |
---|
| 903 | vector<LiteralIdT>::const_iterator it; |
---|
| 904 | toSTDOUT("("); |
---|
| 905 | |
---|
| 906 | for(it = begin(getClause(idCl)); *it != ClauseEnd();it++) |
---|
| 907 | { |
---|
| 908 | if(getVar(*it).isActive()) |
---|
| 909 | { |
---|
| 910 | if(it->polarity()) toSTDOUT(" ") else toSTDOUT("-"); |
---|
| 911 | |
---|
| 912 | toSTDOUT(it->toVarIdx() << " "); |
---|
| 913 | } |
---|
| 914 | } |
---|
| 915 | toSTDOUT(")"); |
---|
| 916 | } |
---|