diff options
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/gia/gia.h | 2 | ||||
-rw-r--r-- | src/aig/gia/giaAbs.c | 6 | ||||
-rw-r--r-- | src/aig/gia/giaDup.c | 22 | ||||
-rw-r--r-- | src/aig/saig/saigAbsGla.c | 135 |
4 files changed, 151 insertions, 14 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index f53d05f3..5f2b94a4 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -603,7 +603,7 @@ Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia ); int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose ); extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame ); extern int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars ); -extern int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars ); +extern int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fUseCnf ); /*=== giaAiger.c ===========================================================*/ extern int Gia_FileSize( char * pFileName ); extern Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck ); diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index 511f418c..e30493a7 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -377,9 +377,9 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit SeeAlso [] ***********************************************************************/ -int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars ) +int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fUseCnf ) { - extern Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose ); + extern Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fUseCnf, int fVerbose ); Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars; Vec_Int_t * vGateClasses; Aig_Man_t * pAig; @@ -393,7 +393,7 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars ) */ // perform abstraction pAig = Gia_ManToAigSimple( pGia ); - vGateClasses = Aig_GlaManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fVerbose ); + vGateClasses = Aig_GlaManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, fUseCnf, p->fVerbose ); Aig_ManStop( pAig ); // update the map diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index b879cb05..974f39d0 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1584,6 +1584,27 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ) /**Function************************************************************* + Synopsis [Duplicates the AIG manager recursively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDupAbsGates_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj ) +{ + if ( ~pObj->Value ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManDupAbsGates_rec( pNew, Gia_ObjFanin0(pObj) ); + Gia_ManDupAbsGates_rec( pNew, Gia_ObjFanin1(pObj) ); + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} + +/**Function************************************************************* + Synopsis [Performs abstraction of the AIG to preserve the included gates.] Description [The array contains 1 for those objects (const, RO, AND) @@ -1642,6 +1663,7 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ) // create internal nodes Gia_ManForEachObjVec( vNodes, p, pObj, i ) pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +// Gia_ManDupAbsGates_rec( pNew, pObj ); // create PO Gia_ManForEachPo( p, pObj, i ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); diff --git a/src/aig/saig/saigAbsGla.c b/src/aig/saig/saigAbsGla.c index 5c8263eb..1de6221c 100644 --- a/src/aig/saig/saigAbsGla.c +++ b/src/aig/saig/saigAbsGla.c @@ -20,6 +20,7 @@ #include "saig.h" #include "satSolver.h" +#include "cnf.h" ABC_NAMESPACE_IMPL_START @@ -49,6 +50,12 @@ struct Aig_GlaMan_t_ Vec_Int_t * vObj2Vec; // maps obj ID into its vec ID Vec_Int_t * vVec2Var; // maps vec ID into its sat Var (nFrames per vec ID) Vec_Int_t * vVar2Inf; // maps sat Var into its frame and obj ID + // CNF computation + Vec_Ptr_t * vLeaves; + Vec_Ptr_t * vVolume; + Vec_Int_t * vCover; + Vec_Ptr_t * vObj2Cnf; + Vec_Int_t * vLits; // SAT solver sat_solver * pSat; // statistics @@ -153,7 +160,7 @@ static inline int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iV SeeAlso [] ***********************************************************************/ -Vec_Int_t * Aig_GlaCollectAssigned( Aig_Man_t * p, Vec_Int_t * vGateClasses ) +Vec_Int_t * Aig_GlaCollectAssigned_( Aig_Man_t * p, Vec_Int_t * vGateClasses ) { Vec_Int_t * vAssigned; Aig_Obj_t * pObj; @@ -242,6 +249,27 @@ void Aig_GlaCollectAbstr( Aig_GlaMan_t * p ) /**Function************************************************************* + Synopsis [Duplicates the AIG manager recursively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_GlaDeriveAbs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj ) +{ + if ( pObj->pData ) + return; + assert( Aig_ObjIsNode(pObj) ); + Aig_GlaDeriveAbs_rec( pNew, Aig_ObjFanin0(pObj) ); + Aig_GlaDeriveAbs_rec( pNew, Aig_ObjFanin1(pObj) ); + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +} + +/**Function************************************************************* + Synopsis [Derives abstraction.] Description [] @@ -274,7 +302,8 @@ Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p ) pObj->pData = Aig_ObjCreatePi(pNew); // create internal nodes Aig_ManForEachObjVec( p->vNodes, p->pAig, pObj, i ) - pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +// pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + Aig_GlaDeriveAbs_rec( pNew, pObj ); // create PO Saig_ManForEachPo( p->pAig, pObj, i ) pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); @@ -371,11 +400,47 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k ) Aig_GlaFetchVar(p, Aig_ObjFanin0(pObjLi), k-1), Aig_ObjFaninC0(pObjLi) ); } - assert( Aig_ObjIsNode(pObj) ); - return Aig_GlaAddNode( p->pSat, Aig_GlaFetchVar(p, pObj, k), - Aig_GlaFetchVar(p, Aig_ObjFanin0(pObj), k), - Aig_GlaFetchVar(p, Aig_ObjFanin1(pObj), k), - Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) ); + else + { + Vec_Int_t * vClauses; + int i, Entry; + assert( Aig_ObjIsNode(pObj) ); + if ( p->vObj2Cnf == NULL ) + return Aig_GlaAddNode( p->pSat, Aig_GlaFetchVar(p, pObj, k), + Aig_GlaFetchVar(p, Aig_ObjFanin0(pObj), k), + Aig_GlaFetchVar(p, Aig_ObjFanin1(pObj), k), + Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) ); + // derive clauses + assert( pObj->fMarkA ); + vClauses = Vec_PtrEntry( p->vObj2Cnf, Aig_ObjId(pObj) ); + if ( vClauses == NULL ) + { + Vec_PtrWriteEntry( p->vObj2Cnf, Aig_ObjId(pObj), (vClauses = Vec_IntAlloc(16)) ); + Cnf_ComputeClauses( p->pAig, pObj, p->vLeaves, p->vVolume, NULL, p->vCover, vClauses ); + } + // derive variables + Cnf_CollectLeaves( pObj, p->vLeaves, 0 ); + Vec_PtrForEachEntry( Aig_Obj_t *, p->vLeaves, pObj, i ) + Aig_GlaFetchVar( p, pObj, k ); + // translate clauses + assert( Vec_IntSize(vClauses) >= 2 ); + assert( Vec_IntEntry(vClauses, 0) == 0 ); + Vec_IntForEachEntry( vClauses, Entry, i ) + { + if ( Entry == 0 ) + { + Vec_IntClear( p->vLits ); + continue; + } + Vec_IntPush( p->vLits, (Entry & 1) ^ (2 * Aig_GlaFetchVar(p, Aig_ManObj(p->pAig, Entry >> 1), k)) ); + if ( i == Vec_IntSize(vClauses) - 1 || Vec_IntEntry(vClauses, i+1) == 0 ) + { + if ( !sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits)+Vec_IntSize(p->vLits) ) ) + return 0; + } + } + return 1; + } } /**Function************************************************************* @@ -389,7 +454,7 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k ) SeeAlso [] ***********************************************************************/ -Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig ) +Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig, int fUseCnf ) { Aig_GlaMan_t * p; int i; @@ -416,6 +481,17 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig ) Vec_IntPush( p->vVar2Inf, -1 ); Vec_IntPush( p->vVar2Inf, -1 ); + // CNF computation + if ( fUseCnf ) + { + p->vLeaves = Vec_PtrAlloc( 100 ); + p->vVolume = Vec_PtrAlloc( 100 ); + p->vCover = Vec_IntAlloc( 1 << 16 ); + p->vObj2Cnf = Vec_PtrStart( Aig_ManObjNumMax(pAig) ); + p->vLits = Vec_IntAlloc( 100 ); + Cnf_DeriveFastMark( pAig ); + } + // start the SAT solver p->pSat = sat_solver_new(); sat_solver_setnvars( p->pSat, 256 ); @@ -448,6 +524,16 @@ void Aig_GlaManStop( Aig_GlaMan_t * p ) Vec_IntFreeP( &p->vVec2Var ); Vec_IntFreeP( &p->vVar2Inf ); + if ( p->vObj2Cnf ) + { + Vec_PtrFreeP( &p->vLeaves ); + Vec_PtrFreeP( &p->vVolume ); + Vec_IntFreeP( &p->vCover ); + Vec_VecFreeP( (Vec_Vec_t **)&p->vObj2Cnf ); + Vec_IntFreeP( &p->vLits ); + Aig_ManCleanMarkA( p->pAig ); + } + if ( p->pSat ) sat_solver_delete( p->pSat ); ABC_FREE( p ); @@ -525,6 +611,34 @@ void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r, int v, int c ) /**Function************************************************************* + Synopsis [Prints current abstraction statistics.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_GlaExtendIncluded( Aig_GlaMan_t * p ) +{ + Aig_Obj_t * pObj; + int i, k; + Aig_ManForEachNode( p->pAig, pObj, i ) + { + if ( !Vec_IntEntry( p->vIncluded, i ) ) + continue; + Cnf_ComputeClauses( p->pAig, pObj, p->vLeaves, p->vVolume, NULL, p->vCover, p->vNodes ); + Vec_PtrForEachEntry( Aig_Obj_t *, p->vVolume, pObj, k ) + { + assert( Aig_ObjId(pObj) <= i ); + Vec_IntWriteEntry( p->vIncluded, Aig_ObjId(pObj), 1 ); + } + } +} + +/**Function************************************************************* + Synopsis [Performs gate-level localization abstraction.] Description [Returns array of objects included in the abstraction. This array @@ -536,7 +650,7 @@ void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r, int v, int c ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose ) +Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fUseCnf, int fVerbose ) { int nStart = 0; Vec_Int_t * vResult = NULL; @@ -558,7 +672,7 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in } // start the solver - p = Aig_GlaManStart( pAig ); + p = Aig_GlaManStart( pAig, fUseCnf ); p->nFramesMax = nFramesMax; p->nConfLimit = nConfLimit; p->fVerbose = fVerbose; @@ -660,6 +774,7 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in ABC_PRTP( "Total ", p->timeTotal, p->timeTotal ); } // prepare return value + Aig_GlaExtendIncluded( p ); vResult = p->vIncluded; p->vIncluded = NULL; Aig_GlaManStop( p ); return vResult; |