/**CFile*********************************************************************** FileName [satImplication.c] PackageName [sat] Synopsis [Routines for BCP.] 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.] ******************************************************************************/ #include "satInt.h" #include "baig.h" static char rcsid[] UNUSED = "$Id: satImplication.c,v 1.10 2009/04/11 18:26:37 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ /**AutomaticEnd***************************************************************/ typedef int (*IMPLY_FN) (satManager_t *cm, satLevel_t *d, long v, long left, long right); IMPLY_FN satImplicationFN[64]= { sat_ImplyStop, /* 0 */ sat_ImplyConflict, /* 1 */ sat_ImplyLeftForward, /* 2 */ sat_ImplyLeftForward, /* 3 */ sat_ImplyStop, /* 4 */ sat_ImplyConflict, /* 5 */ sat_ImplyLeftForward, /* 6 */ sat_ImplyLeftForward, /* 7 */ sat_ImplySplit, /* 8 */ sat_ImplyConflict, /* 9 */ sat_ImplyLeftForward, /* 10 */ sat_ImplyLeftForward, /* 11 */ sat_ImplySplit, /* 12 */ sat_ImplyConflict, /* 13 */ sat_ImplyLeftForward, /* 14 */ sat_ImplyLeftForward, /* 15 */ sat_ImplyStop, /* 16 */ sat_ImplyConflict, /* 17 */ sat_ImplyRightForward, /* 18 */ sat_ImplyRightForward, /* 19 */ sat_ImplyConflict, /* 20 */ sat_ImplyStop, /* 21 */ sat_ImplyForwardOne, /* 22 */ sat_ImplyForwardOne, /* 23 */ sat_ImplyPropRight, /* 24 */ sat_ImplyPropRightOne, /* 25 */ sat_ImplyStop, /* 26 */ sat_ImplyStop, /* 27 */ sat_ImplyPropRight, /* 28 */ sat_ImplyPropRightOne, /* 29 */ sat_ImplyStop, /* 30 */ sat_ImplyStop, /* 31 */ sat_ImplySplit, /* 32 */ sat_ImplyConflict, /* 33 */ sat_ImplyRightForward, /* 34 */ sat_ImplyRightForward, /* 35 */ sat_ImplyPropLeft, /* 36 */ sat_ImplyPropLeftOne, /* 37 */ sat_ImplyStop, /* 38 */ sat_ImplyStop, /* 39 */ sat_ImplySplit, /* 40 */ sat_ImplyPropLeftRight, /* 41 */ sat_ImplyStop, /* 42 */ sat_ImplyStop, /* 43 */ sat_ImplySplit, /* 44 */ sat_ImplyPropLeftRight, /* 45 */ sat_ImplyStop, /* 46 */ sat_ImplyStop, /* 47 */ sat_ImplySplit, /* 48 */ sat_ImplyConflict, /* 49 */ sat_ImplyRightForward, /* 50 */ sat_ImplyRightForward, /* 51 */ sat_ImplyPropLeft, /* 52 */ sat_ImplyPropLeftOne, /* 53 */ sat_ImplyStop, /* 54 */ sat_ImplyStop, /* 55 */ sat_ImplySplit, /* 56 */ sat_ImplyPropLeftRight, /* 57 */ sat_ImplyStop, /* 58 */ sat_ImplyStop, /* 59 */ sat_ImplySplit, /* 60 */ sat_ImplyPropLeftRight, /* 61 */ sat_ImplyStop, /* 62 */ sat_ImplyStop, /* 63 */ }; /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [No further implcation when this function is called.] Description [No further implcation when this function is called. 0 0 0 1 | | | | --- --- --- --- / \ / \ / \ / \ 0 X X 0 0 0 1 1 ] SideEffects [] SeeAlso [] ******************************************************************************/ int sat_ImplyStop( satManager_t *cm, satLevel_t *d, long v, long left, long right) { return(0); } /**Function******************************************************************** Synopsis [No further implcation when this function is called.] Description [No further implcation when this function is called. and need split on output. 0 | --- / \ X X ] SideEffects [] SeeAlso [] ******************************************************************************/ int sat_ImplySplit( satManager_t *cm, satLevel_t *d, long v, long left, long right) { return(0); } /**Function******************************************************************** Synopsis [The conflict happens.] Description [The conflict happens when 0 1 1 1 1 | | | | | --- --- --- --- --- / \ / \ / \ / \ / \ 1 1 X 0 0 X 1 0 0 1 ] SideEffects [] SeeAlso [] ******************************************************************************/ int sat_ImplyConflict( satManager_t *cm, satLevel_t *d, long v, long left, long right) { if(left != 2) { d->conflict = SATnormalNode(v); } return(0); } /**Function******************************************************************** Synopsis [A value implied to output due to left child.] Description [A value implied to output due to left child X X | | --- --- / \ / \ 0 1 0 X ] SideEffects [] SeeAlso [] ******************************************************************************/ int sat_ImplyLeftForward( satManager_t *cm, satLevel_t *d, long v, long left, long right) { v = SATnormalNode(v); left = SATnormalNode(left); SATvalue(v) = 0; SATmakeImplied(v, d); SATante(v) = left; sat_Enqueue(cm->queue, v); SATflags(v) |= InQueueMask; SATflags(v) |= (SATflags(left) & ObjMask); cm->each->nAigImplications++; return(0); } /**Function******************************************************************** Synopsis [A value implied to output due to right child.] Description [A value implied to output due to right child X X | | --- --- / \ / \ 1 0 X 0 ] SideEffects [] SeeAlso [] ******************************************************************************/ int sat_ImplyRightForward( satManager_t *cm, satLevel_t *d, long v, long left, long right) { v = SATnormalNode(v); right = SATnormalNode(right); SATvalue(v) = 0; SATmakeImplied(v, d); SATante(v) = right; sat_Enqueue(cm->queue, v); SATflags(v) |= InQueueMask; SATflags(v) |= (SATflags(right) & ObjMask); cm->each->nAigImplications++; return(0); } /**Function******************************************************************** Synopsis [A value implied to output due to both child.] Description [A value implied to output due to both child X | --- / \ 1 1 ] SideEffects [] SeeAlso [] ******************************************************************************/ int sat_ImplyForwardOne( satManager_t *cm, satLevel_t *d, long v, long left, long right) { v = SATnormalNode(v); left = SATnormalNode(left); right = SATnormalNode(right); SATvalue(v) = 1; SATmakeImplied(v, d); SATante(v) = right; SATante2(v) = left; sat_Enqueue(cm->queue, v); SATflags(v) |= InQueueMask; SATflags(v) |= (SATflags(right) & ObjMask); SATflags(v) |= (SATflags(left) & ObjMask); cm->each->nAigImplications++; return(0); } /**Function******************************************************************** Synopsis [A value implied to right child due to both output and left.] Description [A value implied to right child due to both output and left 0 | --- / \ 1 X ] SideEffects [] SeeAlso [] ******************************************************************************/ int sat_ImplyPropRight( satManager_t *cm, satLevel_t *d, long v, long left, long right) { int isInverted; isInverted = SATisInverted(right); v = SATnormalNode(v); left = SATnormalNode(left); right = SATnormalNode(right); SATmakeImplied(right, d); SATvalue(right) = isInverted; SATante(right) = left; SATante2(right) = v; sat_Enqueue(cm->queue, right); SATflags(right) |= InQueueMask; SATflags(right) |= (SATflags(left) & ObjMask); SATflags(right) |= (SATflags(v) & ObjMask); cm->each->nAigImplications++; return(0); } /**Function******************************************************************** Synopsis [A value implied to right child due to both output and left.] Description [A value implied to right child due to both output and left 1 | --- / \ 1 X ] SideEffects [] SeeAlso [] ******************************************************************************/ int sat_ImplyPropRightOne( satManager_t *cm, satLevel_t *d, long v, long left, long right) { int isInverted; isInverted = SATisInverted(right); v = SATnormalNode(v); left = SATnormalNode(left); right = SATnormalNode(right); SATmakeImplied(right, d); SATante(right) = v; SATvalue(right) = !isInverted; sat_Enqueue(cm->queue, right); SATflags(right) |= InQueueMask; SATflags(right) |= (SATflags(v) & ObjMask); cm->each->nAigImplications++; return(0); } /**Function******************************************************************** Synopsis [A value implied to left child due to both output and right.] Description [A value implied to left child due to both output and right 0 | --- / \ X 1 ] SideEffects [] SeeAlso [] ******************************************************************************/ int sat_ImplyPropLeft( satManager_t *cm, satLevel_t *d, long v, long left, long right) { int isInverted; isInverted = SATisInverted(left); v = SATnormalNode(v); left = SATnormalNode(left); right = SATnormalNode(right); SATmakeImplied(left, d); SATante(left) = v; SATante2(left) = right; SATvalue(left) = isInverted; sat_Enqueue(cm->queue, left); SATflags(left) |= InQueueMask; SATflags(left) |= (SATflags(v) & ObjMask); SATflags(left) |= (SATflags(right) & ObjMask); cm->each->nAigImplications++; return(0); } /**Function******************************************************************** Synopsis [A value implied to left child due to both output and right.] Description [A value implied to left child due to both output and right 1 | --- / \ X 1 ] SideEffects [] SeeAlso [] ******************************************************************************/ int sat_ImplyPropLeftOne( satManager_t *cm, satLevel_t *d, long v, long left, long right) { int isInverted; isInverted = SATisInverted(left); v = SATnormalNode(v); left = SATnormalNode(left); right = SATnormalNode(right); SATmakeImplied(left, d); SATante(left) = v; SATvalue(left) = !isInverted; sat_Enqueue(cm->queue, left); SATflags(left) |= InQueueMask; SATflags(left) |= (SATflags(v) & ObjMask); cm->each->nAigImplications++; return(0); } /**Function******************************************************************** Synopsis [A value implied to left and right child due to output.] Description [A value implied to left and right child due to output 1 | --- / \ X X ] SideEffects [] SeeAlso [] ******************************************************************************/ int sat_ImplyPropLeftRight( satManager_t *cm, satLevel_t *d, long v, long left, long right) { int isLeftInverted; int isRightInverted; if(left == right) return 1; isLeftInverted = SATisInverted(left); isRightInverted = SATisInverted(right); v = SATnormalNode(v); left = SATnormalNode(left); right = SATnormalNode(right); SATmakeImplied(left, d); SATmakeImplied(right, d); SATante(left) = v; SATante(right) = v; SATvalue(left) = !isLeftInverted; SATvalue(right) = !isRightInverted; sat_Enqueue(cm->queue, left); SATflags(left) |= InQueueMask; sat_Enqueue(cm->queue, right); SATflags(right) |= InQueueMask; SATflags(left) |= (SATflags(v) & ObjMask); SATflags(right) |= (SATflags(v) & ObjMask); cm->each->nAigImplications += 2; return(0); } /**Function******************************************************************** Synopsis [Implication based on clause.] Description [Implication based two watched literal scheme ] SideEffects [] SeeAlso [] ******************************************************************************/ void sat_ImplyCNF( satManager_t *cm, satLevel_t *d, long v, satArray_t *wl) { int size, i, j; long *space; long lit, *plit, *tplit; int dir; long nv, tv, *oplit, *wlit; int isInverted, value; int tsize, inverted; long cur, clit; satStatistics_t *stats; satOption_t *option; satQueue_t *Q; satVariable_t *var; size = wl->num; space = wl->space; Q = cm->queue; stats = cm->each; option = cm->option; nv = 0; wlit = 0; for(i=0; iconflict = nv; wl->num = size; return; } else if(value > 1) { /** implication **/ SATvalue(tv) = !isInverted; SATmakeImplied(tv, d); SATante(tv) = nv; if((SATflags(tv) & InQueueMask) == 0) { sat_Enqueue(Q, tv); SATflags(tv) |= InQueueMask; } stats->nCNFImplications++; /** to identify the objective dependent clause for incremental * SAT **/ if(option->incTraceObjective == 1) { tsize = SATnumLits(nv); for(j=0, tplit=(long*)SATfirstLit(nv); jwl[inverted]) { sat_ArrayInsert(var->wl[inverted], (long)oplit); } else { var->wl[inverted] = sat_ArrayAlloc(4); sat_ArrayInsert(var->wl[inverted], (long)oplit); } break; } } wl->num = size; } /**Function******************************************************************** Synopsis [Apply implication on node. If the conflict happens then return 0, otherwise return 1] Description [Apply implication on node. Since the node can be part of AIG and CNF and BDD, the implications on three representation are applied] SideEffects [] SeeAlso [] ******************************************************************************/ int sat_ImplyNode( satManager_t *cm, satLevel_t *d, long v) { long *fan, cur; int value; int i, size; long left, right; satVariable_t *var; satArray_t *wlArray; value = SATvalue(v) ^ 1; var = SATgetVariable(v); wlArray = var->wl[value]; /** implcation on CNF **/ if(wlArray && wlArray->size) { sat_ImplyCNF(cm, d, v, wlArray); } if(d->conflict) return(0); /** implication on AIG **/ fan = (long *)SATfanout(v); size = SATnFanout(v); for(i=0; i> 1; cur = SATnormalNode(cur); left = SATleftChild(cur); right = SATrightChild(cur); value = SATgetValue(left, right, cur); (satImplicationFN[value])(cm, d, cur, left, right); if(d->conflict) return(0); } left = SATleftChild(v); right = SATrightChild(v); value = SATgetValue(left, right, v); (satImplicationFN[value])(cm, d, v, left, right); if(d->conflict) return(0); return(1); } /**Function******************************************************************** Synopsis [Apply implication until the implication queue is empty. ] Description [ Apply implication until the implication queue is empty. Since the node can be part of AIG and CNF and BDD, the implications on three representation are applied] SideEffects [] SeeAlso [] ******************************************************************************/ void sat_ImplicationMain( satManager_t *cm, satLevel_t *d) { satQueue_t *Q, *BDDQ; long v; Q = cm->queue; BDDQ = cm->BDDQueue; while(1) { v = sat_Dequeue(Q); while(v && d->conflict == 0) { sat_ImplyNode(cm, d, v); SATflags(v) &= ResetInQueueMask; v = sat_Dequeue(Q); } if(d->conflict) break; if(cm->option->BDDImplication) { v = sat_Dequeue(Q); while(v && d->conflict == 0) { sat_ImplyBDD(cm, d, v); SATflags(v) &= ResetInQueueMask; v = sat_Dequeue(Q); } } if(Q->size == 0 && BDDQ->size == 0) break; } sat_CleanImplicationQueue(cm); cm->implicatedSoFar += d->implied->num; } /**Function******************************************************************** Synopsis [Clean implication queue. ] Description [Clean implication queue. ] SideEffects [] SeeAlso [] ******************************************************************************/ void sat_CleanImplicationQueue( satManager_t *cm) { satQueue_t *Q; int i; bAigEdge_t v; Q = cm->queue; if(Q->size <=0) return; //Bing: important, can't be zero, since some var's value,which are now in //implication queue will be erased. This may lead to not being able to //identify conflict if(cm->option->AbRf || cm->option->IP || cm->option->arosat){ if(Q->front <= Q->rear) { for(i=Q->front; i<=Q->rear; i++) { v = Q->array[i]; SATflags(v) &= ResetInQueueMask; } } else { for(i=Q->front; imax; i++) { v = Q->array[i]; SATflags(v) &= ResetInQueueMask; } for(i=0; irear; i++) { v = Q->array[i]; SATflags(v) &= ResetInQueueMask; } } } #if 0 if(Q->front <= Q->rear) { for(i=Q->front; i<=Q->rear; i++) { v = Q->array[i]; SATflags(v) &= ResetInQueueMask; SATante(v) = 0; SATante2(v) = 0; SATvalue(v) = 2; } } else { for(i=Q->front; imax; i++) { v = Q->array[i]; SATflags(v) &= ResetInQueueMask; SATante(v) = 0; SATante2(v) = 0; SATvalue(v) = 2; } for(i=0; irear; i++) { v = Q->array[i]; SATflags(v) &= ResetInQueueMask; SATante(v) = 0; SATante2(v) = 0; SATvalue(v) = 2; } } #endif Q->size = 0; Q->front = 1; Q->rear = 0; } /**Function******************************************************************** Synopsis [Add nodes in array into implication queue. ] Description [Add nodes in array into implication queue. ] SideEffects [] SeeAlso [] ******************************************************************************/ void sat_ImplyArray( satManager_t *cm, satLevel_t *d, satArray_t *arr) { int i, size; long v; int inverted, value; satQueue_t *Q; if(arr == 0) return; if(cm->status)return; size = arr->num; Q = cm->queue; for(i=0; ispace[i]; inverted = SATisInverted(v); v = SATnormalNode(v); value = !inverted; if(SATvalue(v) < 2) { if(SATvalue(v) == value) continue; else { cm->status = SAT_UNSAT; d->conflict = v; //Bing: return; } } SATvalue(v) = value; SATmakeImplied(v, d); //Bing: cm->each->nCNFImplications++; if(cm->option->coreGeneration && cm->option->IP){ st_insert(cm->anteTable,(char *)SATnormalNode(v),(char *)SATnormalNode(v)); } if((SATflags(v) & InQueueMask) == 0) { sat_Enqueue(Q, v); SATflags(v) |= InQueueMask; } } } /**Function******************************************************************** Synopsis [Apply implication on BDD node. ] Description [Apply implication on BDD node. ] SideEffects [] SeeAlso [] ******************************************************************************/ void sat_ImplyBDD( satManager_t *cm, satLevel_t *d, long v) { /** CONSIDER ... **/ } /**Function******************************************************************** Synopsis [Build level zero hyper implication graph. ] Description [Build level zero hyper implication graph. ] SideEffects [] SeeAlso [] ******************************************************************************/ void sat_BuildLevelZeroHyperImplicationGraph( satManager_t *cm) { /** CONSIDER... **/ }