diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/acb/acb.h | 48 | ||||
| -rw-r--r-- | src/base/acb/acbMfs.c | 592 | ||||
| -rw-r--r-- | src/sat/bmc/bmcFault.c | 2 |
3 files changed, 619 insertions, 23 deletions
diff --git a/src/base/acb/acb.h b/src/base/acb/acb.h index 0eaf7a47..db3a0564 100644 --- a/src/base/acb/acb.h +++ b/src/base/acb/acb.h @@ -88,9 +88,13 @@ struct Acb_Ntk_t_ Vec_Int_t vLevelR; // level Vec_Int_t vPathD; // path Vec_Int_t vPathR; // path + Vec_Wec_t vClauses; + Vec_Wec_t vCnfs; + Vec_Int_t vCover; // other Vec_Int_t vArray0; Vec_Int_t vArray1; + Vec_Int_t vArray2; }; // design @@ -239,6 +243,7 @@ static inline int Acb_ObjFanOffset( Acb_Ntk_t * p, int i ) { a static inline int * Acb_ObjFanins( Acb_Ntk_t * p, int i ) { return Vec_IntEntryP(&p->vFanSto, Acb_ObjFanOffset(p, i)); } static inline int Acb_ObjFanin( Acb_Ntk_t * p, int i, int k ) { return Acb_ObjFanins(p, i)[k+1]; } static inline int Acb_ObjFaninNum( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[0]; } +static inline int Acb_ObjFanoutNum( Acb_Ntk_t * p, int i ) { return Vec_IntSize( Vec_WecEntry(&p->vFanouts, i) ); } static inline int Acb_ObjFanin0( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[1]; } static inline int Acb_ObjCioId( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[2]; } @@ -272,28 +277,31 @@ static inline int Acb_ObjUpdateLevelR( Acb_Ntk_t * p, int i, int x ) static inline int Acb_ObjAddToPathD( Acb_Ntk_t * p, int i, int x ) { Vec_IntAddToEntry( &p->vPathD, i, x ); return x; } static inline int Acb_ObjAddToPathR( Acb_Ntk_t * p, int i, int x ) { Vec_IntAddToEntry( &p->vPathR, i, x ); return x; } -static inline int Acb_ObjNtkId( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_ObjIsBox(p, i) ? Acb_ObjFanin(p, i, Acb_ObjFaninNum(p, i)) : 0; } -static inline Acb_Ntk_t * Acb_ObjNtk( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_NtkNtk(p, Acb_ObjNtkId(p, i)); } -static inline int Acb_ObjIsSeq( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_ObjIsBox(p, i) ? Acb_ObjNtk(p, i)->fSeq : Acb_TypeIsSeq(Acb_ObjType(p, i)); } +static inline int Acb_ObjNtkId( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_ObjIsBox(p, i) ? Acb_ObjFanin(p, i, Acb_ObjFaninNum(p, i)) : 0; } +static inline Acb_Ntk_t * Acb_ObjNtk( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_NtkNtk(p, Acb_ObjNtkId(p, i)); } +static inline int Acb_ObjIsSeq( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_ObjIsBox(p, i) ? Acb_ObjNtk(p, i)->fSeq : Acb_TypeIsSeq(Acb_ObjType(p, i)); } -static inline int Acb_ObjRangeId( Acb_Ntk_t * p, int i ) { return Acb_NtkHasObjRanges(p) ? Vec_IntGetEntry(&p->vObjRange, i) : 0; } -static inline int Acb_ObjRange( Acb_Ntk_t * p, int i ) { return Abc_Lit2Var( Acb_ObjRangeId(p, i) ); } -static inline int Acb_ObjLeft( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeLeft(p, Acb_ObjRange(p, i)); } -static inline int Acb_ObjRight( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeRight(p, Acb_ObjRange(p, i)); } -static inline int Acb_ObjSigned( Acb_Ntk_t * p, int i ) { return Abc_LitIsCompl(Acb_ObjRangeId(p, i)); } -static inline int Acb_ObjRangeSize( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeSize(p, Acb_ObjRange(p, i)); } +static inline int Acb_ObjRangeId( Acb_Ntk_t * p, int i ) { return Acb_NtkHasObjRanges(p) ? Vec_IntGetEntry(&p->vObjRange, i) : 0; } +static inline int Acb_ObjRange( Acb_Ntk_t * p, int i ) { return Abc_Lit2Var( Acb_ObjRangeId(p, i) ); } +static inline int Acb_ObjLeft( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeLeft(p, Acb_ObjRange(p, i)); } +static inline int Acb_ObjRight( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeRight(p, Acb_ObjRange(p, i)); } +static inline int Acb_ObjSigned( Acb_Ntk_t * p, int i ) { return Abc_LitIsCompl(Acb_ObjRangeId(p, i)); } +static inline int Acb_ObjRangeSize( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeSize(p, Acb_ObjRange(p, i)); } static inline void Acb_ObjSetRangeSign( Acb_Ntk_t * p, int i, int x ) { assert(Acb_NtkHasObjRanges(p)); Vec_IntSetEntry(&p->vObjRange, i, x); } static inline void Acb_ObjSetRange( Acb_Ntk_t * p, int i, int x ) { assert(Acb_NtkHasObjRanges(p)); Vec_IntSetEntry(&p->vObjRange, i, Abc_Var2Lit(x,0)); } static inline void Acb_ObjHashRange( Acb_Ntk_t * p, int i, int l, int r ) { Acb_ObjSetRange( p, i, Acb_NtkHashRange(p, l, r) ); } -static inline int Acb_ObjRangeSign( Acb_Ntk_t * p, int i ) { return Abc_Var2Lit( Acb_ObjRangeSize(p, i), Acb_ObjSigned(p, i) ); } - -static inline int Acb_ObjTravId( Acb_Ntk_t * p, int i ) { return Vec_IntGetEntry(&p->vObjTrav, i); } -static inline int Acb_ObjIsTravIdCur( Acb_Ntk_t * p, int i ) { return Acb_ObjTravId(p, i) == p->nObjTravs; } -static inline int Acb_ObjIsTravIdPrev( Acb_Ntk_t * p, int i ) { return Acb_ObjTravId(p, i) == p->nObjTravs-1; } -static inline int Acb_ObjSetTravIdCur( Acb_Ntk_t * p, int i ) { int r = Acb_ObjIsTravIdCur(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs); return r; } -static inline int Acb_ObjSetTravIdPrev( Acb_Ntk_t * p, int i ) { int r = Acb_ObjIsTravIdPrev(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs-1); return r; } -static inline int Acb_NtkTravId( Acb_Ntk_t * p ) { return p->nObjTravs; } -static inline void Acb_NtkIncTravId( Acb_Ntk_t * p ) { if ( !Acb_NtkHasObjTravs(p) ) Acb_NtkCleanObjTravs(p); p->nObjTravs++; } +static inline int Acb_ObjRangeSign( Acb_Ntk_t * p, int i ) { return Abc_Var2Lit( Acb_ObjRangeSize(p, i), Acb_ObjSigned(p, i) ); } + +static inline int Acb_ObjTravId( Acb_Ntk_t * p, int i ) { return Vec_IntGetEntry(&p->vObjTrav, i); } +static inline int Acb_ObjTravIdDiff( Acb_Ntk_t * p, int i ) { return p->nObjTravs - Vec_IntGetEntry(&p->vObjTrav, i); } +static inline int Acb_ObjIsTravIdCur( Acb_Ntk_t * p, int i ) { return Acb_ObjTravId(p, i) == p->nObjTravs; } +static inline int Acb_ObjIsTravIdPrev( Acb_Ntk_t * p, int i ) { return Acb_ObjTravId(p, i) == p->nObjTravs-1; } +static inline int Acb_ObjIsTravIdDiff( Acb_Ntk_t * p, int i, int d ) { return Acb_ObjTravId(p, i) == p->nObjTravs-d; } +static inline int Acb_ObjSetTravIdCur( Acb_Ntk_t * p, int i ) { int r = Acb_ObjIsTravIdCur(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs); return r; } +static inline int Acb_ObjSetTravIdPrev( Acb_Ntk_t * p, int i ) { int r = Acb_ObjIsTravIdPrev(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs-1); return r; } +static inline int Acb_ObjSetTravIdDiff( Acb_Ntk_t * p, int i, int d ) { int r = Acb_ObjTravIdDiff(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs-d); return r; } +static inline int Acb_NtkTravId( Acb_Ntk_t * p ) { return p->nObjTravs; } +static inline void Acb_NtkIncTravId( Acb_Ntk_t * p ) { if ( !Acb_NtkHasObjTravs(p) ) Acb_NtkCleanObjTravs(p); p->nObjTravs++; } //////////////////////////////////////////////////////////////////////// /// ITERATORS /// @@ -493,6 +501,7 @@ static inline void Acb_NtkFree( Acb_Ntk_t * p ) // other Vec_IntErase( &p->vArray0 ); Vec_IntErase( &p->vArray1 ); + Vec_IntErase( &p->vArray2 ); ABC_FREE( p ); } static inline int Acb_NtkNewStrId( Acb_Ntk_t * pNtk, const char * format, ... ) @@ -663,8 +672,9 @@ static inline int Acb_NtkMemory( Acb_Ntk_t * p ) nMem += (int)Vec_IntMemory(&p->vNtkObjs ); nMem += (int)Vec_IntMemory(&p->vTargets ); // other + nMem += (int)Vec_IntMemory(&p->vArray0 ); nMem += (int)Vec_IntMemory(&p->vArray1 ); - nMem += (int)Vec_IntMemory(&p->vArray1 ); + nMem += (int)Vec_IntMemory(&p->vArray2 ); return nMem; } static inline void Acb_NtkPrintStats( Acb_Ntk_t * p ) diff --git a/src/base/acb/acbMfs.c b/src/base/acb/acbMfs.c index 9d44ae3f..47617a1c 100644 --- a/src/base/acb/acbMfs.c +++ b/src/base/acb/acbMfs.c @@ -1,12 +1,12 @@ /**CFile**************************************************************** - FileName [acb.c] + FileName [abcMfs.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Hierarchical word-level netlist.] - Synopsis [] + Synopsis [Optimization with don't-cares.] Author [Alan Mishchenko] @@ -14,11 +14,13 @@ Date [Ver. 1.0. Started - July 21, 2015.] - Revision [$Id: acb.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $] + 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 @@ -41,7 +43,591 @@ ABC_NAMESPACE_IMPL_START 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 /// diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c index 71eef2c4..0f63fa64 100644 --- a/src/sat/bmc/bmcFault.c +++ b/src/sat/bmc/bmcFault.c @@ -1069,7 +1069,7 @@ Vec_Int_t * Gia_ManGetTestPatterns( char * pFileName ) continue; if ( c != '0' && c != '1' ) { - printf( "Wring symbol (%c) in the input file.\n", c ); + printf( "Wrong symbol (%c) in the input file.\n", c ); Vec_IntFreeP( &vTests ); break; } |