diff options
Diffstat (limited to 'src/sat/pdr/pdrUtil.c')
| -rw-r--r-- | src/sat/pdr/pdrUtil.c | 719 |
1 files changed, 0 insertions, 719 deletions
diff --git a/src/sat/pdr/pdrUtil.c b/src/sat/pdr/pdrUtil.c deleted file mode 100644 index 1107aec7..00000000 --- a/src/sat/pdr/pdrUtil.c +++ /dev/null @@ -1,719 +0,0 @@ -/**CFile**************************************************************** - - FileName [pdrUtil.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Property driven reachability.] - - Synopsis [Various utilities.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - November 20, 2010.] - - Revision [$Id: pdrUtil.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "pdrInt.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Pdr_Set_t * Pdr_SetAlloc( int nSize ) -{ - Pdr_Set_t * p; - assert( nSize >= 0 && nSize < (1<<30) ); - p = (Pdr_Set_t *)ABC_CALLOC( char, sizeof(Pdr_Set_t) + nSize * sizeof(int) ); - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits ) -{ - Pdr_Set_t * p; - int i; - assert( Vec_IntSize(vLits) + Vec_IntSize(vPiLits) < (1<<30) ); - p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (Vec_IntSize(vLits) + Vec_IntSize(vPiLits)) * sizeof(int) ); - p->nLits = Vec_IntSize(vLits); - p->nTotal = Vec_IntSize(vLits) + Vec_IntSize(vPiLits); - p->nRefs = 1; - p->Sign = 0; - for ( i = 0; i < p->nLits; i++ ) - { - p->Lits[i] = Vec_IntEntry(vLits, i); - p->Sign |= ((word)1 << (p->Lits[i] % 63)); - } - Vec_IntSelectSort( p->Lits, p->nLits ); -/* - for ( i = 0; i < p->nLits; i++ ) - printf( "%d ", p->Lits[i] ); - printf( "\n" ); -*/ - // remember PI literals - for ( i = p->nLits; i < p->nTotal; i++ ) - p->Lits[i] = Vec_IntEntry(vPiLits, i-p->nLits); - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove ) -{ - Pdr_Set_t * p; - int i, k = 0; - assert( iRemove >= 0 && iRemove < pSet->nLits ); - p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (pSet->nTotal - 1) * sizeof(int) ); - p->nLits = pSet->nLits - 1; - p->nTotal = pSet->nTotal - 1; - p->nRefs = 1; - p->Sign = 0; - for ( i = 0; i < pSet->nTotal; i++ ) - { - if ( i == iRemove ) - continue; - p->Lits[k++] = pSet->Lits[i]; - if ( i >= pSet->nLits ) - continue; - p->Sign |= ((word)1 << (pSet->Lits[i] % 63)); - } - assert( k == p->nTotal ); - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits ) -{ - Pdr_Set_t * p; - int i, k = 0; - assert( nLits >= 0 && nLits <= pSet->nLits ); - p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (nLits + pSet->nTotal - pSet->nLits) * sizeof(int) ); - p->nLits = nLits; - p->nTotal = nLits + pSet->nTotal - pSet->nLits; - p->nRefs = 1; - p->Sign = 0; - for ( i = 0; i < nLits; i++ ) - { - assert( pLits[i] >= 0 ); - p->Lits[k++] = pLits[i]; - p->Sign |= ((word)1 << (pLits[i] % 63)); - } - Vec_IntSelectSort( p->Lits, p->nLits ); - for ( i = pSet->nLits; i < pSet->nTotal; i++ ) - p->Lits[k++] = pSet->Lits[i]; - assert( k == p->nTotal ); - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet ) -{ - Pdr_Set_t * p; - int i; - p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + pSet->nTotal * sizeof(int) ); - p->nLits = pSet->nLits; - p->nTotal = pSet->nTotal; - p->nRefs = 1; - p->Sign = pSet->Sign; - for ( i = 0; i < pSet->nTotal; i++ ) - p->Lits[i] = pSet->Lits[i]; - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Pdr_Set_t * Pdr_SetRef( Pdr_Set_t * p ) -{ - p->nRefs++; - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Pdr_SetDeref( Pdr_Set_t * p ) -{ - if ( --p->nRefs == 0 ) - ABC_FREE( p ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts ) -{ - char * pBuff; - int i, k, Entry; - pBuff = ABC_ALLOC( char, nRegs + 1 ); - for ( i = 0; i < nRegs; i++ ) - pBuff[i] = '-'; - pBuff[i] = 0; - for ( i = 0; i < p->nLits; i++ ) - { - if ( p->Lits[i] == -1 ) - continue; - pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1'); - } - if ( vFlopCounts ) - { - // skip some literals - k = 0; - Vec_IntForEachEntry( vFlopCounts, Entry, i ) - if ( Entry ) - pBuff[k++] = pBuff[i]; - pBuff[k] = 0; - } - fprintf( pFile, "%s", pBuff ); - ABC_FREE( pBuff ); -} - -/**Function************************************************************* - - Synopsis [Return 1 if pOld set-theoretically contains pNew.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew ) -{ - int * pOldInt, * pNewInt; - assert( pOld->nLits > 0 ); - assert( pNew->nLits > 0 ); - if ( pOld->nLits < pNew->nLits ) - return 0; - if ( (pOld->Sign & pNew->Sign) != pNew->Sign ) - return 0; - pOldInt = pOld->Lits + pOld->nLits - 1; - pNewInt = pNew->Lits + pNew->nLits - 1; - while ( pNew->Lits <= pNewInt ) - { - if ( pOld->Lits > pOldInt ) - return 0; - assert( *pNewInt != -1 ); - assert( *pOldInt != -1 ); - if ( *pNewInt == *pOldInt ) - pNewInt--, pOldInt--; - else if ( *pNewInt < *pOldInt ) - pOldInt--; - else - return 0; - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Return 1 if pOld set-theoretically contains pNew.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew ) -{ - int * pOldInt, * pNewInt; - assert( pOld->nLits > 0 ); - assert( pNew->nLits > 0 ); - pOldInt = pOld->Lits + pOld->nLits - 1; - pNewInt = pNew->Lits + pNew->nLits - 1; - while ( pNew->Lits <= pNewInt ) - { - assert( *pOldInt != -1 ); - if ( *pNewInt == -1 ) - { - pNewInt--; - continue; - } - if ( pOld->Lits > pOldInt ) - return 0; - assert( *pNewInt != -1 ); - assert( *pOldInt != -1 ); - if ( *pNewInt == *pOldInt ) - pNewInt--, pOldInt--; - else if ( *pNewInt < *pOldInt ) - pOldInt--; - else - return 0; - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Return 1 if the state cube contains init state (000...0).] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Pdr_SetIsInit( Pdr_Set_t * pCube, int iRemove ) -{ - int i; - for ( i = 0; i < pCube->nLits; i++ ) - { - assert( pCube->Lits[i] != -1 ); - if ( i == iRemove ) - continue; - if ( lit_sign( pCube->Lits[i] ) == 0 ) - return 0; - } - return 1; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 ) -{ - Pdr_Set_t * p1 = *pp1; - Pdr_Set_t * p2 = *pp2; - int i; - for ( i = 0; i < p1->nLits && i < p2->nLits; i++ ) - { - if ( p1->Lits[i] > p2->Lits[i] ) - return -1; - if ( p1->Lits[i] < p2->Lits[i] ) - return 1; - } - if ( i == p1->nLits && i < p2->nLits ) - return -1; - if ( i < p1->nLits && i == p2->nLits ) - return 1; - return 0; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext ) -{ - Pdr_Obl_t * p; - p = ABC_ALLOC( Pdr_Obl_t, 1 ); - p->iFrame = k; - p->prio = prio; - p->nRefs = 1; - p->pState = pState; - p->pNext = pNext; - p->pLink = NULL; - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p ) -{ - p->nRefs++; - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Pdr_OblDeref( Pdr_Obl_t * p ) -{ - if ( --p->nRefs == 0 ) - { - if ( p->pNext ) - Pdr_OblDeref( p->pNext ); - Pdr_SetDeref( p->pState ); - ABC_FREE( p ); - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Pdr_QueueIsEmpty( Pdr_Man_t * p ) -{ - return p->pQueue == NULL; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Pdr_Obl_t * Pdr_QueueHead( Pdr_Man_t * p ) -{ - return p->pQueue; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p ) -{ - Pdr_Obl_t * pRes = p->pQueue; - if ( p->pQueue == NULL ) - return NULL; - p->pQueue = p->pQueue->pLink; - Pdr_OblDeref( pRes ); - return pRes; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl ) -{ - Pdr_Obl_t * pTemp, ** ppPrev; - p->nObligs++; - Pdr_OblRef( pObl ); - if ( p->pQueue == NULL ) - { - p->pQueue = pObl; - return; - } - for ( ppPrev = &p->pQueue, pTemp = p->pQueue; pTemp; ppPrev = &pTemp->pLink, pTemp = pTemp->pLink ) - if ( pTemp->iFrame > pObl->iFrame || (pTemp->iFrame == pObl->iFrame && pTemp->prio > pObl->prio) ) - break; - *ppPrev = pObl; - pObl->pLink = pTemp; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Pdr_QueuePrint( Pdr_Man_t * p ) -{ - Pdr_Obl_t * pObl; - for ( pObl = p->pQueue; pObl; pObl = pObl->pLink ) - printf( "Frame = %2d. Prio = %8d.\n", pObl->iFrame, pObl->prio ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Pdr_QueueStop( Pdr_Man_t * p ) -{ - Pdr_Obl_t * pObl; - while ( !Pdr_QueueIsEmpty(p) ) - { - pObl = Pdr_QueuePop(p); - Pdr_OblDeref( pObl ); - } - p->pQueue = NULL; -} - - -#define PDR_VAL0 1 -#define PDR_VAL1 2 -#define PDR_VALX 3 - -/**Function************************************************************* - - Synopsis [Returns value (0 or 1) or X if unassigned.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Pdr_ObjSatValue( Aig_Man_t * pAig, Aig_Obj_t * pNode, int fCompl ) -{ - if ( Aig_ObjIsTravIdCurrent(pAig, pNode) ) - return (pNode->fMarkA ^ fCompl) ? PDR_VAL1 : PDR_VAL0; - return PDR_VALX; -} - -/**Function************************************************************* - - Synopsis [Recursively searched for a satisfying assignment.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pdr_Set_t * pCube, int Heur ) -{ - int Value0, Value1; - if ( Aig_ObjIsConst1(pNode) ) - return 1; - if ( Aig_ObjIsTravIdCurrent(pAig, pNode) ) - return ((int)pNode->fMarkA == Value); - Aig_ObjSetTravIdCurrent(pAig, pNode); - pNode->fMarkA = Value; - if ( Aig_ObjIsPi(pNode) ) - { -// if ( vSuppLits ) -// Vec_IntPush( vSuppLits, Aig_Var2Lit( Aig_ObjPioNum(pNode), !Value ) ); - if ( Saig_ObjIsLo(pAig, pNode) ) - { -// pCube->Lits[pCube->nLits++] = Aig_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), !Value ); - pCube->Lits[pCube->nLits++] = Aig_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), Value ); - pCube->Sign |= ((word)1 << (pCube->Lits[pCube->nLits-1] % 63)); - } - return 1; - } - assert( Aig_ObjIsNode(pNode) ); - // propagation - if ( Value ) - { - if ( !Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), !Aig_ObjFaninC0(pNode), pCube, Heur) ) - return 0; - return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), !Aig_ObjFaninC1(pNode), pCube, Heur); - } - // justification - Value0 = Pdr_ObjSatValue( pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode) ); - if ( Value0 == PDR_VAL0 ) - return 1; - Value1 = Pdr_ObjSatValue( pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode) ); - if ( Value1 == PDR_VAL0 ) - return 1; - if ( Value0 == PDR_VAL1 && Value1 == PDR_VAL1 ) - return 0; - if ( Value0 == PDR_VAL1 ) - return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), pCube, Heur); - if ( Value1 == PDR_VAL1 ) - return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), pCube, Heur); - assert( Value0 == PDR_VALX && Value1 == PDR_VALX ); - // decision making -// if ( rand() % 10 == Heur ) - if ( Aig_ObjId(pNode) % 4 == Heur ) - return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), pCube, Heur); - else - return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), pCube, Heur); -} - -/**Function************************************************************* - - Synopsis [Returns 1 if SAT assignment is found; 0 otherwise.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Pdr_ManCubeJust( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) -{ - Aig_Obj_t * pNode; - int i, v, fCompl; -// return 0; - for ( i = 0; i < 4; i++ ) - { - // derive new assignment - p->pCubeJust->nLits = 0; - p->pCubeJust->Sign = 0; - Aig_ManIncrementTravId( p->pAig ); - for ( v = 0; v < pCube->nLits; v++ ) - { - if ( pCube->Lits[v] == -1 ) - continue; - pNode = Saig_ManLi( p->pAig, lit_var(pCube->Lits[v]) ); - fCompl = lit_sign(pCube->Lits[v]) ^ Aig_ObjFaninC0(pNode); - if ( !Pdr_NtkFindSatAssign_rec( p->pAig, Aig_ObjFanin0(pNode), !fCompl, p->pCubeJust, i ) ) - break; - } - if ( v < pCube->nLits ) - continue; - // figure this out!!! - if ( p->pCubeJust->nLits == 0 ) - continue; - // successfully derived new assignment - Vec_IntSelectSort( p->pCubeJust->Lits, p->pCubeJust->nLits ); - // check assignment against this cube - if ( Pdr_SetContainsSimple( p->pCubeJust, pCube ) ) - continue; -//printf( "\n" ); -//Pdr_SetPrint( stdout, pCube, Saig_ManRegNum(p->pAig), NULL ); printf( "\n" ); -//Pdr_SetPrint( stdout, p->pCubeJust, Saig_ManRegNum(p->pAig), NULL ); printf( "\n" ); - // check assignment against the clauses - if ( Pdr_ManCheckContainment( p, k, p->pCubeJust ) ) - continue; - // find good assignment - return 1; - } - return 0; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |