source: vis_dev/sharpSAT/src/shared/Interface/AnalyzerData.cpp @ 42

// Class automatically generated by Dev-C++ New Class wizard

#include "AnalyzerData.h" // class's header file

// class constructor
AnalyzerData::AnalyzerData()
{
    init();
}

void AnalyzerData::init()
{
    nVars = 0;
    nUsedVars = 0;
    
    nOriginalClauses = 0;
    
    nRemovedClauses = 0;    
    
    nAddedClauses = 0;
    
    evalData.clear();
    evalData.resize(XX_MAX_IDX,0.0);
    
    nReceivedSatAssignments = 0;   
    
    rnProbOfSat = 0.0;   
     
    nConflicts = 0;
    nImplications = 0;
    nImplicitImplications = 0;
    nProcessedComponents = 0;
        
    maxDecLevel = 0;
    nDecisions = 0;    
}

void AnalyzerData::loadFromFile(const char *lpcstrFileName)
{
  ifstream in(lpcstrFileName);
  
  init();
  
  const int sz = 1024;
  char buf[sz];
  char desc[100];
  
  bool valIdentified = false;
  
  memset(desc,0,100);
  while(in.getline(desc,100))
  {
    valIdentified = false;
    
    for(unsigned int i = 0; i < INT_MAX_ID; i++)
     if(!strcmp(desc,intDataDesc[i]))
      {
        valIdentified = true;   
        in.getline(buf,sz);
        setI((INT_DATA_ID) i, atoi(buf));
        break;
      }    
    
    
    if(!valIdentified)
     for(int i = 0; i < XX_MAX_IDX; i++)
      if(!strcmp(desc,doubleDataDesc[i]))
      {
        valIdentified = true;
        in.getline(buf,sz);
        evalData[i] = strtod(buf,NULL);
        break;
      }    
     
    if(!valIdentified)
    {
      if(!strcmp(desc,"time"))
      {
       in.getline(buf,sz);
       elapsedTime = strtod(buf,NULL);
      }       
      else if(!strcmp(desc,"SolverExitState"))
      {
         in.getline(buf,sz);
         theExitState = (SOLVER_StateT) atoi(buf);
      } else if(!strcmp(desc,"rnProbOfSAT"))
      {
         in >> rnProbOfSat;      
      }    
    }     
  }
}


void AnalyzerData::writeToFile(const char *lpcstrFileName) const
{
  ofstream out(lpcstrFileName);
  
  for(int i = 0; i < INT_MAX_ID;i++)
  {
     out<<intDataDesc[i]<<endl;   
     out<<getI((INT_DATA_ID)i)<<endl;
  }
  
  for(int i = 0; i < XX_MAX_IDX;i++)
  {
     out<<doubleDataDesc[i]<<endl;   
     out<<get((DATA_IDX)i)<<endl;
  }
  
  out<<"time"<<endl;
  out<<elapsedTime<<endl;
    
  out<<"SolverExitState"<<endl;
  out<<theExitState<<endl;
  
  #ifdef GMP_BIGNUM
    char buf[nVars+2];
    memset(buf,0,nVars+2);
    mp_exp_t exp;
    mpf_get_str(buf,&exp,10,nVars+2,rnProbOfSat.get_mpf_t());
 
    out<<"rnProbOfSAT"<<endl;
    out<<"0."<<buf<<"e"<<exp<<endl;
  #else
    out<<"rnProbOfSAT"<<endl;
    out<<rnProbOfSat<<endl;
  #endif
}



unsigned int AnalyzerData::getI(INT_DATA_ID idataID) const
{
  unsigned int res = 0;
  
  switch(idataID)
  {
    case NVARS: res = nVars;
                break;
    case NUSED_VARS: res = nUsedVars;
                break;
    case NORIGINAL_CLAUSES: res = nOriginalClauses;
                break;
    case NREMOVED_CLAUSES: res = nRemovedClauses;
                break;
    case NADDED_CLAUSES: res = nAddedClauses;
                break;
    case NRECEIVED_ASS:  res = nReceivedSatAssignments;
                break;
    case NCONFLICTS: res = nConflicts; 
                break;
    case NIMPLICATIONS: res = nImplications; 
                break;
    case NIBCPIMPLS: res = nImplicitImplications; 
                break;
    case NPROCESSED_COMPS:res = nProcessedComponents; 
                break;
    case MAX_DL: res = maxDecLevel; 
                break;
    case MAX_SOL_DL: res = maxSolutionLevel;
                break;
    case NDECISIONS: res = nDecisions;     
                break;
    default: break;
  };

  return res;
}


bool AnalyzerData::setI(INT_DATA_ID idataID, int val)
{ 
  switch(idataID)
  {
    case NVARS: nVars = val;
                break;
    case NUSED_VARS: nUsedVars = val;
                break;
    case NORIGINAL_CLAUSES: nOriginalClauses = val;
                break;
    case NREMOVED_CLAUSES: nRemovedClauses = val;
                break;
    case NADDED_CLAUSES: nAddedClauses = val;
                break;
    case NRECEIVED_ASS:  nReceivedSatAssignments = val;
                break;
    case NCONFLICTS: nConflicts = val; 
                break;
    case NIMPLICATIONS: nImplications = val; 
                break;
    case NIBCPIMPLS: nImplicitImplications = val; 
                break;
    case NPROCESSED_COMPS: nProcessedComponents = val; 
                break;
    case MAX_DL:  maxDecLevel = val; 
                break;
    case MAX_SOL_DL: maxSolutionLevel = val;
                break;
    case NDECISIONS: nDecisions = val;     
                break;
    default: return false;
  };
  return true;
}

// class destructor
AnalyzerData::~AnalyzerData()
{
        // insert your code here
}


CRunAnalyzer::CRunAnalyzer()
{
        // insert your code here
}





const AnalyzerData &CRunAnalyzer::getData() const
{               
    return theData;             
}
                
void CRunAnalyzer::init(int nVars, int nClauses)
{
    theData.init();
        
        theData.nVars = nVars;
        theData.nOriginalClauses = nClauses;    
        
    first = true;
}
        

void CRunAnalyzer::setValue(DATA_IDX dataIDX, double someData)  
{
   theData.evalData[dataIDX] = someData;
}

void CRunAnalyzer::addValue(ID_DATA dataID, int actDecLevel, double someData)
{
   switch(dataID)
   {
      case CCL_1stUIP:      
         if(someData > theData.evalData[LONGEST_CCL_1stUIP])
                      theData.evalData[LONGEST_CCL_1stUIP] = someData;
         theData.evalData[AVG_CCL_1stUIP] += (double) someData;
         break;
         
      case CCL_lastUIP:      
         if(someData > theData.evalData[LONGEST_CCL_lastUIP])
                      theData.evalData[LONGEST_CCL_lastUIP] = someData;
         theData.evalData[AVG_CCL_lastUIP] += (double) someData;
         break;
         
      case CONFLICT:         
         theData.nConflicts+= (int) someData;
         theData.evalData[AVG_CONFLICT_LEV] += (double) actDecLevel;
         theData.evalData[AVG_DEC_LEV] += (double) actDecLevel;
         break;
         
      case DECISION:
         theData.nDecisions++;
         
         if (actDecLevel > theData.maxDecLevel)
               theData.maxDecLevel = actDecLevel;
         break;  

      case SOLUTION:
         
         theData.evalData[AVG_SOLUTION_LEV] += (double) actDecLevel;
         theData.evalData[AVG_DEC_LEV] += (double) actDecLevel;    
         theData.nReceivedSatAssignments++;  
         break;
         
      case IMPLICATION:
      
         theData.nImplications += (int) someData;
         break;          
      case IBCPIMPL:
         theData.nImplicitImplications += (int) someData;
         break;          
   };
}     

void CRunAnalyzer::addClause()
{
    theData.nAddedClauses++;
}
 

void CRunAnalyzer::setUsedVars(unsigned int nUsedVars)
{
    theData.nUsedVars = nUsedVars;
}

void CRunAnalyzer::setSatCount(const CRealNum &rnCodedSols)
{ 
 to_div_2exp(theData.rnProbOfSat,rnCodedSols,theData.nUsedVars); 
}

/*
bool CRunAnalyzer::includeInPrBackBone(CAssignment &s, double nSols)
{
    //theData.thePrBackBone.include(s,nSols);
        return true;
}
*/

CRunAnalyzer::~CRunAnalyzer()
{
        // insert your code here
}

// No description
void CRunAnalyzer::finishcountSATAnalysis()
{
   theData.finishcountSATAnalysis();
}


void AnalyzerData::finishcountSATAnalysis()
{
   if (nConflicts != 0)
   {
      evalData[AVG_CONFLICT_LEV] /= (double) nConflicts + nImplicitImplications;
      evalData[AVG_CCL_1stUIP] /= (double) nConflicts + nImplicitImplications;
      evalData[AVG_CCL_lastUIP] /= (double)nConflicts + nImplicitImplications; 
   }
   
   if (nReceivedSatAssignments != 0)
   {
      evalData[AVG_SOLUTION_LEV] /= (double) nReceivedSatAssignments;   
   }
   else evalData[AVG_SOLUTION_LEV] = 0.0;
   
   if (nConflicts != 0  || nReceivedSatAssignments != 0)
      evalData[AVG_DEC_LEV] /= (double) nConflicts + nReceivedSatAssignments;    
}