source: vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/FormulaCache.cpp

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

add sharpSat

File size: 7.3 KB
Line 
1#include "FormulaCache.h"
2
3unsigned int CFormulaCache::oldestEntryAllowed = (unsigned int) -1;
4
5
6CFormulaCache::CFormulaCache()
7{
8    iBuckets = 900001;// =299999;       
9    theData.resize(iBuckets,NULL);
10    theBucketBase.reserve(iBuckets);
11    theEntryBase.reserve(iBuckets*10);
12    scoresDivTime = 50000;
13    lastDivTime = 0;   
14    #ifdef SUN_OS
15      if(CSolverConf::maxCacheSize == 0)
16        CSolverConf::maxCacheSize = 100*1024*1024;
17    #endif
18    #ifndef SUN_OS
19      if(CSolverConf::maxCacheSize == 0)
20      {
21       int pgs = getpagesize();
22       long int pages = get_avphys_pages();
23       CSolverConf::maxCacheSize = (pgs*pages)/2;
24      } 
25    #endif   
26}
27
28
29
30bool CFormulaCache::include(CComponentId &rComp, const CRealNum &val)
31{   
32    #ifdef DEBUG
33    // if everything is correct, a new value to be cached
34    // should not already be stored in the cache
35    assert(rComp.cachedAs == NIL_ENTRY);
36    #endif
37   
38    if(rComp.empty()) return false;   
39    iCacheTries++; 
40   
41    if(memUsage >= CSolverConf::maxCacheSize)  return false;
42   
43    long unsigned int hV = rComp.getHashKey();   
44   
45    CCacheBucket &rBucket = at(clip(hV));
46   
47     
48    CacheEntryId eId = newEntry();
49    CCacheEntry & rEntry = entry(eId);   
50    rBucket.push_back(eId);
51    rEntry.createFrom(rComp);       
52    rEntry.hashKey = hV;
53    rEntry.theVal = val;
54   
55    rComp.cachedAs = eId; // save in the Comp, wwhere it was saved
56    rEntry.theDescendants = rComp.cachedChildren; // save the cache ids of its children
57   
58    rComp.cachedChildren.clear();
59   
60    adjustDescendantsFather(eId);
61   
62   
63    //BEGIN satistics
64   
65    unsigned int memU = memUsage/(10*1024*1024);
66   
67    memUsage += rEntry.memSize();
68   
69    if(memU < memUsage/(10*1024*1024))
70    {     
71      toSTDOUT("Cache: usedMem "<< memUsage<<"Bytes\n");     
72    }   
73    iSumCachedCompSize += rComp.countVars();
74   
75    iCachedComponents++;
76    if(iCachedComponents % 50000 == 0) 
77    {
78       double d = iSumCachedCompSize;
79          d /= (double) iCachedComponents;
80       toSTDOUT("cachedComponents:"<< iCachedComponents<<" avg. size:"<<d<<endl);
81    }
82    //END satistics
83    return true;   
84}
85 
86bool CFormulaCache::extract(CComponentId &rComp, CRealNum &val)
87{       
88    long unsigned int hV = rComp.getHashKey();   
89   
90    unsigned int v = clip(hV);       
91       
92    if(!isBucketAt(v)) return false;   
93    CCacheBucket &rBucket = *theData[v]; // the location of the considered bucket
94   
95    CCacheEntry *pComp;
96   
97    for(CCacheBucket::iterator it = rBucket.begin(); it != rBucket.end();it++)
98    {
99      pComp = &entry(*it);     
100      if(hV == pComp->getHashKey() &&  pComp->equals(rComp)) 
101      {
102        val = pComp->theVal;       
103        pComp->score++;
104        pComp->score+= (unsigned int)pComp->sizeVarVec();       
105       
106        iCacheRetrievals++;
107        iSumRetrieveSize += rComp.countVars();
108       
109        if(iCacheRetrievals % 50000 == 0)
110        {
111          double d = iSumRetrieveSize;
112          d /= (double) iCacheRetrievals;
113          toSTDOUT("cache hits:"<< iCacheRetrievals<<" avg size:"<< d<<endl);
114        }
115        return true;
116       
117     }   
118   }   
119   return false;
120}
121
122int CFormulaCache::removePollutedEntries(CacheEntryId root)
123{
124  vector<CacheEntryId>::iterator it;// theDescendants;
125  CCacheBucket &rBuck = at(clip(entry(root).hashKey));
126  unsigned int n = 0;
127 
128 
129  for(CCacheBucket::iterator jt= rBuck.begin(); jt != rBuck.end(); jt++)
130  {
131    if(*jt == root)
132    {
133     rBuck.erase(jt);
134     n++;
135     break;
136    }     
137  }
138 
139  for(it = entry(root).theDescendants.begin(); it != entry(root).theDescendants.end(); it++)
140  {
141    n += removePollutedEntries(*it); 
142  } 
143 
144  entry(root).clear();
145 
146  return n;
147}
148
149bool CFormulaCache::deleteEntries(CDecisionStack & rDecStack)
150{
151  vector<CCacheBucket>::iterator jt;
152  vector<CCacheEntry>::iterator it,itWrite;
153  CCacheBucket::iterator bt;
154   
155  if(memUsage < (unsigned int) ((double) 0.85* (double)CSolverConf::maxCacheSize)) return false;
156   
157  // first : go through the EntryBase and mark the entries to be deleted as deleted (i.e. EMPTY
158  for(it = beginEntries(); it != endEntries(); it++)
159  {     
160      if(it->score <= minScoreBound)     
161      {
162        deleteFromDescendantsTree(toCacheEntryId(it));   
163        it->clear();   
164      }
165  }
166 
167  // then go through the BucketBase and rease all Links to empty entries
168  for(jt = theBucketBase.begin(); jt != theBucketBase.end(); jt++)
169  {
170    for(bt = jt->end()-1; bt != jt->begin()-1; bt--)
171    {
172      if(entry(*bt).empty()) bt = jt->erase(bt);     
173    }   
174  } 
175 
176  // now: go through the decisionStack. and delete all Links to empty entries 
177  revalidateCacheLinksIn(rDecStack.getAllCompStack());
178 
179  // finally: truly erase the empty entries, but keep the descendants tree consistent
180  long int newSZ = 0;
181  long int SumNumOfVars= 0;
182  CacheEntryId idOld,idNew;
183     
184  itWrite = beginEntries(); 
185  for(it = beginEntries(); it != endEntries(); it++)
186  {   
187    if(!it->empty())
188    {
189      if(it != itWrite)
190      {
191       *itWrite = *it;
192       idNew = toCacheEntryId(itWrite);
193       idOld = toCacheEntryId(it);
194       at(clip(itWrite->getHashKey())).substituteIds(idOld,idNew);                       
195       substituteInDescTree(idOld,idNew);
196       substituteCacheLinksIn(rDecStack.getAllCompStack(),idOld,idNew);
197      }
198      itWrite++;
199      //theEntryBase.pop_back();
200      newSZ += itWrite->memSize();
201      SumNumOfVars += itWrite->sizeVarVec();
202    }
203  }
204 
205  theEntryBase.erase(itWrite,theEntryBase.end()); 
206 
207  iCachedComponents = theEntryBase.size(); 
208  iSumCachedCompSize = SumNumOfVars*sizeof(unsigned int)*8 / CCacheEntry::bitsPerVar();
209 
210  memUsage = newSZ;
211 
212  toSTDOUT("Cache cleaned: "<<iCachedComponents<<" Components ("<< (memUsage>>10)<< " KB remain"<<endl);
213 
214  if(scoresDivTime == 0) scoresDivTime = 1;
215  double dbound = (double) 0.5* (double)CSolverConf::maxCacheSize;
216  if(memUsage < (unsigned int) dbound)
217  {
218    minScoreBound/= 2;
219    if(memUsage < 0.5*dbound) scoresDivTime *= 2;
220  }
221  else if(memUsage > (unsigned int) dbound)
222  {
223    minScoreBound <<= 1;
224    minScoreBound++;
225    scoresDivTime /= 2;
226    if(scoresDivTime < 50000) scoresDivTime = 50000;
227  }
228  toDEBUGOUT("setting scoresDivTime: "<<scoresDivTime<<endl); 
229  toDEBUGOUT("setting minScoreBound: "<<minScoreBound<<endl); 
230 
231  return true;
232}
233
234
235void CFormulaCache::revalidateCacheLinksIn(const vector<CComponentId *> &rComps)
236{
237  vector<CComponentId *>::const_iterator it;
238  vector<unsigned int>::iterator jt;
239  for(it = rComps.begin(); it !=rComps.end(); it++)
240  {
241    if(!isEntry((*it)->cachedAs)) (*it)->cachedAs = 0;
242   
243    if(isEntry((*it)->cachedAs) && entry((*it)->cachedAs).empty()) (*it)->cachedAs = 0;
244   
245    for(jt = (*it)->cachedChildren.end()-1; jt != (*it)->cachedChildren.begin()-1; jt--)
246    {
247      if((!isEntry(*jt)) || entry(*jt).empty())
248      { 
249        toDEBUGOUT("_E"); 
250        jt =(*it)->cachedChildren.erase(jt);
251      }
252    }
253  }
254}
255
256
257void CFormulaCache::substituteCacheLinksIn(const vector<CComponentId *> &rComps, CacheEntryId idOld, CacheEntryId idNew)
258{
259  vector<CComponentId *>::const_iterator it;
260  vector<unsigned int>::iterator jt;
261  for(it = rComps.begin(); it !=rComps.end(); it++)
262  {
263    if((*it)->cachedAs == idOld) (*it)->cachedAs = idNew;
264    for(jt = (*it)->cachedChildren.begin(); jt != (*it)->cachedChildren.end(); jt++)
265    {
266      if(*jt == idOld){ toDEBUGOUT("_D"); *jt = idNew;}
267    }
268  }
269}
Note: See TracBrowser for help on using the repository browser.