source: vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp @ 9

Last change on this file since 9 was 9, checked in by cecile, 13 years ago

add sharpSat
File size: 23.3 KB
Line 
1#include "InstanceGraph.h"
2#include <math.h>
3#include<fstream>
4#include<stdio.h>
5
6CRunAnalyzer theRunAn;
7
8
9// class constructor
10CInstanceGraph::CInstanceGraph()
11{
12
13}
14       
15// class destructor
16CInstanceGraph::~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
29bool 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
55bool 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
66bool 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
79void 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
91bool 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
193bool 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
241bool 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
312bool 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
331bool 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
356bool 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
388bool 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
429bool 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
473bool 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
590bool 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
871unsigned 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
891void 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
901void 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}
Note: See TracBrowser for help on using the repository browser.