Skip to content

A
abc
Commit 9cb52998 by Alan Mishchenko
Options

Other improvements to &vta and &gla.

parent bd4b2521
Showing with 738 additions and 80 deletions
src/aig/gia/gia.h
......@@ -515,6 +515,66 @@ static inline int Gia_XsimAndCond( int Value0, int fCompl0, int Value1, int fCom
return GIA_ONE;
}
static inline void Gia_ObjTerSimSetC( Gia_Obj_t * pObj ) { pObj->fMark0 = 0; pObj->fMark1 = 0; }
static inline void Gia_ObjTerSimSet0( Gia_Obj_t * pObj ) { pObj->fMark0 = 1; pObj->fMark1 = 0; }
static inline void Gia_ObjTerSimSet1( Gia_Obj_t * pObj ) { pObj->fMark0 = 0; pObj->fMark1 = 1; }
static inline void Gia_ObjTerSimSetX( Gia_Obj_t * pObj ) { pObj->fMark0 = 1; pObj->fMark1 = 1; }
static inline int Gia_ObjTerSimGetC( Gia_Obj_t * pObj ) { return !pObj->fMark0 && !pObj->fMark1; }
static inline int Gia_ObjTerSimGet0( Gia_Obj_t * pObj ) { return pObj->fMark0 && !pObj->fMark1; }
static inline int Gia_ObjTerSimGet1( Gia_Obj_t * pObj ) { return !pObj->fMark0 && pObj->fMark1; }
static inline int Gia_ObjTerSimGetX( Gia_Obj_t * pObj ) { return pObj->fMark0 && pObj->fMark1; }
static inline int Gia_ObjTerSimGet0Fanin0( Gia_Obj_t * pObj ) { return (Gia_ObjTerSimGet1(Gia_ObjFanin0(pObj)) && Gia_ObjFaninC0(pObj)) || (Gia_ObjTerSimGet0(Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj)); }
static inline int Gia_ObjTerSimGet1Fanin0( Gia_Obj_t * pObj ) { return (Gia_ObjTerSimGet0(Gia_ObjFanin0(pObj)) && Gia_ObjFaninC0(pObj)) || (Gia_ObjTerSimGet1(Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj)); }
static inline int Gia_ObjTerSimGet0Fanin1( Gia_Obj_t * pObj ) { return (Gia_ObjTerSimGet1(Gia_ObjFanin1(pObj)) && Gia_ObjFaninC1(pObj)) || (Gia_ObjTerSimGet0(Gia_ObjFanin1(pObj)) && !Gia_ObjFaninC1(pObj)); }
static inline int Gia_ObjTerSimGet1Fanin1( Gia_Obj_t * pObj ) { return (Gia_ObjTerSimGet0(Gia_ObjFanin1(pObj)) && Gia_ObjFaninC1(pObj)) || (Gia_ObjTerSimGet1(Gia_ObjFanin1(pObj)) && !Gia_ObjFaninC1(pObj)); }
static inline void Gia_ObjTerSimAnd( Gia_Obj_t * pObj )
{
assert( Gia_ObjIsAnd(pObj) );
assert( !Gia_ObjTerSimGetC( Gia_ObjFanin0(pObj) ) );
assert( !Gia_ObjTerSimGetC( Gia_ObjFanin1(pObj) ) );
if ( Gia_ObjTerSimGet0Fanin0(pObj) || Gia_ObjTerSimGet0Fanin1(pObj) )
Gia_ObjTerSimSet0( pObj );
else if ( Gia_ObjTerSimGet1Fanin0(pObj) && Gia_ObjTerSimGet1Fanin1(pObj) )
Gia_ObjTerSimSet1( pObj );
else
Gia_ObjTerSimSetX( pObj );
}
static inline void Gia_ObjTerSimCo( Gia_Obj_t * pObj )
{
assert( Gia_ObjIsCo(pObj) );
assert( !Gia_ObjTerSimGetC( Gia_ObjFanin0(pObj) ) );
if ( Gia_ObjTerSimGet0Fanin0(pObj) )
Gia_ObjTerSimSet0( pObj );
else if ( Gia_ObjTerSimGet1Fanin0(pObj) )
Gia_ObjTerSimSet1( pObj );
else
Gia_ObjTerSimSetX( pObj );
}
static inline void Gia_ObjTerSimRo( Gia_Man_t * p, Gia_Obj_t * pObj )
{
Gia_Obj_t * pTemp = Gia_ObjRoToRi(p, pObj);
assert( Gia_ObjIsRo(p, pObj) );
assert( !Gia_ObjTerSimGetC( pTemp ) );
pObj->fMark0 = pTemp->fMark0;
pObj->fMark1 = pTemp->fMark1;
}
static inline void Gia_ObjTerSimPrint( Gia_Obj_t * pObj )
{
if ( Gia_ObjTerSimGet0(pObj) )
printf( "0" );
else if ( Gia_ObjTerSimGet1(pObj) )
printf( "1" );
else if ( Gia_ObjTerSimGetX(pObj) )
printf( "X" );
}
static inline Gia_Obj_t * Gia_ObjReprObj( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr == GIA_VOID ? NULL : Gia_ManObj( p, p->pReprs[Id].iRepr ); }
static inline int Gia_ObjRepr( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr; }
static inline void Gia_ObjSetRepr( Gia_Man_t * p, int Id, int Num ) { assert( Num == GIA_VOID || Num < Id ); p->pReprs[Id].iRepr = Num; }
......
src/aig/gia/giaAbsGla.c
......@@ -26,61 +26,84 @@
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Gla_Obj_t_ Gla_Obj_t; // object
typedef struct Rfn_Obj_t_ Rfn_Obj_t; // refinement object
struct Rfn_Obj_t_
{
unsigned Value : 1; // value
unsigned fVisit : 1; // visited
unsigned fPPi : 1; // PPI
unsigned Prio : 28; // priority
};
typedef struct Gla_Obj_t_ Gla_Obj_t; // abstraction object
struct Gla_Obj_t_
{
int iGiaObj; // corresponding GIA obj
unsigned fAbs : 1; // belongs to abstraction
unsigned fCompl0 : 1; // compl bit of the first fanin
// unsigned fCompl1 : 1; // compl bit of the second fanin
unsigned fConst : 1; // object attribute
unsigned fPi : 1; // object attribute
unsigned fPo : 1; // object attribute
unsigned fRo : 1; // object attribute
unsigned fRi : 1; // object attribute
unsigned fAnd : 1; // object attribute
unsigned nFanins : 24; // fanin count
int Fanins[4]; // fanins
Vec_Int_t vFrames; // variables in each timeframe
int iGiaObj; // corresponding GIA obj
unsigned fAbs : 1; // belongs to abstraction
unsigned fCompl0 : 1; // compl bit of the first fanin
unsigned fConst : 1; // object attribute
unsigned fPi : 1; // object attribute
unsigned fPo : 1; // object attribute
unsigned fRo : 1; // object attribute
unsigned fRi : 1; // object attribute
unsigned fAnd : 1; // object attribute
unsigned fMark : 1; // nearby object
unsigned nFanins : 23; // fanin count
int Fanins[4]; // fanins
Vec_Int_t vFrames; // variables in each timeframe
};
typedef struct Gla_Man_t_ Gla_Man_t; // manager
struct Gla_Man_t_
{
// user data
Gia_Man_t * pGia; // AIG manager
Gia_ParVta_t* pPars; // parameters
Gia_Man_t * pGia; // AIG manager
Gia_ParVta_t* pPars; // parameters
// internal data
Vec_Int_t * vAbs; // abstracted objects
Gla_Obj_t * pObjRoot; // the primary output
Gla_Obj_t * pObjs; // objects
int nObjs; // the number of objects
int nAbsOld; // previous abstraction
Vec_Int_t * vAbs; // abstracted objects
Gla_Obj_t * pObjRoot; // the primary output
Gla_Obj_t * pObjs; // objects
unsigned * pObj2Obj; // mapping of GIA obj into GLA obj
int nObjs; // the number of objects
int nAbsOld; // previous abstraction
// other data
int nCexes; // the number of counter-examples
int nSatVars; // the number of SAT variables
Cnf_Dat_t * pCnf; // CNF derived for the nodes
sat_solver2 * pSat; // incremental SAT solver
Vec_Int_t * vCla2Obj; // mapping of clauses into GLA objs
Vec_Int_t * vTemp; // temporary array
Vec_Int_t * vAddedNew; // temporary array
// statistics
int timeInit;
int timeSat;
int timeUnsat;
int timeCex;
int timeOther;
int nCexes; // the number of counter-examples
int nSatVars; // the number of SAT variables
Cnf_Dat_t * pCnf; // CNF derived for the nodes
sat_solver2 * pSat; // incremental SAT solver
Vec_Int_t * vCla2Obj; // mapping of clauses into GLA objs
Vec_Int_t * vTemp; // temporary array
Vec_Int_t * vAddedNew; // temporary array
Vec_Int_t * vPrevCore; // previous core
// refinement
Vec_Int_t * pvRefis; // vectors of each object
Vec_Int_t * vPrioSels; // selected priorities
// statistics
int timeInit;
int timeSat;
int timeUnsat;
int timeCex;
int timeOther;
};
// declarations
static Vec_Int_t * Gla_ManCollectPPis( Gla_Man_t * p, Vec_Int_t * vPis );
static int Gla_ManCheckVar( Gla_Man_t * p, int iObj, int iFrame );
static int Gla_ManGetVar( Gla_Man_t * p, int iObj, int iFrame );
// object procedures
static inline int Gla_ObjId( Gla_Man_t * p, Gla_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; }
static inline Gla_Obj_t * Gla_ManObj( Gla_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; }
static inline Gia_Obj_t * Gla_ManGiaObj( Gla_Man_t * p, Gla_Obj_t * pObj ) { return Gia_ManObj( p->pGia, pObj->iGiaObj ); }
static inline int Gla_ObjId( Gla_Man_t * p, Gla_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; }
static inline Gla_Obj_t * Gla_ManObj( Gla_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; }
static inline Gia_Obj_t * Gla_ManGiaObj( Gla_Man_t * p, Gla_Obj_t * pObj ) { return Gia_ManObj( p->pGia, pObj->iGiaObj ); }
static inline int Gla_ObjSatValue( Gla_Man_t * p, int iGia, int f ) { return Gla_ManCheckVar(p, p->pObj2Obj[iGia], f) ? sat_solver2_var_value( p->pSat, Gla_ManGetVar(p, p->pObj2Obj[iGia], f) ) : 0; }
static inline Rfn_Obj_t * Gla_ObjRef( Gla_Man_t * p, int iObj, int f ) { return (Rfn_Obj_t *)Vec_IntGetEntryP( &(p->pvRefis[iObj]), f ); }
static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) { *((int *)p) = 0; }
// iterator through abstracted objects
#define Gla_ManForEachObj( p, pObj ) \
......@@ -91,7 +114,7 @@ static inline Gia_Obj_t * Gla_ManGiaObj( Gla_Man_t * p, Gla_Obj_t * pObj ) { ret
for ( i = 0; i < Vec_IntSize(vVec) && ((pObj = Gla_ManObj(p, Vec_IntEntry(vVec, i))),1); i++)
// iterator through fanins of an abstracted object
#define Gla_ObjForEachFanin( p, pObj, pFanin, i ) \
#define Gla_ObjForEachFanin( p, pObj, pFanin, i ) \
for ( i = 0; (i < (int)pObj->nFanins) && ((pFanin = Gla_ManObj(p, pObj->Fanins[i])),1); i++ )
////////////////////////////////////////////////////////////////////////
......@@ -240,6 +263,398 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
/**Function*************************************************************
Synopsis [Derives counter-example using current assignments.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Gla_ManDeriveCex( Gla_Man_t * p, Vec_Int_t * vPis )
{
Abc_Cex_t * pCex;
Gia_Obj_t * pObj;
int i, f;
pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
pCex->iPo = 0;
pCex->iFrame = p->pPars->iFrame;
Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
{
assert( Gia_ObjIsPi(p->pGia, pObj) );
for ( f = 0; f <= pCex->iFrame; f++ )
if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Gia_ObjCioId(pObj) );
}
return pCex;
}
/**Function*************************************************************
Synopsis [Collects internal objects in a topo order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gla_ManRefCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vRoAnds, Vec_Int_t * vCos )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
Gia_ObjSetTravIdCurrent(p, pObj);
if ( Gia_ObjIsRo(p, pObj) )
{
Vec_IntPush( vRoAnds, Gia_ObjId(p, pObj) );
Vec_IntPush( vCos, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) );
return;
}
assert( Gia_ObjIsAnd(pObj) );
Gla_ManRefCollect_rec( p, Gia_ObjFanin0(pObj), vRoAnds, vCos );
Gla_ManRefCollect_rec( p, Gia_ObjFanin1(pObj), vRoAnds, vCos );
Vec_IntPush( vRoAnds, Gia_ObjId(p, pObj) );
}
/**Function*************************************************************
Synopsis [Selects assignments to be refined.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vRes )
{
Rfn_Obj_t * pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f );
if ( pRef->fVisit )
return;
pRef->fVisit = 1;
if ( pRef->fPPi )
{
assert( (int)pRef->Prio < Vec_IntSize(p->vPrioSels) );
if ( Vec_IntEntry( p->vPrioSels, pRef->Prio ) == 0 ) // not selected yet
{
Vec_IntWriteEntry( p->vPrioSels, pRef->Prio, 1 );
Vec_IntPush( vRes, Gia_ObjId(p->pGia, pObj) );
}
return;
}
if ( Gia_ObjIsPi(p->pGia, pObj) || Gia_ObjIsConst0(pObj) )
return;
if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( f > 0 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj)), f-1, vRes );
return;
}
assert( Gia_ObjIsAnd(pObj) );
if ( pRef->Value == 1 )
{
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes );
Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes );
}
else // select one value
{
Rfn_Obj_t * pRef0 = Gla_ObjRef( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
Rfn_Obj_t * pRef1 = Gla_ObjRef( p, Gia_ObjFaninId1p(p->pGia, pObj), f );
int fSel0 = Vec_IntEntry( p->vPrioSels, pRef0->Prio );
int fSel1 = Vec_IntEntry( p->vPrioSels, pRef1->Prio );
if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
{
if ( !fSel0 && !fSel1 )
{
if ( pRef0->Prio <= pRef1->Prio ) // choice
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes );
else
Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes );
}
}
else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 )
{
if ( !fSel0 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes );
}
else
{
if ( !fSel1 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes );
}
}
}
/**Function*************************************************************
Synopsis [Performs refinement.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
{
int fVerify = 0;
Vec_Int_t * vPis, * vPPis, * vRoAnds, * vCos, * vRes = NULL;
Rfn_Obj_t * pRef, * pRef0, * pRef1;
Gia_Obj_t * pObj;
Gla_Obj_t * pGla;
int i, f;
// compute PIs and pseudo-PIs
vPis = Vec_IntAlloc( 100 );
vPPis = Gla_ManCollectPPis( p, vPis );
// remap into GIA
Gla_ManForEachObjAbsVec( vPis, p, pGla, i )
Vec_IntWriteEntry( vPis, i, pGla->iGiaObj );
Gla_ManForEachObjAbsVec( vPPis, p, pGla, i )
Vec_IntWriteEntry( vPPis, i, pGla->iGiaObj );
// prepare boundary objects
Gia_ManIncrementTravId( p->pGia );
Gia_ObjSetTravIdCurrent( p->pGia, Gia_ManConst0(p->pGia) );
Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
Gia_ObjSetTravIdCurrent( p->pGia, pObj );
Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
Gia_ObjSetTravIdCurrent( p->pGia, pObj );
// collect internal objects
vCos = Vec_IntAlloc( 1000 );
vRoAnds = Vec_IntAlloc( 1000 );
Vec_IntPush( vCos, Gia_ObjId(p->pGia, Gia_ManPo(p->pGia, 0)) );
Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
Gla_ManRefCollect_rec( p->pGia, Gia_ObjFanin0(pObj), vRoAnds, vCos );
// propagate values
for ( f = 0; f <= p->pPars->iFrame; f++ )
{
// constant
pRef = Gla_ObjRef( p, 0, f ); Gla_ObjClearRef( pRef );
pRef->Value = 0;
pRef->Prio = 0;
// primary input
Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
{
pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef );
pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f );
pRef->Prio = 0;
}
// primary input
Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
{
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef );
pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f );
pRef->Prio = i+1;
pRef->fPPi = 1;
}
// internal nodes
Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i )
{
pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef );
if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( f == 0 )
{
pRef->Value = 0;
pRef->Prio = 0;
}
else
{
pRef0 = Gla_ObjRef( p, Gia_ObjId(p->pGia, Gia_ObjRoToRi(p->pGia, pObj)), f-1 );
pRef->Value = pRef0->Value;
pRef->Prio = pRef0->Prio;
}
continue;
}
assert( Gia_ObjIsAnd(pObj) );
pRef0 = Gla_ObjRef( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
pRef1 = Gla_ObjRef( p, Gia_ObjFaninId1p(p->pGia, pObj), f );
pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj)) & (pRef1->Value ^ Gia_ObjFaninC1(pObj));
// if ( p->pCnf->pObj2Count[Gia_ObjId(p->pGia, pObj)] >= 0 )
// assert( (int)pRef->Value == Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) );
if ( pRef->Value == 1 )
pRef->Prio = Abc_MaxInt( pRef0->Prio, pRef1->Prio );
else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
pRef->Prio = Abc_MinInt( pRef0->Prio, pRef1->Prio ); // choice
else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 )
pRef->Prio = pRef0->Prio;
else
pRef->Prio = pRef1->Prio;
}
// output nodes
Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
{
pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef );
pRef0 = Gla_ObjRef( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj));
pRef->Prio = pRef0->Prio;
}
}
// make sure the output value is 1
pObj = Gia_ManPo( p->pGia, 0 );
pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), p->pPars->iFrame );
assert( pRef->Value == 1 );
// check the CEX
if ( pRef->Prio == 0 )
{
p->pGia->pCexSeq = Gla_ManDeriveCex( p, vPis );
Vec_IntFree( vPis );
Vec_IntFree( vPPis );
Vec_IntFree( vRoAnds );
Vec_IntFree( vCos );
return 0;
}
// select objects
vRes = Vec_IntAlloc( 100 );
Vec_IntFill( p->vPrioSels, Vec_IntSize(vPPis)+1, 0 );
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), p->pPars->iFrame, vRes );
if ( fVerify )
{
Gia_ManForEachObj( p->pGia, pObj, i )
assert( Gia_ObjTerSimGetC(pObj) );
for ( f = 0; f <= p->pPars->iFrame; f++ )
{
Gia_ObjTerSimSet0( Gia_ManConst0(p->pGia) );
Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
{
if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
Gia_ObjTerSimSet1( pObj );
else
Gia_ObjTerSimSet0( pObj );
}
Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
{
if ( Vec_IntEntry(p->vPrioSels, i+1) == 0 ) // not selected
Gia_ObjTerSimSetX( pObj );
else if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
Gia_ObjTerSimSet1( pObj );
else
Gia_ObjTerSimSet0( pObj );
}
Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i )
{
if ( Gia_ObjIsAnd(pObj) )
Gia_ObjTerSimAnd( pObj );
else if ( f == 0 )
Gia_ObjTerSimSet0( pObj );
else
Gia_ObjTerSimRo( p->pGia, pObj );
}
Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
Gia_ObjTerSimCo( pObj );
}
pObj = Gia_ManPo( p->pGia, 0 );
if ( !Gia_ObjTerSimGet1(pObj) )
printf( "Refinement verification has failed!!!" );
// clear
Gia_ObjTerSimSetC( Gia_ManConst0(p->pGia) );
Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
Gia_ObjTerSimSetC( pObj );
Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
Gia_ObjTerSimSetC( pObj );
Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i )
Gia_ObjTerSimSetC( pObj );
Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
Gia_ObjTerSimSetC( pObj );
}
// remap them into GLA objects
Gia_ManForEachObjVec( vRes, p->pGia, pObj, i )
Vec_IntWriteEntry( vRes, i, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] );
Vec_IntFree( vPis );
Vec_IntFree( vPPis );
Vec_IntFree( vRoAnds );
Vec_IntFree( vCos );
return vRes;
}
/**Function*************************************************************
Synopsis [Selects items that are new in the current abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gla_ManRegionStart( Gla_Man_t * p, Vec_Int_t * vCore )
{
Vec_Int_t * vRes;
Gla_Obj_t * pGla;
int i;
vRes = Vec_IntAlloc( 100 );
Gla_ManForEachObjAbsVec( vCore, p, pGla, i )
if ( !pGla->fAbs )
Vec_IntPush( vRes, Gla_ObjId(p, pGla) );
return vRes;
}
/**Function*************************************************************
Synopsis [Finds adjacent to previous core among select (or all if NULL).]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gla_ManRegionFilter( Gla_Man_t * p, Vec_Int_t * vSelected, Vec_Int_t * vPrevCore )
{
Vec_Int_t * vRes;
Gla_Obj_t * pGla, * pFanin;
int i, k;
// mark fanins of previous core
Gla_ManForEachObjAbsVec( vPrevCore, p, pGla, i )
{
assert( pGla->fMark == 0 );
Gla_ObjForEachFanin( p, pGla, pFanin, k )
pFanin->fMark = 1;
}
// select those not marked and included in the abstraction
vRes = Vec_IntAlloc( 100 );
if ( vSelected == NULL )
{
Gla_ManForEachObj( p, pGla )
if ( !pGla->fAbs && pGla->fMark )
Vec_IntPush( vRes, Gla_ObjId(p, pGla) );
}
else
{
Gla_ManForEachObjAbsVec( vSelected, p, pGla, i )
if ( !pGla->fAbs && pGla->fMark )
Vec_IntPush( vRes, Gla_ObjId(p, pGla) );
}
// unmark fanins of previous core
Gla_ManForEachObjAbsVec( vPrevCore, p, pGla, i )
Gla_ObjForEachFanin( p, pGla, pFanin, k )
pFanin->fMark = 0;
return vRes;
}
/**Function*************************************************************
......@@ -292,6 +707,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p->vAbs = Vec_IntAlloc( 100 );
p->vTemp = Vec_IntAlloc( 100 );
p->vAddedNew = Vec_IntAlloc( 100 );
p->vPrioSels = Vec_IntAlloc( 100 );
// internal data
pAig = Gia_ManToAigSimple( p->pGia );
p->pCnf = Cnf_DeriveOther( pAig );
......@@ -311,16 +727,18 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
assert( ~pObj->Value );
pLits[i] = toLitCond( pObj->Value, lit_sign(pLits[i]) );
}
// create objects
p->pObjs = ABC_CALLOC( Gla_Obj_t, p->nObjs );
// create objects
p->pObjs = ABC_CALLOC( Gla_Obj_t, p->nObjs );
p->pObj2Obj = ABC_FALLOC( unsigned, Gia_ManObjNum(p->pGia) );
p->pvRefis = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(p->pGia) );
Gia_ManForEachObj( p->pGia, pObj, i )
{
p->pObj2Obj[i] = pObj->Value;
if ( !~pObj->Value )
continue;
pGla = Gla_ManObj( p, pObj->Value );
pGla->iGiaObj = i;
pGla->fCompl0 = Gia_ObjFaninC0(pObj);
// pGla->fCompl1 = Gia_ObjFaninC1(pObj);
pGla->fConst = Gia_ObjIsConst0(pObj);
pGla->fPi = Gia_ObjIsPi(p->pGia, pObj);
pGla->fPo = Gia_ObjIsPo(p->pGia, pObj);
......@@ -379,10 +797,14 @@ void Gla_ManStop( Gla_Man_t * p )
ABC_FREE( pGla->vFrames.pArray );
Cnf_DataFree( p->pCnf );
sat_solver2_delete( p->pSat );
Vec_IntFree( p->vCla2Obj );
Vec_IntFree( p->vAddedNew );
Vec_IntFree( p->vTemp );
Vec_IntFree( p->vAbs );
Vec_IntFreeP( &p->vCla2Obj );
Vec_IntFreeP( &p->vPrevCore );
Vec_IntFreeP( &p->vAddedNew );
Vec_IntFreeP( &p->vPrioSels );
Vec_IntFreeP( &p->vTemp );
Vec_IntFreeP( &p->vAbs );
ABC_FREE( p->pvRefis );
ABC_FREE( p->pObj2Obj );
ABC_FREE( p->pObjs );
ABC_FREE( p );
}
......@@ -475,53 +897,53 @@ Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p )
SeeAlso []
***********************************************************************/
Vec_Int_t * Gla_ManCollectPPis( Gla_Man_t * p )
Vec_Int_t * Gla_ManCollectPPis( Gla_Man_t * p, Vec_Int_t * vPis )
{
Vec_Int_t * vPPis;
Gla_Obj_t * pObj, * pFanin;
int i, k;
vPPis = Vec_IntAlloc( 1000 );
if ( vPis )
Vec_IntClear( vPis );
Gla_ManForEachObjAbs( p, pObj, i )
{
assert( pObj->fConst || pObj->fRo || pObj->fAnd );
Gla_ObjForEachFanin( p, pObj, pFanin, k )
if ( !pFanin->fPi && !pFanin->fAbs )
Vec_IntPush( vPPis, pObj->Fanins[k] );
else if ( vPis && pFanin->fPi && !pFanin->fAbs )
Vec_IntPush( vPis, pObj->Fanins[k] );
}
Vec_IntUniqify( vPPis );
Vec_IntReverseOrder( vPPis );
if ( vPis )
Vec_IntUniqify( vPis );
return vPPis;
}
int Gla_ManCountPPis( Gla_Man_t * p )
{
Vec_Int_t * vPPis = Gla_ManCollectPPis( p );
Vec_Int_t * vPPis = Gla_ManCollectPPis( p, NULL );
int RetValue = Vec_IntSize( vPPis );
Vec_IntFree( vPPis );
return RetValue;
}
void Gla_ManExplorePPis( Gla_Man_t * p, Vec_Int_t * vPPis )
{
static int Round = 0;
Gla_Obj_t * pObj, * pFanin;
int i, j, k, Count;
if ( (Round++ % 3) == 0 )
if ( (Round++ % 5) == 0 )
return;
// printf( "\n" );
j = 0;
Gla_ManForEachObjAbsVec( vPPis, p, pObj, i )
{
assert( pObj->fAbs == 0 );
// printf( "%6d ", Gla_ObjId(p, pObj) );
// printf( "Fanins=%d ", pObj->nFanins );
// Gla_ObjForEachFanin( p, pObj, pFanin, k )
// printf( "%d", pFanin->fAbs );
// printf( "\n" );
Count = 0;
Gla_ObjForEachFanin( p, pObj, pFanin, k )
Count += pFanin->fAbs;
if ( Count == 0 )
if ( Count == 0 || ((Round & 1) && Count == 1) )
continue;
Vec_IntWriteEntry( vPPis, j++, Gla_ObjId(p, pObj) );
}
......@@ -529,6 +951,99 @@ void Gla_ManExplorePPis( Gla_Man_t * p, Vec_Int_t * vPPis )
Vec_IntShrink( vPPis, j );
}
// add those having more than one shared fanin
void Gla_ManExplorePPis2( Gla_Man_t * p, Vec_Int_t * vPPis )
{
static int Round = 0;
Vec_Int_t * vTemp;
Gla_Obj_t * pGla, * pFanin;
int i, k, Entry, Count;
if ( p->vPrevCore == NULL )
return;
if ( (Round++ % 10) == 0 )
{
p->vPrevCore = Gla_ManRegionFilter( p, vPPis, vTemp = p->vPrevCore );
Vec_IntFree( vTemp );
}
else
{
p->vPrevCore = Gla_ManRegionFilter( p, NULL, vTemp = p->vPrevCore );
Vec_IntFree( vTemp );
// save a copy
vTemp = Vec_IntDup( vPPis );
// udpate
Vec_IntClear( vPPis );
Vec_IntForEachEntry( p->vPrevCore, Entry, i )
Vec_IntPush( vPPis, Entry );
// mark those included as abstracted
Gla_ManForEachObjAbsVec( vPPis, p, pGla, i )
{
assert( pGla->fAbs == 0 );
pGla->fAbs = 1;
}
// add those not included but to close to abstracted
Gla_ManForEachObjAbsVec( vTemp, p, pGla, i )
{
if ( pGla->fAbs )
continue;
Count = 0;
Gla_ObjForEachFanin( p, pGla, pFanin, k )
Count += pFanin->fAbs;
if ( Count == 0 || Count == 1 )
continue;
Vec_IntPush( vPPis, Gla_ObjId(p, pGla) );
}
// unmark those included
Gla_ManForEachObjAbsVec( vPPis, p, pGla, i )
pGla->fAbs = 0;
// cleanup
Vec_IntFree( vTemp );
}
}
/*
void Gla_ManExplorePPis2( Gla_Man_t * p, Vec_Int_t * vPPis, int iIter )
{
Gla_Obj_t * pObj, * pFanin;
int i, j, k;
if ( iIter > 10 )
{
Gla_ManForEachObj( p, pObj )
pObj->fMark = 0;
return;
}
j = 0;
Gla_ManForEachObjAbsVec( vPPis, p, pObj, i )
{
assert( pObj->fAbs == 0 );
if ( pObj->fMark == 0 )
{
Gla_ObjForEachFanin( p, pObj, pFanin, k )
if ( pObj->fMark )
break;
if ( k == (int)pObj->nFanins )
continue;
}
Vec_IntWriteEntry( vPPis, j++, Gla_ObjId(p, pObj) );
}
// printf( "\n%d -> %d\n", Vec_IntSize(vPPis), j );
Vec_IntShrink( vPPis, j );
// update
Gla_ManForEachObj( p, pObj )
pObj->fMark = 0;
Gla_ManForEachObjAbsVec( vPPis, p, pObj, i )
Gla_ObjForEachFanin( p, pObj, pFanin, k )
pFanin->fMark = 1;
}
*/
/**Function*************************************************************
......@@ -541,6 +1056,13 @@ void Gla_ManExplorePPis( Gla_Man_t * p, Vec_Int_t * vPPis )
SeeAlso []
***********************************************************************/
int Gla_ManCheckVar( Gla_Man_t * p, int iObj, int iFrame )
{
Gla_Obj_t * pGla = Gla_ManObj( p, iObj );
int iVar = Vec_IntGetEntry( &pGla->vFrames, iFrame );
assert( !pGla->fPo && !pGla->fRi );
return (iVar > 0);
}
int Gla_ManGetVar( Gla_Man_t * p, int iObj, int iFrame )
{
Gla_Obj_t * pGla = Gla_ManObj( p, iObj );
......@@ -772,25 +1294,31 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl
void Gla_ManReportMemory( Gla_Man_t * p )
{
Gla_Obj_t * pGla;
int i;
double memTot = 0;
double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t);
double memSat = sat_solver2_memory( p->pSat );
double memPro = sat_solver2_memory_proof( p->pSat );
double memMap = p->nObjs * sizeof(Gla_Obj_t);
double memMap = p->nObjs * sizeof(Gla_Obj_t) + Gia_ManObjNum(p->pGia) * sizeof(int);
double memRef = Gia_ManObjNum(p->pGia) * sizeof(Vec_Int_t) + Vec_IntCap(p->vPrioSels) * sizeof(int);
double memOth = sizeof(Gla_Man_t);
for ( pGla = p->pObjs; pGla < p->pObjs + p->nObjs; pGla++ )
memMap += Vec_IntCap(&pGla->vFrames) * sizeof(int);
for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
memRef += Vec_IntCap(&p->pvRefis[i]) * sizeof(int);
memOth += Vec_IntCap(p->vCla2Obj) * sizeof(int);
memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
memOth += (p->vPrevCore ? Vec_IntCap(p->vPrevCore) : 0) * sizeof(int);
memOth += Vec_IntCap(p->vTemp) * sizeof(int);
memOth += Vec_IntCap(p->vAbs) * 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 );
memTot = memAig + memSat + memPro + memMap + memRef + 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: Refine", memRef, memTot );
ABC_PRMP( "Memory: Other ", memOth, memTot );
ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
}
......@@ -920,11 +1448,17 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
p->nCexes++;
// perform the refinement
clk2 = clock();
// pCex = Vta_ManRefineAbstraction( p, f );
pCex = NULL;
vPPis = Gla_ManCollectPPis( p );
/*
vPPis = Gla_ManRefinement( p );
if ( vPPis == NULL )
{
pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
break;
}
*/
vPPis = Gla_ManCollectPPis( p, NULL );
Gla_ManExplorePPis( p, vPPis );
Gia_GlaAddToAbs( p, vPPis, 1 );
Gia_GlaAddOneSlice( p, f, vPPis );
Vec_IntFree( vPPis );
......@@ -952,6 +1486,8 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Gla_ManRollBack( p );
Vec_IntShrink( p->vCla2Obj, (int)p->pSat->stats.clauses+1 );
// load this timeframe
Vec_IntFreeP( &p->vPrevCore );
p->vPrevCore = Gla_ManRegionStart( p, vCore );
Gia_GlaAddToAbs( p, vCore, 0 );
Gia_GlaAddOneSlice( p, f, vCore );
Vec_IntFree( vCore );
......@@ -965,6 +1501,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
break;
if ( Status == 0 )
{
assert( 0 );
// Vta_ManSatVerify( p );
// make sure, there was no initial abstraction (otherwise, it was invalid)
assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart );
......
src/aig/gia/giaAbsVta.c
......@@ -532,8 +532,8 @@ static inline void Vta_ObjPreds( Vta_Man_t * p, Vta_Obj_t * pThis, Gia_Obj_t * p
{
*ppThis0 = NULL;
*ppThis1 = NULL;
if ( !pThis->fAdded )
return;
// if ( !pThis->fAdded )
// return;
assert( !Gia_ObjIsPi(p->pGia, pObj) );
if ( Gia_ObjIsConst0(pObj) || (Gia_ObjIsCi(pObj) && pThis->iFrame == 0) )
return;
......@@ -541,13 +541,13 @@ static inline void Vta_ObjPreds( Vta_Man_t * p, Vta_Obj_t * pThis, Gia_Obj_t * p
{
*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 );
// 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 );
// assert( *ppThis0 );
}
/**Function*************************************************************
......@@ -569,9 +569,12 @@ void Vta_ManCollectNodes_rec( Vta_Man_t * p, Vta_Obj_t * pThis, Vec_Int_t * vOrd
return;
pThis->fVisit = 1;
pObj = Gia_ManObj( p->pGia, pThis->iObj );
Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
if ( pThis0 ) Vta_ManCollectNodes_rec( p, pThis0, vOrder );
if ( pThis1 ) Vta_ManCollectNodes_rec( p, pThis1, vOrder );
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 )
......@@ -728,6 +731,41 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
if ( pThis1 )
pThis1->Prio = Abc_MinInt( pThis1->Prio, pThis->Prio + 1 );
}
/*
// update priorities according to reconvergest 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 reconvergest 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
......@@ -747,9 +785,6 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
pThis->Prio = Counter++;
// Abc_Print( 1, "Used %d Unused %d\n", Vec_PtrSize(vTermsUsed), Vec_PtrSize(vTermsUnused) );
Vec_PtrFree( vTermsUsed );
Vec_PtrFree( vTermsUnused );
// propagate in the direct order
Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
......@@ -885,6 +920,33 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
assert( 0 );
}
// 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 )
{
......@@ -955,7 +1017,6 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
pCex = Vga_ManDeriveCex( p );
else
{
// int nObjOld = p->nObjs;
Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
if ( !Gia_ObjIsPi(p->pGia, pObj) )
Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment