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 | } |
---|