From dc56a65582a911ebfa4befcf57fe0ae722bff9d8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 31 Jul 2012 14:51:48 -0700 Subject: Scalable gate-level abstraction. --- src/aig/gia/giaAbsGla2.c | 130 ++++++++++++++++++++++++++++------------------- 1 file changed, 79 insertions(+), 51 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index da36b849..88b168fa 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -57,12 +57,12 @@ struct Ga2_Man_t_ Vec_Ptr_t * vId2Lit; // mapping, for each timeframe, of object ID into SAT literal sat_solver2 * pSat; // incremental SAT solver int nSatVars; // the number of SAT variables + int nCexes; // the number of counter-examples + int nObjAdded; // objs added during refinement // temporaries Vec_Int_t * vLits; Vec_Int_t * vIsopMem; char * pSopSizes, ** pSops; // CNF representation - int nCexes; // the number of counter-examples - int nObjAdded; // objs added during refinement // statistics clock_t timeStart; clock_t timeInit; @@ -97,15 +97,11 @@ 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) >= 0 && Ga2_ObjId(p,pObj) < Vec_IntSize(p->vValues) ); - if ( f == Vec_PtrSize(p->vId2Lit) ) - Vec_PtrPush( p->vId2Lit, Vec_IntStartFull(Vec_IntSize(p->vValues)) ); - assert( f < Vec_PtrSize(p->vId2Lit) ); return Vec_IntEntry( Ga2_MapFrameMap(p, f), Ga2_ObjId(p,pObj) ); } // inserts literal of this object static inline void Ga2_ObjAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f, int Lit ) { -// assert( Lit > 1 || Gia_ObjIsConst0(pObj) ); assert( Lit > 1 ); assert( Ga2_ObjFindLit(p, pObj, f) == -1 ); Vec_IntSetEntry( Ga2_MapFrameMap(p, f), Ga2_ObjId(p,pObj), Lit ); @@ -119,7 +115,6 @@ static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) Lit = toLitCond( p->nSatVars++, 0 ); Ga2_ObjAddLit( p, pObj, f, Lit ); } -// assert( Lit > 1 || Gia_ObjIsConst0(pObj) ); assert( Lit > 1 ); return Lit; } @@ -245,6 +240,9 @@ int Ga2_ManMarkup( Gia_Man_t * p, int N ) Vec_Int_t * vLeaves; Gia_Obj_t * pObj; int i, k, Leaf, CountMarks; + vLeaves = Vec_IntAlloc( 100 ); + +/* // label nodes with multiple fanouts and inputs MUXes Gia_ManForEachObj( p, pObj, i ) { @@ -271,7 +269,6 @@ int Ga2_ManMarkup( Gia_Man_t * p, int N ) pObj->fPhase = 1; } // add marks when needed - vLeaves = Vec_IntAlloc( 100 ); Gia_ManForEachAnd( p, pObj, i ) { if ( !pObj->fPhase ) @@ -281,6 +278,10 @@ int Ga2_ManMarkup( Gia_Man_t * p, int N ) if ( Vec_IntSize(vLeaves) > N ) Ga2_ManBreakTree_rec( p, pObj, 1, N ); } +*/ + Gia_ManForEachObj( p, pObj, i ) + pObj->fPhase = !Gia_ObjIsCo(pObj); + // verify that the tree is split correctly Vec_IntFreeP( &p->vMapping ); p->vMapping = Vec_IntStart( Gia_ManObjNum(p) ); @@ -372,12 +373,13 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) Vec_PtrPush( p->vCnfs, Vec_IntAlloc(0) ); // abstraction p->vIds = Vec_IntStartFull( Gia_ManObjNum(pGia) ); - p->vProofIds = Vec_IntAlloc(0); + p->vProofIds = Vec_IntAlloc( 0 ); p->vAbs = Vec_IntAlloc( 1000 ); p->vValues = Vec_IntAlloc( 1000 ); - // add constant + // add constant node to abstraction Ga2_ObjSetId( p, Gia_ManConst0(pGia), 0 ); Vec_IntPush( p->vValues, 0 ); + Vec_IntPush( p->vAbs, 0 ); // refinement p->pRnm = Rnm_ManStart( pGia ); // SAT solver and variables @@ -618,9 +620,13 @@ static inline void Ga2_ManCnfAddStatic( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_In else if ( Literal != 0 ) assert( 0 ); } +// for ( b = 0; b < nClaLits; b++ ) +// printf( "%d ", ClaLits[b] ); +// printf( "\n" ); sat_solver2_addclause( p->pSat, ClaLits, ClaLits+nClaLits, ProofId ); } } + b = 0; } @@ -657,7 +663,7 @@ void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs ) assert( Ga2_ObjCnf0(p, pObj) == NULL ); if ( !fAbs ) return; - assert( Vec_IntFind(p->vAbs, Gia_ObjId(p->pGia, pObj)) == -1 ); +// assert( Vec_IntFind(p->vAbs, Gia_ObjId(p->pGia, pObj)) == -1 ); Vec_IntPush( p->vAbs, Gia_ObjId(p->pGia, pObj) ); assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) ); // compute parameters @@ -673,6 +679,7 @@ void Ga2_ManAddToAbsOneStatic( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) Vec_Int_t * vLeaves; Gia_Obj_t * pFanin; int k, iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f ); + assert( !Gia_ObjIsConst0(pObj) ); assert( iLitOut > 1 ); assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) ); if ( f == 0 && Gia_ObjIsRo(p->pGia, pObj) ) @@ -692,13 +699,23 @@ void Ga2_ManAddToAbsOneStatic( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f ) { + int fSimple = 1; Gia_Obj_t * pObj; - int i; + int i, Lit; +/* + Vec_Int_t * vMap = (f < Vec_PtrSize(p->vId2Lit) ? Ga2_MapFrameMap( p, f ) : NULL); // Ga2_ObjAddLit( p, Gia_ManConst0(p->pGia), f, 0 ); - int Lit = Ga2_ObjFindOrAddLit( p, Gia_ManConst0(p->pGia), f ); - Lit = Abc_LitNot( Lit ); - sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, 0 ); - + if ( f == 5 ) + { + int s = 0; + } +*/ + if ( fSimple ) + { + Lit = Ga2_ObjFindOrAddLit( p, Gia_ManConst0(p->pGia), f ); + Lit = Abc_LitNot( Lit ); + sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, 0 ); + } Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i ) if ( i >= p->LimAbs ) Ga2_ManAddToAbsOneStatic( p, pObj, f ); @@ -706,7 +723,7 @@ void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f ) void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd ) { - Vec_Int_t * vLeaves, * vMap; + Vec_Int_t * vLeaves; Gia_Obj_t * pObj, * pFanin; int f, i, k; // add abstraction objects @@ -719,39 +736,32 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd ) // add PPI objects Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i ) { -/* - if ( Gia_ObjIsRo(p->pGia, pObj) ) - { - pFanin = Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj)); - if ( !Ga2_ObjId( p, pFanin ) ) - Ga2_ManSetupNode( p, pFanin, 0 ); - continue; - } -*/ vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) if ( Ga2_ObjId( p, pFanin ) == -1 ) Ga2_ManSetupNode( p, pFanin, 0 ); } - // clean mapping in the timeframes - Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i ) - Vec_IntFillExtra( vMap, Vec_IntSize(p->vValues), -1 ); // add new clauses to the timeframes for ( f = 0; f <= p->pPars->iFrame; f++ ) + { + Vec_IntFillExtra( Ga2_MapFrameMap(p, f), Vec_IntSize(p->vValues), -1 ); Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i ) Ga2_ManAddToAbsOneStatic( p, pObj, f ); + } } -void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues ) +void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues, int nSatVars ) { Vec_Int_t * vMap; Gia_Obj_t * pObj; int i; - assert( nAbs >= 0 ); + assert( nAbs > 0 ); assert( nValues > 0 ); + assert( nSatVars > 0 ); // shrink abstraction Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i ) { + if ( !i ) continue; assert( Ga2_ObjCnf0(p, pObj) != NULL ); assert( Ga2_ObjCnf1(p, pObj) != NULL ); if ( i < nAbs ) @@ -774,7 +784,9 @@ void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues ) Vec_PtrShrink( p->vCnfs, 2 * nValues ); // clean mapping for each timeframe Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i ) - Vec_IntShrink( vMap, nValues ); + Vec_IntClear( vMap ); + // shrink SAT variables + p->nSatVars = nSatVars; } /**Function************************************************************* @@ -840,23 +852,23 @@ Vec_Int_t * Ga2_ManAbsDerive( Gia_Man_t * p ) void Ga2_ManRestart( Ga2_Man_t * p ) { Vec_Int_t * vToAdd; - int Lit; + int Lit = 1; assert( p->pGia != NULL && p->pGia->vGateClasses != NULL ); assert( Gia_ManPi(p->pGia, 0)->fPhase ); // marks are set - // clear mappings from objects - Ga2_ManShrinkAbs( p, 0, 1 ); // clear SAT variable numbers (begin with 1) if ( p->pSat ) sat_solver2_delete( p->pSat ); p->pSat = sat_solver2_new(); - p->nSatVars = 1; // add clause x0 = 0 (lit0 = 1; lit1 = 0) - Lit = 1; sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, 0 ); - // start abstraction + // remove previous abstraction + Ga2_ManShrinkAbs( p, 1, 1, 1 ); + // start new abstraction vToAdd = Ga2_ManAbsDerive( p->pGia ); + assert( p->pSat->pPrf2 == NULL ); + assert( p->pPars->iFrame < 0 ); Ga2_ManAddToAbs( p, vToAdd ); Vec_IntFree( vToAdd ); - p->LimAbs = Vec_IntSize(p->vAbs) + 1; + p->LimAbs = Vec_IntSize(p->vAbs); p->LimPpi = Vec_IntSize(p->vValues); // set runtime limit if ( p->pPars->nTimeOut ) @@ -1016,7 +1028,6 @@ void Ga2_GlaPrepareCexAndMap( Ga2_Man_t * p, Abc_Cex_t ** ppCex, Vec_Int_t ** pv vMap = Vec_IntAlloc( 1000 ); Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i ) { - pObj->Value = 0; if ( !i ) continue; Id = Ga2_ObjId(p, pObj); k = Gia_ObjId(p->pGia, pObj); @@ -1157,7 +1168,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Ga2_Man_t * p; Vec_Int_t * vCore, * vPPis; clock_t clk2, clk = clock(); - int nAbs, nValues, Status, RetValue = -1; + int Status, RetValue = -1; int i, c, f, Lit; // check trivial case assert( Gia_ManPoNum(pAig) == 1 ); @@ -1196,21 +1207,30 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) // iterate unrolling for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ ) { + // remember the timeframe + p->pPars->iFrame = -1; // create new SAT solver Ga2_ManRestart( p ); - // remember current limits - nAbs = Vec_IntSize(p->vAbs); - nValues = Vec_IntSize(p->vValues); // unroll the circuit for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ ) { + // remember current limits int nConflsBeg = sat_solver2_nconflicts(p->pSat); + int nAbs = Vec_IntSize(p->vAbs); + int nValues = Vec_IntSize(p->vValues); + int nVarsOld; + // extend and clear storage + if ( f == Vec_PtrSize(p->vId2Lit) ) + Vec_PtrPush( p->vId2Lit, Vec_IntAlloc(0) ); + Vec_IntFillExtra( Ga2_MapFrameMap(p, f), Vec_IntSize(p->vValues), -1 ); + // remember the timeframe p->pPars->iFrame = f; // add static clauses to this timeframe Ga2_ManAddAbsClauses( p, f ); // get the output literal Lit = Ga2_ManUnroll_rec( p, Gia_ManPo(pAig,0), f ); // check for counter-examples + nVarsOld = p->nSatVars; for ( c = 0; ; c++ ) { // perform SAT solving @@ -1224,10 +1244,17 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) vPPis = Ga2_ManRefine( p ); p->timeCex += clock() - clk2; if ( vPPis == NULL ) + { + if ( pPars->fVerbose ) + Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 ); goto finish; + } if ( c == 0 ) { + // create bookmark to be used for rollback + assert( nVarsOld == p->pSat->size ); + sat_solver2_bookmark( p->pSat ); // start incremental proof manager assert( p->pSat->pPrf2 == NULL ); p->pSat->pPrf2 = Prf_ManAlloc(); @@ -1262,17 +1289,17 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) assert( RetValue == l_False ); if ( c == 0 ) break; - // reduce abstraction - Ga2_ManShrinkAbs( p, nAbs, nValues ); - // derive UNSAT core + + // derive the core + assert( p->pSat->pPrf2 != NULL ); vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat ); Prf_ManStopP( &p->pSat->pPrf2 ); - // use UNSAT core + // update the SAT solver + sat_solver2_rollback( p->pSat ); + // reduce abstraction + Ga2_ManShrinkAbs( p, nAbs, nValues, nVarsOld ); Ga2_ManAddToAbs( p, vCore ); Vec_IntFree( vCore ); - // remember current limits - nAbs = Vec_IntSize(p->vAbs); - nValues = Vec_IntSize(p->vValues); // verify if ( Vec_IntCheckUnique(p->vAbs) ) printf( "Vector has %d duplicated entries.\n", Vec_IntCheckUnique(p->vAbs) ); @@ -1284,6 +1311,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) { Vec_IntFreeP( &pAig->vGateClasses ); pAig->vGateClasses = Ga2_ManAbsTranslate( p ); + printf( "\n" ); break; // temporary } } -- cgit v1.2.3