VIS
Functions | Variables

src/sat/satUtil.c File Reference

#include "satInt.h"
Include dependency graph for satUtil.c:

Go to the source code of this file.

Functions

static int NodeIndexCompare (const void *x, const void *y)
long sat_AddConflictClause (satManager_t *cm, satArray_t *clauseArray, int objectFlag)
long sat_AddConflictClauseNoScoreUpdate (satManager_t *cm, satArray_t *clauseArray, int objectFlag)
long sat_AddUnitConflictClause (satManager_t *cm, satArray_t *clauseArray, int objectFlag)
long sat_AddUnitBlockingClause (satManager_t *cm, satArray_t *clauseArray)
long sat_AddUnitClause (satManager_t *cm, satArray_t *clauseArray)
long sat_AddClauseIncremental (satManager_t *cm, satArray_t *clauseArray, int objectFlag, int fromDistill)
long sat_AddClause (satManager_t *cm, satArray_t *clauseArray)
long sat_AddBlockingClause (satManager_t *cm, satArray_t *clauseArray)
void sat_AddWL (satManager_t *cm, long c, int index, int dir)
satArray_t * sat_ArrayAlloc (long number)
satArray_t * sat_ArrayDuplicate (satArray_t *old)
void sat_ArrayInsert (satArray_t *array, long datum)
void sat_ArrayFree (satArray_t *array)
satQueue_t * sat_CreateQueue (long MaxElements)
void sat_FreeQueue (satQueue_t *Q)
void sat_Enqueue (satQueue_t *Q, long v)
long sat_Dequeue (satQueue_t *Q)
satLevel_t * sat_AllocLevel (satManager_t *cm)
void sat_CleanLevel (satLevel_t *d)
void sat_ClauseDeletion (satManager_t *cm)
void sat_DeleteClause (satManager_t *cm, long v)
void sat_CompactClauses (satManager_t *cm)
int sat_EnlargeLiteralDB (satManager_t *cm)
void sat_AllocLiteralsDB (satManager_t *cm)
void sat_FreeLiteralsDB (satLiteralDB_t *literals)
void sat_CleanDatabase (satManager_t *cm)
void sat_CompactFanout (satManager_t *cm)
void sat_RestoreFanout (satManager_t *cm)
int sat_GetFanoutSize (satManager_t *cm, long v)
void sat_MarkTransitiveFaninForArray (satManager_t *cm, satArray_t *arr, unsigned int mask)
void sat_MarkTransitiveFaninForNode (satManager_t *cm, long v, unsigned int mask)
void sat_UnmarkTransitiveFaninForArray (satManager_t *cm, satArray_t *arr, unsigned int mask, unsigned int resetMask)
void sat_UnmarkTransitiveFaninForNode (satManager_t *cm, long v, unsigned int mask, unsigned int resetMask)
void sat_SetConeOfInfluence (satManager_t *cm)
satManager_t * sat_InitManager (satInterface_t *interface)
void sat_FreeManager (satManager_t *cm)
void sat_FreeOption (satOption_t *option)
void sat_FreeStatistics (satStatistics_t *stats)
satOption_t * sat_InitOption ()
void sat_ReportStatistics (satManager_t *cm, satStatistics_t *stats)
satStatistics_t * sat_InitStatistics (void)
void sat_SetIncrementalOption (satOption_t *option, int incFlag)
void sat_RestoreBlockingClauses (satManager_t *cm)
void sat_RestoreFrontierClauses (satManager_t *cm)
void sat_RestoreClauses (satManager_t *cm, satArray_t *cnfArray)
void sat_CollectBlockingClause (satManager_t *cm)
void sat_FreeInterface (satInterface_t *interface)
long sat_CreateNode (satManager_t *cm, long left, long right)
int sat_MemUsage (satManager_t *cm)
long sat_GetCanonical (satManager_t *cm, long v)
void sat_CombineStatistics (satManager_t *cm)
int sat_GetNumberOfInitialClauses (satManager_t *cm)
int sat_GetNumberOfInitialVariables (satManager_t *cm)
satArray_t * sat_ReadForcedAssignment (char *filename)
int sat_ApplyForcedAssigment (satManager_t *cm, satArray_t *arr, satLevel_t *d)
void sat_ApplyForcedAssignmentMain (satManager_t *cm, satLevel_t *d)
void sat_PutAssignmentValueMain (satManager_t *cm, satLevel_t *d, satArray_t *arr)
void sat_ClauseDeletionLatestActivity (satManager_t *cm)
long sat_GetClauseFromLit (satManager_t *cm, long *lit)

Variables

static char rcsid[] UNUSED = "$Id: satUtil.c,v 1.37 2009/04/11 18:26:37 fabio Exp $"

Function Documentation

static int NodeIndexCompare ( const void *  x,
const void *  y 
) [static]

AutomaticStart

Function********************************************************************

Synopsis [ Compare node index to sort ]

Description [ Compare node index to sort ]

SideEffects []

SeeAlso []

Definition at line 3197 of file satUtil.c.

{
long n1, n2;

  n1 = *(long *)x;
  n2 = *(long *)y;
  return(n1 > n2);
}

Here is the caller graph for this function:

long sat_AddBlockingClause ( satManager_t *  cm,
satArray_t *  clauseArray 
)

Function********************************************************************

Synopsis [ Add clause into clause database]

Description [ Add clause into clause database]

SideEffects []

SeeAlso []

SATfirstLit(c) = (int)last;

Definition at line 897 of file satUtil.c.

{
satLiteralDB_t *literals;
satStatistics_t *stats;
long c, v;
int inverted;
long *last, *space;
int i, size;
int maxLevel, maxIndex;
int value, level;
int otherWLIndex;

  literals = cm->literals;
  stats = cm->each;

  while(literals->last + clauseArray->num + 2 >= literals->end) {
    if(!sat_EnlargeLiteralDB(cm)) {
      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
              cm->comment);
      exit(0);
    }
  }

  if(clauseArray->num == 1)
    return(sat_AddUnitBlockingClause(cm, clauseArray));

  c = 0;
  if(cm->unusedAigQueue)
    c = sat_Dequeue(cm->unusedAigQueue);
  if(c == 0)
    c = sat_CreateNode(cm, 2, 2);

  last = literals->last;
  *(last) = (-c);
  last++;

  (cm->nodesArray[c+satFirstLit]) = (long)last;
  SATnumLits(c) = clauseArray->num;
  SATflags(c) |= IsCNFMask;
  SATsetInUse(c);
  SATnumConflict(c) = 0;

  size = clauseArray->num;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = !SATisInverted(v);
    v = SATnormalNode(v);

    *(last) = ((v^inverted) << 2);
    last++;
  }
  *(last) = (-c);
  last++;

  literals->last = last;

  maxLevel = -1;
  maxIndex = -1;
  otherWLIndex = -1;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(value == 2) {
      sat_AddWL(cm, c, i, 1);
      otherWLIndex = i;
      break;
    }
    else {
      level = SATlevel(v);
      if(level > maxLevel) {
        maxLevel = level;
        maxIndex = i;
      }
    }
  }
  if(i >= size) {
    sat_AddWL(cm, c, maxIndex, 1);
    otherWLIndex = maxIndex;
  }

  maxLevel = -1;
  maxIndex = -1;
  space = clauseArray->space+size-1;
  for(i=size-1; i>=0; i--, space--) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(i != otherWLIndex) {
      if(value == 2) {
        sat_AddWL(cm, c, i, -1);
        break;
      }
      else {
        level = SATlevel(v);
        if(level > maxLevel) {
          maxLevel = level;
          maxIndex = i;
        }
      }
    }
  }
  if(i < 0)
    sat_AddWL(cm, c, maxIndex, -1);

  SATflags(c) |= IsBlockingMask;

  stats = cm->each;
  stats->nBlockingCl++;
  stats->nBlockingLit += clauseArray->num;

  return(c);
}

Here is the call graph for this function:

Here is the caller graph for this function:

long sat_AddClause ( satManager_t *  cm,
satArray_t *  clauseArray 
)

Function********************************************************************

Synopsis [ Add clause into clause database]

Description [ Add clause into clause database]

SideEffects []

SeeAlso []

SATfirstLit(c) = (int)last;

Definition at line 773 of file satUtil.c.

{
satLiteralDB_t *literals;
long c, v;
int inverted;
long *last, *space;
int i, size;
int maxLevel, maxIndex;
int value, level;
int otherWLIndex;

  literals = cm->literals;

  while(literals->last + clauseArray->num + 2 >= literals->end) {
    if(!sat_EnlargeLiteralDB(cm)) {
      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
              cm->comment);
      exit(0);
    }
  }
  c = 0;
  if(cm->unusedAigQueue)
    c = sat_Dequeue(cm->unusedAigQueue);
  if(c == 0)
    c = sat_CreateNode(cm, 2, 2);

  last = literals->last;
  *(last) = (-c);
  last++;

  (cm->nodesArray[c+satFirstLit]) = (long)last;
  SATnumLits(c) = clauseArray->num;
  SATflags(c) |= IsCNFMask;
  SATsetInUse(c);
  SATnumConflict(c) = 0;

  size = clauseArray->num;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = !SATisInverted(v);
    v = SATnormalNode(v);

    *(last) = ((v^inverted) << 2);
    last++;
  }
  *(last) = (-c);
  last++;

  literals->last = last;

  maxLevel = -1;
  maxIndex = -1;
  otherWLIndex = -1;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(value == 2) {
      sat_AddWL(cm, c, i, 1);
      otherWLIndex = i;
      break;
    }
    else {
      level = SATlevel(v);
      if(level > maxLevel) {
        maxLevel = level;
        maxIndex = i;
      }
    }
  }
  if(i >= size) {
    sat_AddWL(cm, c, maxIndex, 1);
    otherWLIndex = maxIndex;
  }

  maxLevel = -1;
  maxIndex = -1;
  space = clauseArray->space+size-1;
  for(i=size-1; i>=0; i--, space--) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(i != otherWLIndex) {
      if(value == 2) {
        sat_AddWL(cm, c, i, -1);
        break;
      }
      else {
        level = SATlevel(v);
        if(level > maxLevel) {
          maxLevel = level;
          maxIndex = i;
        }
      }
    }
  }
  if(i < 0)
    sat_AddWL(cm, c, maxIndex, -1);


  return(c);
}

Here is the call graph for this function:

Here is the caller graph for this function:

long sat_AddClauseIncremental ( satManager_t *  cm,
satArray_t *  clauseArray,
int  objectFlag,
int  fromDistill 
)

Function********************************************************************

Synopsis [ Add conflict clause into clause database]

Description [ Add conflict clause into clause database]

SideEffects []

SeeAlso []

SATfirstLit(c) = (int)last;

Definition at line 605 of file satUtil.c.

{
satLiteralDB_t *literals;
satStatistics_t *stats;
satVariable_t *var;
long c, v;
int inverted;
long *last, *space;
int i, size;
int maxLevel, maxIndex;
int value, level;
int otherWLIndex;

  literals = cm->literals;
  stats = cm->each;

  while(literals->last + clauseArray->num + 2 >= literals->end) {
    if(!sat_EnlargeLiteralDB(cm)) {
      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
              cm->comment);
      exit(0);
    }
  }

  c = 0;
  if(cm->unusedAigQueue)
    c = sat_Dequeue(cm->unusedAigQueue);
  if(c == 0)
    c = sat_CreateNode(cm, 2, 2);

  last = literals->last;
  *(last) = (-c);
  last++;


  (cm->nodesArray[c+satFirstLit]) = (long)last;
  SATnumLits(c) = clauseArray->num;
  SATflags(c) |= IsCNFMask;
  SATsetInUse(c);
  SATnumConflict(c) = 0;

  size = clauseArray->num;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = !SATisInverted(v);
    v = SATnormalNode(v);

    *(last) = ((v^inverted) << 2);
    last++;

    var = SATgetVariable(v);
    if(inverted){
      if(fromDistill)
        (var->litsCount[0])++;
      (var->conflictLits[0])++;
    }
    else        {
      if(fromDistill)
        (var->litsCount[1])++;
      (var->conflictLits[1])++;
    }
  }
  *(last) = (-c);
  last++;

  literals->last = last;


  /* Bing: UNSAT core generation */
 if(clauseArray->num>1){
  maxLevel = -1;
  maxIndex = -1;
  otherWLIndex = -1;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(value == 2) {
      sat_AddWL(cm, c, i, 1);
      otherWLIndex = i;
      break;
    }
    else {
      level = SATlevel(v);
      if(level > maxLevel) {
        maxLevel = level;
        maxIndex = i;
      }
    }
  }
  if(i >= size) {
    sat_AddWL(cm, c, maxIndex, 1);
    otherWLIndex = maxIndex;
  }

  maxLevel = -1;
  maxIndex = -1;
  space = clauseArray->space+size-1;
  for(i=size-1; i>=0; i--, space--) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(i != otherWLIndex) {
      if(value == 2) {
        sat_AddWL(cm, c, i, -1);
        break;
      }
      else {
        level = SATlevel(v);
        if(level > maxLevel) {
          maxLevel = level;
          maxIndex = i;
        }
      }
    }
  }
  if(i < 0)
    sat_AddWL(cm, c, maxIndex, -1);
 }

  if(objectFlag)SATflags(c) |= ObjMask;
  else          SATflags(c) |= NonobjMask;
  /*SATflags(c) |= IsConflictMask;*/
  //Bing:change??
  if(!cm->option->coreGeneration)
    SATflags(c) |= IsConflictMask;

  if(objectFlag) {
    stats->nInitObjConflictCl++;
    stats->nInitObjConflictLit += clauseArray->num;
    stats->nObjConflictCl++;
    stats->nObjConflictLit += clauseArray->num;
  }
  else {
    stats->nInitNonobjConflictCl++;
    stats->nInitNonobjConflictLit += clauseArray->num;
    stats->nObjConflictCl++;
    stats->nObjConflictLit += clauseArray->num;
  }
  stats->nConflictCl++;
  stats->nConflictLit += clauseArray->num;

  return(c);
}

Here is the call graph for this function:

Here is the caller graph for this function:

long sat_AddConflictClause ( satManager_t *  cm,
satArray_t *  clauseArray,
int  objectFlag 
)

AutomaticEnd Function********************************************************************

Synopsis [ Add conflict clause into clause database]

Description [ Add conflict clause into clause database]

SideEffects []

SeeAlso []

SATfirstLit(c) = (int)last;

Definition at line 55 of file satUtil.c.

{
satStatistics_t *stats;
satLiteralDB_t *literals;
satVariable_t *var;
long v, c;
int inverted;
long *last;
long *space;
int i, size;
int maxLevel, maxIndex;
int value, level;
int otherWLIndex;

  literals = cm->literals;

  while(literals->last + clauseArray->num + 2 >= literals->end) {
    if(!sat_EnlargeLiteralDB(cm)) {
      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
              cm->comment);
      exit(0);
    }
  }

  c = 0;
  if(cm->unusedAigQueue)
    c = sat_Dequeue(cm->unusedAigQueue);
  if(c == 0)
    c = sat_CreateNode(cm, 2, 2);


  last = literals->last;
  *(last) = (-c);
  last++;

  (cm->nodesArray[c+satFirstLit]) = (long)last;
  SATnumLits(c) = clauseArray->num;
  SATflags(c) |= IsCNFMask;
  SATsetInUse(c);
  SATnumConflict(c) = 0;

  size = clauseArray->num;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = !SATisInverted(v);
    v = SATnormalNode(v);

    *(last) = ((v^inverted) << 2);
    last++;

    var = SATgetVariable(v);

    if(inverted){
      (var->litsCount[0])++;
      (var->conflictLits[0])++;
    }
    else        {
      (var->litsCount[1])++;
      (var->conflictLits[1])++;
    }
  }
  *(last) = (-c);
  last++;

  literals->last = last;

  maxLevel = -1;
  maxIndex = -1;
  otherWLIndex = -1;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(value == 2) {
      sat_AddWL(cm, c, i, 1);
      otherWLIndex = i;
      break;
    }
    else {
      level = SATlevel(v);
      if(level > maxLevel) {
        maxLevel = level;
        maxIndex = i;
      }
    }
  }
  if(i >= size) {
    sat_AddWL(cm, c, maxIndex, 1);
    otherWLIndex = maxIndex;
  }

  maxLevel = -1;
  maxIndex = -1;
  space = clauseArray->space+size-1;
  for(i=size-1; i>=0; i--, space--) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(i != otherWLIndex) {
      if(value == 2) {
        sat_AddWL(cm, c, i, -1);
        break;
      }
      else {
        level = SATlevel(v);
        if(level > maxLevel) {
          maxLevel = level;
          maxIndex = i;
        }
      }
    }
  }
  if(i < 0)
    sat_AddWL(cm, c, maxIndex, -1);


  SATflags(c) |= IsConflictMask;

  stats = cm->each;
  stats->nConflictCl++;
  stats->nConflictLit += clauseArray->num;
  if(objectFlag) {
    stats->nObjConflictCl++;
    stats->nObjConflictLit += clauseArray->num;
    SATflags(c) |= ObjMask;
  }
  else {
    stats->nNonobjConflictCl++;
    stats->nNonobjConflictLit += clauseArray->num;
    SATflags(c) |= NonobjMask;
  }


  return(c);
}

Here is the call graph for this function:

Here is the caller graph for this function:

long sat_AddConflictClauseNoScoreUpdate ( satManager_t *  cm,
satArray_t *  clauseArray,
int  objectFlag 
)

Function********************************************************************

Synopsis [ Add conflict clause into clause database without updating score]

Description [ Add conflict clause into clause database without updating score]

SideEffects []

SeeAlso []

SATfirstLit(c) = (int)last;

Definition at line 213 of file satUtil.c.

{
satStatistics_t *stats;
satLiteralDB_t *literals;
satVariable_t *var;
long v, c;
int inverted;
long *last;
long *space;
int i, size;
int maxLevel, maxIndex;
int value, level;
int otherWLIndex;

  literals = cm->literals;

  while(literals->last + clauseArray->num + 2 >= literals->end) {
    if(!sat_EnlargeLiteralDB(cm)) {
      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
              cm->comment);
      exit(0);
    }
  }

  c = 0;
  if(cm->unusedAigQueue)
    c = sat_Dequeue(cm->unusedAigQueue);
  if(c == 0)
    c = sat_CreateNode(cm, 2, 2);


  last = literals->last;
  *(last) = (-c);
  last++;

  (cm->nodesArray[c+satFirstLit]) = (long)last;
  SATnumLits(c) = clauseArray->num;
  SATflags(c) |= IsCNFMask;
  SATsetInUse(c);
  SATnumConflict(c) = 0;

  size = clauseArray->num;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = !SATisInverted(v);
    v = SATnormalNode(v);

    *(last) = ((v^inverted) << 2);
    last++;

    var = SATgetVariable(v);

    if(inverted){
      (var->litsCount[0])++;
      (var->conflictLits[0])++;
    }
    else        {
      (var->litsCount[1])++;
      (var->conflictLits[1])++;
    }
  }
  *(last) = (-c);
  last++;

  literals->last = last;

  maxLevel = -1;
  maxIndex = -1;
  otherWLIndex = -1;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(value == 2) {
      sat_AddWL(cm, c, i, 1);
      otherWLIndex = i;
      break;
    }
    else {
      level = SATlevel(v);
      if(level > maxLevel) {
        maxLevel = level;
        maxIndex = i;
      }
    }
  }
  if(i >= size) {
    sat_AddWL(cm, c, maxIndex, 1);
    otherWLIndex = maxIndex;
  }

  maxLevel = -1;
  maxIndex = -1;
  space = clauseArray->space+size-1;
  for(i=size-1; i>=0; i--, space--) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(i != otherWLIndex) {
      if(value == 2) {
        sat_AddWL(cm, c, i, -1);
        break;
      }
      else {
        level = SATlevel(v);
        if(level > maxLevel) {
          maxLevel = level;
          maxIndex = i;
        }
      }
    }
  }
  if(i < 0)
    sat_AddWL(cm, c, maxIndex, -1);


  SATflags(c) |= IsConflictMask;

  stats = cm->each;
  stats->nConflictCl++;
  stats->nConflictLit += clauseArray->num;
  if(objectFlag) {
    stats->nObjConflictCl++;
    stats->nObjConflictLit += clauseArray->num;
    SATflags(c) |= ObjMask;
  }
  else {
    stats->nNonobjConflictCl++;
    stats->nNonobjConflictLit += clauseArray->num;
    SATflags(c) |= NonobjMask;
  }


  return(c);
}

Here is the call graph for this function:

Here is the caller graph for this function:

long sat_AddUnitBlockingClause ( satManager_t *  cm,
satArray_t *  clauseArray 
)

Function********************************************************************

Synopsis [ Add unit blocking clause into clause database]

Description [ Add unit blocking clause into clause database]

SideEffects []

SeeAlso []

SATfirstLit(c) = (int)last;

Definition at line 456 of file satUtil.c.

{
satLiteralDB_t *literals;
satStatistics_t *stats;
long c, v;
int inverted;
long *last, *space;
int i, size;

  literals = cm->literals;
  stats = cm->each;

  while(literals->last + clauseArray->num + 2 >= literals->end) {
    if(!sat_EnlargeLiteralDB(cm)) {
      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
              cm->comment);
      exit(0);
    }
  }

  c = 0;
  if(cm->unusedAigQueue)
    c = sat_Dequeue(cm->unusedAigQueue);
  if(c == 0)
    c = sat_CreateNode(cm, 2, 2);


  last = literals->last;
  *(last) = (-c);
  last++;

  (cm->nodesArray[c+satFirstLit]) = (long)last;
  SATnumLits(c) = clauseArray->num;
  SATflags(c) |= IsCNFMask;
  SATsetInUse(c);
  SATnumConflict(c) = 0;

  size = clauseArray->num;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = !SATisInverted(v);
    v = SATnormalNode(v);

    *(last) = ((v^inverted) << 2);
    last++;
  }
  *(last) = (-c);
  last++;

  literals->last = last;

  SATflags(c) |= IsBlockingMask;

  stats = cm->each;
  stats->nBlockingCl++;
  stats->nBlockingLit += clauseArray->num;
  return(c);
}

Here is the call graph for this function:

Here is the caller graph for this function:

long sat_AddUnitClause ( satManager_t *  cm,
satArray_t *  clauseArray 
)

Function********************************************************************

Synopsis [ Add unit conflict clause into clause database]

Description [ Add unit conflict clause into clause database]

SideEffects [ UNSAT Core generation]

SeeAlso []

SATfirstLit(c) = (int)last;

Definition at line 534 of file satUtil.c.

{
satLiteralDB_t *literals;
long c = 0, v;
int inverted;
long *last, *space;
int i, size;

  literals = cm->literals;

  while(literals->last + clauseArray->num + 2 >= literals->end) {
    if(!sat_EnlargeLiteralDB(cm)) {
      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
              cm->comment);
      exit(0);
    }
  }


  c = 0;
  if(cm->unusedAigQueue)
    c = sat_Dequeue(cm->unusedAigQueue);
  if(c == 0)
    c = sat_CreateNode(cm, 2, 2);


  last = literals->last;
  *(last) = (-c);
  last++;

  (cm->nodesArray[c+satFirstLit]) = (long)last;
  SATnumLits(c) = clauseArray->num;
  SATflags(c) |= IsCNFMask;
  SATsetInUse(c);
  SATnumConflict(c) = 0;

  size = clauseArray->num;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = !SATisInverted(v);
    v = SATnormalNode(v);

    *(last) = ((v^inverted) << 2);
    last++;
  }
  *(last) = (-c);
  last++;

  literals->last = last;

  return(c);
}

Here is the call graph for this function:

Here is the caller graph for this function:

long sat_AddUnitConflictClause ( satManager_t *  cm,
satArray_t *  clauseArray,
int  objectFlag 
)

Function********************************************************************

Synopsis [ Add unit conflict clause into clause database]

Description [ Add unit conflict clause into clause database]

SideEffects []

SeeAlso []

SATfirstLit(c) = (int)last;

Definition at line 370 of file satUtil.c.

{
satLiteralDB_t *literals;
satStatistics_t *stats;
long c, v;
int inverted;
long *last, *space;
int i, size;

  literals = cm->literals;

  while(literals->last + clauseArray->num + 2 >= literals->end) {
    if(!sat_EnlargeLiteralDB(cm)) {
      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
              cm->comment);
      exit(0);
    }
  }

  c = 0;
  if(cm->unusedAigQueue)
    c = sat_Dequeue(cm->unusedAigQueue);
  if(c == 0)
    c = sat_CreateNode(cm, 2, 2);


  last = literals->last;
  *(last) = (-c);
  last++;

  (cm->nodesArray[c+satFirstLit]) = (long)last;
  SATnumLits(c) = clauseArray->num;
  SATflags(c) |= IsCNFMask;
  SATsetInUse(c);
  SATnumConflict(c) = 0;

  size = clauseArray->num;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = !SATisInverted(v);
    v = SATnormalNode(v);

    *(last) = ((v^inverted) << 2);
    last++;
  }
  *(last) = (-c);
  last++;

  literals->last = last;

  SATflags(c) |= IsConflictMask;
  stats = cm->each;
  stats->nConflictCl++;
  stats->nConflictLit += clauseArray->num;
  if(objectFlag) {
    stats->nObjConflictCl++;
    stats->nObjConflictLit += clauseArray->num;
    SATflags(c) |= ObjMask;
  }
  else {
    stats->nNonobjConflictCl++;
    stats->nNonobjConflictLit += clauseArray->num;
    SATflags(c) |= NonobjMask;
  }

  return(c);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_AddWL ( satManager_t *  cm,
long  c,
int  index,
int  dir 
)

Function********************************************************************

Synopsis [ Make literal watched ]

Description [ Make literal watched ]

SideEffects []

SeeAlso []

Definition at line 1033 of file satUtil.c.

{
long *plit, v;
int inverted;
satVariable_t *var;

  plit = (long*)SATfirstLit(c) + index;
  v = SATgetNode(*plit);
  inverted = !SATisInverted(v);
  v = SATnormalNode(v);
  var = SATgetVariable(v);

  if(var->wl[inverted] == 0)
    var->wl[inverted] = sat_ArrayAlloc(4);
  sat_ArrayInsert(var->wl[inverted], (long)plit);
  SATsetWL(plit, dir);
}

Here is the call graph for this function:

Here is the caller graph for this function:

satLevel_t* sat_AllocLevel ( satManager_t *  cm)

Function********************************************************************

Synopsis [ Allocate decision level ]

Description [ Allocate decision level ]

SideEffects []

SeeAlso []

Definition at line 1310 of file satUtil.c.

{
satStatistics_t *stats;
satLevel_t *d;
satArray_t *implied;
int size;

  if(cm->decisionHeadSize == 0) {
    size = cm->currentDecision+2;
    cm->decisionHeadSize = size;
    cm->decisionHead = REALLOC(satLevel_t, cm->decisionHead, size);
    memset(cm->decisionHead, 0, sizeof(satLevel_t) * size);
  }

  if(cm->currentDecision+1 >= cm->decisionHeadSize) {
    size = cm->decisionHeadSize;
    cm->decisionHeadSize <<=1;
    cm->decisionHead = REALLOC(satLevel_t, cm->decisionHead,
                               cm->decisionHeadSize);
    memset(cm->decisionHead+size, 0, sizeof(satLevel_t) * size);
  }

  cm->currentDecision++;
  d = &(cm->decisionHead[cm->currentDecision]);
  implied = d->implied;
  memset(d, 0, sizeof(satLevel_t));
  d->implied = implied;
  if(d->implied == 0){
    d->implied = sat_ArrayAlloc(64);
    //Bing: avoid seg fault
    if(d->implied == 0){
      printf("out of mem, exit\n");
      exit(0);
    }
  }

  d->level = cm->currentDecision;
  d->conflict = 0;

  stats = cm->each;
  if(stats->maxDecisionLevel < d->level)
    stats->maxDecisionLevel = d->level;

  return(d);

}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_AllocLiteralsDB ( satManager_t *  cm)

Function********************************************************************

Synopsis [ Allocate clause database ]

Description [ Allocate clause database ]

SideEffects []

SeeAlso []

CONSIDER...

Definition at line 1709 of file satUtil.c.

{
satLiteralDB_t *literals;
int size;

  literals = cm->literals;
  if(literals)  return;

  literals = ALLOC(satLiteralDB_t, 1);
  cm->literals = literals;

  size = 1024 * 1024;
  literals->begin = ALLOC(long, size);
  *(literals->begin) = 0;
  literals->last = literals->begin + 1;
  literals->end = literals->begin + size;
  literals->initialSize = literals->last;

}

Here is the caller graph for this function:

int sat_ApplyForcedAssigment ( satManager_t *  cm,
satArray_t *  arr,
satLevel_t *  d 
)

Function********************************************************************

Synopsis [ Apply forced assignments.]

Description [ Apply forced assignments.]

SideEffects []

SeeAlso []

Definition at line 2935 of file satUtil.c.

{
long v;
int i, inverted, errorFlag;

  errorFlag = 0;
  for(i=0; i<arr->num; i++) {
    v = arr->space[i];
    inverted = SATisInverted(v);
    v = SATnormalNode(v);

    SATvalue(v) = !inverted;
    SATmakeImplied(v, d);
    sat_Enqueue(cm->queue, v);
    SATflags(v) |= InQueueMask;
    sat_ImplicationMain(cm, d);
    if(d->conflict) {
      fprintf(cm->stdOut,
              "%s WARNING : conflict happens at level %d while applying forced assignments\n", cm->comment, d->level);
      errorFlag = 1;
      break;
    }
  }
  if(errorFlag)
    return(SAT_UNSAT);
  else
    return(0);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_ApplyForcedAssignmentMain ( satManager_t *  cm,
satLevel_t *  d 
)

Function********************************************************************

Synopsis [ Apply forced assignments.]

Description [ Apply forced assignments.]

SideEffects []

SeeAlso []

Definition at line 2979 of file satUtil.c.

{
satArray_t *forcedArr;
int flag;

  forcedArr = cm->option->forcedAssignArr;
  flag = 0;
  if(forcedArr) {
    flag = sat_ApplyForcedAssigment(cm, forcedArr, d);
  }

  if(flag == SAT_UNSAT) {
    cm->status = SAT_UNSAT;
    return;
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

satArray_t* sat_ArrayAlloc ( long  number)

Function********************************************************************

Synopsis [ Allocate array ]

Description [ Allocate array ]

SideEffects []

SeeAlso []

Definition at line 1068 of file satUtil.c.

{
satArray_t *array;

  array = ALLOC(satArray_t, 1);
  if (array) {
    array->num = 0;
    array->size = number;
    array->space = ALLOC(long, number);
    if (array->space) {
      return array;
    }
  }
  //Bing: To avoid segmentation fault
  if(array==0 || (number>0&&array->space==0)){
    printf("can't alloc mem, exit\n");
    exit(0);
  }
  return 0;
}
satArray_t* sat_ArrayDuplicate ( satArray_t *  old)

Function********************************************************************

Synopsis [ Duplicate array ]

Description [ Duplicate array ]

SideEffects []

SeeAlso []

Definition at line 1101 of file satUtil.c.

{
satArray_t *array;

  array = (satArray_t *)malloc(sizeof(satArray_t));
  if (array) {
    array->num = old->num;
    array->size = old->num;
    array->space = (long *)malloc(sizeof(long) * old->num);
    memcpy(array->space, old->space, sizeof(long)*old->num);
    if (array->space) {
      return array;
    }
  }
  return 0;
}

Here is the caller graph for this function:

void sat_ArrayFree ( satArray_t *  array)

Function********************************************************************

Synopsis [ Free array ]

Description [ Free array ]

SideEffects []

SeeAlso []

Definition at line 1158 of file satUtil.c.

{
  free(array->space);
  free(array);
}
void sat_ArrayInsert ( satArray_t *  array,
long  datum 
)

Function********************************************************************

Synopsis [ Insert entries to array ]

Description [ Insert entries to array ]

SideEffects []

SeeAlso []

Definition at line 1130 of file satUtil.c.

{
  if(array->num < array->size) {
    array->space[array->num++] = datum;
  }
  else {
    array->size <<= 1;
    array->space = REALLOC(long, array->space, array->size);
    if(array->space == 0) {
      fprintf(stdout, "ERROR : Can't allocate memory in sat_ArrayInsert\n");
      exit(0);
    }
    array->space[array->num++] = datum;
  }
}
void sat_ClauseDeletion ( satManager_t *  cm)

Function********************************************************************

Synopsis [ Delete conflict clauses ]

Description [ Delete conflict clauses ]

SideEffects []

SeeAlso []

LATEST_ACTIVITY_DELETION MAX_UNRELEVANCE_DELETION SIMPLE_LATEST_DELETION

Definition at line 1392 of file satUtil.c.

{
satLiteralDB_t *literals;
satOption_t *option;
long v, *plit, nv, lit;
int size, n0, n1x, deleteFlag;
int unrelevance;
int inverted, i;
int value;
double ratio;

  option = cm->option;
  if(option->clauseDeletionHeuristic == 0)      return;

  literals = cm->literals;
  for(v=cm->beginConflict; v<cm->nodesArraySize; v+=satNodeSize) {
    if(!(SATflags(v) & IsCNFMask))      continue;
    if(SATreadInUse(v) == 0)            continue;

    if(option->incPreserveNonobjective && (SATflags(v) & NonobjMask))
      continue;

    size = SATnumLits(v);
    if(size < option->minLitsLimit)     continue;

    plit = (long*)SATfirstLit(v);

    unrelevance = option->unrelevance;
    if(option->clauseDeletionHeuristic & SIMPLE_LATEST_DELETION) {
      ratio = (double)(plit-literals->initialSize)/
          (double)(literals->last-literals->initialSize);
      if(ratio > 0.8)   unrelevance <<= 3;
    }
    if(!(option->clauseDeletionHeuristic & MAX_UNRELEVANCE_DELETION)) {
      unrelevance = MAXINT;
    }

    n0 = n1x = 0;
    deleteFlag = 0;
    for(i=0; i<size; i++, plit++) {
      lit = *plit;
      nv = SATgetNode(lit);
      inverted = SATisInverted(nv);
      nv = SATnormalNode(nv);
      value = SATvalue(nv) ^ inverted;

      if(value == 0)    n0++;
      else if(value == 1) {
        n1x++;
        if(SATlevel(nv) == 0 && cm->option->coreGeneration == 0)
          deleteFlag = 1;
      }
      else      n1x++;

      if(deleteFlag) {
        sat_DeleteClause(cm, v);
        sat_Enqueue(cm->unusedAigQueue, v);
        break;
      }
      if((size > option->maxLitsLimit) && (n1x > 1)) {
        sat_DeleteClause(cm, v);
        sat_Enqueue(cm->unusedAigQueue, v);
        break;
      }
      if(n1x > unrelevance) {
        sat_DeleteClause(cm, v);
        sat_Enqueue(cm->unusedAigQueue, v);
        break;
      }
    }

  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_ClauseDeletionLatestActivity ( satManager_t *  cm)

Function********************************************************************

Synopsis [ Clause deletion heuristic based on usage of conflict clause ]

Description [ Clause deletion heuristic based on usage of conflict clause ]

SideEffects []

SeeAlso []

LATEST_ACTIVITY_DELETION MAX_UNRELEVANCE_DELETION SIMPLE_LATEST_DELETION

Definition at line 3048 of file satUtil.c.

{
satLiteralDB_t *literals;
satOption_t *option;
long nv, v, *plit, *clit;
long usage, totalConflictCl;
long index, lit;

int size, n0, n1x, deleteFlag;
int unrelevance;
int usedLimit;
int inverted, i;
int value;
int nLatestCl;
int nDeletedCl;
double ratio;

  option = cm->option;
  if(option->clauseDeletionHeuristic == 0)      return;

  totalConflictCl = (cm->nodesArraySize - cm->beginConflict)/satNodeSize;
  nDeletedCl = cm->each->nDeletedCl;
  nLatestCl = totalConflictCl/option->latestRate;
  literals = cm->literals;
  index = 0;
  for(clit = literals->last-1; clit > literals->begin; clit--){
    if(*clit == 0)
      continue;
    if(index >= totalConflictCl)
      break;
    v = -(*clit);

    plit = (long*)SATfirstLit(v);
    clit = plit - 1;
    index++;

    if(nLatestCl > 0) {
      nLatestCl--;
      unrelevance = option->latestUnrelevance;
    }
    else {
      unrelevance = option->obsoleteUnrelevance;
    }

    if(!(SATflags(v) & IsConflictMask)) continue;
    if((SATflags(v) & IsFrontierMask))  continue;

    if(option->incPreserveNonobjective && (SATflags(v) & NonobjMask))
      continue;

    usage = SATconflictUsage(v);
    SATconflictUsage(v) = usage/2;
    size = SATnumLits(v);
//    if(size < option->minLitsLimit)   continue;
    if(size < unrelevance)
      continue;

    usedLimit = option->obsoleteUsage +
        (option->latestUsage-option->obsoleteUsage)*index/totalConflictCl;
    if(usage > usedLimit)
      continue;


    n0 = n1x = 0;
    deleteFlag = 0;
    for(i=0; i<size; i++, plit++) {
      lit = *plit;
      nv = SATgetNode(lit);
      inverted = SATisInverted(nv);
      nv = SATnormalNode(nv);
      value = SATvalue(nv) ^ inverted;

      if(value == 0)    n0++;
      else if(value == 1) {
        n1x++;
        if(SATlevel(nv) == 0)   deleteFlag = 1;
      }
      else      n1x++;

      if(deleteFlag) {
        sat_DeleteClause(cm, v);
        sat_Enqueue(cm->unusedAigQueue, v);
        break;
      }
      if((size > option->maxLitsLimit) && (n1x > 1)) {
        sat_DeleteClause(cm, v);
        sat_Enqueue(cm->unusedAigQueue, v);
        break;
      }
      if(n1x > unrelevance) {
        sat_DeleteClause(cm, v);
        sat_Enqueue(cm->unusedAigQueue, v);
        break;
      }
    }

  }

  cm->each->nDeletedButUncompacted += cm->each->nDeletedCl - nDeletedCl;
  ratio = (double)cm->each->nDeletedButUncompacted/
          (double)(cm->each->nConflictCl-cm->each->nDeletedCl);

  if(ratio> 0.2) {
    sat_CompactClauses(cm);
    cm->each->nDeletedButUncompacted = 0;
  }

}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_CleanDatabase ( satManager_t *  cm)

Function********************************************************************

Synopsis [ clean value and flag of node ]

Description [ clean value and flag of node ]

SideEffects []

SeeAlso []

Definition at line 1764 of file satUtil.c.

{
long v, i;

  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    v = i;
    SATvalue(v) = 2;
    SATflags(v) &= PreserveMask;
  }
}

Here is the caller graph for this function:

void sat_CleanLevel ( satLevel_t *  d)

Function********************************************************************

Synopsis [ Clean decision level when backtracking ]

Description [ Clean decision level when backtracking ]

SideEffects []

SeeAlso []

Definition at line 1370 of file satUtil.c.

{
  if(d->implied)
    d->implied->num = 0;
  if(d->satisfied)
    d->satisfied->num = 0;
  d->currentVarPos = 0;
}
void sat_CollectBlockingClause ( satManager_t *  cm)

Function********************************************************************

Synopsis [ Collect blocking clauses]

Description [ Collect blocking clauses]

SideEffects []

SeeAlso []

fprintf(stdout, "Frontier processed\n"); sat_PrintNode(cm, i);

Definition at line 2622 of file satUtil.c.

{
satArray_t *reached, *frontier;
long i, v, tv, *plit;
int j, size;
int inverted, num;
int nReachs, nFrontiers;

  if(cm->reached == 0)  cm->reached = sat_ArrayAlloc(1024);
  if(cm->frontier == 0) cm->frontier = sat_ArrayAlloc(1024);

  frontier = cm->frontier;
  reached = cm->reached;

  frontier->num = 0;
  reached->num = 0;
  sat_ArrayInsert(frontier, 0);
  sat_ArrayInsert(reached, 0);
  nReachs = nFrontiers = 0;

  for(i=cm->beginConflict; i<cm->nodesArraySize; i+=satNodeSize) {
    if(!(SATflags(i) & IsBlockingMask))
      continue;

    if(SATreadInUse(i) == 0)            continue;

    if((SATflags(i) & IsFrontierMask)) {

      plit = (long*)SATfirstLit(i);
      size = SATnumLits(i);
      num = frontier->num;
      for(j=0; j<size; j++, plit++) {
        v = SATgetNode(*plit);
        inverted = SATisInverted(v);
        tv = SATnormalNode(v);
        sat_ArrayInsert(frontier, v);
      }
      nFrontiers++;
      sat_ArrayInsert(frontier, 0);
    }

    plit = (long*)SATfirstLit(i);
    size = SATnumLits(i);
    for(j=0; j<size; j++, plit++) {
      v = SATgetNode(*plit);
      sat_ArrayInsert(reached, v);
    }
    sat_ArrayInsert(reached, 0);
    nReachs ++;
  }



  cm->frontier = frontier;
  cm->reached = reached;
  fprintf(stdout, "NOTICE : %d frontier are collected\n", nFrontiers);
  fprintf(stdout, "NOTICE : %d blocking clauses are collected\n", nReachs);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_CombineStatistics ( satManager_t *  cm)

Function********************************************************************

Synopsis [ Combine statistics of several runs]

Description [ Combine statistics of several runs]

SideEffects []

SeeAlso []

Definition at line 2833 of file satUtil.c.

{
    /* CONSIDER ... */
}

Here is the caller graph for this function:

void sat_CompactClauses ( satManager_t *  cm)

Function********************************************************************

Synopsis [ Compact clause database ]

Description [ Compact clause database ]

SideEffects []

SeeAlso []

SATfirstLit(v) = (int)(&(plit[i]) - SATnumLits(v));

Definition at line 1519 of file satUtil.c.

{
satLiteralDB_t *literals;
long *plit, v, lit;
int i, size, index;
int inverted;
satVariable_t *var;

  literals = cm->literals;
  size = literals->last - literals->begin;

  plit = literals->begin;
  index = literals->initialSize-literals->begin;
  for(i=literals->initialSize-literals->begin; i<size; i++) {
    if(i < 2) {
      plit[index] = plit[i];
      index++;
      continue;
    }

    if(plit[i-1] == 0 && plit[i] < 0)   continue;
    else if(plit[i-1] == 0 && plit[i] == 0)     continue;
    else if(plit[i-1] < 0 && plit[i] == 0)      continue;
    else if(plit[i-1] < 0 && plit[i] < 0 && plit[i+1] == 0)     continue;
    else {
      plit[index] = plit[i];
      index++;
    }
  }

  literals->last = literals->begin + index;
  for(v=satNodeSize; v<cm->beginConflict; v+=satNodeSize) {
    if(SATflags(v) & IsCNFMask) continue;
    var = SATgetVariable(v);
    if(var->wl[0]) var->wl[0]->num = 0;
    if(var->wl[1]) var->wl[1]->num = 0;
  }

  size = literals->last - literals->begin;
  plit = literals->begin;
  for(i=0; i<size; i++) {
    lit = plit[i];
    if(lit > 0 && SATisWL(lit)) {
      v = SATgetNode(lit);
      inverted = !(SATisInverted(v));
      v = SATnormalNode(v);
      var = SATgetVariable(v);
      if(var->wl[inverted] == 0)
        var->wl[inverted] = sat_ArrayAlloc(4);
      sat_ArrayInsert(var->wl[inverted], (long)(&(plit[i])));
    }

    if(lit <= 0) {
      v = -lit;
      (cm->nodesArray[v+satFirstLit]) = (long)(&(plit[i]) - SATnumLits(v));
    }
  }

  plit = literals->last - 1;
  cm->currentTopConflict = plit;
  cm->currentTopConflictCount = 0;

}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_CompactFanout ( satManager_t *  cm)

Function********************************************************************

Synopsis [ Compact fanout of AIG node ]

Description [ Compact fanout of AIG node ]

SideEffects []

SeeAlso []

Definition at line 1787 of file satUtil.c.

{
int bufSize, bufIndex;
long *buf, *fan;
long i, v, cur;
int j, size, tsize;

  bufSize = 1024;
  bufIndex = 0;
  buf = ALLOC(long, bufSize);
  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    v = i;

    if(!(SATflags(v) & CoiMask))
      continue;

    size = SATnFanout(v);
    if(size >= bufSize) {
      bufSize <<= 1;
      if(size >= bufSize)
        bufSize = size + 1;
      buf = REALLOC(long, buf, bufSize);
    }

    bufIndex = 0;
    for(j=0, fan = SATfanout(v); j<size; j++) {
      cur = fan[j];
      cur >>= 1;
      cur = SATnormalNode(cur);
      if(!(SATflags(cur) & CoiMask))
        continue;
      buf[bufIndex++] = fan[j];
    }

    if(bufIndex > 0) {
      tsize = bufIndex;
      for(j=0, fan=SATfanout(v); j<size; j++) {
        cur = fan[j];
        cur >>= 1;
        cur = SATnormalNode(cur);
        if(!(SATflags(cur) & CoiMask))  {
          buf[bufIndex++] = fan[j];
          continue;
        }
      }
      buf[bufIndex] = 0;
      memcpy(fan, buf, sizeof(long)*(size+1));
      SATnFanout(v) = tsize;
    }
    else {
      SATnFanout(v) = 0;
    }
  }

  free(buf);

  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    v = i;
    if(!(SATflags(v) & CoiMask))
      continue;
    fan = SATfanout(v);
    size = SATnFanout(v);
    qsort(fan, size, sizeof(long), NodeIndexCompare);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

long sat_CreateNode ( satManager_t *  cm,
long  left,
long  right 
)

Function********************************************************************

Synopsis [ Create AIG node ]

Description [ Create AIG node, This function is identical with bAig_CreateNode, We have this function here to isolate this package from baig]

SideEffects []

SeeAlso []

SATfanout(newNode) = 0;

Definition at line 2727 of file satUtil.c.

{
long newNode;

  newNode = cm->nodesArraySize;
  //Bing: to deal with the case that cm->maxNodesArraySize is not multiple of
  // satNodeSize
  cm->nodesArraySize += satNodeSize;

  if(cm->nodesArraySize >= cm->maxNodesArraySize) {
    cm->maxNodesArraySize = 2* cm->maxNodesArraySize;
    cm->nodesArray = REALLOC(long, cm->nodesArray, cm->maxNodesArraySize);
  }
  cm->nodesArray[newNode + satRight] = right;
  cm->nodesArray[newNode + satLeft] = left;

  //cm->nodesArraySize += satNodeSize;

  SATflags(newNode) = 0;
  SATnext(newNode) = 2;
  SATnFanout(newNode) = 0;
  (cm->nodesArray[newNode+satFanout]) = 0;
  //Bing:
  SATvalue(newNode) = 2;

  return(newNode);
}

Here is the caller graph for this function:

satQueue_t* sat_CreateQueue ( long  MaxElements)

Function********************************************************************

Synopsis [ Create queue ]

Description [ Create queue ]

SideEffects []

SeeAlso []

Definition at line 1177 of file satUtil.c.

{
satQueue_t *Q;

  Q = ALLOC(satQueue_t, 1);
  if( Q == NULL )
    fprintf(stderr, "Out of space!!!\n" );

  Q->array = ALLOC(long, MaxElements );
  if( Q->array == NULL )
    fprintf(stderr, "Out of space!!!\n" );
  Q->max = MaxElements;
  Q->size = 0;
  Q->front = 1;
  Q->rear = 0;
  return Q;
}

Here is the caller graph for this function:

void sat_DeleteClause ( satManager_t *  cm,
long  v 
)

Function********************************************************************

Synopsis [ Delete conflict clauses ]

Description [ Delete conflict clauses ]

SideEffects []

SeeAlso []

SATresetInUse(v);

Definition at line 1484 of file satUtil.c.

{
satStatistics_t *stats;
int size, i;
long nv, *plit;

  stats = cm->each;
  size = SATnumLits(v);
  stats->nDeletedCl++;
  stats->nDeletedLit += size;

  SATflags(v) = 0;
  SATflags(v) |= IsCNFMask;

  for(i=0, plit=(long*)SATfirstLit(v); i<size; i++, plit++) {
    nv = SATgetNode(*plit);
    *plit = 0;
  }
}

Here is the caller graph for this function:

long sat_Dequeue ( satQueue_t *  Q)

Function********************************************************************

Synopsis [ Dequeue ]

Description [ Dequeue ]

SideEffects []

SeeAlso []

Definition at line 1281 of file satUtil.c.

{
  long front;
  long v;

  if(Q->size > 0) {
    Q->size--;
    front = Q->front;
    v = Q->array[front];
    Q->front = (++(front) == Q->max) ? 0 : front;
    return v;
  }
  else
    return(0);
}

Here is the caller graph for this function:

int sat_EnlargeLiteralDB ( satManager_t *  cm)

Function********************************************************************

Synopsis [ Enlarge clause database ]

Description [ Enlarge clause database ]

SideEffects []

SeeAlso []

SATfirstLit(tv) = (int)((int*)(SATfirstLit(tv)) + offset);

SATfirstLit(tv) = (int)((int*)(SATfirstLit(tv)) + offset);

Definition at line 1598 of file satUtil.c.

{
satLiteralDB_t *literals;
int nLiveConflictCl, nLiveConflictLit;
double ratio, growRatio;
double memUsage;
long *oldBegin, *oldEnd;
long newSize, oldSize;
int offset, index, size;
int i, j, nodesSize;
long tv;
int arrSize;
satVariable_t *var;
satArray_t *wl;
satStatistics_t *stats;
satOption_t *option;


  literals = cm->literals;
  option = cm->option;
  stats = cm->each;

  size = literals->last - literals->begin;
  nLiveConflictCl = cm->initNumClauses + stats->nConflictCl + stats->nBlockingCl - stats->nDeletedCl;
  nLiveConflictLit = cm->initNumLiterals + stats->nBlockingLit +
                     stats->nConflictLit - stats->nDeletedLit ;
  ratio = (double)(nLiveConflictLit + (nLiveConflictCl << 1)) /
          (double)(size);

  if(ratio < 0.8) {
    sat_CompactClauses(cm);
    return(1);
  }

  memUsage = (double)sat_MemUsage(cm);
  growRatio = 1.0;
  if(memUsage < (double)option->memoryLimit/4.0)        growRatio = 2.0;
  else if(memUsage < (double)option->memoryLimit/2.0)   growRatio = 1.5;
  else if(memUsage < (double)option->memoryLimit*0.8)   growRatio = 1.2;

  if(growRatio < 1.5) {
    if(ratio < 0.9) {
      sat_CompactClauses(cm);
      return(1);
    }
  }

  oldBegin = literals->begin;
  oldEnd = literals->end;
  oldSize = literals->last - literals->begin;
  newSize = oldSize * (int)growRatio;

  literals->begin = REALLOC(long, oldBegin, newSize);
  literals->last = literals->begin + oldSize;
  literals->end = literals->begin + newSize;

  offset = literals->begin - oldBegin;
  nodesSize = cm->nodesArraySize;
  for(i=satNodeSize; i<nodesSize; i+= satNodeSize) {
    tv = i;
    if(SATflags(tv) & IsCNFMask) {
      if(SATreadInUse(tv))
        (cm->nodesArray[tv+satFirstLit]) = (long)((long*)(SATfirstLit(tv)) + offset);
    }
    else if(SATflags(tv) & IsBDDMask) {
      (cm->nodesArray[tv+satFirstLit]) = (long)((long*)(SATfirstLit(tv)) + offset);
    }
    else {
      var = SATgetVariable(tv);
      wl = var->wl[0];
      if(wl) {
        arrSize = wl->num;
        for(j=0, index=0; j<arrSize; j++) {
          if(wl->space[j] == 0) continue;
          wl->space[j] = (long)(((long*)(wl->space[j])) + offset);
        }
      }
      wl = var->wl[1];
      if(wl) {
        arrSize = wl->num;
        for(j=0, index=0; j<arrSize; j++) {
          if(wl->space[j] == 0) continue;
          wl->space[j] = (long)(((long*)(wl->space[j])) + offset);
        }
      }
    }
  }
  literals->initialSize = literals->initialSize + offset;
  cm->currentTopConflict += offset;

  return(1);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_Enqueue ( satQueue_t *  Q,
long  v 
)

Function********************************************************************

Synopsis [ Enqueue node ]

Description [ Enqueue node ]

SideEffects []

SeeAlso []

Definition at line 1228 of file satUtil.c.

{
  long *arr, *oarr;
  long rear;

  if(Q->size < Q->max) {
    Q->size++;
    rear = Q->rear;
    rear = (++(rear) == Q->max) ? 0 : rear;
    Q->array[rear] = v;
    Q->rear = rear;
  }
  else {
    arr = ALLOC(long, Q->size * 2 );
    if(arr == NULL )
       fprintf(stderr, "Out of space!!!\n" );
    oarr = Q->array;
    if(Q->front > Q->rear) {
       memcpy(&(arr[1]), &(oarr[Q->front]),
               sizeof(long) *(Q->max-Q->front));
       memcpy(&(arr[Q->size-Q->front+1]), &(oarr[0]),
               sizeof(long) *(Q->rear+1));
    }
    else if(Q->front < Q->rear) {
       memcpy(&(arr[1]), &(oarr[Q->front]), sizeof(long) *(Q->size));
    }
    free(oarr);
    Q->array = arr;
    Q->front = 1;
    Q->rear = Q->size;
    Q->max *= 2;

    Q->size++;
    rear = Q->rear;
    rear = (++(rear) == Q->max) ? 0 : rear;
    Q->array[rear] = v;
    Q->rear = rear;
  }
}

Here is the caller graph for this function:

void sat_FreeInterface ( satInterface_t *  interface)

Function********************************************************************

Synopsis [ Free interface]

Description [ Free interface]

SideEffects []

SeeAlso []

Definition at line 2698 of file satUtil.c.

{
  if(interface == 0)    return;

  if(interface->total)
    free(interface->total);
  if(interface->nonobjUnitLitArray)
    sat_ArrayFree(interface->nonobjUnitLitArray);
  if(interface->objUnitLitArray)
    sat_ArrayFree(interface->objUnitLitArray);
  if(interface->savedConflictClauses)
    free(interface->savedConflictClauses);
  free(interface);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_FreeLiteralsDB ( satLiteralDB_t *  literals)

Function********************************************************************

Synopsis [ Free clause database ]

Description [ Free clause database ]

SideEffects []

SeeAlso []

Definition at line 1743 of file satUtil.c.

{

  if(literals == 0)     return;
  free(literals->begin);
  literals->begin = 0;
  free(literals);
}

Here is the caller graph for this function:

void sat_FreeManager ( satManager_t *  cm)

Function********************************************************************

Synopsis [ Free manager after SAT solving]

Description [ Free manager after SAT solving]

SideEffects []

SeeAlso []

Definition at line 2092 of file satUtil.c.

{
satVariable_t *var;
satLevel_t *d;
int i;

  if(cm->option)        sat_FreeOption(cm->option);
  if(cm->total)         sat_FreeStatistics(cm->total);
  if(cm->each)          sat_FreeStatistics(cm->each);

  if(cm->literals)      sat_FreeLiteralsDB(cm->literals);

  if(cm->decisionHead) {
    for(i=0; i<cm->decisionHeadSize; i++) {
      d = &(cm->decisionHead[i]);
      if(d->implied)
        sat_ArrayFree(d->implied);
      if(d->satisfied)
        sat_ArrayFree(d->satisfied);
    }
    free(cm->decisionHead);
    cm->decisionHead = 0;
    cm->decisionHeadSize = 0;
  }

  if(cm->queue)         sat_FreeQueue(cm->queue);
  if(cm->BDDQueue)      sat_FreeQueue(cm->BDDQueue);
  if(cm->unusedAigQueue)sat_FreeQueue(cm->unusedAigQueue);
  cm->queue = 0;
  cm->BDDQueue = 0;
  cm->unusedAigQueue = 0;

  if(cm->auxObj)               sat_ArrayFree(cm->auxObj);
  if(cm->obj)                  sat_ArrayFree(cm->obj);
  if(cm->unitLits)             sat_ArrayFree(cm->unitLits);
  if(cm->pureLits)             sat_ArrayFree(cm->pureLits);
  if(cm->assertion)            sat_ArrayFree(cm->assertion);
  if(cm->auxArray)             sat_ArrayFree(cm->auxArray);
  if(cm->nonobjUnitLitArray)   sat_ArrayFree(cm->nonobjUnitLitArray);
  if(cm->objUnitLitArray)      sat_ArrayFree(cm->objUnitLitArray);
  if(cm->orderedVariableArray) sat_ArrayFree(cm->orderedVariableArray);
  if(cm->clauseIndexInCore)    sat_ArrayFree(cm->clauseIndexInCore);
  cm->auxObj = 0;
  cm->obj = 0;
  cm->unitLits = 0;
  cm->pureLits = 0;
  cm->assertion = 0;
  cm->auxArray = 0;
  cm->nonobjUnitLitArray = 0;
  cm->objUnitLitArray = 0;
  cm->orderedVariableArray = 0;

  if(cm->variableArray) {
    for(i=0; i<=cm->initNumVariables; i++) {
      var = &(cm->variableArray[i]);
      if(var->wl[0]) {
        sat_ArrayFree(var->wl[0]);
        var->wl[0] = 0;
      }
      if(var->wl[1]) {
        sat_ArrayFree(var->wl[1]);
        var->wl[1] = 0;
      }
    }
    free(cm->variableArray);
    cm->variableArray = 0;
  }


  if(cm->comment)       free(cm->comment);

  if(cm->nodesArray)    free(cm->nodesArray);
  free(cm);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_FreeOption ( satOption_t *  option)

Function********************************************************************

Synopsis [ Free option after SAT solving]

Description [ Free option after SAT solving]

SideEffects []

SeeAlso []

Definition at line 2179 of file satUtil.c.

{
  if(option)
    free(option);
}

Here is the caller graph for this function:

void sat_FreeQueue ( satQueue_t *  Q)

Function********************************************************************

Synopsis [ Free queue ]

Description [ Free queue ]

SideEffects []

SeeAlso []

Definition at line 1207 of file satUtil.c.

{
  if( Q != NULL ) {
    free( Q->array );
    free( Q );
  }
}

Here is the caller graph for this function:

void sat_FreeStatistics ( satStatistics_t *  stats)

Function********************************************************************

Synopsis [ Free statistic after SAT solving]

Description [ Free statistic after SAT solving]

SideEffects []

SeeAlso []

Definition at line 2197 of file satUtil.c.

{
  if(stats)
    free(stats);
}

Here is the caller graph for this function:

long sat_GetCanonical ( satManager_t *  cm,
long  v 
)

Function********************************************************************

Synopsis [ Get canonical node ]

Description [ Get canonical node ]

SideEffects []

SeeAlso []

Definition at line 2802 of file satUtil.c.

{
long nv;
int inverted;

  if(v == 2)    return(2);

  while(!(SATflags(SATnormalNode(v))) & CanonicalBitMask) {
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    nv = SATcanonical(v);
    if(inverted)
      nv = SATnot(nv);
    v = nv;
  }
  return(v);
}

Here is the caller graph for this function:

long sat_GetClauseFromLit ( satManager_t *  cm,
long *  lit 
)

Function********************************************************************

Synopsis [ Find a clause index from literal pointer.]

Description [ Find a clause index from literal pointer.]

SideEffects []

SeeAlso []

Definition at line 3176 of file satUtil.c.

{
  while(*lit > 0) {
    lit++;
  }
  return(-(*lit));
}
int sat_GetFanoutSize ( satManager_t *  cm,
long  v 
)

Function********************************************************************

Synopsis [ Get fanout size of AIG node ]

Description [ Get fanout size of AIG node ]

SideEffects []

SeeAlso []

Definition at line 1891 of file satUtil.c.

{
long *fan;
int i;

  fan = SATfanout(v);
  if(fan == 0)  return(0);

  for(i=0; fan[i]!=0; i++);
  return(i);
}

Here is the caller graph for this function:

int sat_GetNumberOfInitialClauses ( satManager_t *  cm)

Function********************************************************************

Synopsis [ Get the number of initial clauses ]

Description [ Get the number of initial clauses. This function works properly only CNF sat case]

SideEffects []

SeeAlso []

Definition at line 2851 of file satUtil.c.

{
  return(cm->initNumClauses);
}

Here is the caller graph for this function:

int sat_GetNumberOfInitialVariables ( satManager_t *  cm)

Function********************************************************************

Synopsis [ Get the number of initial variables ]

Description [ Get the number of initial variables. This function works properly only CNF sat case]

SideEffects []

SeeAlso []

Definition at line 2869 of file satUtil.c.

{
  return(cm->initNumVariables);
}

Here is the caller graph for this function:

satManager_t* sat_InitManager ( satInterface_t *  interface)

Function********************************************************************

Synopsis [ Allocate manager for SAT solving]

Description [ Allocate manager for SAT solving]

SideEffects []

SeeAlso []

Definition at line 2057 of file satUtil.c.

{
satManager_t *cm;

  cm = ALLOC(satManager_t, 1);
  memset(cm, 0, sizeof(satManager_t));

  if(interface) {
    cm->total = interface->total;
    cm->nonobjUnitLitArray = interface->nonobjUnitLitArray;
    cm->savedConflictClauses = interface->savedConflictClauses;
    cm->trieArray = interface->trieArray;
    cm->objUnitLitArray = sat_ArrayAlloc(8);
  }
  else {
    cm->total = sat_InitStatistics();
    cm->objUnitLitArray = sat_ArrayAlloc(8);
    cm->nonobjUnitLitArray = sat_ArrayAlloc(8);
  }

  return(cm);
}

Here is the call graph for this function:

Here is the caller graph for this function:

satOption_t* sat_InitOption ( )

Function********************************************************************

Synopsis [ Allocate option]

Description [ Allocate option ]

SideEffects []

SeeAlso []

option->decisionHeuristic |= DVH_DECISION;

option->clauseDeletionHeuristic |= MAX_UNRELEVANCE_DELETION; option->clauseDeletionHeuristic |= SIMPLE_LATEST_DELETION;

50

Definition at line 2216 of file satUtil.c.

{
satOption_t *option;

  option = ALLOC(satOption_t, 1);
  memset(option, 0, sizeof(satOption_t));

  option->decisionHeuristic |= LATEST_CONFLICT_DECISION;
  option->decisionAgeInterval = 0xff;
  option->decisionAgeRestart = 1;
  option->minConflictForDecision = 50;
  option->maxConflictForDecision = 10000;
  option->skipSatisfiedClauseForDecision = 0;


  option->clauseDeletionHeuristic |= LATEST_ACTIVITY_DELETION;
  option->clauseDeletionInterval = 2500;
  option->nextClauseDeletion = option->clauseDeletionInterval*5;
  option->unrelevance = 20;
  option->minLitsLimit = 20;
  option->maxLitsLimit = 1000;

  option->latestUnrelevance = 45;
  option->obsoleteUnrelevance = 20;//6
  option->latestUsage = 100;
  option->obsoleteUsage = 2;
  option->latestRate = 16;

  option->incNumObjLitsLimit = 20; 
  option->incNumNonobjLitsLimit = 50;

  option->incPreserveNonobjective = 1;
  option->minimizeConflictClause = 1;


  option->BDDMonolithic = 0;
  option->BDDDPLL = 0;
  option->maxLimitOfVariablesForMonolithicBDD = 2000;
  option->maxLimitOfClausesForMonolithicBDD = 20000;
  option->maxLimitOfCutSizeForMonolithicBDD = 2000;

  option->maxLimitOfVariablesForBDDDPLL = 200;
  option->maxLimitOfClausesForBDDDPLL = 2000;
  option->maxLimitOfCutSizeForBDDDPLL = 500;

  option->maxLimitOfVariablesForBDD = 50;

  option->memoryLimit = 1024 * 1024 * 1024;

  return(option);
}

Here is the caller graph for this function:

satStatistics_t* sat_InitStatistics ( void  )

Function********************************************************************

Synopsis [ Allocate statistics]

Description [ Allocate statistics]

SideEffects []

SeeAlso []

Definition at line 2383 of file satUtil.c.

{
satStatistics_t *stats;

  stats = ALLOC(satStatistics_t, 1);
  memset(stats, 0, sizeof(satStatistics_t));

  return(stats);
}

Here is the caller graph for this function:

void sat_MarkTransitiveFaninForArray ( satManager_t *  cm,
satArray_t *  arr,
unsigned int  mask 
)

Function********************************************************************

Synopsis [ Mark transitive fanin of given array of node ]

Description [ Mark transitive fanin of given array of node ]

SideEffects []

SeeAlso []

Definition at line 1917 of file satUtil.c.

{
long v;
int i, size;

  if(arr == 0)  return;
  size = arr->num;

  for(i=0; i<size; i++) {
    v = arr->space[i];
    sat_MarkTransitiveFaninForNode(cm, v, mask);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_MarkTransitiveFaninForNode ( satManager_t *  cm,
long  v,
unsigned int  mask 
)

Function********************************************************************

Synopsis [ Mark transitive fanin of given node ]

Description [ Mark transitive fanin of given node ]

SideEffects []

SeeAlso []

Definition at line 1946 of file satUtil.c.

{
  if(v == 2)    return;

  v = SATnormalNode(v);

  if(SATflags(v) & mask)        return;

  SATflags(v) |= mask;

  sat_MarkTransitiveFaninForNode(cm, SATleftChild(v), mask);
  sat_MarkTransitiveFaninForNode(cm, SATrightChild(v), mask);
}

Here is the caller graph for this function:

int sat_MemUsage ( satManager_t *  cm)

Function********************************************************************

Synopsis [ Usage of memory ]

Description [ Usage of memory ]

SideEffects []

SeeAlso []

Definition at line 2773 of file satUtil.c.

{
satLiteralDB_t *literals;
satStatistics_t *stats;
int aigSize, cnfSize, watchedSize;

  literals = cm->literals;
  stats = cm->each;
  aigSize = sizeof(int) * cm->maxNodesArraySize;
  cnfSize = sizeof(int) * (literals->end - literals->begin);
  watchedSize = sizeof(int) * 2 *
                 (stats->nConflictCl - stats->nDeletedCl);
  return(aigSize + cnfSize + watchedSize);
}

Here is the caller graph for this function:

void sat_PutAssignmentValueMain ( satManager_t *  cm,
satLevel_t *  d,
satArray_t *  arr 
)

Function********************************************************************

Synopsis [ Put assignments.]

Description [ Put assignments.]

SideEffects []

SeeAlso []

Definition at line 3010 of file satUtil.c.

{
long v;
int i;
int inverted;

  if(arr == 0)  return;

  if(cm->variableArray == 0) {
    cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
    memset(cm->variableArray, 0,
            sizeof(satVariable_t) * (cm->initNumVariables+1));
  }

  for(i=0; i<arr->num; i++) {
    v = arr->space[i];
    inverted = SATisInverted(v);
    v = SATnormalNode(v);

    SATvalue(v) = !inverted;
  }
}

Here is the caller graph for this function:

satArray_t* sat_ReadForcedAssignment ( char *  filename)

Function********************************************************************

Synopsis [ Read forced assignments.]

Description [ Read forced assignments.]

SideEffects []

SeeAlso []

Definition at line 2886 of file satUtil.c.

{
FILE *fin;
char line[102400], word[1024];
char *lp;
satArray_t *arr;
long v;

  if(!(fin = fopen(filename, "r"))) {
    fprintf(stdout, "ERROR : Can't open file %s\n", filename);
    return(0);
  }

  arr = sat_ArrayAlloc(64);
  while(fgets(line, 102400, fin)) {
    lp = sat_RemoveSpace(line);
    if(lp[0] == '\n')   continue;
    while(1) {
      lp = sat_RemoveSpace(lp);
      lp = sat_CopyWord(lp, word);
      if(strlen(word)) {
        v = atoi(word);
        v *= satNodeSize;
        if(v < 0)       v = SATnot(-v);
        sat_ArrayInsert(arr, v);
      }
      else {
        break;
      }
    }
  }
  fclose(fin);

  return(arr);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_ReportStatistics ( satManager_t *  cm,
satStatistics_t *  stats 
)

Function********************************************************************

Synopsis [ Report statistics]

Description [ Report statistics]

SideEffects []

SeeAlso []

Definition at line 2287 of file satUtil.c.

{
satOption_t *option;

  option = cm->option;
  fprintf(cm->stdOut, "%s Number of decisions %d\n",
              cm->comment, stats->nDecisions);
  if(option->decisionHeuristic & DVH_DECISION) {
    fprintf(cm->stdOut, "%s Number of DVH decisions %d\n",
              cm->comment, stats->nDVHDecisions);
  }
  if(option->decisionHeuristic & LATEST_CONFLICT_DECISION) {
    fprintf(cm->stdOut, "%s Number of latest conflict decisions %d\n",
              cm->comment, stats->nLatestConflictDecisions);
  }
  fprintf(cm->stdOut, "%s Number of backtracks %d\n",
              cm->comment, stats->nBacktracks);

  fprintf(cm->stdOut, "%s Number of CNF implications %d\n",
              cm->comment, stats->nCNFImplications);
  fprintf(cm->stdOut, "%s Number of Aig implications %d\n",
              cm->comment, stats->nAigImplications);
  fprintf(cm->stdOut, "%s Number of BDD implications %d\n",
              cm->comment, stats->nBDDImplications);

  fprintf(cm->stdOut, "%s Number of unit conflict clauses %d\n",
              cm->comment, stats->nUnitConflictCl);
  fprintf(cm->stdOut, "%s Number of conflict clauses %d\n",
              cm->comment, stats->nConflictCl);
  fprintf(cm->stdOut, "%s Number of conflict literals %d\n",
              cm->comment, stats->nConflictLit);
  fprintf(cm->stdOut, "%s Number of deleted clauses %d\n",
              cm->comment, stats->nDeletedCl);
  fprintf(cm->stdOut, "%s Number of deleted literals %d\n",
              cm->comment, stats->nDeletedLit);

  if(option->incTraceObjective + option->incDistill) {
    fprintf(cm->stdOut, "%s Number of init object conflict clauses %d\n",
              cm->comment, stats->nInitObjConflictCl);
    fprintf(cm->stdOut, "%s Number of init object conflict literals %d\n",
              cm->comment, stats->nInitObjConflictLit);
    fprintf(cm->stdOut, "%s Number of init non-object conflict clauses %d\n",
              cm->comment, stats->nInitNonobjConflictCl);
    fprintf(cm->stdOut, "%s Number of init non-object conflict literals %d\n",
              cm->comment, stats->nInitNonobjConflictLit);
    fprintf(cm->stdOut, "%s Number of object conflict clauses %d\n",
              cm->comment, stats->nObjConflictCl);
    fprintf(cm->stdOut, "%s Number of object conflict literals %d\n",
              cm->comment, stats->nObjConflictLit);
    fprintf(cm->stdOut, "%s Number of non-object conflict clauses %d\n",
              cm->comment, stats->nNonobjConflictCl);
    fprintf(cm->stdOut, "%s Number of non-object conflict literals %d\n",
              cm->comment, stats->nNonobjConflictLit);
  }
  if(option->incDistill) {
    fprintf(cm->stdOut, "%s Number of distill object conflict clauses %d\n",
              cm->comment, stats->nDistillObjConflictCl);
    fprintf(cm->stdOut, "%s Number of distill object conflict literals %d\n",
              cm->comment, stats->nDistillObjConflictLit);
    fprintf(cm->stdOut, "%s Number of distill non-object conflict clauses %d\n",
              cm->comment, stats->nDistillNonobjConflictCl);
    fprintf(cm->stdOut, "%s Number of distill non-object conflict literals %d\n",
              cm->comment, stats->nDistillNonobjConflictLit);
  }
  if(option->allSatMode) {
    fprintf(cm->stdOut, "%s Number of blocking clauses %d\n",
              cm->comment, stats->nBlockingCl);
    fprintf(cm->stdOut, "%s Number of blocking literals %d\n",
              cm->comment, stats->nBlockingLit);
  }

  fprintf(cm->stdOut, "%s Maximum decision level %d\n",
              cm->comment, stats->maxDecisionLevel);
  fprintf(cm->stdOut, "%s Number of low score decisions %d\n",
              cm->comment, stats->nLowScoreDecisions);
  fprintf(cm->stdOut, "%s Total nonchronological backtracks %d\n",
              cm->comment, stats->nNonchonologicalBacktracks);
  fprintf(cm->stdOut, "%s Total run time %10g\n", cm->comment, stats->satTime);
  fflush(cm->stdOut);

}

Here is the caller graph for this function:

void sat_RestoreBlockingClauses ( satManager_t *  cm)

Function********************************************************************

Synopsis [ Restore blocking clauses]

Description [ Restore blocking clauses]

SideEffects []

SeeAlso []

fprintf(stdout, "NOTICE : forwarded blocking clause\n"); sat_PrintNode(cm, c);

Definition at line 2435 of file satUtil.c.

{
long *space, *start;
long c, v;
int i;
satArray_t *reached;
satArray_t *clause;
satArray_t *unitLits;

  reached = cm->reached;
  if(reached == 0)
    return;

  unitLits = cm->unitLits;
  if(unitLits == 0)
    unitLits = cm->unitLits = sat_ArrayAlloc(16);

  clause = sat_ArrayAlloc(50);

  for(i=0, space=reached->space; i<reached->num; i++, space++){
    if(*space <= 0) {
      space++;
      i++;
      if(i>=reached->num)
        break;
      start = space;
      clause->num = 0;
      while(*space > 0) {
        v = (*space);
        sat_ArrayInsert(clause, SATnot(v));
        i++;
        space++;
      }

      c = sat_AddBlockingClause(cm, clause);

      if(clause->num == 1)
        sat_ArrayInsert(unitLits, (v));
      i--;
      space--;
    }
  }
  sat_ArrayFree(clause);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_RestoreClauses ( satManager_t *  cm,
satArray_t *  cnfArray 
)

Function********************************************************************

Synopsis [ Restore clauses]

Description [ Restore clauses]

SideEffects []

SeeAlso []

Definition at line 2563 of file satUtil.c.

{
long *space, *start;
long c, v;
int i;
satArray_t *clause;
satArray_t *unitLits;


  unitLits = cm->unitLits;
  if(unitLits == 0)
    unitLits = cm->unitLits = sat_ArrayAlloc(16);

  clause = sat_ArrayAlloc(50);

  for(i=0, space=cnfArray->space; i<cnfArray->num; i++, space++){
    if(*space <= 0) {
      space++;
      i++;
      if(i>=cnfArray->num)
        break;
      start = space;
      clause->num = 0;
      while(*space > 0) {
        v = (*space);
        sat_ArrayInsert(clause, SATnot(v));
        i++;
        space++;
      }

      if(clause->num == 1) {
        sat_ArrayInsert(unitLits, (v));
      }
      else {
        c = sat_AddClause(cm, clause);
      }

      cm->initNumClauses++;
      cm->initNumLiterals += clause->num;

      i--;
      space--;
    }
  }
  sat_ArrayFree(clause);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_RestoreFanout ( satManager_t *  cm)

Function********************************************************************

Synopsis [ Restore fanout of AIG node ]

Description [ Restore fanout of AIG node ]

SideEffects []

SeeAlso []

Definition at line 1867 of file satUtil.c.

{
long i, v;

  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    v = i;
    if((SATflags(v) & IsCNFMask))
      continue;
    SATnFanout(v) = sat_GetFanoutSize(cm, v);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_RestoreFrontierClauses ( satManager_t *  cm)

Function********************************************************************

Synopsis [ Restore Frontier clauses]

Description [ Restore Frontier clauses]

SideEffects []

SeeAlso []

sat_PrintNode(cm, c);

Definition at line 2497 of file satUtil.c.

{
long *space, *start;
long c, v;
int i;
satArray_t *frontier;
satArray_t *clause;
satArray_t *unitLits;

  frontier = cm->frontier;
  cm->frontierNodesEnd = cm->nodesArraySize;
  if(frontier == 0)
    return;

  unitLits = cm->unitLits;
  if(unitLits == 0)
    unitLits = cm->unitLits = sat_ArrayAlloc(16);

  clause = sat_ArrayAlloc(50);

  for(i=0, space=frontier->space; i<frontier->num; i++, space++){
    if(*space <= 0) {
      space++;
      i++;
      if(i>=frontier->num)
        break;
      start = space;
      clause->num = 0;
      while(*space > 0) {
        v = (*space);
        sat_ArrayInsert(clause, SATnot(v));
        i++;
        space++;
      }

      c = sat_AddClause(cm, clause);

      cm->initNumClauses++;
      cm->initNumLiterals += clause->num;
      if(clause->num == 1)
        sat_ArrayInsert(unitLits, (v));

      i--;
      space--;
    }
  }
  sat_ArrayFree(clause);
  cm->frontierNodesEnd = cm->nodesArraySize;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_SetConeOfInfluence ( satManager_t *  cm)

Function********************************************************************

Synopsis [ Set COIMask ]

Description [ Set COIMask. The COIMask of flags of node has be set to apply implication on it ]

SideEffects []

SeeAlso []

Definition at line 2035 of file satUtil.c.

{
  sat_MarkTransitiveFaninForArray(cm, cm->assertion, CoiMask);
  sat_MarkTransitiveFaninForArray(cm, cm->auxObj, CoiMask);
  sat_MarkTransitiveFaninForArray(cm, cm->obj, CoiMask);
  //Bing:
  sat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_SetIncrementalOption ( satOption_t *  option,
int  incFlag 
)

Function********************************************************************

Synopsis [ Set incremental option ]

Description [ Set incremental option ]

SideEffects []

SeeAlso []

Definition at line 2406 of file satUtil.c.

{
  if(incFlag == 0) return;

  if(incFlag == 1)  { /* TraceObjective */
    option->incTraceObjective = 1;
  }
  else if(incFlag == 2)  { /* Distill */
    option->incDistill = 1;
  }
  else if(incFlag == 3)  { /* TraceObjective & Distill */
    option->incTraceObjective = 1;
    option->incDistill = 1;
  }

}

Here is the caller graph for this function:

void sat_UnmarkTransitiveFaninForArray ( satManager_t *  cm,
satArray_t *  arr,
unsigned int  mask,
unsigned int  resetMask 
)

Function********************************************************************

Synopsis [ Unmark transitive fanin of given array of node ]

Description [ Unmark transitive fanin of given array of node ]

SideEffects []

SeeAlso []

Definition at line 1975 of file satUtil.c.

{
long v;
int i, size;

  size = arr->num;

  for(i=0; i<size; i++) {
    v = arr->space[i];
    sat_UnmarkTransitiveFaninForNode(cm, v, mask, resetMask);
  }
}

Here is the call graph for this function:

void sat_UnmarkTransitiveFaninForNode ( satManager_t *  cm,
long  v,
unsigned int  mask,
unsigned int  resetMask 
)

Function********************************************************************

Synopsis [ Unmark transitive fanin of given node ]

Description [ Unmark transitive fanin of given node ]

SideEffects []

SeeAlso []

Definition at line 2004 of file satUtil.c.

{
  if(v == 2)    return;

  v = SATnormalNode(v);

  if(!(SATflags(v) & mask))     return;

  SATflags(v) &= resetMask;
  sat_UnmarkTransitiveFaninForNode(cm, SATleftChild(v), mask, resetMask);
  sat_UnmarkTransitiveFaninForNode(cm, SATrightChild(v), mask, resetMask);
}

Here is the caller graph for this function:

Variable Documentation

char rcsid [] UNUSED = "$Id: satUtil.c,v 1.37 2009/04/11 18:26:37 fabio Exp $" [static]

CFile***********************************************************************

FileName [satUtil.c]

PackageName [sat]

Synopsis [Routines for various utility function.]

Author [HoonSang Jin]

Copyright [ This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]

Definition at line 21 of file satUtil.c.