Skip to content

A
abc
Commit b20ca62e by Alan Mishchenko
Options

Scalable gate-level abstraction.

parent 51d5055e
Showing with 158 additions and 49 deletions
src/aig/gia/giaAbsGla2.c
...@@ -46,7 +46,7 @@ struct Ga2_Man_t_ ...@@ -46,7 +46,7 @@ struct Ga2_Man_t_
Vec_Int_t * vIds; // abstraction ID for each GIA object Vec_Int_t * vIds; // abstraction ID for each GIA object
Vec_Int_t * vAbs; // array of abstracted objects Vec_Int_t * vAbs; // array of abstracted objects
Vec_Int_t * vValues; // array of objects with abstraction ID assigned Vec_Int_t * vValues; // array of objects with abstraction ID assigned
Vec_Int_t * vProofIds; // proof IDs for these objects (1-to-1 with vValues) Vec_Int_t * vProofIds; // mapping of GIA objects into their proof IDs
int nProofIds; // the counter of proof IDs int nProofIds; // the counter of proof IDs
int LimAbs; // limit value for starting abstraction objects int LimAbs; // limit value for starting abstraction objects
int LimPpi; // limit value for starting PPI objects int LimPpi; // limit value for starting PPI objects
...@@ -82,8 +82,8 @@ static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj ) ...@@ -82,8 +82,8 @@ static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj )
static inline int Ga2_ObjId( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vIds, Gia_ObjId(p->pGia, pObj)); } static inline int Ga2_ObjId( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vIds, Gia_ObjId(p->pGia, pObj)); }
static inline void Ga2_ObjSetId( Ga2_Man_t * p, Gia_Obj_t * pObj, int i ) { Vec_IntWriteEntry(p->vIds, Gia_ObjId(p->pGia, pObj), i); } static inline void Ga2_ObjSetId( Ga2_Man_t * p, Gia_Obj_t * pObj, int i ) { Vec_IntWriteEntry(p->vIds, Gia_ObjId(p->pGia, pObj), i); }
static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Vec_PtrEntry(p->vCnfs, (Ga2_ObjId(p,pObj) << 1) ); } static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj) ); }
static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Vec_PtrEntry(p->vCnfs, (Ga2_ObjId(p,pObj) << 1)+1); } static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)+1 ); }
static inline int Ga2_ObjIsAbs( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Ga2_ObjId(p,pObj) < p->LimAbs; } static inline int Ga2_ObjIsAbs( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Ga2_ObjId(p,pObj) < p->LimAbs; }
static inline int Ga2_ObjIsPpi( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Ga2_ObjId(p,pObj) >= p->LimAbs && Ga2_ObjId(p,pObj) < p->LimPpi; } static inline int Ga2_ObjIsPpi( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Ga2_ObjId(p,pObj) >= p->LimAbs && Ga2_ObjId(p,pObj) < p->LimPpi; }
...@@ -93,6 +93,7 @@ static inline Vec_Int_t * Ga2_MapFrameMap( Ga2_Man_t * p, int f ) ...@@ -93,6 +93,7 @@ static inline Vec_Int_t * Ga2_MapFrameMap( Ga2_Man_t * p, int f )
// returns literal of this object, or -1 if SAT variable of the object is not assigned // returns literal of this object, or -1 if SAT variable of the object is not assigned
static inline int Ga2_ObjFindLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) static inline int Ga2_ObjFindLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
{ {
int Id = Ga2_ObjId(p,pObj);
assert( Ga2_ObjId(p,pObj) && Ga2_ObjId(p,pObj) < Vec_IntSize(p->vValues) ); assert( Ga2_ObjId(p,pObj) && Ga2_ObjId(p,pObj) < Vec_IntSize(p->vValues) );
if ( f == Vec_PtrSize(p->vId2Lit) ) if ( f == Vec_PtrSize(p->vId2Lit) )
Vec_PtrPush( p->vId2Lit, Vec_IntStartFull(Vec_IntSize(p->vValues)) ); Vec_PtrPush( p->vId2Lit, Vec_IntStartFull(Vec_IntSize(p->vValues)) );
...@@ -357,9 +358,8 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) ...@@ -357,9 +358,8 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p->vIds = Vec_IntStart( Gia_ManObjNum(pGia) ); p->vIds = Vec_IntStart( Gia_ManObjNum(pGia) );
p->vAbs = Vec_IntAlloc( 1000 ); p->vAbs = Vec_IntAlloc( 1000 );
p->vValues = Vec_IntAlloc( 1000 ); p->vValues = Vec_IntAlloc( 1000 );
p->vProofIds = Vec_IntAlloc( 1000 ); p->vProofIds = Vec_IntAlloc(0);
Vec_IntPush( p->vValues, -1 ); Vec_IntPush( p->vValues, -1 );
Vec_IntPush( p->vProofIds, -1 );
// refinement // refinement
p->pRnm = Rnm_ManStart( pGia ); p->pRnm = Rnm_ManStart( pGia );
// SAT solver and variables // SAT solver and variables
...@@ -401,8 +401,10 @@ void Ga2_ManStop( Ga2_Man_t * p ) ...@@ -401,8 +401,10 @@ void Ga2_ManStop( Ga2_Man_t * p )
Vec_IntFreeP( &p->pGia->vMapping ); Vec_IntFreeP( &p->pGia->vMapping );
Gia_ManSetPhase( p->pGia ); Gia_ManSetPhase( p->pGia );
// if ( p->pPars->fVerbose ) // if ( p->pPars->fVerbose )
Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Reduce = %d Cex = %d ObjsAdded = %d\n", Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d ObjsAdded = %d\n",
sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded ); 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 );
if( p->pSat ) sat_solver2_delete( p->pSat ); if( p->pSat ) sat_solver2_delete( p->pSat );
Vec_VecFree( (Vec_Vec_t *)p->vCnfs ); Vec_VecFree( (Vec_Vec_t *)p->vCnfs );
Vec_VecFree( (Vec_Vec_t *)p->vId2Lit ); Vec_VecFree( (Vec_Vec_t *)p->vId2Lit );
...@@ -615,35 +617,33 @@ static inline void Ga2_ManCnfAddStatic( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_In ...@@ -615,35 +617,33 @@ static inline void Ga2_ManCnfAddStatic( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_In
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs, int ProofId ) void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs )
{ {
unsigned uTruth; unsigned uTruth;
int nLeaves; int nLeaves;
assert( pObj->fPhase ); assert( pObj->fPhase );
assert( Vec_PtrSize(p->vCnfs) == 2 * Vec_IntSize(p->vValues) ); assert( Vec_PtrSize(p->vCnfs) == 2 * Vec_IntSize(p->vValues) );
assert( Vec_IntSize(p->vProofIds) == Vec_IntSize(p->vValues) );
// assign abstraction ID to the node // assign abstraction ID to the node
if ( Ga2_ObjId(p,pObj) == 0 ) if ( Ga2_ObjId(p,pObj) == 0 )
{ {
Ga2_ObjSetId( p, pObj, Vec_IntSize(p->vValues) ); Ga2_ObjSetId( p, pObj, Vec_IntSize(p->vValues) );
Vec_IntPush( p->vValues, Gia_ObjId(p->pGia, pObj) ); Vec_IntPush( p->vValues, Gia_ObjId(p->pGia, pObj) );
Vec_IntPush( p->vProofIds, ProofId );
Vec_PtrPush( p->vCnfs, NULL ); Vec_PtrPush( p->vCnfs, NULL );
Vec_PtrPush( p->vCnfs, NULL ); Vec_PtrPush( p->vCnfs, NULL );
} }
assert( Ga2_ObjCnf0(p, pObj) == NULL ); assert( Ga2_ObjCnf0(p, pObj) == NULL );
if ( !fAbs ) if ( !fAbs || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsConst0(pObj) )
return; return;
assert( Gia_ObjIsAnd(pObj) );
// compute parameters // compute parameters
nLeaves = Ga2_ObjLeaveNum(p->pGia, pObj); nLeaves = Ga2_ObjLeaveNum(p->pGia, pObj);
// create CNF for pos/neg phases
uTruth = Ga2_ObjTruth( p->pGia, pObj ); uTruth = Ga2_ObjTruth( p->pGia, pObj );
Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj), Ga2_ManCnfCompute(uTruth, nLeaves, p->vIsopMem) ); // create CNF for pos/neg phases
uTruth = (~uTruth) & Abc_InfoMask( (1 << nLeaves) ); Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj), Ga2_ManCnfCompute( uTruth, nLeaves, p->vIsopMem) );
Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, Ga2_ManCnfCompute(uTruth, nLeaves, p->vIsopMem) ); Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, Ga2_ManCnfCompute(~uTruth, nLeaves, p->vIsopMem) );
} }
void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd, int ProofId ) void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
{ {
Vec_Int_t * vLeaves, * vMap; Vec_Int_t * vLeaves, * vMap;
Gia_Obj_t * pObj, * pFanin; Gia_Obj_t * pObj, * pFanin;
...@@ -651,16 +651,25 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd, int ProofId ) ...@@ -651,16 +651,25 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd, int ProofId )
// add abstraction objects // add abstraction objects
Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i ) Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
{ {
Ga2_ManSetupNode( p, pObj, 1, ProofId ); Ga2_ManSetupNode( p, pObj, 1 );
Vec_IntPush( p->vAbs, Gia_ObjId(p->pGia, pObj) ); Vec_IntPush( p->vAbs, Gia_ObjId(p->pGia, pObj) );
Vec_IntPush( p->vProofIds, ProofId ); if ( p->pSat->pPrf2 )
Vec_IntWriteEntry( p->vProofIds, Gia_ObjId(p->pGia, pObj), p->nProofIds++ );
} }
// add PPI objects // add PPI objects
Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i ) Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
{ {
if ( Gia_ObjIsRo(p->pGia, pObj) )
{
pFanin = Gia_ObjRoToRi(p->pGia, pObj);
if ( !Ga2_ObjId( p, Gia_ObjFanin0(pFanin) ) )
Ga2_ManSetupNode( p, Gia_ObjFanin0(pFanin), 0 );
continue;
}
vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
Ga2_ManSetupNode( p, pObj, 0, -1 ); if ( !Ga2_ObjId( p, pFanin ) )
Ga2_ManSetupNode( p, pFanin, 0 );
} }
// clean mapping in the timeframes // clean mapping in the timeframes
Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i ) Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i )
...@@ -674,12 +683,8 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd, int ProofId ) ...@@ -674,12 +683,8 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd, int ProofId )
Vec_IntClear( p->vLits ); Vec_IntClear( p->vLits );
Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f ) ); Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f ) );
Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Vec_IntEntry(p->vProofIds, Ga2_ObjId(p, pObj)) ); Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj) );
} }
// verify -- if ProofId == -1, all proof IDs should be the same
if ( ProofId == -1 )
Vec_IntForEachEntry( p->vProofIds, k, i )
assert( k == -1 );
} }
void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f ) void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f )
...@@ -696,7 +701,7 @@ void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f ) ...@@ -696,7 +701,7 @@ void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f )
Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f ) ); Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f ) );
iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f ); iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f );
Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, i - p->LimAbs ); Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj) );
} }
} }
...@@ -723,13 +728,13 @@ void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues ) ...@@ -723,13 +728,13 @@ void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues )
// shrink values // shrink values
Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i ) Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
{ {
if ( !i ) continue;
assert( Ga2_ObjId(p,pObj) ); assert( Ga2_ObjId(p,pObj) );
if ( i < nValues ) if ( i < nValues )
continue; continue;
Ga2_ObjSetId( p, pObj, 0 ); Ga2_ObjSetId( p, pObj, 0 );
} }
Vec_IntShrink( p->vValues, nValues ); Vec_IntShrink( p->vValues, nValues );
Vec_IntShrink( p->vProofIds, nValues );
Vec_PtrShrink( p->vCnfs, 2 * nValues ); Vec_PtrShrink( p->vCnfs, 2 * nValues );
// clean mapping into timeframes // clean mapping into timeframes
Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i ) Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i )
...@@ -763,8 +768,20 @@ Vec_Int_t * Ga2_ManAbsTranslate( Ga2_Man_t * p ) ...@@ -763,8 +768,20 @@ Vec_Int_t * Ga2_ManAbsTranslate( Ga2_Man_t * p )
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
int i; int i;
vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) ); vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) );
Vec_IntWriteEntry( vGateClasses, 0, 1 );
Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i ) Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
{
if ( Gia_ObjIsRo(p->pGia, pObj) )
{
Vec_IntWriteEntry( vGateClasses, Gia_ObjId(p->pGia, pObj), 1 );
pObj = Gia_ObjRoToRi( p->pGia, pObj );
Vec_IntWriteEntry( vGateClasses, Gia_ObjFaninId0p(p->pGia, pObj), 1 );
}
else if ( Gia_ObjIsAnd(pObj) )
Ga2_ManAbsTranslate_rec( p->pGia, pObj, vGateClasses, 1 ); Ga2_ManAbsTranslate_rec( p->pGia, pObj, vGateClasses, 1 );
else if ( !Gia_ObjIsConst0(pObj) )
assert( 0 );
}
return vGateClasses; return vGateClasses;
} }
...@@ -774,9 +791,10 @@ Vec_Int_t * Ga2_ManAbsDerive( Gia_Man_t * p ) ...@@ -774,9 +791,10 @@ Vec_Int_t * Ga2_ManAbsDerive( Gia_Man_t * p )
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
int i; int i;
vToAdd = Vec_IntAlloc( 1000 ); vToAdd = Vec_IntAlloc( 1000 );
Vec_IntPush( vToAdd, 0 ); // const 0
Gia_ManForEachRo( p, pObj, i ) Gia_ManForEachRo( p, pObj, i )
if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, i) ) if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, Gia_ObjId(p, pObj)) )
Vec_IntPush( vToAdd, i ); Vec_IntPush( vToAdd, Gia_ObjId(p, pObj) );
Gia_ManForEachAnd( p, pObj, i ) Gia_ManForEachAnd( p, pObj, i )
if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, i) ) if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, i) )
Vec_IntPush( vToAdd, i ); Vec_IntPush( vToAdd, i );
...@@ -788,7 +806,6 @@ void Ga2_ManRestart( Ga2_Man_t * p ) ...@@ -788,7 +806,6 @@ void Ga2_ManRestart( Ga2_Man_t * p )
Vec_Int_t * vToAdd; Vec_Int_t * vToAdd;
assert( p->pGia != NULL && p->pGia->vGateClasses != NULL ); assert( p->pGia != NULL && p->pGia->vGateClasses != NULL );
assert( Gia_ManPi(p->pGia, 0)->fPhase ); // marks are set assert( Gia_ManPi(p->pGia, 0)->fPhase ); // marks are set
p->nProofIds = 0;
// clear mappings from objects // clear mappings from objects
Ga2_ManShrinkAbs( p, 0, 1 ); Ga2_ManShrinkAbs( p, 0, 1 );
// clear SAT variable numbers (begin with 1) // clear SAT variable numbers (begin with 1)
...@@ -797,7 +814,7 @@ void Ga2_ManRestart( Ga2_Man_t * p ) ...@@ -797,7 +814,7 @@ void Ga2_ManRestart( Ga2_Man_t * p )
p->nSatVars = 1; p->nSatVars = 1;
// start abstraction // start abstraction
vToAdd = Ga2_ManAbsDerive( p->pGia ); vToAdd = Ga2_ManAbsDerive( p->pGia );
Ga2_ManAddToAbs( p, vToAdd, -1 ); Ga2_ManAddToAbs( p, vToAdd );
Vec_IntFree( vToAdd ); Vec_IntFree( vToAdd );
p->LimAbs = Vec_IntSize(p->vAbs) + 1; p->LimAbs = Vec_IntSize(p->vAbs) + 1;
p->LimPpi = Vec_IntSize(p->vValues); p->LimPpi = Vec_IntSize(p->vValues);
...@@ -820,6 +837,7 @@ void Ga2_ManRestart( Ga2_Man_t * p ) ...@@ -820,6 +837,7 @@ void Ga2_ManRestart( Ga2_Man_t * p )
int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
{ {
int fSimple = 1; int fSimple = 1;
int Id = Gia_ObjId(p->pGia, pObj);
unsigned uTruth; unsigned uTruth;
Gia_Obj_t * pLeaf; Gia_Obj_t * pLeaf;
int nLeaves, * pLeaves; int nLeaves, * pLeaves;
...@@ -839,11 +857,11 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) ...@@ -839,11 +857,11 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
return 0; return 0;
} }
assert( pObj->fPhase ); assert( pObj->fPhase );
if ( Gia_ObjIsPi(p->pGia, pObj) || Ga2_ObjIsPpi(p, pObj) )
return Ga2_ObjFindOrAddLit( p, pObj, f );
Lit = Ga2_ObjFindLit( p, pObj, f ); Lit = Ga2_ObjFindLit( p, pObj, f );
if ( Lit >= 0 ) if ( Lit >= 0 )
return Lit; return Lit;
if ( Gia_ObjIsPi(p->pGia, pObj) )
return Ga2_ObjFindOrAddLit( p, pObj, f );
if ( Gia_ObjIsRo(p->pGia, pObj) ) if ( Gia_ObjIsRo(p->pGia, pObj) )
{ {
assert( f > 0 ); assert( f > 0 );
...@@ -851,6 +869,7 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) ...@@ -851,6 +869,7 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
Ga2_ObjAddLit( p, pObj, f, Lit ); Ga2_ObjAddLit( p, pObj, f, Lit );
return Lit; return Lit;
} }
assert( Gia_ObjIsAnd(pObj) );
nLeaves = Ga2_ObjLeaveNum( p->pGia, pObj ); nLeaves = Ga2_ObjLeaveNum( p->pGia, pObj );
pLeaves = Ga2_ObjLeavePtr( p->pGia, pObj ); pLeaves = Ga2_ObjLeavePtr( p->pGia, pObj );
if ( fSimple ) if ( fSimple )
...@@ -864,7 +883,7 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) ...@@ -864,7 +883,7 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
// create fanout literal // create fanout literal
Lit = Ga2_ObjFindOrAddLit( p, pObj, f ); Lit = Ga2_ObjFindOrAddLit( p, pObj, f );
// create clauses // create clauses
Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), pLits, Lit, -1 ); Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), pLits, Lit, Gia_ObjId(p->pGia, pObj) );
return Lit; return Lit;
} }
// collect fanin literals // collect fanin literals
...@@ -901,7 +920,7 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) ...@@ -901,7 +920,7 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
// add new node // add new node
Lit = Ga2_ObjFindOrAddLit(p, pObj, f); Lit = Ga2_ObjFindOrAddLit(p, pObj, f);
Ga2_ManCnfAddDynamic( p, uTruth, Vec_IntArray(p->vLits), Lit, -1 ); Ga2_ManCnfAddDynamic( p, uTruth, Vec_IntArray(p->vLits), Lit, Gia_ObjId(p->pGia, pObj) );
} }
Ga2_ObjAddLit( p, pObj, f, Lit ); Ga2_ObjAddLit( p, pObj, f, Lit );
return Lit; return Lit;
...@@ -956,6 +975,7 @@ void Ga2_GlaPrepareCexAndMap( Ga2_Man_t * p, Abc_Cex_t ** ppCex, Vec_Int_t ** pv ...@@ -956,6 +975,7 @@ void Ga2_GlaPrepareCexAndMap( Ga2_Man_t * p, Abc_Cex_t ** ppCex, Vec_Int_t ** pv
vMap = Vec_IntAlloc( 1000 ); vMap = Vec_IntAlloc( 1000 );
Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i ) Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
{ {
if ( !i ) continue;
if ( Ga2_ObjIsAbs(p, pObj) ) if ( Ga2_ObjIsAbs(p, pObj) )
continue; continue;
assert( Ga2_ObjIsPpi(p, pObj) ); assert( Ga2_ObjIsPpi(p, pObj) );
...@@ -1018,6 +1038,66 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p ) ...@@ -1018,6 +1038,66 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Creates a new manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ga2_GlaAbsCount( Ga2_Man_t * p, int fRo, int fAnd )
{
Gia_Obj_t * pObj;
int i, Counter = 0;
if ( fRo )
Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
Counter += Gia_ObjIsRo(p->pGia, pObj);
else if ( fAnd )
Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
Counter += Gia_ObjIsAnd(pObj);
else assert( 0 );
return Counter;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ga2_ManAbsPrintFrame( Ga2_Man_t * p, int nFrames, int nConfls, int nCexes, clock_t Time, int fFinal )
{
if ( Abc_FrameIsBatchMode() && !fFinal )
return;
Abc_Print( 1, "%4d :", nFrames );
Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * Vec_IntSize(p->vAbs) / p->nMarked) );
Abc_Print( 1, "%6d", Vec_IntSize(p->vAbs) );
Abc_Print( 1, "%5d", Vec_IntSize(p->vValues)-Vec_IntSize(p->vAbs)-1 );
Abc_Print( 1, "%5d", Ga2_GlaAbsCount(p, 1, 0) );
Abc_Print( 1, "%6d", Ga2_GlaAbsCount(p, 0, 1) );
Abc_Print( 1, "%8d", nConfls );
if ( nCexes == 0 )
Abc_Print( 1, "%5c", '-' );
else
Abc_Print( 1, "%5d", nCexes );
Abc_PrintInt( sat_solver2_nvars(p->pSat) );
Abc_PrintInt( sat_solver2_nclauses(p->pSat) );
Abc_PrintInt( sat_solver2_nlearnts(p->pSat) );
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, "%s", fFinal ? "\n" : "\r" );
fflush( stdout );
}
/**Function*************************************************************
Synopsis [Performs gate-level abstraction.] Synopsis [Performs gate-level abstraction.]
Description [] Description []
...@@ -1031,11 +1111,9 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) ...@@ -1031,11 +1111,9 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{ {
Ga2_Man_t * p; Ga2_Man_t * p;
Vec_Int_t * vCore, * vPPis; Vec_Int_t * vCore, * vPPis;
clock_t clk = clock(); clock_t clk2, clk = clock();
int nAbs, nValues, Status, RetValue = -1; int nAbs, nValues, Status, RetValue = -1;
int i, c, f, Lit; int i, c, f, Lit;
// start the manager
p = Ga2_ManStart( pAig, pPars );
// check trivial case // check trivial case
assert( Gia_ManPoNum(pAig) == 1 ); assert( Gia_ManPoNum(pAig) == 1 );
ABC_FREE( pAig->pCexSeq ); ABC_FREE( pAig->pCexSeq );
...@@ -1068,7 +1146,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) ...@@ -1068,7 +1146,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin ); pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin );
Abc_Print( 1, "LearnStart = %d LearnDelta = %d LearnRatio = %d %%.\n", Abc_Print( 1, "LearnStart = %d LearnDelta = %d LearnRatio = %d %%.\n",
pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce ); pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce );
Abc_Print( 1, "Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" ); Abc_Print( 1, " Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" );
} }
// iterate unrolling // iterate unrolling
for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ ) for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ )
...@@ -1081,6 +1159,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) ...@@ -1081,6 +1159,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// unroll the circuit // unroll the circuit
for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ ) for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ )
{ {
int nConflsBeg = sat_solver2_nconflicts(p->pSat);
p->pPars->iFrame = f; p->pPars->iFrame = f;
// add static clauses to this timeframe // add static clauses to this timeframe
Ga2_ManAddAbsClauses( p, f ); Ga2_ManAddAbsClauses( p, f );
...@@ -1090,35 +1169,62 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) ...@@ -1090,35 +1169,62 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
for ( c = 0; ; c++ ) for ( c = 0; ; c++ )
{ {
// perform SAT solving // perform SAT solving
clk = clock(); clk2 = clock();
Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( Status == l_True ) // perform refinement if ( Status == l_True ) // perform refinement
{ {
p->timeSat += clock() - clk; p->timeSat += clock() - clk2;
clk = clock();
clk2 = clock();
vPPis = Ga2_ManRefine( p ); vPPis = Ga2_ManRefine( p );
p->timeCex += clock() - clk; p->timeCex += clock() - clk2;
if ( vPPis == NULL ) if ( vPPis == NULL )
goto finish; goto finish;
Ga2_ManAddToAbs( p, vPPis, p->nProofIds++ );
if ( c == 0 )
{
// start incremental proof manager
assert( p->pSat->pPrf2 == NULL );
p->pSat->pPrf2 = Prf_ManAlloc();
if ( p->pSat->pPrf2 )
{
p->nProofIds = 0;
Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vPPis) );
}
}
else
{
// resize the proof logger
if ( p->pSat->pPrf2 )
Prf_ManGrow( p->pSat->pPrf2, p->nProofIds + Vec_IntSize(vPPis) );
}
Ga2_ManAddToAbs( p, vPPis );
Vec_IntFree( vPPis ); Vec_IntFree( vPPis );
if ( pPars->fVerbose )
Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 0 );
// verify // verify
if ( Vec_IntCheckUnique(p->vAbs) ) if ( Vec_IntCheckUnique(p->vAbs) )
printf( "Vector has %d duplicated entries.\n", Vec_IntCheckUnique(p->vAbs) ); printf( "Vector has %d duplicated entries.\n", Vec_IntCheckUnique(p->vAbs) );
continue; continue;
} }
p->timeUnsat += clock() - clk; p->timeUnsat += clock() - clk2;
if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit ) // timeout
goto finish;
if ( Status == l_Undef ) // ran out of resources if ( Status == l_Undef ) // ran out of resources
goto finish; goto finish;
if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit ) // timeout
goto finish;
assert( RetValue == l_False ); assert( RetValue == l_False );
if ( c == 0 )
break;
// reduce abstraction
Ga2_ManShrinkAbs( p, nAbs, nValues );
// derive UNSAT core // derive UNSAT core
vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat ); vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat );
Ga2_ManShrinkAbs( p, nAbs, nValues ); Prf_ManStopP( &p->pSat->pPrf2 );
Ga2_ManAddToAbs( p, vCore, -1 ); // use UNSAT core
Ga2_ManAddToAbs( p, vCore );
Vec_IntFree( vCore ); Vec_IntFree( vCore );
p->nProofIds = 0;
// remember current limits // remember current limits
nAbs = Vec_IntSize(p->vAbs); nAbs = Vec_IntSize(p->vAbs);
nValues = Vec_IntSize(p->vValues); nValues = Vec_IntSize(p->vValues);
...@@ -1127,6 +1233,8 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) ...@@ -1127,6 +1233,8 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
printf( "Vector has %d duplicated entries.\n", Vec_IntCheckUnique(p->vAbs) ); printf( "Vector has %d duplicated entries.\n", Vec_IntCheckUnique(p->vAbs) );
break; break;
} }
if ( pPars->fVerbose )
Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 );
if ( c > 0 ) if ( c > 0 )
{ {
Vec_IntFreeP( &pAig->vGateClasses ); Vec_IntFreeP( &pAig->vGateClasses );
...@@ -1142,6 +1250,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) ...@@ -1142,6 +1250,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
} }
} }
finish: finish:
Prf_ManStopP( &p->pSat->pPrf2 );
// analize the results // analize the results
if ( pAig->pCexSeq == NULL ) if ( pAig->pCexSeq == NULL )
{ {
......
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