/**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" #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; satoko_options(p->pSat)->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( satoko_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, satoko_var_polarity(p->pSat, Gia_Min2ObjSatId(p->pGia, Gia_ManObj(p->pGia, iTemp))) == SATOKO_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