luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
abc/src/aig/gia/giaAbsVta.c

1795 lines
60 KiB
C
Raw Blame History

/**CFile****************************************************************
FileName [giaAbsVta.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [Variable time-frame abstraction.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaAbsVta.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "sat/bsat/satSolver2.h"
#include "base/main/main.h"
ABC_NAMESPACE_IMPL_START
#define VTA_LARGE 0xFFFFFFF
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Vta_Obj_t_ Vta_Obj_t; // object
struct Vta_Obj_t_
{
int iObj;
int iFrame;
int iNext;
unsigned Prio : 28; // related to VTA_LARGE
unsigned Value : 2;
unsigned fAdded : 1;
unsigned fVisit : 1;
};
typedef struct Vta_Man_t_ Vta_Man_t; // manager
struct Vta_Man_t_
{
// user data
Gia_Man_t * pGia; // AIG manager
Gia_ParVta_t* pPars; // parameters
// internal data
int nObjs; // the number of objects
int nObjsAlloc; // the number of objects allocated
int nBins; // number of hash table entries
int * pBins; // hash table bins
Vta_Obj_t * pObjs; // storage for objects
Vec_Int_t * vOrder; // objects in DPS order
// abstraction
int nObjBits; // the number of bits to represent objects
unsigned nObjMask; // object mask
Vec_Ptr_t * vFrames; // start abstraction for each frame
int nWords; // the number of words in the record
int nCexes; // the number of CEXes
int nObjAdded; // objects added to the abstraction
Vec_Int_t * vSeens; // seen objects
Vec_Bit_t * vSeenGla; // seen objects in all frames
int nSeenGla; // seen objects in all frames
int nSeenAll; // seen objects in all frames
// other data
Vec_Ptr_t * vCores; // unsat core for each frame
sat_solver2 * pSat; // incremental SAT solver
Vec_Int_t * vAddedNew; // the IDs of variables added to the solver
// statistics
clock_t timeSat;
clock_t timeUnsat;
clock_t timeCex;
clock_t timeOther;
};
// ternary simulation
#define VTA_VAR0 1
#define VTA_VAR1 2
#define VTA_VARX 3
static inline int Vta_ValIs0( Vta_Obj_t * pThis, int fCompl )
{
if ( pThis->Value == VTA_VAR1 && fCompl )
return 1;
if ( pThis->Value == VTA_VAR0 && !fCompl )
return 1;
return 0;
}
static inline int Vta_ValIs1( Vta_Obj_t * pThis, int fCompl )
{
if ( pThis->Value == VTA_VAR0 && fCompl )
return 1;
if ( pThis->Value == VTA_VAR1 && !fCompl )
return 1;
return 0;
}
static inline Vta_Obj_t * Vta_ManObj( Vta_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; }
static inline int Vta_ObjId( Vta_Man_t * p, Vta_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; }
#define Vta_ManForEachObj( p, pObj, i ) \
for ( i = 1; (i < p->nObjs) && ((pObj) = Vta_ManObj(p, i)); i++ )
#define Vta_ManForEachObjObj( p, pObjVta, pObjGia, i ) \
for ( i = 1; (i < p->nObjs) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )
#define Vta_ManForEachObjObjReverse( p, pObjVta, pObjGia, i ) \
for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )
#define Vta_ManForEachObjVec( vVec, p, pObj, i ) \
for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i++ )
#define Vta_ManForEachObjVecReverse( vVec, p, pObj, i ) \
for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i-- )
#define Vta_ManForEachObjObjVec( vVec, p, pObj, pObjG, i ) \
for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i++ )
#define Vta_ManForEachObjObjVecReverse( vVec, p, pObj, pObjG, i ) \
for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i-- )
// abstraction is given as an array of integers:
// - the first entry is the number of timeframes (F)
// - the next (F+1) entries give the beginning position of each timeframe
// - the following entries give the object IDs
// invariant: assert( vec[vec[0]+1] == size(vec) );
extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [This procedure sets default parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
{
memset( p, 0, sizeof(Gia_ParVta_t) );
p->nFramesMax = 0; // maximum frames
p->nFramesStart = 0; // starting frame
p->nFramesPast = 4; // overlap frames
p->nConfLimit = 0; // conflict limit
p->nLearnedMax = 1000; // max number of learned clauses
p->nLearnedStart = 1000; // max number of learned clauses
p->nLearnedDelta = 200; // max number of learned clauses
p->nLearnedPerce = 70; // max number of learned clauses
p->nTimeOut = 0; // timeout in seconds
p->nRatioMin = 20; // stop when less than this % of object is abstracted
p->nRatioMax = 30; // restart when more than this % of object is abstracted
p->fUseTermVars = 0; // use terminal variables
p->fUseRollback = 0; // use rollback to the starting number of frames
p->fPropFanout = 1; // propagate fanouts during refinement
p->fVerbose = 0; // verbose flag
p->iFrame = -1; // the number of frames covered
}
/**Function*************************************************************
Synopsis [Converting from one array to per-frame arrays.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Gia_VtaAbsToFrames( Vec_Int_t * vAbs )
{
Vec_Ptr_t * vFrames;
Vec_Int_t * vFrame;
int i, k, Entry, iStart, iStop = -1;
int nFrames = Vec_IntEntry( vAbs, 0 );
assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) );
vFrames = Vec_PtrAlloc( nFrames );
for ( i = 0; i < nFrames; i++ )
{
iStart = Vec_IntEntry( vAbs, i+1 );
iStop = Vec_IntEntry( vAbs, i+2 );
vFrame = Vec_IntAlloc( iStop - iStart );
Vec_IntForEachEntryStartStop( vAbs, Entry, k, iStart, iStop )
Vec_IntPush( vFrame, Entry );
Vec_PtrPush( vFrames, vFrame );
}
assert( iStop == Vec_IntSize(vAbs) );
return vFrames;
}
/**Function*************************************************************
Synopsis [Converting from per-frame arrays to one integer array.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_VtaFramesToAbs( Vec_Vec_t * vFrames )
{
Vec_Int_t * vOne, * vAbs;
int i, k, Entry, nSize;
vAbs = Vec_IntAlloc( 2 + Vec_VecSize(vFrames) + Vec_VecSizeSize(vFrames) );
Vec_IntPush( vAbs, Vec_VecSize(vFrames) );
nSize = Vec_VecSize(vFrames) + 2;
Vec_VecForEachLevelInt( vFrames, vOne, i )
{
Vec_IntPush( vAbs, nSize );
nSize += Vec_IntSize( vOne );
}
Vec_IntPush( vAbs, nSize );
assert( Vec_IntSize(vAbs) == Vec_VecSize(vFrames) + 2 );
Vec_VecForEachLevelInt( vFrames, vOne, i )
Vec_IntForEachEntry( vOne, Entry, k )
Vec_IntPush( vAbs, Entry );
assert( Vec_IntEntry(vAbs, Vec_IntEntry(vAbs,0)+1) == Vec_IntSize(vAbs) );
return vAbs;
}
/**Function*************************************************************
Synopsis [Detects how many frames are completed.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Int_t * Vta_ManDeriveAbsAll( Vec_Int_t * p, int nWords )
{
Vec_Int_t * vRes;
unsigned * pThis;
int i, w, nObjs = Vec_IntSize(p) / nWords;
assert( Vec_IntSize(p) % nWords == 0 );
vRes = Vec_IntAlloc( nObjs );
for ( i = 0; i < nObjs; i++ )
{
pThis = (unsigned *)Vec_IntEntryP( p, nWords * i );
for ( w = 0; w < nWords; w++ )
if ( pThis[w] )
break;
Vec_IntPush( vRes, (int)(w < nWords) );
}
return vRes;
}
/**Function*************************************************************
Synopsis [Collect nodes/flops involved in different timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Vec_IntDoubleWidth( Vec_Int_t * p, int nWords )
{
int * pArray = ABC_CALLOC( int, Vec_IntSize(p) * 2 );
int i, w, nObjs = Vec_IntSize(p) / nWords;
assert( Vec_IntSize(p) % nWords == 0 );
for ( i = 0; i < nObjs; i++ )
for ( w = 0; w < nWords; w++ )
pArray[2 * nWords * i + w] = p->pArray[nWords * i + w];
ABC_FREE( p->pArray );
p->pArray = pArray;
p->nSize *= 2;
p->nCap = p->nSize;
return 2 * nWords;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vga_ManHash( int iObj, int iFrame, int nBins )
{
return ((unsigned)((iObj + iFrame)*(iObj + iFrame + 1))) % nBins;
}
static inline int * Vga_ManLookup( Vta_Man_t * p, int iObj, int iFrame )
{
Vta_Obj_t * pThis;
int * pPlace = p->pBins + Vga_ManHash( iObj, iFrame, p->nBins );
for ( pThis = Vta_ManObj(p, *pPlace);
pThis; pPlace = &pThis->iNext,
pThis = Vta_ManObj(p, *pPlace) )
if ( pThis->iObj == iObj && pThis->iFrame == iFrame )
break;
return pPlace;
}
static inline Vta_Obj_t * Vga_ManFind( Vta_Man_t * p, int iObj, int iFrame )
{
int * pPlace = Vga_ManLookup( p, iObj, iFrame );
return Vta_ManObj(p, *pPlace);
}
static inline Vta_Obj_t * Vga_ManFindOrAdd( Vta_Man_t * p, int iObj, int iFrame )
{
Vta_Obj_t * pThis;
int i, * pPlace;
assert( iObj >= 0 && iFrame >= -1 );
if ( p->nObjs == p->nObjsAlloc )
{
// resize objects
p->pObjs = ABC_REALLOC( Vta_Obj_t, p->pObjs, 2 * p->nObjsAlloc );
memset( p->pObjs + p->nObjsAlloc, 0, p->nObjsAlloc * sizeof(Vta_Obj_t) );
p->nObjsAlloc *= 2;
// rehash entries in the table
ABC_FREE( p->pBins );
p->nBins = Abc_PrimeCudd( 2 * p->nBins );
p->pBins = ABC_CALLOC( int, p->nBins );
Vta_ManForEachObj( p, pThis, i )
{
pThis->iNext = 0;
pPlace = Vga_ManLookup( p, pThis->iObj, pThis->iFrame );
assert( *pPlace == 0 );
*pPlace = i;
}
}
pPlace = Vga_ManLookup( p, iObj, iFrame );
if ( *pPlace )
return Vta_ManObj(p, *pPlace);
*pPlace = p->nObjs++;
pThis = Vta_ManObj(p, *pPlace);
pThis->iObj = iObj;
pThis->iFrame = iFrame;
return pThis;
}
static inline void Vga_ManDelete( Vta_Man_t * p, int iObj, int iFrame )
{
int * pPlace = Vga_ManLookup( p, iObj, iFrame );
Vta_Obj_t * pThis = Vta_ManObj(p, *pPlace);
assert( pThis != NULL );
*pPlace = pThis->iNext;
pThis->iNext = -1;
}
/**Function*************************************************************
Synopsis [Derives counter-example using current assignments.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Vga_ManDeriveCex( Vta_Man_t * p )
{
Abc_Cex_t * pCex;
Vta_Obj_t * pThis;
Gia_Obj_t * pObj;
int i;
pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
pCex->iPo = 0;
pCex->iFrame = p->pPars->iFrame;
Vta_ManForEachObjObj( p, pThis, pObj, i )
if ( Gia_ObjIsPi(p->pGia, pObj) && sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) )
Abc_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
return pCex;
}
/**Function*************************************************************
Synopsis [Remaps core into frame/node pairs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Vta_ManUnsatCoreRemap( Vta_Man_t * p, Vec_Int_t * vCore )
{
Vta_Obj_t * pThis;
int i, Entry;
Vec_IntForEachEntry( vCore, Entry, i )
{
pThis = Vta_ManObj( p, Entry );
Entry = (pThis->iFrame << p->nObjBits) | pThis->iObj;
Vec_IntWriteEntry( vCore, i, Entry );
}
}
/**Function*************************************************************
Synopsis [Compares two objects by their distance.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Vta_ManComputeDepthIncrease( Vta_Obj_t ** pp1, Vta_Obj_t ** pp2 )
{
int Diff = (*pp1)->Prio - (*pp2)->Prio;
if ( Diff < 0 )
return -1;
if ( Diff > 0 )
return 1;
Diff = (*pp1) - (*pp2);
if ( Diff < 0 )
return -1;
if ( Diff > 0 )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Returns 1 if the object is already used.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Vta_ManObjIsUsed( Vta_Man_t * p, int iObj )
{
int i;
unsigned * pInfo = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj );
for ( i = 0; i < p->nWords; i++ )
if ( pInfo[i] )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Finds predecessors of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vta_ObjPreds( Vta_Man_t * p, Vta_Obj_t * pThis, Gia_Obj_t * pObj, Vta_Obj_t ** ppThis0, Vta_Obj_t ** ppThis1 )
{
*ppThis0 = NULL;
*ppThis1 = NULL;
// if ( !pThis->fAdded )
// return;
assert( !Gia_ObjIsPi(p->pGia, pObj) );
if ( Gia_ObjIsConst0(pObj) || (Gia_ObjIsCi(pObj) && pThis->iFrame == 0) )
return;
if ( Gia_ObjIsAnd(pObj) )
{
*ppThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
*ppThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
// assert( *ppThis0 && *ppThis1 );
return;
}
assert( Gia_ObjIsRo(p->pGia, pObj) && pThis->iFrame > 0 );
pObj = Gia_ObjRoToRi( p->pGia, pObj );
*ppThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
// assert( *ppThis0 );
}
/**Function*************************************************************
Synopsis [Collect const/PI/RO/AND in a topological order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Vta_ManCollectNodes_rec( Vta_Man_t * p, Vta_Obj_t * pThis, Vec_Int_t * vOrder )
{
Gia_Obj_t * pObj;
Vta_Obj_t * pThis0, * pThis1;
if ( pThis->fVisit )
return;
pThis->fVisit = 1;
pObj = Gia_ManObj( p->pGia, pThis->iObj );
if ( pThis->fAdded )
{
Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
if ( pThis0 ) Vta_ManCollectNodes_rec( p, pThis0, vOrder );
if ( pThis1 ) Vta_ManCollectNodes_rec( p, pThis1, vOrder );
}
Vec_IntPush( vOrder, Vta_ObjId(p, pThis) );
}
Vec_Int_t * Vta_ManCollectNodes( Vta_Man_t * p, int f )
{
Vta_Obj_t * pThis;
Gia_Obj_t * pObj;
Vec_IntClear( p->vOrder );
pObj = Gia_ManPo( p->pGia, 0 );
pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
assert( pThis != NULL );
assert( !pThis->fVisit );
Vta_ManCollectNodes_rec( p, pThis, p->vOrder );
assert( pThis->fVisit );
return p->vOrder;
}
/**Function*************************************************************
Synopsis [Refines abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Vta_ManSatVerify( Vta_Man_t * p )
{
Vta_Obj_t * pThis, * pThis0, * pThis1;
Gia_Obj_t * pObj;
int i;
Vta_ManForEachObj( p, pThis, i )
pThis->Value = (sat_solver2_var_value(p->pSat, i) ? VTA_VAR1 : VTA_VAR0);
Vta_ManForEachObjObj( p, pThis, pObj, i )
{
if ( !pThis->fAdded )
continue;
Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
if ( Gia_ObjIsAnd(pObj) )
{
if ( pThis->Value == VTA_VAR1 )
assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
else if ( pThis->Value == VTA_VAR0 )
assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) );
else assert( 0 );
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
pObj = Gia_ObjRoToRi( p->pGia, pObj );
if ( pThis->iFrame == 0 )
assert( pThis->Value == VTA_VAR0 );
else if ( pThis->Value == VTA_VAR0 )
assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) );
else if ( pThis->Value == VTA_VAR1 )
assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) );
else assert( 0 );
}
}
}
/**Function*************************************************************
Synopsis [Refines abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Vta_ManProfileAddition( Vta_Man_t * p, Vec_Int_t * vTermsToAdd )
{
Vta_Obj_t * pThis;
Gia_Obj_t * pObj;
// profile the added ones
int i, * pCounters = ABC_CALLOC( int, p->pPars->iFrame+1 );
Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
pCounters[pThis->iFrame]++;
for ( i = 0; i <= p->pPars->iFrame; i++ )
Abc_Print( 1, "%2d", pCounters[i] );
Abc_Print( 1, "***\n" );
}
/**Function*************************************************************
Synopsis [Refines abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
{
int fVerify = 0;
Abc_Cex_t * pCex = NULL;
Vec_Int_t * vOrder, * vTermsToAdd;
Vec_Ptr_t * vTermsUsed, * vTermsUnused;
Vta_Obj_t * pThis, * pThis0, * pThis1, * pTop;
Gia_Obj_t * pObj;
int i, Counter;
if ( fVerify )
Vta_ManSatVerify( p );
// collect nodes in a topological order
vOrder = Vta_ManCollectNodes( p, f );
Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
{
pThis->Prio = VTA_LARGE;
pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
pThis->fVisit = 0;
}
// verify
if ( fVerify )
Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
{
if ( !pThis->fAdded )
continue;
Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
if ( Gia_ObjIsAnd(pObj) )
{
if ( pThis->Value == VTA_VAR1 )
assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
else if ( pThis->Value == VTA_VAR0 )
assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) );
else assert( 0 );
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
pObj = Gia_ObjRoToRi( p->pGia, pObj );
if ( pThis->iFrame == 0 )
assert( pThis->Value == VTA_VAR0 );
else if ( pThis->Value == VTA_VAR0 )
assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) );
else if ( pThis->Value == VTA_VAR1 )
assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) );
else assert( 0 );
}
}
// compute distance in reverse order
pThis = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
pThis->Prio = 1;
// collect used and unused terms
vTermsUsed = Vec_PtrAlloc( 1015 );
vTermsUnused = Vec_PtrAlloc( 1016 );
Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
{
// there is no unreachable states
assert( pThis->Prio < VTA_LARGE );
// skip constants and PIs
if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) )
{
pThis->Prio = 0; // set highest priority
continue;
}
// collect terminals
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
if ( !pThis->fAdded )
{
assert( pThis->Prio > 0 );
if ( Vta_ManObjIsUsed(p, pThis->iObj) )
Vec_PtrPush( vTermsUsed, pThis );
else
Vec_PtrPush( vTermsUnused, pThis );
continue;
}
// propagate
Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
if ( pThis0 )
pThis0->Prio = Abc_MinInt( pThis0->Prio, pThis->Prio + 1 );
if ( pThis1 )
pThis1->Prio = Abc_MinInt( pThis1->Prio, pThis->Prio + 1 );
}
/*
Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
if ( pThis->Prio > 0 )
pThis->Prio = 10;
*/
/*
// update priorities according to reconvergence counters
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
{
Vta_Obj_t * pThis0, * pThis1;
Gia_Obj_t * pObj = Gia_ManObj( p->pGia, pThis->iObj );
Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
pThis->Prio += 10000000;
if ( pThis0 )
pThis->Prio -= 1000000 * pThis0->fAdded;
if ( pThis1 )
pThis->Prio -= 1000000 * pThis1->fAdded;
}
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
{
Vta_Obj_t * pThis0, * pThis1;
Gia_Obj_t * pObj = Gia_ManObj( p->pGia, pThis->iObj );
Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
pThis->Prio += 10000000;
if ( pThis0 )
pThis->Prio -= 1000000 * pThis0->fAdded;
if ( pThis1 )
pThis->Prio -= 1000000 * pThis1->fAdded;
}
*/
// update priorities according to reconvergence counters
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
pThis->Prio = pThis->iObj;
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
pThis->Prio = pThis->iObj;
// objects with equal distance should receive priority based on number
// those objects whose prototypes have been added in other timeframes
// should have higher priority than the current object
Vec_PtrSort( vTermsUsed, (int (*)(void))Vta_ManComputeDepthIncrease );
Vec_PtrSort( vTermsUnused, (int (*)(void))Vta_ManComputeDepthIncrease );
if ( Vec_PtrSize(vTermsUsed) > 1 )
{
pThis0 = (Vta_Obj_t *)Vec_PtrEntry(vTermsUsed, 0);
pThis1 = (Vta_Obj_t *)Vec_PtrEntryLast(vTermsUsed);
assert( pThis0->Prio <= pThis1->Prio );
}
// assign the priority based on these orders
Counter = 1;
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
pThis->Prio = Counter++;
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
pThis->Prio = Counter++;
// Abc_Print( 1, "Used %d Unused %d\n", Vec_PtrSize(vTermsUsed), Vec_PtrSize(vTermsUnused) );
// propagate in the direct order
Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
{
assert( pThis->fVisit == 0 );
assert( pThis->Prio < VTA_LARGE );
// skip terminal objects
if ( !pThis->fAdded )
continue;
// assumes that values are assigned!!!
assert( pThis->Value != 0 );
// propagate
if ( Gia_ObjIsAnd(pObj) )
{
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
assert( pThis0 && pThis1 );
if ( pThis->Value == VTA_VAR1 )
{
assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
pThis->Prio = Abc_MaxInt( pThis0->Prio, pThis1->Prio );
}
else if ( pThis->Value == VTA_VAR0 )
{
if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
pThis->Prio = Abc_MinInt( pThis0->Prio, pThis1->Prio ); // choice!!!
else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
pThis->Prio = pThis0->Prio;
else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
pThis->Prio = pThis1->Prio;
else assert( 0 );
}
else assert( 0 );
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( pThis->iFrame > 0 )
{
pObj = Gia_ObjRoToRi( p->pGia, pObj );
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
assert( pThis0 );
pThis->Prio = pThis0->Prio;
}
else
pThis->Prio = 0;
}
else if ( Gia_ObjIsConst0(pObj) )
pThis->Prio = 0;
else
assert( 0 );
}
// select important values
pTop = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
pTop->fVisit = 1;
vTermsToAdd = Vec_IntAlloc( 100 );
Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
{
if ( !pThis->fVisit )
continue;
pThis->fVisit = 0;
assert( pThis->Prio >= 0 && pThis->Prio <= pTop->Prio );
// skip terminal objects
if ( !pThis->fAdded )
{
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) );
Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
continue;
}
// assumes that values are assigned!!!
assert( pThis->Value != 0 );
// propagate
if ( Gia_ObjIsAnd(pObj) )
{
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
assert( pThis0 && pThis1 );
if ( pThis->Value == VTA_VAR1 )
{
assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
assert( pThis0->Prio <= pThis->Prio );
assert( pThis1->Prio <= pThis->Prio );
pThis0->fVisit = 1;
pThis1->fVisit = 1;
}
else if ( pThis->Value == VTA_VAR0 )
{
if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
{
if ( pThis0->fVisit )
{
}
else if ( pThis1->fVisit )
{
}
else if ( pThis0->Prio <= pThis1->Prio ) // choice!!!
{
pThis0->fVisit = 1;
assert( pThis0->Prio == pThis->Prio );
}
else
{
pThis1->fVisit = 1;
assert( pThis1->Prio == pThis->Prio );
}
}
else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
{
pThis0->fVisit = 1;
assert( pThis0->Prio == pThis->Prio );
}
else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
{
pThis1->fVisit = 1;
assert( pThis1->Prio == pThis->Prio );
}
else assert( 0 );
}
else assert( 0 );
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( pThis->iFrame > 0 )
{
pObj = Gia_ObjRoToRi( p->pGia, pObj );
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
assert( pThis0 );
pThis0->fVisit = 1;
assert( pThis0->Prio == pThis->Prio );
}
}
else if ( !Gia_ObjIsConst0(pObj) )
assert( 0 );
}
if ( p->pPars->fAddLayer )
{
// mark those currently included
Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
{
assert( pThis->fVisit == 0 );
pThis->fVisit = 1;
}
// add used terms, which have close relationship
Counter = Vec_IntSize(vTermsToAdd);
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
{
if ( pThis->fVisit )
continue;
// Vta_ObjPreds( p, pThis, Gia_ManObj(p->pGia, pThis->iObj), &pThis0, &pThis1 );
// if ( (pThis0 && (pThis0->fAdded || pThis0->fVisit)) || (pThis1 && (pThis1->fAdded || pThis1->fVisit)) )
Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
}
// remove those currenty included
Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
pThis->fVisit = 0;
}
// printf( "\n%d -> %d\n", Counter, Vec_IntSize(vTermsToAdd) );
//Vec_IntReverseOrder( vTermsToAdd );
//Vec_IntSort( vTermsToAdd, 1 );
// cleanup
Vec_PtrFree( vTermsUsed );
Vec_PtrFree( vTermsUnused );
if ( fVerify )
{
// verify
Vta_ManForEachObjVec( vOrder, p, pThis, i )
pThis->Value = VTA_VARX;
Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
{
assert( !pThis->fAdded );
pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
}
// simulate
Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
{
assert( pThis->fVisit == 0 );
if ( !pThis->fAdded )
continue;
if ( Gia_ObjIsAnd(pObj) )
{
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
assert( pThis0 && pThis1 );
if ( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) )
pThis->Value = VTA_VAR1;
else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
pThis->Value = VTA_VAR0;
else
pThis->Value = VTA_VARX;
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( pThis->iFrame > 0 )
{
pObj = Gia_ObjRoToRi( p->pGia, pObj );
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
assert( pThis0 );
if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
pThis->Value = VTA_VAR0;
else if ( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) )
pThis->Value = VTA_VAR1;
else
pThis->Value = VTA_VARX;
}
else
{
pThis->Value = VTA_VAR0;
}
}
else if ( Gia_ObjIsConst0(pObj) )
{
pThis->Value = VTA_VAR0;
}
else assert( 0 );
// double check the solver
assert( pThis->Value == VTA_VARX || (int)pThis->Value == (sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0) );
}
// check the output
if ( !Vta_ValIs1(pTop, Gia_ObjFaninC0(Gia_ManPo(p->pGia, 0))) )
Abc_Print( 1, "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
// else
// Abc_Print( 1, "Verification OK.\n" );
}
// produce true counter-example
if ( pTop->Prio == 0 )
pCex = Vga_ManDeriveCex( p );
else
{
// Vta_ManProfileAddition( p, vTermsToAdd );
Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
if ( !Gia_ObjIsPi(p->pGia, pObj) )
Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
sat_solver2_simplify( p->pSat );
}
p->nObjAdded += Vec_IntSize(vTermsToAdd);
Vec_IntFree( vTermsToAdd );
return pCex;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
{
Vta_Man_t * p;
p = ABC_CALLOC( Vta_Man_t, 1 );
p->pGia = pGia;
p->pPars = pPars;
// internal data
p->nObjsAlloc = (1 << 18);
p->pObjs = ABC_CALLOC( Vta_Obj_t, p->nObjsAlloc );
p->nObjs = 1;
p->nBins = Abc_PrimeCudd( 2*p->nObjsAlloc );
p->pBins = ABC_CALLOC( int, p->nBins );
p->vOrder = Vec_IntAlloc( 1013 );
// abstraction
p->nObjBits = Abc_Base2Log( Gia_ManObjNum(pGia) );
p->nObjMask = (1 << p->nObjBits) - 1;
assert( Gia_ManObjNum(pGia) <= (int)p->nObjMask );
p->nWords = 1;
p->vSeens = Vec_IntStart( Gia_ManObjNum(pGia) * p->nWords );
p->vSeenGla = Vec_BitStart( Gia_ManObjNum(pGia) );
p->nSeenGla = 1;
p->nSeenAll = 1;
// other data
p->vCores = Vec_PtrAlloc( 100 );
p->pSat = sat_solver2_new();
p->pSat->pPrf1 = Vec_SetAlloc( 20 );
// p->pSat->fVerbose = p->pPars->fVerbose;
// sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax );
p->pSat->nLearntStart = p->pPars->nLearnedStart;
p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
p->pSat->nLearntMax = p->pSat->nLearntStart;
// start the abstraction
assert( pGia->vObjClasses != NULL );
p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses );
p->vAddedNew = Vec_IntAlloc( 1000 );
return p;
}
/**Function*************************************************************
Synopsis [Delete manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Vga_ManStop( Vta_Man_t * p )
{
if ( p->pPars->fVerbose )
Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d Objs+ = %d\n",
sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat),
sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
Vec_VecFreeP( (Vec_Vec_t **)&p->vCores );
Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames );
Vec_BitFreeP( &p->vSeenGla );
Vec_IntFreeP( &p->vSeens );
Vec_IntFreeP( &p->vOrder );
Vec_IntFreeP( &p->vAddedNew );
sat_solver2_delete( p->pSat );
ABC_FREE( p->pBins );
ABC_FREE( p->pObjs );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Returns the output literal.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f )
{
Gia_Obj_t * pObj = Gia_ManPo(p->pGia, 0);
Vta_Obj_t * pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
assert( pThis != NULL && pThis->fAdded );
if ( f == 0 && Gia_ObjIsRo(p->pGia, Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj) )
return -Vta_ObjId(p, pThis);
return Abc_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) );
}
/**Function*************************************************************
Synopsis [Finds the set of clauses involved in the UNSAT core.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Vta_ManUnsatCore( int iLit, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls )
{
clock_t clk = clock();
Vec_Int_t * vCore;
int RetValue, nConfPrev = pSat->stats.conflicts;
if ( piRetValue )
*piRetValue = 1;
// consider special case when PO points to the flop
// this leads to immediate conflict in the first timeframe
if ( iLit < 0 )
{
vCore = Vec_IntAlloc( 1 );
Vec_IntPush( vCore, -iLit );
return vCore;
}
// solve the problem
RetValue = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( pnConfls )
*pnConfls = (int)pSat->stats.conflicts - nConfPrev;
if ( RetValue == l_Undef )
{
if ( piRetValue )
*piRetValue = -1;
return NULL;
}
if ( RetValue == l_True )
{
if ( piRetValue )
*piRetValue = 0;
return NULL;
}
if ( fVerbose )
{
// Abc_Print( 1, "%6d", (int)pSat->stats.conflicts - nConfPrev );
// Abc_Print( 1, "UNSAT after %7d conflicts. ", pSat->stats.conflicts );
// Abc_PrintTime( 1, "Time", clock() - clk );
}
assert( RetValue == l_False );
// derive the UNSAT core
clk = clock();
vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
if ( fVerbose )
{
// Abc_Print( 1, "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
// Abc_PrintTime( 1, "Time", clock() - clk );
}
return vCore;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nConfls, int nCexes, clock_t Time, int fVerbose )
{
unsigned * pInfo;
int * pCountAll = NULL, * pCountUni = NULL;
int i, iFrame, iObj, Entry, fChanges = 0;
// print info about frames
if ( vCore )
{
pCountAll = ABC_CALLOC( int, nFrames + 1 );
pCountUni = ABC_CALLOC( int, nFrames + 1 );
Vec_IntForEachEntry( vCore, Entry, i )
{
iObj = (Entry & p->nObjMask);
iFrame = (Entry >> p->nObjBits);
assert( iFrame < nFrames );
pInfo = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj );
if ( !Abc_InfoHasBit(pInfo, iFrame) )
{
Abc_InfoSetBit( pInfo, iFrame );
pCountUni[iFrame+1]++;
pCountUni[0]++;
p->nSeenAll++;
}
pCountAll[iFrame+1]++;
pCountAll[0]++;
if ( !Vec_BitEntry(p->vSeenGla, iObj) )
{
Vec_BitWriteEntry(p->vSeenGla, iObj, 1);
p->nSeenGla++;
fChanges = 1;
}
}
}
if ( !fVerbose )
{
ABC_FREE( pCountAll );
ABC_FREE( pCountUni );
return fChanges;
}
if ( Abc_FrameIsBatchMode() && !vCore )
return fChanges;
// Abc_Print( 1, "%5d%5d", pCountAll[0], pCountUni[0] );
Abc_Print( 1, "%4d :", nFrames-1 );
Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenGla / (Gia_ManRegNum(p->pGia) + Gia_ManAndNum(p->pGia) + 1)) );
Abc_Print( 1, "%6d", p->nSeenGla );
Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenAll / (p->nSeenGla * nFrames)) );
Abc_Print( 1, "%8d", nConfls );
if ( nCexes == 0 )
Abc_Print( 1, "%5c", '-' );
else
Abc_Print( 1, "%5d", nCexes );
// Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) );
Abc_PrintInt( sat_solver2_nvars(p->pSat) );
Abc_PrintInt( sat_solver2_nclauses(p->pSat) );
Abc_PrintInt( sat_solver2_nlearnts(p->pSat) );
if ( vCore == NULL )
{
Abc_Print( 1, " ..." );
// for ( k = 0; k < 7; k++ )
// Abc_Print( 1, " " );
Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
Abc_Print( 1, "\r" );
}
else
{
Abc_PrintInt( pCountAll[0] );
/*
if ( nFrames > 7 )
{
for ( k = 0; k < 3; k++ )
Abc_Print( 1, "%5d", pCountAll[k+1] );
Abc_Print( 1, " ..." );
for ( k = nFrames-3; k < nFrames; k++ )
Abc_Print( 1, "%5d", pCountAll[k+1] );
}
else
{
for ( k = 0; k < nFrames; k++ )
Abc_Print( 1, "%5d", pCountAll[k+1] );
for ( k = nFrames; k < 7; k++ )
Abc_Print( 1, " " );
}
*/
Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
Abc_Print( 1, "\n" );
}
fflush( stdout );
if ( vCore )
{
ABC_FREE( pCountAll );
ABC_FREE( pCountUni );
}
return fChanges;
}
/**Function*************************************************************
Synopsis [Adds clauses to the solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame )
{
Vta_Obj_t * pThis0, * pThis1;
Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
Vta_Obj_t * pThis = Vga_ManFindOrAdd( p, iObj, iFrame );
int iThis0, iMainVar = Vta_ObjId(p, pThis);
assert( pThis->iObj == iObj && pThis->iFrame == iFrame );
if ( pThis->fAdded )
return;
pThis->fAdded = 1;
Vec_IntPush( p->vAddedNew, iMainVar );
if ( Gia_ObjIsAnd(pObj) )
{
pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame );
iThis0 = Vta_ObjId(p, pThis0);
pThis1 = Vga_ManFindOrAdd( p, Gia_ObjFaninId1p(p->pGia, pObj), iFrame );
sat_solver2_add_and( p->pSat, iMainVar, iThis0, Vta_ObjId(p, pThis1),
Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0, iMainVar );
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( iFrame == 0 )
{
if ( p->pPars->fUseTermVars )
{
pThis0 = Vga_ManFindOrAdd( p, iObj, -1 );
sat_solver2_add_constraint( p->pSat, iMainVar, Vta_ObjId(p, pThis0), 1, 0, iMainVar );
}
else
{
sat_solver2_add_const( p->pSat, iMainVar, 1, 0, iMainVar );
}
}
else
{
pObj = Gia_ObjRoToRi( p->pGia, pObj );
pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame-1 );
sat_solver2_add_buffer( p->pSat, iMainVar, Vta_ObjId(p, pThis0), Gia_ObjFaninC0(pObj), 0, iMainVar );
}
}
else if ( Gia_ObjIsConst0(pObj) )
{
sat_solver2_add_const( p->pSat, iMainVar, 1, 0, iMainVar );
}
else //if ( !Gia_ObjIsPi(p->pGia, pObj) )
assert( 0 );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift )
{
int i, Entry;
Vec_IntForEachEntry( vOne, Entry, i )
Vga_ManAddClausesOne( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift );
sat_solver2_simplify( p->pSat );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Vga_ManPrintCore( Vta_Man_t * p, Vec_Int_t * vCore, int Lift )
{
int i, Entry, iObj, iFrame;
Vec_IntForEachEntry( vCore, Entry, i )
{
iObj = (Entry & p->nObjMask);
iFrame = (Entry >> p->nObjBits);
Abc_Print( 1, "%d*%d ", iObj, iFrame+Lift );
}
Abc_Print( 1, "\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Vga_ManRollBack( Vta_Man_t * p, int nObjOld )
{
Vta_Obj_t * pThis = p->pObjs + nObjOld;
Vta_Obj_t * pLimit = p->pObjs + p->nObjs;
int i, Entry;
for ( ; pThis < pLimit; pThis++ )
Vga_ManDelete( p, pThis->iObj, pThis->iFrame );
memset( p->pObjs + nObjOld, 0, sizeof(Vta_Obj_t) * (p->nObjs - nObjOld) );
p->nObjs = nObjOld;
Vec_IntForEachEntry( p->vAddedNew, Entry, i )
if ( Entry < p->nObjs )
{
pThis = Vta_ManObj(p, Entry);
assert( pThis->fAdded == 1 );
pThis->fAdded = 0;
}
}
/**Function*************************************************************
Synopsis [Send abstracted model or send cancel.]
Description [Counter-example will be sent automatically when &vta terminates.]
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_VtaSendAbsracted( Vta_Man_t * p, int fVerbose )
{
extern int Gia_ManToBridgeAbsNetlist( FILE * pFile, Gia_Man_t * p );
Gia_Man_t * pAbs;
assert( Abc_FrameIsBridgeMode() );
// if ( fVerbose )
// Abc_Print( 1, "Sending abstracted model...\n" );
// create obj classes
Vec_IntFreeP( &p->pGia->vObjClasses );
p->pGia->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
// create gate classes
Vec_IntFreeP( &p->pGia->vGateClasses );
p->pGia->vGateClasses = Gia_VtaConvertToGla( p->pGia, p->pGia->vObjClasses );
Vec_IntFreeP( &p->pGia->vObjClasses );
// create abstrated model
pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
Vec_IntFreeP( &p->pGia->vGateClasses );
// send it out
Gia_ManToBridgeAbsNetlist( stdout, pAbs );
Gia_ManStop( pAbs );
}
void Gia_VtaSendCancel( Vta_Man_t * p, int fVerbose )
{
extern int Gia_ManToBridgeBadAbs( FILE * pFile );
assert( Abc_FrameIsBridgeMode() );
// if ( fVerbose )
// Abc_Print( 1, "Cancelling previously sent model...\n" );
Gia_ManToBridgeBadAbs( stdout );
}
/**Function*************************************************************
Synopsis [Send abstracted model or send cancel.]
Description [Counter-example will be sent automatically when &vta terminates.]
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_VtaDumpAbsracted( Vta_Man_t * p, int fVerbose )
{
char * pFileNameDef = "vabs.aig";
char * pFileName = p->pPars->pFileVabs ? p->pPars->pFileVabs : pFileNameDef;
Gia_Man_t * pAbs;
if ( fVerbose )
Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
// create obj classes
Vec_IntFreeP( &p->pGia->vObjClasses );
p->pGia->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
// create gate classes
Vec_IntFreeP( &p->pGia->vGateClasses );
p->pGia->vGateClasses = Gia_VtaConvertToGla( p->pGia, p->pGia->vObjClasses );
Vec_IntFreeP( &p->pGia->vObjClasses );
// create abstrated model
pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
Vec_IntFreeP( &p->pGia->vGateClasses );
// send it out
Gia_WriteAiger( pAbs, pFileName, 0, 0 );
Gia_ManStop( pAbs );
}
/**Function*************************************************************
Synopsis [Print memory report.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_VtaPrintMemory( Vta_Man_t * p )
{
double memTot = 0;
double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t);
double memSat = sat_solver2_memory( p->pSat, 1 );
double memPro = sat_solver2_memory_proof( p->pSat );
double memMap = p->nObjsAlloc * sizeof(Vta_Obj_t) + p->nBins * sizeof(int);
double memOth = sizeof(Vta_Man_t);
memOth += Vec_IntCap(p->vOrder) * sizeof(int);
memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vFrames );
memOth += Vec_BitCap(p->vSeenGla) * sizeof(int);
memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCores );
memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
memTot = memAig + memSat + memPro + memMap + memOth;
ABC_PRMP( "Memory: AIG ", memAig, memTot );
ABC_PRMP( "Memory: SAT ", memSat, memTot );
ABC_PRMP( "Memory: Proof ", memPro, memTot );
ABC_PRMP( "Memory: Map ", memMap, memTot );
ABC_PRMP( "Memory: Other ", memOth, memTot );
ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
}
/**Function*************************************************************
Synopsis [Collect nodes/flops involved in different timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{
Vta_Man_t * p;
Vec_Int_t * vCore;
Abc_Cex_t * pCex = NULL;
int i, f, nConfls, Status, nObjOld, RetValue = -1, nCountNoChange = 0, fOneIsSent = 0;
clock_t clk = clock(), clk2;
// preconditions
assert( Gia_ManPoNum(pAig) == 1 );
assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) )
{
if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) )
{
printf( "Sequential miter is trivially UNSAT.\n" );
return 1;
}
ABC_FREE( pAig->pCexSeq );
pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 );
printf( "Sequential miter is trivially SAT.\n" );
return 0;
}
// compute intial abstraction
if ( pAig->vObjClasses == NULL )
{
pAig->vObjClasses = Vec_IntAlloc( 5 );
Vec_IntPush( pAig->vObjClasses, 1 );
Vec_IntPush( pAig->vObjClasses, 3 );
Vec_IntPush( pAig->vObjClasses, 4 );
Vec_IntPush( pAig->vObjClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) );
}
// start the manager
p = Vga_ManStart( pAig, pPars );
// set runtime limit
if ( p->pPars->nTimeOut )
sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + clock() );
// perform initial abstraction
if ( p->pPars->fVerbose )
{
Abc_Print( 1, "Running variable-timeframe abstraction (VTA) with the following parameters:\n" );
Abc_Print( 1, "FramePast = %d FrameMax = %d ConfMax = %d Timeout = %d RatioMin = %d %%\n",
pPars->nFramesPast, pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin );
Abc_Print( 1, "LearnStart = %d LearnDelta = %d LearnRatio = %d %%.\n",
pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce );
// Abc_Print( 1, "Frame %% Abs %% Confl Cex SatVar Core F0 F1 F2 ...\n" );
Abc_Print( 1, " Frame %% Abs %% Confl Cex Vars Clas Lrns Core Time Mem\n" );
}
assert( Vec_PtrSize(p->vFrames) > 0 );
for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
{
int nConflsBeg = sat_solver2_nconflicts(p->pSat);
p->pPars->iFrame = f;
// realloc storage for abstraction marks
if ( f == p->nWords * 32 )
p->nWords = Vec_IntDoubleWidth( p->vSeens, p->nWords );
// create bookmark to be used for rollback
nObjOld = p->nObjs;
sat_solver2_bookmark( p->pSat );
Vec_IntClear( p->vAddedNew );
// load new timeframe
Vga_ManAddClausesOne( p, 0, f );
if ( f < Vec_PtrSize(p->vFrames) )
Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
else
{
for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesPast, f); i++ )
Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
}
// iterate as long as there are counter-examples
for ( i = 0; ; i++ )
{
clk2 = clock();
vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
assert( (vCore != NULL) == (Status == 1) );
if ( Status == -1 ) // resource limit is reached
{
Vga_ManRollBack( p, nObjOld );
goto finish;
}
// check timeout
if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit )
{
Vga_ManRollBack( p, nObjOld );
goto finish;
}
if ( vCore != NULL )
{
p->timeUnsat += clock() - clk2;
break;
}
p->timeSat += clock() - clk2;
assert( Status == 0 );
p->nCexes++;
// perform the refinement
clk2 = clock();
pCex = Vta_ManRefineAbstraction( p, f );
p->timeCex += clock() - clk2;
if ( pCex != NULL )
goto finish;
// print the result (do not count it towards change)
Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk, p->pPars->fVerbose );
}
assert( Status == 1 );
// valid core is obtained
Vta_ManUnsatCoreRemap( p, vCore );
Vec_IntSort( vCore, 1 );
// update the SAT solver
sat_solver2_rollback( p->pSat );
// update storage
Vga_ManRollBack( p, nObjOld );
// load this timeframe
Vga_ManLoadSlice( p, vCore, 0 );
Vec_IntFree( vCore );
// run SAT solver
clk2 = clock();
vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
p->timeUnsat += clock() - clk2;
assert( (vCore != NULL) == (Status == 1) );
if ( Status == -1 ) // resource limit is reached
break;
if ( Status == 0 )
{
Vta_ManSatVerify( p );
// make sure, there was no initial abstraction (otherwise, it was invalid)
assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart );
pCex = Vga_ManDeriveCex( p );
break;
}
// add the core
Vta_ManUnsatCoreRemap( p, vCore );
// add in direct topological order
Vec_IntSort( vCore, 1 );
Vec_PtrPush( p->vCores, vCore );
// print the result
if ( Vta_ManAbsPrintFrame( p, vCore, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk, p->pPars->fVerbose ) )
{
// reset the counter of frames without change
nCountNoChange = 1;
p->pPars->nFramesNoChange = 0;
}
else if ( ++nCountNoChange == 2 ) // time to send
{
p->pPars->nFramesNoChange++;
if ( Abc_FrameIsBridgeMode() )
{
// cancel old one if it was sent
if ( fOneIsSent )
Gia_VtaSendCancel( p, pPars->fVerbose );
// send new one
Gia_VtaSendAbsracted( p, pPars->fVerbose );
fOneIsSent = 1;
}
}
// dump the model
if ( p->pPars->fDumpVabs && (f & 1) )
{
Abc_FrameSetCex( NULL );
Abc_FrameSetNFrames( f+1 );
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "write_status vta.status" );
Gia_VtaDumpAbsracted( p, pPars->fVerbose );
}
// check if the number of objects is below limit
if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )
{
Status = -1;
break;
}
}
finish:
// analize the results
if ( pCex == NULL )
{
if ( p->pPars->fVerbose && Status == -1 )
printf( "\n" );
if ( Vec_PtrSize(p->vCores) == 0 )
Abc_Print( 1, "Abstraction is not produced because first frame is not solved. " );
else
{
assert( Vec_PtrSize(p->vCores) > 0 );
// if ( pAig->vObjClasses != NULL )
// Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
Vec_IntFreeP( &pAig->vObjClasses );
pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
if ( Status == -1 )
{
if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit )
Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange );
else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, f, p->pPars->nFramesNoChange );
else if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )
Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f );
else
Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f );
}
else
{
p->pPars->iFrame++;
Abc_Print( 1, "Completed %d frames with a %d-stable abstraction. ", f, p->pPars->nFramesNoChange );
}
}
}
else
{
if ( p->pPars->fVerbose )
printf( "\n" );
ABC_FREE( p->pGia->pCexSeq );
p->pGia->pCexSeq = pCex;
if ( !Gia_ManVerifyCex( p->pGia, pCex, 0 ) )
Abc_Print( 1, " Gia_VtaPerform(): CEX verification has failed!\n" );
Abc_Print( 1, "Counter-example detected in frame %d. ", f );
p->pPars->iFrame = pCex->iFrame - 1;
Vec_IntFreeP( &pAig->vObjClasses );
RetValue = 0;
}
Abc_PrintTime( 1, "Time", clock() - clk );
if ( p->pPars->fVerbose )
{
p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex;
ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, clock() - clk );
ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, clock() - clk );
ABC_PRTP( "Runtime: Refinement ", p->timeCex, clock() - clk );
ABC_PRTP( "Runtime: Other ", p->timeOther, clock() - clk );
ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk );
Gia_VtaPrintMemory( p );
}
Vga_ManStop( p );
fflush( stdout );
return RetValue;
}
/**Function*************************************************************
Synopsis [Collect nodes/flops involved in different timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{
int RetValue = -1;
if ( pAig->vObjClasses == NULL && pPars->fUseRollback )
{
int nFramesMaxOld = pPars->nFramesMax;
pPars->nFramesMax = pPars->nFramesStart;
RetValue = Gia_VtaPerformInt( pAig, pPars );
pPars->nFramesMax = nFramesMaxOld;
}
if ( RetValue == 0 )
return RetValue;
return Gia_VtaPerformInt( pAig, pPars );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
Reference in New Issue View Git Blame Copy Permalink