clausedb.cpp

多核环境下运行了可满足性分析的工具软件

/********************************************************************************************
MiraXT -- Copyright (c) 2007, Tobias Schubert, Matthew Lewis, Natalia Kalinnik, Bernd Becker 

Permission is hereby granted, free of charge, to any person obtaining a copy of this 
software and associated documentation files (the "Software"), to deal in the Software 
without restriction, including without limitation the rights to use, copy, modify, merge, 
publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons 
to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING 
BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, 
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
********************************************************************************************/

// Each clause is saved in the following way:
// (clause number, clause length, ID of the thread that generated the clause, x1, ..., xn, 0).

// Definition of the clause database.
class clauseDB
{

private:

  pthread_mutex_t   db_mutex;           
  pthread_mutex_t** db_thread_mutex;
  pthread_mutex_t   db_delete_mutex;           

public:

  vec<int* >       masterBaseClauseVec;       // Original clauses of the benchmark problem to be solved.
  vec<int* >       masterClauseVec;           // Generated conflict clauses only.
  vec< vec<bool> > clauseDeleted;             // Flag to indicate which thread has marked which clause to be deleted.

  int*             cEIThread;                 // "Clauses End Index". One for each thread, marking which clauses have 
                                              // been already processed / integrated by that threat and which clauses 
                                              // are new ones (restricted to conflict clauses only).

  int*             cEIBaseThread;             // Similar to cEIThread, but focussing on original clauses only.
  int              cEIBase;                   // Marks the end of the "normal" clause database, containing only 
                                              // clauses of the given benchmark problem.

  int              numThreads;                // Number of threads.
  int              delMasterClausesShrinkCtr; // Counts the number of removed conflict clauses 
                                              // during "cleanMasterClauseDB".

  // Constructor / Destructor.
  clauseDB(int numThreadsSelected);
  ~clauseDB(void);

  // Size operations.
  void clauseDBGrow(int numClauses);

  // Clause operations.
  int* getNewClause(int threadNum);
  int* getNewClauseInit(int threadNum);
  void addNewClause(int* clause, int clauseLength, int threadNum);
  void addNewClauseInit(int* clause, int clauseLength, int threadNum);  
  void cleanMasterClauseDB();
  void setCEIBase(void) { cEIBase = masterBaseClauseVec.size(); }

  // Lock operations.
  void makeMyLock(int threadNum)
  {
    db_thread_mutex[threadNum] = new pthread_mutex_t; 
    pthread_mutex_init(db_thread_mutex[threadNum], NULL); 
  }
  
  void getAllThreadLocks(void)
  { 
    for (int i=0; i<numThreads; i++) { if (db_thread_mutex[i] != 0) { pthread_mutex_lock(db_thread_mutex[i]); } }
    pthread_mutex_lock(&db_delete_mutex); 
  }
        				      
  void releaseAllThreadLocks(void)
  { 
    pthread_mutex_unlock(&db_delete_mutex); 
    for (int i=numThreads-1; i>=0; i--) { if (db_thread_mutex[i] != 0) { pthread_mutex_unlock(db_thread_mutex[i]); } }
  }
    
  // Mark a clause to be deleted.
  void deleteClause(int* clause, int threadNum) 
  { 
    pthread_mutex_lock(db_thread_mutex[threadNum]); 
    clauseDeleted[threadNum][clause[clauseNumberPos]] = true; 
    pthread_mutex_unlock(db_thread_mutex[threadNum]); 
  }    
};

// Constructor.
clauseDB::clauseDB(int numThreadsSelected)
{
  cEIBase = 0;
  delMasterClausesShrinkCtr = 0;
  numThreads = numThreadsSelected;
  pthread_mutex_init(&db_mutex, NULL);
  db_thread_mutex = new pthread_mutex_t*[numThreads];
  pthread_mutex_init(&db_delete_mutex, NULL);
  cEIThread = new int[numThreads];
  cEIBaseThread = new int[numThreads];
  clauseDeleted.growTo(numThreads);
  for(int i=0; i<numThreads; i++) 
    { cEIThread[i] = 0; cEIBaseThread[i] = 0; db_thread_mutex[i] = 0; }
}

// Destructor
clauseDB::~clauseDB()
{
  // Delete all generated conflict clauses.
  int max = masterClauseVec.size();
  for(int i=0; i<max; i++) { if (masterClauseVec[i] != NULL) { delete [] masterClauseVec[i]; } }

  // Delete all original conflict clauses.
  max = masterBaseClauseVec.size();
  for(int i=0; i<max; i++) { delete [] masterBaseClauseVec[i]; } 

  // Delete all locks.
  for(int i=0; i<numThreads; i++) { delete db_thread_mutex[i]; }

  // Delete all thread markers.
  delete [] db_thread_mutex;
  delete [] cEIThread;
  delete [] cEIBaseThread;
}

// Initialize both the original clause database and the
// conflict clauses database to be able to store "numClauses" clauses.
// Additionally, update also the thread's status registers.
void clauseDB::clauseDBGrow(int numClauses)
{
  pthread_mutex_lock(&db_mutex);
  masterBaseClauseVec.getMem(numClauses+1);
  masterClauseVec.getMem(numClauses+1);
  for (int t=0; t<numThreads; t++) { clauseDeleted[t].getMem(numClauses+1); }
  pthread_mutex_unlock(&db_mutex);
}

// Returns a pointer to a clause, that has not been processed by thread 
// "threadNum" so far (focussing on generated conflict clauses only).
int* clauseDB::getNewClause(int threadNum)
{
  int* returnClause = NULL;
  pthread_mutex_lock(db_thread_mutex[threadNum]);

  // Is the thread's marker really less than the size of the DB? In such 
  // cases there is at least one clause that hasn't been processed by thread "threadNum".
  if (cEIThread[threadNum] < masterClauseVec.size())
    {
      // Get the actual position within the conflict clauses database.
      int pos = cEIThread[threadNum];
      
      // Get the pointer to the first unchecked clause.
      returnClause = masterClauseVec[pos];

      // Move the thread's marker to the next clause.
      cEIThread[threadNum] = pos+1;
    }

  pthread_mutex_unlock(db_thread_mutex[threadNum]);
  return returnClause;
}         

// The same as "getNewClause", but operating on the original clause set of 
// the benchmark to be solved. There is no need for any locks, since the 
// original database is build up before the threads start and is not 
// modified during the search process.
int* clauseDB::getNewClauseInit(int threadNum)
{
  int* returnClause = NULL;
  if (cEIBaseThread[threadNum] < cEIBase)
    {
      int pos = cEIBaseThread[threadNum];
      returnClause = masterBaseClauseVec[pos];
      cEIBaseThread[threadNum] = pos+1;
    }
  return returnClause;
} 

// Adds a new conflict clause to the conflict clause database.
void clauseDB::addNewClause(int* clause, int clauseLength, int threadNum)
{
  // Allocate memory for the new clause. "+clauseStart" to have enough space to store 
  // also the clause number, the length, and the ID of the thread that generated the clause.
  int* tmpClause = new int[clauseLength+clauseStart];

  // Not enough memory?
  if (tmpClause == NULL) 
    { 
      fprintf(stdout,"c Add New Clause: Not enough memory\n");
      fprintf(stdout,"s UNKNOWN\n");

      // Exit code 0: UNKNOWN.
      exit(0);
    }

  // Store all information about the clause in tmpClause.
  tmpClause[clauseLengthPos]   = clauseLength;
  tmpClause[clauseThreadIDPos] = threadNum;
  for(int i=0; i<clauseLength; i++) { tmpClause[i+clauseStart] = clause[i]; }

  pthread_mutex_lock(&db_mutex);
    
  // Clause database almost completely filled?
  if ((masterClauseVec.size() + 10) > masterClauseVec.memAlloc()) 
    {
      getAllThreadLocks();

      // Allocate some more memory.
      masterClauseVec.getMem(masterClauseVec.memAlloc() + 131072);
      for(int i=0; i<numThreads; i++) clauseDeleted[i].getMem(clauseDeleted[i].memAlloc() + 131072);

      releaseAllThreadLocks();
    }

  // Now, integrate the new clause into the exisiting database.
  tmpClause[clauseNumberPos] = masterClauseVec.size();  
  masterClauseVec.push(tmpClause);
  for(int i=0; i<numThreads; i++) { clauseDeleted[i].push(false); } 

  pthread_mutex_unlock(&db_mutex);
}          
         
// Similar to AddNewClause but adding clauses to the original 
// clause set, representing the user specified CNF file.
void clauseDB::addNewClauseInit(int* clause, int clauseLength, int threadNum)
{
  // Allocate memory.
  int* tmpClause = new int[clauseLength+clauseStart];

  // Not enough memory?
  if (tmpClause == NULL) 
    { 
      fprintf(stdout,"c Add New Clause Init: Not enough memory\n");
      fprintf(stdout,"s UNKNOWN\n");

      // Exit code 0: UNKNOWN.
      exit(0);
    }

  // Store all information about the clause in tmpClause.
  tmpClause[clauseNumberPos]   = -1;           // Indicating that it is an original clause 
                                               // (in this case the clause number doesn't matter).
  tmpClause[clauseLengthPos]   = clauseLength; // The clause number.
  tmpClause[clauseThreadIDPos] = -1;           // Indicating that it is an original clause, not 
                                               // generated by any thread (in this case the 
                                               // thread ID doesn't matter).
  for(int i=0; i<clauseLength; i++) { tmpClause[i+clauseStart] = clause[i]; }

  // Now, add the clause to the corresponding database.
  masterBaseClauseVec.push(tmpClause);    
} 

// Physically delete all those conflict clauses that have been marked "to be deleted" by all threads.
void clauseDB::cleanMasterClauseDB()
{
  // Lock database.
  pthread_mutex_lock(&db_delete_mutex);

  // First, check all conflict clauses "clause by clause" and delete them if possible.
  int c = 0; int cEI = masterClauseVec.size(); bool ok2remove; int t;
  while(c < cEI)
    {       
      // Check the current clause.
      if (masterClauseVec[c] != NULL)
        {
	  // Intialization.
	  ok2remove = true;

	  // Clause c marked "to be deleted" by all threads?
	  for (t=0; t<numThreads; t++) { if (clauseDeleted[t][c] == false) { ok2remove = false; break; } }

	  // Is it safe to delete the clause?
	  if (ok2remove)
            {
	      // Delete the clause.
	      delete [] masterClauseVec[c];
	      masterClauseVec[c] = NULL;
	      
	      // Increment the number of deleted clauses so far.
	      delMasterClausesShrinkCtr++;
            }
        }

      // Check the next clause.
      c++;
    }

  // Release the database lock.
  pthread_mutex_unlock(&db_delete_mutex);
  
  // Now, test if we did a lot of clause deletion operations. 
  // Then the database gets compacted to get rid of all "NULL entries" within "masterClauseVec". 
  if (delMasterClausesShrinkCtr > 16384)
    {
      // Lock the database.
      pthread_mutex_lock(&db_mutex);
      getAllThreadLocks();

      // Set the clause deletion counter to 0.
      delMasterClausesShrinkCtr = 0;

      // Variables.
      int c = 0;
      int p = 0;
      int t;
      int Removed = 0;
      cEI = masterClauseVec.size();

      // Again, check all clauses "clause by clause", but now focus on "NULL entries".
      while(c < cEI)
        {
	  if (masterClauseVec[c] == NULL) 
            { Removed++; }
	  else
            { 
	      // Remove "NULL entries" by shifting the real clauses as much as 
	      // possible to the beginning of the clause database.
	      masterClauseVec[p] = masterClauseVec[c];
	      masterClauseVec[p][clauseNumberPos] = p;
	      for (t=0; t<numThreads; t++) { clauseDeleted[t][p] = clauseDeleted[t][c]; }
	      p++;
            }
	  
	  // Check the next clause.
	  c++;
        }

      // Finally, delete all unused clause IDs at the end of the database and 
      // update also the thread's status variables due to this modifications.
      masterClauseVec.popto(p);
      for (t=0; t<numThreads; t++) { clauseDeleted[t].popto(p); cEIThread[t] -= Removed; }

      // Release database locks.
      releaseAllThreadLocks();
      pthread_mutex_unlock(&db_mutex);
    }
}