VIS
|
#include "satInt.h"
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 $" |
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); }
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); }
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); }
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); }
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); }
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); }
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); }
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); }
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); }
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); }
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); }
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; }
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); }
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; } }
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; }
void sat_ArrayFree | ( | satArray_t * | 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; } } } }
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; } }
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; } }
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); }
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 ... */
}
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; }
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); } }
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); }
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; }
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; } }
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); }
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); }
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; } }
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); }
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); }
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); }
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);
}
void sat_FreeQueue | ( | satQueue_t * | Q | ) |
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);
}
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); }
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); }
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);
}
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);
}
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); }
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); }
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); }
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); } }
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); }
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); }
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; } }
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); }
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); }
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); }
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); }
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); } }
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; }
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); }
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; } }
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); } }
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); }
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.]