diff options
author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-06-06 23:16:55 -0700 |
---|---|---|
committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-06-06 23:16:55 -0700 |
commit | 584e28e8f4f8beb70e577c38719f8e7b532123e1 (patch) | |
tree | d8a78ae811e2a1cd14f88518d574e90a58d0aed2 /src/aig | |
parent | 10f5e944c99626d5f8e68aa874e43462569cabf7 (diff) | |
parent | e140ef7e5a45b23823bdf1189070573439966ac8 (diff) | |
download | abc-584e28e8f4f8beb70e577c38719f8e7b532123e1.tar.gz abc-584e28e8f4f8beb70e577c38719f8e7b532123e1.tar.bz2 abc-584e28e8f4f8beb70e577c38719f8e7b532123e1.zip |
merge
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/gia/gia.h | 10 | ||||
-rw-r--r-- | src/aig/gia/giaDup.c | 51 | ||||
-rw-r--r-- | src/aig/gia/giaEsop.c | 2 | ||||
-rw-r--r-- | src/aig/gia/giaIf.c | 54 | ||||
-rw-r--r-- | src/aig/gia/giaSupp.c | 887 | ||||
-rw-r--r-- | src/aig/gia/module.make | 1 | ||||
-rw-r--r-- | src/aig/miniaig/miniaig.h | 12 | ||||
-rw-r--r-- | src/aig/miniaig/minilut.h | 20 | ||||
-rw-r--r-- | src/aig/miniaig/ndr.h | 10 |
9 files changed, 1022 insertions, 25 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 5ad87008..f8e36a4f 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -577,6 +577,7 @@ static inline int Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pO static inline int Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds - 1); } static inline void Gia_ObjSetTravIdCurrentId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); p->pTravIds[Id] = p->nTravIds; } static inline int Gia_ObjIsTravIdCurrentId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); return (p->pTravIds[Id] == p->nTravIds); } +static inline int Gia_ObjIsTravIdPreviousId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); return (p->pTravIds[Id] == p->nTravIds - 1); } static inline void Gia_ManTimeClean( Gia_Man_t * p ) { int i; assert( p->vTiming != NULL ); Vec_FltFill(p->vTiming, 3*Gia_ManObjNum(p), 0); for ( i = 0; i < Gia_ManObjNum(p); i++ ) Vec_FltWriteEntry( p->vTiming, 3*i+1, (float)(ABC_INFINITY) ); } static inline void Gia_ManTimeStart( Gia_Man_t * p ) { assert( p->vTiming == NULL ); p->vTiming = Vec_FltAlloc(0); Gia_ManTimeClean( p ); } @@ -1464,6 +1465,15 @@ extern int Gia_ManComputeOneWin( Gia_Man_t * p, int iPivot, Vec_ /*=== giaStg.c ============================================================*/ extern void Gia_ManStgPrint( FILE * pFile, Vec_Int_t * vLines, int nIns, int nOuts, int nStates ); extern Gia_Man_t * Gia_ManStgRead( char * pFileName, int kHot, int fVerbose ); +/*=== giaSupp.c ============================================================*/ +typedef struct Gia_ManMin_t_ Gia_ManMin_t; +extern Gia_ManMin_t * Gia_ManSuppStart( Gia_Man_t * pGia ); +extern void Gia_ManSuppStop( Gia_ManMin_t * p ); +extern int Gia_ManSupportAnd( Gia_ManMin_t * p, int iLit0, int iLit1 ); +typedef struct Gia_Man2Min_t_ Gia_Man2Min_t; +extern Gia_Man2Min_t * Gia_Man2SuppStart( Gia_Man_t * pGia ); +extern void Gia_Man2SuppStop( Gia_Man2Min_t * p ); +extern int Gia_Man2SupportAnd( Gia_Man2Min_t * p, int iLit0, int iLit1 ); /*=== giaSweep.c ============================================================*/ extern Gia_Man_t * Gia_ManFraigSweepSimple( Gia_Man_t * p, void * pPars ); extern Gia_Man_t * Gia_ManSweepWithBoxes( Gia_Man_t * p, void * pParsC, void * pParsS, int fConst, int fEquiv, int fVerbose, int fVerbEquivs ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index ee709df4..5e7dc639 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1638,6 +1638,57 @@ Gia_Man_t * Gia_ManDupExist( Gia_Man_t * p, int iVar ) /**Function************************************************************* + Synopsis [Existentially quantified given variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupUniv( Gia_Man_t * p, int iVar ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i; + assert( iVar >= 0 && iVar < Gia_ManPiNum(p) ); + assert( Gia_ManRegNum(p) == 0 ); + Gia_ManFillValue( p ); + // find the cofactoring variable + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManHashAlloc( pNew ); + // compute negative cofactor + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 0 ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachPo( p, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + // compute the positive cofactor + Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 1 ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + // create OR gate + Gia_ManForEachPo( p, pObj, i ) + { + if ( i == 0 ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashAnd(pNew, Gia_ObjFanin0Copy(pObj), pObj->Value) ); + else + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + Synopsis [Existentially quantifies the given variable.] Description [] diff --git a/src/aig/gia/giaEsop.c b/src/aig/gia/giaEsop.c index 13627c0c..a819bc20 100644 --- a/src/aig/gia/giaEsop.c +++ b/src/aig/gia/giaEsop.c @@ -167,7 +167,7 @@ Vec_Wec_t * Eso_ManCoverDerive( Eso_Man_t * p, Vec_Ptr_t * vCover ) } } } - assert( Abc_MaxInt(Vec_WecSize(vRes), 8) == Vec_WecCap(vRes) ); + //assert( Abc_MaxInt(Vec_WecSize(vRes), 8) == Vec_WecCap(vRes) ); return vRes; } Gia_Man_t * Eso_ManCoverConvert( Eso_Man_t * p, Vec_Ptr_t * vCover ) diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index ab80a762..0f656b03 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -1498,7 +1498,7 @@ int Gia_ManFromIfLogicFindLut( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t * p SeeAlso [] ***********************************************************************/ -void Gia_ManFromIfGetConfig( Vec_Int_t * vConfigs, If_Man_t * pIfMan, If_Cut_t * pCutBest, int fCompl ) +void Gia_ManFromIfGetConfig( Vec_Int_t * vConfigs, If_Man_t * pIfMan, If_Cut_t * pCutBest, int iLit, Vec_Str_t * vConfigsStr ) { If_Obj_t * pIfObj; word * pPerm = If_DsdManGetFuncConfig( pIfMan->pIfDsdMan, If_CutDsdLit(pIfMan, pCutBest) ); // cell input -> DSD input @@ -1537,10 +1537,33 @@ void Gia_ManFromIfGetConfig( Vec_Int_t * vConfigs, If_Man_t * pIfMan, If_Cut_t * } // remember complementation assert( nTtBitNum + nPermBitNum < 32 * nIntNum ); - if ( Abc_LitIsCompl(If_CutDsdLit(pIfMan, pCutBest)) ^ pCutBest->fCompl ^ fCompl ) + if ( Abc_LitIsCompl(If_CutDsdLit(pIfMan, pCutBest)) ^ pCutBest->fCompl ^ Abc_LitIsCompl(iLit) ) Abc_TtSetBit( pArray, nTtBitNum + nPermBitNum ); // update count Vec_IntAddToEntry( vConfigs, 0, 1 ); + // write configs + if ( vConfigsStr ) + { + Vec_StrPrintF( vConfigsStr, "%d", Abc_Lit2Var(iLit) ); + Vec_StrPush( vConfigsStr, ' ' ); + for ( i = 0; i < nTtBitNum; i++ ) + Vec_StrPush( vConfigsStr, (char)(Abc_TtGetBit(pArray, i) ? '1' : '0') ); + Vec_StrPush( vConfigsStr, ' ' ); + Vec_StrPush( vConfigsStr, ' ' ); + for ( v = 0; v < nVarNum; v++ ) + { + for ( i = 0; i < nPermBitOne; i++ ) + { + Vec_StrPush( vConfigsStr, (char)(Abc_TtGetBit(pArray, nTtBitNum + v * nPermBitOne + i) ? '1' : '0') ); + if ( i == 0 ) + Vec_StrPush( vConfigsStr, ' ' ); + } + Vec_StrPush( vConfigsStr, ' ' ); + Vec_StrPush( vConfigsStr, ' ' ); + } + Vec_StrPush( vConfigsStr, (char)(Abc_TtGetBit(pArray, nTtBitNum + nPermBitNum) ? '1' : '0') ); + Vec_StrPush( vConfigsStr, '\n' ); + } } int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, Gia_Man_t * pTemp, If_Cut_t * pCutBest, Ifn_Ntk_t * pNtkCell, int nLutMax, Vec_Int_t * vLeaves, Vec_Int_t * vLits, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vConfigs ) { @@ -1730,11 +1753,13 @@ int Gia_ManFromIfLogicAndVars( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Cut_t * p ***********************************************************************/ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) { + int fWriteConfigs = 1; Gia_Man_t * pNew, * pHashed = NULL; If_Cut_t * pCutBest; If_Obj_t * pIfObj, * pIfLeaf; Vec_Int_t * vMapping, * vMapping2, * vPacking = NULL, * vConfigs = NULL; Vec_Int_t * vLeaves, * vLeaves2, * vCover, * vLits; + Vec_Str_t * vConfigsStr = NULL; Ifn_Ntk_t * pNtkCell = NULL; sat_solver * pSat = NULL; int i, k, Entry; @@ -1757,6 +1782,8 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) vConfigs = Vec_IntAlloc( 1000 ); Vec_IntPush( vConfigs, 0 ); Vec_IntPush( vConfigs, nConfigInts ); + if ( fWriteConfigs ) + vConfigsStr = Vec_StrAlloc( 1000 ); } // create new manager pNew = Gia_ManStart( If_ManObjNum(pIfMan) ); @@ -1840,7 +1867,7 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) pIfObj->iCopy = Gia_ManFromIfLogicNode( pIfMan, pNew, i, vLeaves, vLeaves2, pTruth, pIfMan->pPars->pLutStruct, vCover, vMapping, vMapping2, vPacking, (pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u), pIfMan->pPars->fEnableCheck07 ); pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl ); if ( vConfigs && Vec_IntSize(vLeaves) > 1 && !Gia_ObjIsCi(Gia_ManObj(pNew, Abc_Lit2Var(pIfObj->iCopy))) && pIfObj->iCopy > 1 ) - Gia_ManFromIfGetConfig( vConfigs, pIfMan, pCutBest, Abc_LitIsCompl(pIfObj->iCopy) ); + Gia_ManFromIfGetConfig( vConfigs, pIfMan, pCutBest, pIfObj->iCopy, vConfigsStr ); } else { @@ -1921,6 +1948,27 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) Gia_ManForEachCi( pNew, pObj, i ) assert( !Gia_ObjIsLut(pNew, Gia_ObjId(pNew, pObj)) ); } + // dump configuration strings + if ( vConfigsStr ) + { + FILE * pFile; int status; + char * pStr, Buffer[1000] = {0}; + char * pNameGen = pIfMan->pName? Extra_FileNameGeneric( pIfMan->pName ) : "nameless_"; + sprintf( Buffer, "%s_configs.txt", pNameGen ); + ABC_FREE( pNameGen ); + pFile = fopen( Buffer, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\".\n", Buffer ); + return pNew; + } + Vec_StrPush( vConfigsStr, '\0' ); + pStr = Vec_StrArray(vConfigsStr); + status = fwrite( pStr, strlen(pStr), 1, pFile ); + Vec_StrFree( vConfigsStr ); + fclose( pFile ); + printf( "Finished dumping configs into file \"%s\".\n", Buffer ); + } return pNew; } diff --git a/src/aig/gia/giaSupp.c b/src/aig/gia/giaSupp.c new file mode 100644 index 00000000..d9ba4e70 --- /dev/null +++ b/src/aig/gia/giaSupp.c @@ -0,0 +1,887 @@ +/**CFile**************************************************************** + + FileName [giaSupp.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Support minimization for AIGs.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaSupp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "sat/satoko/satoko.h" +#include "sat/satoko/solver.h" + +#ifdef ABC_USE_CUDD +#include "bdd/extrab/extraBdd.h" +#endif + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#ifdef ABC_USE_CUDD + +struct Gia_ManMin_t_ +{ + // problem formulation + Gia_Man_t * pGia; + int iLits[2]; + // structural information + Vec_Int_t * vCis[2]; + Vec_Int_t * vObjs[2]; + Vec_Int_t * vCleared; + // intermediate functions + DdManager * dd; + Vec_Ptr_t * vFuncs; + Vec_Int_t * vSupp; +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Create/delete the data representation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_ManMin_t * Gia_ManSuppStart( Gia_Man_t * pGia ) +{ + Gia_ManMin_t * p; + p = ABC_CALLOC( Gia_ManMin_t, 1 ); + p->pGia = pGia; + p->vCis[0] = Vec_IntAlloc( 512 ); + p->vCis[1] = Vec_IntAlloc( 512 ); + p->vObjs[0] = Vec_IntAlloc( 512 ); + p->vObjs[1] = Vec_IntAlloc( 512 ); + p->vCleared = Vec_IntAlloc( 512 ); + p->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); +// Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT ); + Cudd_AutodynDisable( p->dd ); + p->vFuncs = Vec_PtrAlloc( 10000 ); + p->vSupp = Vec_IntAlloc( 10000 ); + return p; +} +void Gia_ManSuppStop( Gia_ManMin_t * p ) +{ + Vec_IntFreeP( &p->vCis[0] ); + Vec_IntFreeP( &p->vCis[1] ); + Vec_IntFreeP( &p->vObjs[0] ); + Vec_IntFreeP( &p->vObjs[1] ); + Vec_IntFreeP( &p->vCleared ); + Vec_PtrFreeP( &p->vFuncs ); + Vec_IntFreeP( &p->vSupp ); + printf( "Refs = %d. \n", Cudd_CheckZeroRef( p->dd ) ); + Cudd_Quit( p->dd ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Compute variables, which are not in the support.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManFindRemoved( Gia_ManMin_t * p ) +{ + extern void ddSupportStep2( DdNode * f, int * support ); + extern void ddClearFlag2( DdNode * f ); + + //int fVerbose = 1; + int nBddLimit = 100000; + int nPart0 = Vec_IntSize(p->vCis[0]); + int n, i, iObj, nVars = 0; + DdNode * bFunc0, * bFunc1, * bFunc; + Vec_PtrFillExtra( p->vFuncs, Gia_ManObjNum(p->pGia), NULL ); + // assign variables + for ( n = 0; n < 2; n++ ) + Vec_IntForEachEntry( p->vCis[n], iObj, i ) + Vec_PtrWriteEntry( p->vFuncs, iObj, Cudd_bddIthVar(p->dd, nVars++) ); + // create nodes + for ( n = 0; n < 2; n++ ) + Vec_IntForEachEntry( p->vObjs[n], iObj, i ) + { + Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj ); + bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(p->vFuncs, Gia_ObjFaninId0(pObj, iObj)), Gia_ObjFaninC0(pObj) ); + bFunc1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(p->vFuncs, Gia_ObjFaninId1(pObj, iObj)), Gia_ObjFaninC1(pObj) ); + bFunc = Cudd_bddAndLimit( p->dd, bFunc0, bFunc1, nBddLimit ); + assert( bFunc != NULL ); + Cudd_Ref( bFunc ); + Vec_PtrWriteEntry( p->vFuncs, iObj, bFunc ); + } + // create new node + bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(p->vFuncs, Abc_Lit2Var(p->iLits[0])), Abc_LitIsCompl(p->iLits[0]) ); + bFunc1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(p->vFuncs, Abc_Lit2Var(p->iLits[1])), Abc_LitIsCompl(p->iLits[1]) ); + bFunc = Cudd_bddAndLimit( p->dd, bFunc0, bFunc1, nBddLimit ); + assert( bFunc != NULL ); + Cudd_Ref( bFunc ); + //if ( fVerbose ) Extra_bddPrint( p->dd, bFunc ), printf( "\n" ); + // collect support + Vec_IntFill( p->vSupp, nVars, 0 ); + ddSupportStep2( Cudd_Regular(bFunc), Vec_IntArray(p->vSupp) ); + ddClearFlag2( Cudd_Regular(bFunc) ); + // find variables not present in the support + Vec_IntClear( p->vCleared ); + for ( i = 0; i < nVars; i++ ) + if ( Vec_IntEntry(p->vSupp, i) == 0 ) + Vec_IntPush( p->vCleared, i < nPart0 ? Vec_IntEntry(p->vCis[0], i) : Vec_IntEntry(p->vCis[1], i-nPart0) ); + //printf( "%d(%d)%d ", Cudd_SupportSize(p->dd, bFunc), Vec_IntSize(p->vCleared), Cudd_DagSize(bFunc) ); + // deref results + Cudd_RecursiveDeref( p->dd, bFunc ); + for ( n = 0; n < 2; n++ ) + Vec_IntForEachEntry( p->vObjs[n], iObj, i ) + Cudd_RecursiveDeref( p->dd, (DdNode *)Vec_PtrEntry(p->vFuncs, iObj) ); + //Vec_IntPrint( p->vCleared ); + return Vec_IntSize(p->vCleared); +} + +/**Function************************************************************* + + Synopsis [Compute variables, which are not in the support.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManRebuildOne( Gia_ManMin_t * p, int n ) +{ + int i, iObj, iGiaLitNew = -1; + Vec_Int_t * vTempIns = p->vCis[n]; + Vec_Int_t * vTempNds = p->vObjs[n]; + Vec_Int_t * vCopies = &p->pGia->vCopies; + Vec_IntFillExtra( vCopies, Gia_ManObjNum(p->pGia), -1 ); + assert( p->iLits[n] >= 2 ); + // process inputs + Vec_IntForEachEntry( vTempIns, iObj, i ) + Vec_IntWriteEntry( vCopies, iObj, Abc_Var2Lit(iObj, 0) ); + // process constants + assert( Vec_IntSize(p->vCleared) > 0 ); + Vec_IntForEachEntry( p->vCleared, iObj, i ) + Vec_IntWriteEntry( vCopies, iObj, 0 ); + if ( Vec_IntSize(vTempNds) == 0 ) + iGiaLitNew = Vec_IntEntry( vCopies, Abc_Lit2Var(p->iLits[n]) ); + else + { + Vec_IntForEachEntry( vTempNds, iObj, i ) + { + Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj ); + int iGiaLit0 = Vec_IntEntry( vCopies, Gia_ObjFaninId0p(p->pGia, pObj) ); + int iGiaLit1 = Vec_IntEntry( vCopies, Gia_ObjFaninId1p(p->pGia, pObj) ); + iGiaLit0 = Abc_LitNotCond( iGiaLit0, Gia_ObjFaninC0(pObj) ); + iGiaLit1 = Abc_LitNotCond( iGiaLit1, Gia_ObjFaninC1(pObj) ); + iGiaLitNew = Gia_ManHashAnd( p->pGia, iGiaLit0, iGiaLit1 ); + Vec_IntWriteEntry( vCopies, iObj, iGiaLitNew ); + } + assert( Abc_Lit2Var(p->iLits[n]) == iObj ); + } + return Abc_LitNotCond( iGiaLitNew, Abc_LitIsCompl(p->iLits[n]) ); +} + +/**Function************************************************************* + + Synopsis [Collect nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManGatherSupp_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vCis, Vec_Int_t * vObjs ) +{ + int Val0, Val1; + Gia_Obj_t * pObj; + if ( Gia_ObjIsTravIdPreviousId(p, iObj) ) + return 1; + if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) + return 0; + Gia_ObjSetTravIdCurrentId(p, iObj); + pObj = Gia_ManObj( p, iObj ); + if ( Gia_ObjIsCi(pObj) ) + { + Vec_IntPush( vCis, iObj ); + return 0; + } + assert( Gia_ObjIsAnd(pObj) ); + Val0 = Gia_ManGatherSupp_rec( p, Gia_ObjFaninId0(pObj, iObj), vCis, vObjs ); + Val1 = Gia_ManGatherSupp_rec( p, Gia_ObjFaninId1(pObj, iObj), vCis, vObjs ); + Vec_IntPush( vObjs, iObj ); + return Val0 || Val1; +} +int Gia_ManGatherSupp( Gia_ManMin_t * p ) +{ + int n, Overlap = 0; + Gia_ManIncrementTravId( p->pGia ); + for ( n = 0; n < 2; n++ ) + { + Vec_IntClear( p->vCis[n] ); + Vec_IntClear( p->vObjs[n] ); + Gia_ManIncrementTravId( p->pGia ); + Overlap = Gia_ManGatherSupp_rec( p->pGia, Abc_Lit2Var(p->iLits[n]), p->vCis[n], p->vObjs[n] ); + assert( n || !Overlap ); + } + return Overlap; +} + +/**Function************************************************************* + + Synopsis [Takes a literal and returns a support-minized literal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManSupportAnd( Gia_ManMin_t * p, int iLit0, int iLit1 ) +{ + int iLitNew0, iLitNew1; + p->iLits[0] = iLit0; + p->iLits[1] = iLit1; + if ( iLit0 < 2 || iLit1 < 2 || !Gia_ManGatherSupp(p) || !Gia_ManFindRemoved(p) ) + return Gia_ManHashAnd( p->pGia, iLit0, iLit1 ); + iLitNew0 = Gia_ManRebuildOne( p, 0 ); + iLitNew1 = Gia_ManRebuildOne( p, 1 ); + return Gia_ManHashAnd( p->pGia, iLitNew0, iLitNew1 ); +} + + +#else + +Gia_ManMin_t * Gia_ManSuppStart( Gia_Man_t * pGia ) { return NULL; } +int Gia_ManSupportAnd( Gia_ManMin_t * p, int iLit0, int iLit1 ) { return 0; } +void Gia_ManSuppStop( Gia_ManMin_t * p ) {} + +#endif + + +/**Function************************************************************* + + Synopsis [Testbench.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManSupportAndTest( Gia_Man_t * pGia ) +{ + Gia_ManMin_t * pMan; + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i; + Gia_ManFillValue( pGia ); + pNew = Gia_ManStart( Gia_ManObjNum(pGia) ); + pNew->pName = Abc_UtilStrsav( pGia->pName ); + pNew->pSpec = Abc_UtilStrsav( pGia->pSpec ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(pGia)->Value = 0; + pMan = Gia_ManSuppStart( pNew ); + Gia_ManForEachObj1( pGia, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + { +// pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + pObj->Value = Gia_ManSupportAnd( pMan, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + else if ( Gia_ObjIsCi(pObj) ) + pObj->Value = Gia_ManAppendCi( pNew ); + else if ( Gia_ObjIsCo(pObj) ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + else assert( 0 ); + + if ( i % 10000 == 0 ) + printf( "%d\n", i ); + } + Gia_ManSuppStop( pMan ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia) ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + + + + +struct Gia_Man2Min_t_ +{ + // problem formulation + Gia_Man_t * pGia; + int iLits[2]; + // structural information + Vec_Int_t * vCis[2]; + Vec_Int_t * vObjs[2]; + // SAT solving + satoko_t * pSat; // SAT solver + Vec_Wrd_t * vSims; // simulation + Vec_Ptr_t * vFrontier; // CNF construction + Vec_Ptr_t * vFanins; // CNF construction + Vec_Int_t * vSatVars; // nodes + int nCisOld; // previous number of CIs + int iPattern; // the next pattern to write + int nSatSat; + int nSatUnsat; + int nCalls; + int nSims; + int nSupps; +}; + +static inline int Gia_Min2ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjCopyArray(p, Gia_ObjId(p, pObj)); } +static inline int Gia_Min2ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num ) { assert(Gia_Min2ObjSatId(p, pObj) == -1); Gia_ObjSetCopyArray(p, Gia_ObjId(p, pObj), Num); return Num; } +static inline void Gia_Min2ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(Gia_Min2ObjSatId(p, pObj) != -1); Gia_ObjSetCopyArray(p, Gia_ObjId(p, pObj), -1); } + + +/**Function************************************************************* + + Synopsis [Create/delete the data representation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man2Min_t * Gia_Man2SuppStart( Gia_Man_t * pGia ) +{ + Gia_Man2Min_t * p; + p = ABC_CALLOC( Gia_Man2Min_t, 1 ); + p->pGia = pGia; + p->vCis[0] = Vec_IntAlloc( 512 ); + p->vCis[1] = Vec_IntAlloc( 512 ); + p->vObjs[0] = Vec_IntAlloc( 512 ); + p->vObjs[1] = Vec_IntAlloc( 512 ); + // SAT solving + p->pSat = satoko_create(); + p->vSims = Vec_WrdAlloc( 1000 ); + p->vFrontier = Vec_PtrAlloc( 1000 ); + p->vFanins = Vec_PtrAlloc( 100 ); + p->vSatVars = Vec_IntAlloc( 100 ); + p->iPattern = 1; + p->pSat->opts.learnt_ratio = 0; // prevent garbage collection + return p; +} +void Gia_Man2SuppStop( Gia_Man2Min_t * p ) +{ + printf( "Total calls = %8d. Supps = %6d. Sims = %6d. SAT = %6d. UNSAT = %6d.\n", + p->nCalls, p->nSupps, p->nSims, p->nSatSat, p->nSatUnsat ); + Vec_IntFreeP( &p->vCis[0] ); + Vec_IntFreeP( &p->vCis[1] ); + Vec_IntFreeP( &p->vObjs[0] ); + Vec_IntFreeP( &p->vObjs[1] ); + Gia_ManCleanMark01( p->pGia ); + satoko_destroy( p->pSat ); + Vec_WrdFreeP( &p->vSims ); + Vec_PtrFreeP( &p->vFrontier ); + Vec_PtrFreeP( &p->vFanins ); + Vec_IntFreeP( &p->vSatVars ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Adds clauses to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_Min2AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, satoko_t * pSat ) +{ + int fPolarFlip = 0; + Gia_Obj_t * pNodeI, * pNodeT, * pNodeE; + int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE; + + assert( !Gia_IsComplement( pNode ) ); + assert( pNode->fMark0 ); + // get nodes (I = if, T = then, E = else) + pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); + // get the variable numbers + VarF = Gia_Min2ObjSatId(p, pNode); + VarI = Gia_Min2ObjSatId(p, pNodeI); + VarT = Gia_Min2ObjSatId(p, Gia_Regular(pNodeT)); + VarE = Gia_Min2ObjSatId(p, Gia_Regular(pNodeE)); + // get the complementation flags + fCompT = Gia_IsComplement(pNodeT); + fCompE = Gia_IsComplement(pNodeE); + + // f = ITE(i, t, e) + + // i' + t' + f + // i' + t + f' + // i + e' + f + // i + e + f' + + // create four clauses + pLits[0] = Abc_Var2Lit(VarI, 1); + pLits[1] = Abc_Var2Lit(VarT, 1^fCompT); + pLits[2] = Abc_Var2Lit(VarF, 0); + if ( fPolarFlip ) + { + if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); + if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); + } + RetValue = satoko_add_clause( pSat, pLits, 3 ); + assert( RetValue ); + pLits[0] = Abc_Var2Lit(VarI, 1); + pLits[1] = Abc_Var2Lit(VarT, 0^fCompT); + pLits[2] = Abc_Var2Lit(VarF, 1); + if ( fPolarFlip ) + { + if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); + if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); + } + RetValue = satoko_add_clause( pSat, pLits, 3 ); + assert( RetValue ); + pLits[0] = Abc_Var2Lit(VarI, 0); + pLits[1] = Abc_Var2Lit(VarE, 1^fCompE); + pLits[2] = Abc_Var2Lit(VarF, 0); + if ( fPolarFlip ) + { + if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); + if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); + } + RetValue = satoko_add_clause( pSat, pLits, 3 ); + assert( RetValue ); + pLits[0] = Abc_Var2Lit(VarI, 0); + pLits[1] = Abc_Var2Lit(VarE, 0^fCompE); + pLits[2] = Abc_Var2Lit(VarF, 1); + if ( fPolarFlip ) + { + if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); + if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); + } + RetValue = satoko_add_clause( pSat, pLits, 3 ); + assert( RetValue ); + + // two additional clauses + // t' & e' -> f' + // t & e -> f + + // t + e + f' + // t' + e' + f + + if ( VarT == VarE ) + { +// assert( fCompT == !fCompE ); + return; + } + + pLits[0] = Abc_Var2Lit(VarT, 0^fCompT); + pLits[1] = Abc_Var2Lit(VarE, 0^fCompE); + pLits[2] = Abc_Var2Lit(VarF, 1); + if ( fPolarFlip ) + { + if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); + if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); + } + RetValue = satoko_add_clause( pSat, pLits, 3 ); + assert( RetValue ); + pLits[0] = Abc_Var2Lit(VarT, 1^fCompT); + pLits[1] = Abc_Var2Lit(VarE, 1^fCompE); + pLits[2] = Abc_Var2Lit(VarF, 0); + if ( fPolarFlip ) + { + if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); + if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); + } + RetValue = satoko_add_clause( pSat, pLits, 3 ); + assert( RetValue ); +} +void Gia_Min2AddClausesSuper( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper, satoko_t * pSat ) +{ + int fPolarFlip = 0; + Gia_Obj_t * pFanin; + int * pLits, nLits, RetValue, i; + assert( !Gia_IsComplement(pNode) ); + assert( Gia_ObjIsAnd( pNode ) ); + // create storage for literals + nLits = Vec_PtrSize(vSuper) + 1; + pLits = ABC_ALLOC( int, nLits ); + // suppose AND-gate is A & B = C + // add !A => !C or A + !C + Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i ) + { + pLits[0] = Abc_Var2Lit(Gia_Min2ObjSatId(p, Gia_Regular(pFanin)), Gia_IsComplement(pFanin)); + pLits[1] = Abc_Var2Lit(Gia_Min2ObjSatId(p, pNode), 1); + if ( fPolarFlip ) + { + if ( Gia_Regular(pFanin)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); + if ( pNode->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); + } + RetValue = satoko_add_clause( pSat, pLits, 2 ); + assert( RetValue ); + } + // add A & B => C or !A + !B + C + Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i ) + { + pLits[i] = Abc_Var2Lit(Gia_Min2ObjSatId(p, Gia_Regular(pFanin)), !Gia_IsComplement(pFanin)); + if ( fPolarFlip ) + { + if ( Gia_Regular(pFanin)->fPhase ) pLits[i] = Abc_LitNot( pLits[i] ); + } + } + pLits[nLits-1] = Abc_Var2Lit(Gia_Min2ObjSatId(p, pNode), 0); + if ( fPolarFlip ) + { + if ( pNode->fPhase ) pLits[nLits-1] = Abc_LitNot( pLits[nLits-1] ); + } + RetValue = satoko_add_clause( pSat, pLits, nLits ); + assert( RetValue ); + ABC_FREE( pLits ); +} + +/**Function************************************************************* + + Synopsis [Adds clauses and returns CNF variable of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_Min2CollectSuper_rec( Gia_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes ) +{ + // if the new node is complemented or a PI, another gate begins + if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) || + (!fFirst && Gia_ObjValue(pObj) > 1) || + (fUseMuxes && pObj->fMark0) ) + { + Vec_PtrPushUnique( vSuper, pObj ); + return; + } + // go through the branches + Gia_Min2CollectSuper_rec( Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes ); + Gia_Min2CollectSuper_rec( Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes ); +} +void Gia_Min2CollectSuper( Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper ) +{ + assert( !Gia_IsComplement(pObj) ); + assert( !Gia_ObjIsCi(pObj) ); + Vec_PtrClear( vSuper ); + Gia_Min2CollectSuper_rec( pObj, vSuper, 1, fUseMuxes ); +} +void Gia_Min2ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier, satoko_t * pSat, Vec_Int_t * vSatVars ) +{ + assert( !Gia_IsComplement(pObj) ); + assert( !Gia_ObjIsConst0(pObj) ); + if ( Gia_Min2ObjSatId(p, pObj) >= 0 ) + return; + assert( Gia_Min2ObjSatId(p, pObj) == -1 ); + Vec_IntPush( vSatVars, Gia_ObjId(p, pObj) ); + Gia_Min2ObjSetSatId( p, pObj, satoko_add_variable(pSat, 0) ); + if ( Gia_ObjIsAnd(pObj) ) + Vec_PtrPush( vFrontier, pObj ); +} +int Gia_Min2ObjGetCnfVar( Gia_Man2Min_t * p, int iObj ) +{ + Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj); + Gia_Obj_t * pNode, * pFanin; + int i, k, fUseMuxes = 1; + if ( Gia_Min2ObjSatId(p->pGia, pObj) >= 0 ) + return Gia_Min2ObjSatId(p->pGia, pObj); + if ( Gia_ObjIsCi(pObj) ) + { + Vec_IntPush( p->vSatVars, iObj ); + return Gia_Min2ObjSetSatId( p->pGia, pObj, satoko_add_variable(p->pSat, 0) ); + } + assert( Gia_ObjIsAnd(pObj) ); + // start the frontier + Vec_PtrClear( p->vFrontier ); + Gia_Min2ObjAddToFrontier( p->pGia, pObj, p->vFrontier, p->pSat, p->vSatVars ); + // explore nodes in the frontier + Vec_PtrForEachEntry( Gia_Obj_t *, p->vFrontier, pNode, i ) + { + assert( Gia_Min2ObjSatId(p->pGia,pNode) >= 0 ); + if ( fUseMuxes && pNode->fMark0 ) + { + Vec_PtrClear( p->vFanins ); + Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin0(pNode) ) ); + Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin1(pNode) ) ); + Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin0(pNode) ) ); + Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin1(pNode) ) ); + Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k ) + Gia_Min2ObjAddToFrontier( p->pGia, Gia_Regular(pFanin), p->vFrontier, p->pSat, p->vSatVars ); + Gia_Min2AddClausesMux( p->pGia, pNode, p->pSat ); + } + else + { + Gia_Min2CollectSuper( pNode, fUseMuxes, p->vFanins ); + Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k ) + Gia_Min2ObjAddToFrontier( p->pGia, Gia_Regular(pFanin), p->vFrontier, p->pSat, p->vSatVars ); + Gia_Min2AddClausesSuper( p->pGia, pNode, p->vFanins, p->pSat ); + } + assert( Vec_PtrSize(p->vFanins) > 1 ); + } + return Gia_Min2ObjSatId(p->pGia,pObj); +} + +/**Function************************************************************* + + Synopsis [Returns 0 if the node is not a constant.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_Min2ManSimulate( Gia_Man2Min_t * p ) +{ + word Sim0, Sim1; int n, i, iObj; + p->nSims++; + // add random values to new CIs + Vec_WrdFillExtra( p->vSims, Gia_ManObjNum(p->pGia), 0 ); + for ( i = p->nCisOld; i < Gia_ManCiNum(p->pGia); i++ ) + Vec_WrdWriteEntry( p->vSims, Gia_ManCiIdToId(p->pGia, i), Gia_ManRandomW( 0 ) << 1 ); + p->nCisOld = Gia_ManCiNum(p->pGia); + // simulate internal nodes + for ( n = 0; n < 2; n++ ) + Vec_IntForEachEntry( p->vObjs[n], iObj, i ) + { + Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj ); + Sim0 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId0p(p->pGia, pObj) ); + Sim1 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId1p(p->pGia, pObj) ); + Sim0 = Gia_ObjFaninC0(pObj) ? ~Sim0 : Sim0; + Sim1 = Gia_ObjFaninC1(pObj) ? ~Sim1 : Sim1; + Vec_WrdWriteEntry( p->vSims, iObj, Sim0 & Sim1 ); + } + Sim0 = Vec_WrdEntry( p->vSims, Abc_Lit2Var(p->iLits[0]) ); + Sim1 = Vec_WrdEntry( p->vSims, Abc_Lit2Var(p->iLits[1]) ); + Sim0 = Abc_LitIsCompl(p->iLits[0]) ? ~Sim0 : Sim0; + Sim1 = Abc_LitIsCompl(p->iLits[1]) ? ~Sim1 : Sim1; +// assert( (Sim0 & Sim1) != ~0 ); + return (Sim0 & Sim1) == 0; +} + +/**Function************************************************************* + + Synopsis [Internal simulation APIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_Min2SimSetInputBit( Gia_Man2Min_t * p, int iObj, int Bit, int iPattern ) +{ + word * pSim = Vec_WrdEntryP( p->vSims, iObj ); + assert( iPattern > 0 && iPattern < 64 ); + if ( Abc_InfoHasBit( (unsigned*)pSim, iPattern ) != Bit ) + Abc_InfoXorBit( (unsigned*)pSim, iPattern ); +} +int Gia_Min2ManSolve( Gia_Man2Min_t * p ) +{ + int iObj0 = Abc_Lit2Var(p->iLits[0]); + int iObj1 = Abc_Lit2Var(p->iLits[1]); + int n, i, status, iVar0, iVar1, iTemp; + assert( iObj0 > 0 && iObj1 > 0 ); +// Vec_IntForEachEntry( &p->pGia->vCopies, iTemp, i ) +// assert( iTemp == -1 ); + Vec_IntFillExtra( &p->pGia->vCopies, Gia_ManObjNum(p->pGia), -1 ); + Vec_IntClear( p->vSatVars ); + assert( solver_varnum(p->pSat) == 0 ); + iVar0 = Gia_Min2ObjGetCnfVar( p, iObj0 ); + iVar1 = Gia_Min2ObjGetCnfVar( p, iObj1 ); + satoko_assump_push( p->pSat, Abc_Var2Lit(iVar0, Abc_LitIsCompl(p->iLits[0])) ); + satoko_assump_push( p->pSat, Abc_Var2Lit(iVar1, Abc_LitIsCompl(p->iLits[1])) ); + status = satoko_solve( p->pSat ); + satoko_assump_pop( p->pSat ); + satoko_assump_pop( p->pSat ); + if ( status == SATOKO_SAT ) + { + //printf( "Disproved %d %d\n", p->iLits[0], p->iLits[1] ); + assert( Gia_Min2ManSimulate(p) == 1 ); + for ( n = 0; n < 2; n++ ) + Vec_IntForEachEntry( p->vCis[n], iTemp, i ) + Gia_Min2SimSetInputBit( p, iTemp, var_polarity(p->pSat, Gia_Min2ObjSatId(p->pGia, Gia_ManObj(p->pGia, iTemp))) == LIT_TRUE, p->iPattern ); + assert( Gia_Min2ManSimulate(p) == 0 ); + p->iPattern = p->iPattern == 63 ? 1 : p->iPattern + 1; + p->nSatSat++; + } + //printf( "supp %d node %d vars %d\n", + // Vec_IntSize(p->vCis[0]) + Vec_IntSize(p->vCis[1]), + // Vec_IntSize(p->vObjs[0]) + Vec_IntSize(p->vObjs[1]), + // Vec_IntSize(p->vSatVars) ); + satoko_rollback( p->pSat ); + Vec_IntForEachEntry( p->vSatVars, iTemp, i ) + Gia_Min2ObjCleanSatId( p->pGia, Gia_ManObj(p->pGia, iTemp) ); + return status == SATOKO_UNSAT; +} + +/**Function************************************************************* + + Synopsis [Collect nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_Min2ManGatherSupp_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vCis, Vec_Int_t * vObjs ) +{ + int Val0, Val1; + Gia_Obj_t * pObj; + if ( Gia_ObjIsTravIdPreviousId(p, iObj) ) + return 1; + if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) + return 0; + Gia_ObjSetTravIdCurrentId(p, iObj); + pObj = Gia_ManObj( p, iObj ); + if ( Gia_ObjIsCi(pObj) ) + { + Vec_IntPush( vCis, iObj ); + return 0; + } + assert( Gia_ObjIsAnd(pObj) ); + Val0 = Gia_Min2ManGatherSupp_rec( p, Gia_ObjFaninId0(pObj, iObj), vCis, vObjs ); + Val1 = Gia_Min2ManGatherSupp_rec( p, Gia_ObjFaninId1(pObj, iObj), vCis, vObjs ); + Vec_IntPush( vObjs, iObj ); + return Val0 || Val1; +} +int Gia_Min2ManGatherSupp( Gia_Man2Min_t * p ) +{ + int n, Overlap = 0; + p->nSupps++; + Gia_ManIncrementTravId( p->pGia ); + for ( n = 0; n < 2; n++ ) + { + Vec_IntClear( p->vCis[n] ); + Vec_IntClear( p->vObjs[n] ); + Gia_ManIncrementTravId( p->pGia ); + Overlap = Gia_Min2ManGatherSupp_rec( p->pGia, Abc_Lit2Var(p->iLits[n]), p->vCis[n], p->vObjs[n] ); + assert( n || !Overlap ); + } + return Overlap; +} + +/**Function************************************************************* + + Synopsis [Takes a literal and returns a support-minized literal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_Man2SupportAnd( Gia_Man2Min_t * p, int iLit0, int iLit1 ) +{ + p->nCalls++; + //return Gia_ManHashAnd( p->pGia, iLit0, iLit1 ); + p->iLits[0] = iLit0; + p->iLits[1] = iLit1; + if ( iLit0 < 2 || iLit1 < 2 || Abc_Lit2Var(iLit0) == Abc_Lit2Var(iLit1) || Gia_ManHashLookupInt(p->pGia, iLit0, iLit1) || + !Gia_Min2ManGatherSupp(p) || !Gia_Min2ManSimulate(p) || !Gia_Min2ManSolve(p) ) + return Gia_ManHashAnd( p->pGia, iLit0, iLit1 ); + //printf( "%d %d\n", iLit0, iLit1 ); + p->nSatUnsat++; + return 0; +} + +/**Function************************************************************* + + Synopsis [Testbench.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_Man2SupportAndTest( Gia_Man_t * pGia ) +{ + Gia_Man2Min_t * pMan; + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i; + Gia_ManRandomW( 1 ); + Gia_ManFillValue( pGia ); + pNew = Gia_ManStart( Gia_ManObjNum(pGia) ); + pNew->pName = Abc_UtilStrsav( pGia->pName ); + pNew->pSpec = Abc_UtilStrsav( pGia->pSpec ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(pGia)->Value = 0; + pMan = Gia_Man2SuppStart( pNew ); + Gia_ManForEachObj1( pGia, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + { +// pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + pObj->Value = Gia_Man2SupportAnd( pMan, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + else if ( Gia_ObjIsCi(pObj) ) + pObj->Value = Gia_ManAppendCi( pNew ); + else if ( Gia_ObjIsCo(pObj) ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + else assert( 0 ); + + //if ( i % 10000 == 0 ) + // printf( "%d\n", i ); + } + Gia_Man2SuppStop( pMan ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia) ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 1f4c4c07..7ffd6bc5 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -76,6 +76,7 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaStg.c \ src/aig/gia/giaStr.c \ src/aig/gia/giaSupMin.c \ + src/aig/gia/giaSupp.c \ src/aig/gia/giaSweep.c \ src/aig/gia/giaSweeper.c \ src/aig/gia/giaSwitch.c \ diff --git a/src/aig/miniaig/miniaig.h b/src/aig/miniaig/miniaig.h index 6843648e..217fea51 100644 --- a/src/aig/miniaig/miniaig.h +++ b/src/aig/miniaig/miniaig.h @@ -171,9 +171,9 @@ static void Mini_AigDump( Mini_Aig_t * p, char * pFileName ) printf( "Cannot open file for writing \"%s\".\n", pFileName ); return; } - RetValue = fwrite( &p->nSize, sizeof(int), 1, pFile ); - RetValue = fwrite( &p->nRegs, sizeof(int), 1, pFile ); - RetValue = fwrite( p->pArray, sizeof(int), p->nSize, pFile ); + RetValue = (int)fwrite( &p->nSize, sizeof(int), 1, pFile ); + RetValue = (int)fwrite( &p->nRegs, sizeof(int), 1, pFile ); + RetValue = (int)fwrite( p->pArray, sizeof(int), p->nSize, pFile ); fclose( pFile ); } static Mini_Aig_t * Mini_AigLoad( char * pFileName ) @@ -187,12 +187,12 @@ static Mini_Aig_t * Mini_AigLoad( char * pFileName ) printf( "Cannot open file for reading \"%s\".\n", pFileName ); return NULL; } - RetValue = fread( &nSize, sizeof(int), 1, pFile ); + RetValue = (int)fread( &nSize, sizeof(int), 1, pFile ); p = MINI_AIG_CALLOC( Mini_Aig_t, 1 ); p->nSize = p->nCap = nSize; p->pArray = MINI_AIG_ALLOC( int, p->nCap ); - RetValue = fread( &p->nRegs, sizeof(int), 1, pFile ); - RetValue = fread( p->pArray, sizeof(int), p->nSize, pFile ); + RetValue = (int)fread( &p->nRegs, sizeof(int), 1, pFile ); + RetValue = (int)fread( p->pArray, sizeof(int), p->nSize, pFile ); fclose( pFile ); return p; } diff --git a/src/aig/miniaig/minilut.h b/src/aig/miniaig/minilut.h index 5040f4b7..e84428d4 100644 --- a/src/aig/miniaig/minilut.h +++ b/src/aig/miniaig/minilut.h @@ -191,11 +191,11 @@ static void Mini_LutDump( Mini_Lut_t * p, char * pFileName ) printf( "Cannot open file for writing \"%s\".\n", pFileName ); return; } - RetValue = fwrite( &p->nSize, sizeof(int), 1, pFile ); - RetValue = fwrite( &p->nRegs, sizeof(int), 1, pFile ); - RetValue = fwrite( &p->LutSize, sizeof(int), 1, pFile ); - RetValue = fwrite( p->pArray, sizeof(int), p->nSize * p->LutSize, pFile ); - RetValue = fwrite( p->pTruths, sizeof(int), p->nSize * Mini_LutWordNum(p->LutSize), pFile ); + RetValue = (int)fwrite( &p->nSize, sizeof(int), 1, pFile ); + RetValue = (int)fwrite( &p->nRegs, sizeof(int), 1, pFile ); + RetValue = (int)fwrite( &p->LutSize, sizeof(int), 1, pFile ); + RetValue = (int)fwrite( p->pArray, sizeof(int), p->nSize * p->LutSize, pFile ); + RetValue = (int)fwrite( p->pTruths, sizeof(int), p->nSize * Mini_LutWordNum(p->LutSize), pFile ); fclose( pFile ); } static Mini_Lut_t * Mini_LutLoad( char * pFileName ) @@ -209,15 +209,15 @@ static Mini_Lut_t * Mini_LutLoad( char * pFileName ) printf( "Cannot open file for reading \"%s\".\n", pFileName ); return NULL; } - RetValue = fread( &nSize, sizeof(int), 1, pFile ); + RetValue = (int)fread( &nSize, sizeof(int), 1, pFile ); p = MINI_LUT_CALLOC( Mini_Lut_t, 1 ); p->nSize = p->nCap = nSize; - RetValue = fread( &p->nRegs, sizeof(int), 1, pFile ); - RetValue = fread( &p->LutSize, sizeof(int), 1, pFile ); + RetValue = (int)fread( &p->nRegs, sizeof(int), 1, pFile ); + RetValue = (int)fread( &p->LutSize, sizeof(int), 1, pFile ); p->pArray = MINI_LUT_ALLOC( int, p->nCap * p->LutSize ); p->pTruths = MINI_LUT_ALLOC( unsigned, p->nCap * Mini_LutWordNum(p->LutSize) ); - RetValue = fread( p->pArray, sizeof(int), p->nCap * p->LutSize, pFile ); - RetValue = fread( p->pTruths, sizeof(int), p->nCap * Mini_LutWordNum(p->LutSize), pFile ); + RetValue = (int)fread( p->pArray, sizeof(int), p->nCap * p->LutSize, pFile ); + RetValue = (int)fread( p->pTruths, sizeof(int), p->nCap * Mini_LutWordNum(p->LutSize), pFile ); fclose( pFile ); return p; } diff --git a/src/aig/miniaig/ndr.h b/src/aig/miniaig/ndr.h index 4450d22c..9e85c870 100644 --- a/src/aig/miniaig/ndr.h +++ b/src/aig/miniaig/ndr.h @@ -220,7 +220,7 @@ static inline void Ndr_DataPushString( Ndr_Data_t * p, int Type, char * pFunc ) { if ( !pFunc ) return; - Ndr_DataPushArray( p, Type, (strlen(pFunc) + 4) / 4, (int *)pFunc ); + Ndr_DataPushArray( p, Type, ((int)strlen(pFunc) + 4) / 4, (int *)pFunc ); } //////////////////////////////////////////////////////////////////////// @@ -457,8 +457,8 @@ static inline void * Ndr_ModuleRead( char * pFileName ) p->nSize = p->nCap = nFileSize / 5; p->pHead = malloc( p->nCap ); p->pBody = malloc( p->nCap * 4 ); - RetValue = fread( p->pBody, 4, p->nCap, pFile ); - RetValue = fread( p->pHead, 1, p->nCap, pFile ); + RetValue = (int)fread( p->pBody, 4, p->nCap, pFile ); + RetValue = (int)fread( p->pHead, 1, p->nCap, pFile ); assert( p->nSize == (int)p->pBody[0] ); fclose( pFile ); return p; @@ -468,8 +468,8 @@ static inline void Ndr_ModuleWrite( char * pFileName, void * pModule ) Ndr_Data_t * p = (Ndr_Data_t *)pModule; int RetValue; FILE * pFile = fopen( pFileName, "wb" ); if ( pFile == NULL ) { printf( "Cannot open file \"%s\" for writing.\n", pFileName ); return; } - RetValue = fwrite( p->pBody, 4, p->pBody[0], pFile ); - RetValue = fwrite( p->pHead, 1, p->pBody[0], pFile ); + RetValue = (int)fwrite( p->pBody, 4, p->pBody[0], pFile ); + RetValue = (int)fwrite( p->pHead, 1, p->pBody[0], pFile ); fclose( pFile ); } |