/**CFile**************************************************************** FileName [abcMfs.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Hierarchical word-level netlist.] Synopsis [Optimization with don't-cares.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - July 21, 2015.] Revision [$Id: abcMfs.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $] ***********************************************************************/ #include "acb.h" #include "bool/kit/kit.h" #include "sat/bsat/satSolver.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Acb_Truth2Cnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf ) { Vec_StrClear( vCnf ); if ( Truth == 0 || ~Truth == 0 ) { // assert( nVars == 0 ); Vec_StrPush( vCnf, (char)(Truth == 0) ); Vec_StrPush( vCnf, (char)-1 ); return 1; } else { int i, k, c, RetValue, Literal, Cube, nCubes = 0; assert( nVars > 0 ); for ( c = 0; c < 2; c ++ ) { Truth = c ? ~Truth : Truth; RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 ); assert( RetValue == 0 ); nCubes += Vec_IntSize( vCover ); Vec_IntForEachEntry( vCover, Cube, i ) { for ( k = 0; k < nVars; k++ ) { Literal = 3 & (Cube >> (k << 1)); if ( Literal == 1 ) // '0' -> pos lit Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 0) ); else if ( Literal == 2 ) // '1' -> neg lit Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 1) ); else if ( Literal != 0 ) assert( 0 ); } Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) ); Vec_StrPush( vCnf, (char)-1 ); } } return nCubes; } } Vec_Wec_t * Acb_NtkDeriveCnf( Acb_Ntk_t * p ) { Vec_Wec_t * vCnfs = Vec_WecStart( Acb_NtkObjNumMax(p) ); Vec_Str_t * vCnf = Vec_StrAlloc( 100 ); int iObj; Acb_NtkForEachNode( p, iObj ) { int nCubes = Acb_Truth2Cnf( Acb_ObjTruth(p, iObj), Acb_ObjFaninNum(p, iObj), &p->vCover, vCnf ); Vec_Str_t * vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, iObj ); Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) ); memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), Vec_StrSize(vCnf) ); vCnfBase->nSize = Vec_StrSize(vCnf); } Vec_StrFree( vCnf ); return vCnfs; } void Acb_CnfTranslate( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vSatVars, int iPivotVar ) { Vec_Int_t * vClause; signed char Entry; int i, Lit; Vec_WecClear( vRes ); vClause = Vec_WecPushLevel( vRes ); Vec_StrForEachEntry( vCnf, Entry, i ) { if ( (int)Entry == -1 ) { vClause = Vec_WecPushLevel( vRes ); continue; } Lit = Abc_Lit2LitV( Vec_IntArray(vSatVars), (int)Entry ); Lit = Abc_LitNotCond( Lit, Abc_Lit2Var(Lit) == iPivotVar ); Vec_IntPush( vClause, Lit ); } } int Acb_ObjCreateCnf( sat_solver * pSat, Acb_Ntk_t * p, int iObj, Vec_Int_t * vSatVars, int iPivotVar ) { Vec_Int_t * vClause; int k, RetValue; Acb_CnfTranslate( &p->vClauses, (Vec_Str_t *)Vec_WecEntry(&p->vCnfs, iObj), vSatVars, iPivotVar ); Vec_WecForEachLevel( &p->vClauses, vClause, k ) { if ( Vec_IntSize(vClause) == 0 ) break; RetValue = sat_solver_addclause( pSat, Vec_IntArray(vClause), Vec_IntLimit(vClause) ); if ( RetValue == 0 ) return 0; } return 1; } /**Function************************************************************* Synopsis [Constructs SAT solver for the window.] Description [The window for the pivot node is represented as a DFS ordered array of objects (vWinObjs) whose indexes are used as SAT variable IDs (stored in p->vCopies). PivotVar is the index of the pivot node in array vWinObjs. The nodes before (after) PivotVar are TFI (TFO) nodes. The leaf (root) nodes are labeled with Abc_LitIsCompl(). If fQbf is 1, returns the instance meant for QBF solving. It uses the last variable (LastVar) as the placeholder for the second copy of the pivot node.] SideEffects [] SeeAlso [] ***********************************************************************/ int Acb_NtkCountRoots( Vec_Int_t * vWinObjs, int PivotVar ) { int i, iObjLit, nRoots = 0; Vec_IntForEachEntryStart( vWinObjs, iObjLit, i, PivotVar + 1 ) nRoots += Abc_LitIsCompl(iObjLit); return nRoots; } sat_solver * Acb_NtkWindow2Solver( sat_solver * pSat, Acb_Ntk_t * p, int Pivot, Vec_Int_t * vWinObjs, int fQbf ) { Vec_Int_t * vFaninVars = Vec_IntAlloc( 8 ); int PivotVar = Vec_IntFind(vWinObjs, Abc_Var2Lit(Pivot, 0)); int nRoots = Acb_NtkCountRoots(vWinObjs, PivotVar); int TfoStart = PivotVar + 1; int nTfoSize = Vec_IntSize(vWinObjs) - TfoStart; int LastVar = Vec_IntSize(vWinObjs) + TfoStart + nRoots; int i, k, iLit = 1, RetValue, iObj, iObjLit, iFanin, * pFanins; //Vec_IntPrint( vWinObjs ); // mark new SAT variables Vec_IntForEachEntry( vWinObjs, iObj, i ) Acb_ObjSetCopy( p, i, iObj ); // create SAT solver if ( pSat == NULL ) pSat = sat_solver_new(); else sat_solver_restart( pSat ); sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + nTfoSize + nRoots + 1 ); // create constant 0 clause sat_solver_addclause( pSat, &iLit, &iLit + 1 ); // add clauses for all nodes Vec_IntForEachEntryStop( vWinObjs, iObjLit, i, TfoStart ) { if ( Abc_LitIsCompl(iObjLit) ) continue; iObj = Abc_Lit2Var(iObjLit); assert( !Acb_ObjIsCio(p, iObj) ); // collect SAT variables Vec_IntClear( vFaninVars ); Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iFanin) ); Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iObj) ); // derive CNF for the node RetValue = Acb_ObjCreateCnf( pSat, p, iObj, vFaninVars, -1 ); assert( RetValue ); } // add second clauses for the TFO Vec_IntForEachEntryStart( vWinObjs, iObjLit, i, TfoStart ) { iObj = Abc_Lit2Var(iObjLit); assert( !Acb_ObjIsCio(p, iObj) ); // collect SAT variables Vec_IntClear( vFaninVars ); Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) Vec_IntPush( vFaninVars, (fQbf && iFanin == Pivot) ? LastVar : Acb_ObjCopy(p, iFanin) ); Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iObj) ); // derive CNF for the node RetValue = Acb_ObjCreateCnf( pSat, p, iObj, vFaninVars, fQbf ? -1 : PivotVar ); assert( RetValue ); } if ( nRoots > 0 ) { // create XOR clauses for the roots int nVars = Vec_IntSize(vWinObjs) + nTfoSize; Vec_IntClear( vFaninVars ); Vec_IntForEachEntryStart( vWinObjs, iObjLit, i, TfoStart ) { if ( !Abc_LitIsCompl(iObjLit) ) continue; Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars, 0) ); sat_solver_add_xor( pSat, Acb_ObjCopy(p, iObj), Acb_ObjCopy(p, iObj) + nTfoSize, nVars++, 0 ); } // make OR clause for the last nRoots variables RetValue = sat_solver_addclause( pSat, Vec_IntArray(vFaninVars), Vec_IntLimit(vFaninVars) ); if ( RetValue == 0 ) { Vec_IntFree( vFaninVars ); sat_solver_delete( pSat ); return NULL; } assert( sat_solver_nvars(pSat) == nVars + 1 ); } else if ( fQbf ) { int n, pLits[2]; for ( n = 0; n < 2; n++ ) { pLits[0] = Abc_Var2Lit( PivotVar, n ); pLits[1] = Abc_Var2Lit( LastVar, n ); RetValue = sat_solver_addclause( pSat, pLits, pLits + 2 ); assert( RetValue ); } } Vec_IntFree( vFaninVars ); // finalize RetValue = sat_solver_simplify( pSat ); if ( RetValue == 0 ) { sat_solver_delete( pSat ); return NULL; } return pSat; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Acb_NtkUnmarkWindow( Acb_Ntk_t * p, Vec_Int_t * vWin ) { int i, iObj; Vec_IntForEachEntry( vWin, iObj, i ) Vec_IntWriteEntry( &p->vObjCopy, iObj, -1 ); } /**Function************************************************************* Synopsis [Collects divisors.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline int Acb_ObjIsCritFanin( Acb_Ntk_t * p, int i, int f ) { return Acb_ObjLevelR(p, i) + Acb_ObjLevelD(p, f) == p->LevelMax; } Vec_Int_t * Acb_NtkDivisors( Acb_Ntk_t * p, int Pivot, int nTfiLevMin ) { int i, k, iObj, iFanin, iFanin2, * pFanins, * pFanins2, Lev, Level = Acb_ObjLevelD(p, Pivot); // include non-critical pivot fanins AND fanins of critical pivot fanins Vec_Int_t * vDivs = Vec_IntAlloc( 100 ); Acb_ObjForEachFaninFast( p, Pivot, pFanins, iFanin, i ) { if ( !Acb_ObjIsCritFanin(p, Pivot, iFanin) ) // non-critical fanin Vec_IntPush( vDivs, iFanin ); else // critical fanin Acb_ObjForEachFaninFast( p, iFanin, pFanins2, iFanin2, k ) Vec_IntPushUnique( vDivs, iFanin2 ); } // continue for a few more levels for ( Lev = Level-2; Lev >= nTfiLevMin; Lev-- ) { Vec_IntForEachEntry( vDivs, iObj, i ) if ( Acb_ObjLevelD(p, iObj) == Lev ) Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) Vec_IntPushUnique( vDivs, iFanin ); } // sort them by level Vec_IntSelectSortCost( Vec_IntArray(vDivs), Vec_IntSize(vDivs), &p->vLevelD ); return vDivs; } /**Function************************************************************* Synopsis [Marks TFO of divisors.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Acb_ObjMarkTfo_rec( Acb_Ntk_t * p, int iObj, int Pivot, int nTfoLevMax, int nFanMax ) { int iFanout, i; if ( Acb_ObjSetTravIdCur(p, iObj) ) return; if ( Acb_ObjLevelD(p, iObj) > nTfoLevMax || Acb_ObjFanoutNum(p, iObj) >= nFanMax || iObj == Pivot ) return; Acb_ObjForEachFanout( p, iObj, iFanout, i ) Acb_ObjMarkTfo_rec( p, iFanout, Pivot, nTfoLevMax, nFanMax ); } void Acb_ObjMarkTfo( Acb_Ntk_t * p, Vec_Int_t * vDivs, int Pivot, int nTfoLevMax, int nFanMax ) { int i, iObj; Acb_NtkIncTravId( p ); Vec_IntForEachEntry( vDivs, iObj, i ) Acb_ObjMarkTfo_rec( p, iObj, Pivot, nTfoLevMax, nFanMax ); } /**Function************************************************************* Synopsis [Labels TFO nodes with {none, root, inner} based on their type.] Description [Assuming TFO of TFI is marked with the current trav ID.] SideEffects [] SeeAlso [] ***********************************************************************/ int Acb_ObjLabelTfo_rec( Acb_Ntk_t * p, int iObj, int nTfoLevMax, int nFanMax ) { int iFanout, i, Diff, fHasNone = 0; if ( (Diff = Acb_ObjTravIdDiff(p, iObj)) <= 2 ) return Diff; Acb_ObjSetTravIdDiff( p, iObj, 2 ); if ( Acb_ObjIsCo(p, iObj) || Acb_ObjLevelD(p, iObj) > nTfoLevMax ) return 2; if ( Acb_ObjLevelD(p, iObj) == nTfoLevMax || Acb_ObjFanoutNum(p, iObj) >= nFanMax ) { if ( Diff == 3 ) Acb_ObjSetTravIdDiff( p, iObj, 1 ); // mark root return Acb_ObjTravIdDiff(p, iObj); } Acb_ObjForEachFanout( p, iObj, iFanout, i ) fHasNone |= 2 == Acb_ObjLabelTfo_rec( p, iFanout, nTfoLevMax, nFanMax ); if ( fHasNone && Diff == 3 ) Acb_ObjSetTravIdDiff( p, iObj, 1 ); // root else Acb_ObjSetTravIdDiff( p, iObj, 0 ); // inner return Acb_ObjTravIdDiff(p, iObj); } int Acb_ObjLabelTfo( Acb_Ntk_t * p, int Root, int nTfoLevMax, int nFanMax ) { Acb_NtkIncTravId( p ); // none (2) marked (3) unmarked (4) Acb_NtkIncTravId( p ); // root (1) Acb_NtkIncTravId( p ); // inner (0) assert( Acb_ObjTravIdDiff(p, Root) < 3 ); return Acb_ObjLabelTfo_rec( p, Root, nTfoLevMax, nFanMax ); } /**Function************************************************************* Synopsis [Collects labeled TFO.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Acb_ObjDeriveTfo_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vTfo, Vec_Int_t * vRoots ) { int iFanout, i, Diff = Acb_ObjTravIdDiff(p, iObj); if ( Acb_ObjSetTravIdCur(p, iObj) ) return; if ( Diff == 2 ) // root { Vec_IntPush( vRoots, Diff ); return; } assert( Diff == 1 ); Acb_ObjForEachFanout( p, iObj, iFanout, i ) Acb_ObjDeriveTfo_rec( p, iFanout, vTfo, vRoots ); Vec_IntPush( vTfo, Diff ); } void Acb_ObjDeriveTfo( Acb_Ntk_t * p, int Root, int nTfoLevMax, int nFanMax, Vec_Int_t ** pvTfo, Vec_Int_t ** pvRoots ) { int Res = Acb_ObjLabelTfo( p, Root, nTfoLevMax, nFanMax ); Vec_Int_t * vTfo = *pvTfo = Vec_IntAlloc( 100 ); Vec_Int_t * vRoots = *pvRoots = Vec_IntAlloc( 100 ); if ( Res ) // none or root return; Acb_NtkIncTravId( p ); // root (2) inner (1) visited (0) Acb_ObjDeriveTfo_rec( p, Root, vTfo, vRoots ); assert( Vec_IntEntryLast(vTfo) == Root ); Vec_IntPop( vTfo ); assert( Vec_IntEntryLast(vRoots) != Root ); Vec_IntReverseOrder( vTfo ); Vec_IntReverseOrder( vRoots ); } /**Function************************************************************* Synopsis [Collect side-inputs of the TFO, except the node.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Acb_NtkCollectTfoSideInputs( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vTfo ) { Vec_Int_t * vSide = Vec_IntAlloc( 100 ); int i, k, Node, iFanin, * pFanins; Acb_NtkIncTravId( p ); Vec_IntForEachEntry( vTfo, Node, i ) Acb_ObjSetTravIdCur( p, Node ), assert( Node != Pivot ); Vec_IntForEachEntry( vTfo, Node, i ) Acb_ObjForEachFaninFast( p, Node, pFanins, iFanin, k ) if ( !Acb_ObjSetTravIdCur(p, iFanin) && iFanin != Pivot ) Vec_IntPush( vSide, iFanin ); return vSide; } /**Function************************************************************* Synopsis [From side inputs, collect marked nodes and their unmarked fanins.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Acb_NtkCollectNewTfi1_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vTfiNew ) { int i, iFanin, * pFanins; if ( !Acb_ObjIsTravIdPrev(p, iObj) ) return; if ( Acb_ObjSetTravIdCur(p, iObj) ) return; Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, i ) Acb_NtkCollectNewTfi1_rec( p, iFanin, vTfiNew ); Vec_IntPush( vTfiNew, iObj ); } void Acb_NtkCollectNewTfi2_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vTfiNew ) { int i, iFanin, * pFanins; int fTravIdPrev = Acb_ObjIsTravIdPrev(p, iObj); if ( Acb_ObjSetTravIdCur(p, iObj) ) return; if ( fTravIdPrev && !Acb_ObjIsCi(p, iObj) ) Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, i ) Acb_NtkCollectNewTfi2_rec( p, iFanin, vTfiNew ); Vec_IntPush( vTfiNew, iObj ); } Vec_Int_t * Acb_NtkCollectNewTfi( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vSide ) { Vec_Int_t * vTfiNew = Vec_IntAlloc( 100 ); int i, Node; Acb_NtkIncTravId( p ); Acb_NtkCollectNewTfi1_rec( p, Pivot, vTfiNew ); assert( Vec_IntEntryLast(vTfiNew) == Pivot ); Vec_IntPop( vTfiNew ); Vec_IntForEachEntry( vSide, Node, i ) Acb_NtkCollectNewTfi2_rec( p, Node, vTfiNew ); Vec_IntPush( vTfiNew, Pivot ); return vTfiNew; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Acb_NtkCollectWindow( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vTfi, Vec_Int_t * vTfo, Vec_Int_t * vRoots ) { Vec_Int_t * vWin = Vec_IntAlloc( 100 ); int i, k, iObj, iFanin, * pFanins; // mark leaves Acb_NtkIncTravId( p ); Vec_IntForEachEntry( vTfi, iObj, i ) Acb_ObjSetTravIdCur(p, iObj); Acb_NtkIncTravId( p ); Vec_IntForEachEntry( vTfi, iObj, i ) if ( !Acb_ObjIsCi(p, iObj) ) Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) if ( !Acb_ObjIsTravIdCur(p, iFanin) ) Acb_ObjSetTravIdCur(p, iObj); // add TFI Vec_IntForEachEntry( vTfi, iObj, i ) Vec_IntPush( vWin, Abc_Var2Lit( iObj, Acb_ObjIsTravIdCur(p, iObj)) ); // mark roots Vec_IntForEachEntry( vRoots, iObj, i ) Acb_ObjSetTravIdCur(p, iObj); // add TFO Vec_IntForEachEntry( vTfo, iObj, i ) Vec_IntPush( vWin, Abc_Var2Lit( iObj, Acb_ObjIsTravIdCur(p, iObj)) ); return vWin; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Acb_NtkWindow( Acb_Ntk_t * p, int Pivot, int nTfiLevs, int nTfoLevs, int nFanMax, Vec_Int_t ** pvDivs ) { int nTfiLevMin = Acb_ObjLevelD(p, Pivot) - nTfiLevs; int nTfoLevMax = Acb_ObjLevelD(p, Pivot) + nTfoLevs; Vec_Int_t * vWin, * vDivs, * vTfo, * vRoots, * vSide, * vTfi; // collect divisors by traversing limited TFI vDivs = Acb_NtkDivisors( p, Pivot, nTfiLevMin ); // mark limited TFO of the divisors Acb_ObjMarkTfo( p, vDivs, Pivot, nTfoLevMax, nFanMax ); // collect TFO and roots Acb_ObjDeriveTfo( p, Pivot, nTfoLevMax, nFanMax, &vTfo, &vRoots ); // collect side inputs of the TFO vSide = Acb_NtkCollectTfoSideInputs( p, Pivot, vTfo ); // collect new TFI vTfi = Acb_NtkCollectNewTfi( p, Pivot, vSide ); // collect all nodes vWin = Acb_NtkCollectWindow( p, Pivot, vTfi, vTfo, vRoots ); // cleanup Vec_IntFree( vTfi ); Vec_IntFree( vTfo ); Vec_IntFree( vRoots ); Vec_IntFree( vSide ); *pvDivs = vDivs; return vWin; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Acb_NtkFindSupp( sat_solver * pSat, Acb_Ntk_t * p, Vec_Int_t * vWin, Vec_Int_t * vDivs, int nBTLimit ) { int i, iObj, nDivsNew; // reload divisors in terms of SAT variables Vec_IntForEachEntry( vDivs, iObj, i ) Vec_IntWriteEntry( vDivs, i, Acb_ObjCopy(p, iObj) ); // try solving nDivsNew = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vDivs), Vec_IntSize(vDivs), nBTLimit ); Vec_IntShrink( vDivs, nDivsNew ); // reload divisors in terms of network variables Vec_IntForEachEntry( vDivs, iObj, i ) Vec_IntWriteEntry( vDivs, i, Vec_IntEntry(vWin, iObj) ); return Vec_IntSize(vDivs); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Acb_NtkOptNode( Acb_Ntk_t * p, int Pivot, int nTfiLevs, int nTfoLevs, int nFanMax ) { Vec_Int_t * vSupp = &p->vArray0; Vec_Int_t * vDivs, * vWin = Acb_NtkWindow( p, Pivot, nTfiLevs, nTfoLevs, nFanMax, &vDivs ); sat_solver * pSat = Acb_NtkWindow2Solver( pSat, p, Pivot, vWin, 0 ); int nSuppNew, Level = Acb_ObjLevelD( p, Pivot ); // try solving the original support Vec_IntClear( vSupp ); Vec_IntAppend( vSupp, vDivs ); nSuppNew = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 ); Vec_IntShrink( vSupp, nSuppNew ); // try solving by level Acb_NtkUnmarkWindow( p, vWin ); Vec_IntFree( vWin ); Vec_IntFree( vDivs ); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END