From 5b80d704a1f8ce9514b282b9f722b6caa3671d0e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 9 Aug 2012 17:53:38 -0700 Subject: Improved abstraction refinement. --- src/aig/gia/giaAbsGla2.c | 12 +-- src/aig/gia/giaAbsRef.c | 239 ++++++++++++++++++++++++++++++++++++++++- src/aig/gia/giaAbsRef2.c | 274 ++++++++++++++++++++++++++++++++++++++++++----- src/misc/vec/vecInt.h | 10 +- 4 files changed, 491 insertions(+), 44 deletions(-) diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index 6910f334..d8a18930 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -20,7 +20,7 @@ #include "gia.h" #include "giaAbsRef.h" -#include "giaAbsRef2.h" +//#include "giaAbsRef2.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satSolver2.h" #include "base/main/main.h" @@ -52,7 +52,7 @@ struct Ga2_Man_t_ int nMarked; // total number of marked nodes and flops // refinement Rnm_Man_t * pRnm; // refinement manager - Rf2_Man_t * pRf2; // refinement manager +// Rf2_Man_t * pRf2; // refinement manager // SAT solver and variables Vec_Ptr_t * vId2Lit; // mapping, for each timeframe, of object ID into SAT literal sat_solver2 * pSat; // incremental SAT solver @@ -396,7 +396,7 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) Vec_IntPush( p->vAbs, 0 ); // refinement p->pRnm = Rnm_ManStart( pGia ); - p->pRf2 = Rf2_ManStart( pGia ); +// p->pRf2 = Rf2_ManStart( pGia ); // SAT solver and variables p->vId2Lit = Vec_PtrAlloc( 1000 ); // temporaries @@ -459,7 +459,7 @@ void Ga2_ManStop( Ga2_Man_t * p ) Vec_IntFree( p->vLits ); Vec_IntFree( p->vIsopMem ); Rnm_ManStop( p->pRnm, p->pPars->fVerbose ); - Rf2_ManStop( p->pRf2, p->pPars->fVerbose ); +// Rf2_ManStop( p->pRf2, p->pPars->fVerbose ); ABC_FREE( p->pTable ); ABC_FREE( p->pSopSizes ); ABC_FREE( p->pSops[1] ); @@ -1224,11 +1224,9 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p ) Gia_Obj_t * pObj; int i; Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap ); - -// Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 ); + // Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 ); vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1 ); // printf( "Refinement %d\n", Vec_IntSize(vVec) ); - Abc_CexFree( pCex ); if ( Vec_IntSize(vVec) == 0 ) { diff --git a/src/aig/gia/giaAbsRef.c b/src/aig/gia/giaAbsRef.c index 5b7bcee2..21a87c33 100644 --- a/src/aig/gia/giaAbsRef.c +++ b/src/aig/gia/giaAbsRef.c @@ -77,6 +77,7 @@ struct Rnm_Obj_t_ { unsigned Value : 1; // binary value unsigned fVisit : 1; // visited object + unsigned fVisit0 : 1; // visited object unsigned fPPi : 1; // PPI object unsigned Prio : 24; // priority (0 - highest) }; @@ -91,6 +92,8 @@ struct Rnm_Man_t_ int fVerbose; // verbose flag // traversing data Vec_Int_t * vObjs; // internal objects used in value propagation + Vec_Str_t * vCounts; // fanin counters + Vec_Int_t * vFanins; // fanins // internal data Rnm_Obj_t * pObjs; // refinement objects int nObjs; // the number of used objects @@ -98,6 +101,7 @@ struct Rnm_Man_t_ int nObjsFrame; // the number of used objects in each frame int nCalls; // total number of calls int nRefines; // total refined objects + int nVisited; // visited during justification // statistics clock_t timeFwd; // forward propagation clock_t timeBwd; // backward propagation @@ -114,6 +118,17 @@ static inline Rnm_Obj_t * Rnm_ManObj( Rnm_Man_t * p, Gia_Obj_t * pObj, int f ) return p->pObjs + f * p->nObjsFrame + pObj->Value; } +static inline int Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj)); } +static inline int Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj)); } +static inline int * Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1); } +static inline unsigned Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1); } +static inline int Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2); } +static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj ) { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v; } + +static inline int Rnm_ObjCount( Rnm_Man_t * p, Gia_Obj_t * pObj ) { return Vec_StrEntry( p->vCounts, Gia_ObjId(p->pGia, pObj) ); } +static inline void Rnm_ObjSetCount( Rnm_Man_t * p, Gia_Obj_t * pObj, int c ) { Vec_StrWriteEntry( p->vCounts, Gia_ObjId(p->pGia, pObj), (char)c ); } +static inline int Rnm_ObjAddToCount( Rnm_Man_t * p, Gia_Obj_t * pObj ) { int c = Rnm_ObjCount(p, pObj); if ( c < 16 ) Rnm_ObjSetCount(p, pObj, c+1); return c; } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -136,6 +151,8 @@ Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia ) p = ABC_CALLOC( Rnm_Man_t, 1 ); p->pGia = pGia; p->vObjs = Vec_IntAlloc( 100 ); + p->vCounts = Vec_StrStart( Gia_ManObjNum(pGia) ); + p->vFanins = Vec_IntAlloc( 100 ); p->nObjsAlloc = 10000; p->pObjs = ABC_ALLOC( Rnm_Obj_t, p->nObjsAlloc ); if ( p->pGia->vFanout == NULL ) @@ -168,6 +185,8 @@ void Rnm_ManStop( Rnm_Man_t * p, int fProfile ) Gia_ManCleanMark1(p->pGia); Gia_ManStaticFanoutStop(p->pGia); // Gia_ManSetPhase(p->pGia); + Vec_StrFree( p->vCounts ); + Vec_IntFree( p->vFanins ); Vec_IntFree( p->vObjs ); ABC_FREE( p->pObjs ); ABC_FREE( p ); @@ -332,6 +351,11 @@ void Rnm_ManJustifyPropFanout_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_I int i, k;//, Id = Gia_ObjId(p->pGia, pObj); assert( pRnm->fVisit == 0 ); pRnm->fVisit = 1; + if ( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 ) + { + Rnm_ManObj( p, pObj, 0 )->fVisit0 = 1; + p->nVisited++; + } if ( pRnm->fPPi ) { assert( (int)pRnm->Prio > 0 ); @@ -383,7 +407,14 @@ void Rnm_ManJustify_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSe if ( p->fPropFanout ) Rnm_ManJustifyPropFanout_rec( p, pObj, f, vSelect ); else + { pRnm->fVisit = 1; + if ( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 ) + { + Rnm_ManObj( p, pObj, 0 )->fVisit0 = 1; + p->nVisited++; + } + } if ( pRnm->fPPi ) { assert( (int)pRnm->Prio > 0 ); @@ -505,6 +536,177 @@ void Rnm_ManVerifyUsingTerSim( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap Abc_Print( 1, "\nRefinement verification has failed!!!\n" ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rnm_ManPrintSelected( Rnm_Man_t * p, Vec_Int_t * vSelected ) +{ + Gia_Obj_t * pObj; + int i, Counter = 0; + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + { + if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI + { + if ( Vec_IntFind(vSelected, Gia_ObjId(p->pGia, pObj)) >= 0 ) + printf( "1" ), Counter++; + else + printf( "0" ); + } + else + printf( "-" ); + } + printf( " %3d\n", Counter ); +} + + + + + +/**Function************************************************************* + + Synopsis [Perform structural analysis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ga2_StructAnalize( Gia_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInter, Vec_Int_t * vSelect ) +{ + Vec_Int_t * vLeaves; + Gia_Obj_t * pObj, * pFanin; + int i, k; + // clean labels + Gia_ManForEachObj( p, pObj, i ) + pObj->fMark0 = pObj->fMark1 = 0; + // label frontier + Gia_ManForEachObjVec( vFront, p, pObj, i ) + pObj->fMark0 = 1, pObj->fMark1 = 0; + // label objects + Gia_ManForEachObjVec( vInter, p, pObj, i ) + pObj->fMark1 = 0, pObj->fMark1 = 1; + // label selected + Gia_ManForEachObjVec( vSelect, p, pObj, i ) + pObj->fMark1 = 1, pObj->fMark1 = 1; + // explore selected + printf( "\n" ); + Gia_ManForEachObjVec( vSelect, p, pObj, i ) + { + printf( "Selected %6d : ", Gia_ObjId(p, pObj) ); + printf( "\n" ); + vLeaves = Ga2_ObjLeaves( p, pObj ); + Gia_ManForEachObjVec( vLeaves, p, pFanin, k ) + { + printf( " " ); + printf( "%6d ", Gia_ObjId(p, pFanin) ); + if ( pFanin->fMark0 && pFanin->fMark1 ) + printf( "select" ); + else if ( pFanin->fMark0 && !pFanin->fMark1 ) + printf( "front" ); + else if ( !pFanin->fMark0 && pFanin->fMark1 ) + printf( "internal" ); + else if ( !pFanin->fMark0 && !pFanin->fMark1 ) + printf( "new" ); + printf( "\n" ); + } + } +} + + +/**Function************************************************************* + + Synopsis [Finds essential objects.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ga2_FilterSelected( Rnm_Man_t * p, Vec_Int_t * vSelect ) +{ + Vec_Int_t * vNew, * vLeaves; + Gia_Obj_t * pObj, * pFanin; + int i, k, RetValue;//, Counters[3] = {0}; +/* + // check that selected are not visited + Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i ) + assert( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 1 ); + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + if ( Vec_IntFind(vSelect, Gia_ObjId(p->pGia, pObj)) == -1 ) + assert( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 ); +*/ + + // verify +// Gia_ManForEachObj( p->pGia, pObj, i ) +// assert( Rnm_ObjCount(p, pObj) == 0 ); + + // increment fanin counters + Vec_IntClear( p->vFanins ); + Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i ) + { + vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); + Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) + if ( Rnm_ObjAddToCount(p, pFanin) == 0 ) + Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin) ); + } + + // find selected objects, which create potential constraints + // - flop objects + // - objects whose fanin belongs to the justified area + // - objects whose fanins overlap + // (these do not guantee reconvergence, but may potentially have it) + // (other objects cannot have reconvergence, even if they are added) + vNew = Vec_IntAlloc( 100 ); + Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i ) + { + if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + Vec_IntPush( vNew, Gia_ObjId(p->pGia, pObj) ); + continue; + } + vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); + Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) + { + if ( Gia_ObjIsConst0(pFanin) + || (pFanin->Value && Rnm_ManObj(p, pFanin, 0)->fVisit0 == 1) + || Rnm_ObjCount(p, pFanin) > 1 + ) + { + Vec_IntPush( vNew, Gia_ObjId(p->pGia, pObj) ); + break; + } + } +// Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) +// { +// Counters[1] += (pFanin->Value && Rnm_ManObj( p, pFanin, 0 )->fVisit0 == 1); +// Counters[2] += (Rnm_ObjCount(p, pFanin) > 1); +// } + } + RetValue = Vec_IntUniqify( vNew ); + assert( RetValue == 0 ); + +// printf( "\n*** Select = %5d. New = %5d. Flops = %5d. Visited = %5d. Fanins = %5d.\n", +// Vec_IntSize(vSelect), Vec_IntSize(vNew), Counters[0], Counters[1], Counters[2] ); + + // clear fanin counters + Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i ) + Rnm_ObjSetCount( p, pObj, 0 ); + return vNew; +} + + /**Function************************************************************* Synopsis [Computes the refinement for a given counter-example.] @@ -518,8 +720,11 @@ void Rnm_ManVerifyUsingTerSim( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap ***********************************************************************/ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose ) { + int fVerify = 0; Vec_Int_t * vSelected = Vec_IntAlloc( 100 ); + Vec_Int_t * vNew; clock_t clk, clk2 = clock(); + int RetValue; p->nCalls++; // Gia_ManCleanValue( p->pGia ); // initialize @@ -542,17 +747,43 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in p->timeFwd += clock() - clk; // select refinement clk = clock(); + p->nVisited = 0; Rnm_ManJustify_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), pCex->iFrame, vSelected ); + RetValue = Vec_IntUniqify( vSelected ); +// assert( RetValue == 0 ); p->timeBwd += clock() - clk; } + + vNew = Ga2_FilterSelected( p, vSelected ); + if ( Vec_IntSize(vNew) > 0 ) + { + Vec_IntFree( vSelected ); + vSelected = vNew; + } + else + { + Vec_IntFree( vNew ); +// printf( "\nBig refinement.\n" ); + } + // clean values Rnm_ManCleanValues( p ); + // verify (empty) refinement - clk = clock(); - Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected ); - Vec_IntUniqify( vSelected ); + if ( fVerify ) + { + clk = clock(); + Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected ); + p->timeVer += clock() - clk; + } + +// printf( "\nOriginal (%d): \n", Vec_IntSize(p->vMap) ); +// Rnm_ManPrintSelected( p, vSelected ); + +// Ga2_StructAnalize( p->pGia, vMap, p->vObjs, vSelected ); +// printf( "\nObjects = %5d. Visited = %5d.\n", Vec_IntSize(p->vObjs), p->nVisited ); + // Vec_IntReverseOrder( vSelected ); - p->timeVer += clock() - clk; p->timeTotal += clock() - clk2; p->nRefines += Vec_IntSize(vSelected); return vSelected; diff --git a/src/aig/gia/giaAbsRef2.c b/src/aig/gia/giaAbsRef2.c index 03f1d9a2..e5bf3b0f 100644 --- a/src/aig/gia/giaAbsRef2.c +++ b/src/aig/gia/giaAbsRef2.c @@ -93,7 +93,8 @@ struct Rf2_Man_t_ Vec_Int_t * vObjs; // internal objects used in value propagation Vec_Int_t * vFanins; // fanins of the PPI nodes Vec_Int_t * pvVecs; // vectors of integers for each object - Vec_Vec_t * vNod2Ppi; // for each node, the set of PPIs to include + Vec_Vec_t * vGrp2Ppi; // for each node, the set of PPIs to include + int nMapWords; // internal data Rf2_Obj_t * pObjs; // refinement objects int nObjs; // the number of used objects @@ -122,6 +123,76 @@ static inline Vec_Int_t * Rf2_ObjVec( Rf2_Man_t * p, Gia_Obj_t * pObj ) return p->pvVecs + Gia_ObjId(p->pGia, pObj); } + +static inline unsigned * Rf2_ObjA( Rf2_Man_t * p, Gia_Obj_t * pObj ) +{ + return (unsigned *)Vec_IntArray(Rf2_ObjVec(p, pObj)); +} +static inline unsigned * Rf2_ObjN( Rf2_Man_t * p, Gia_Obj_t * pObj ) +{ + return (unsigned *)Vec_IntArray(Rf2_ObjVec(p, pObj)) + p->nMapWords; +} +static inline void Rf2_ObjClear( Rf2_Man_t * p, Gia_Obj_t * pObj ) +{ + Vec_IntFill( Rf2_ObjVec(p, pObj), 2*p->nMapWords, 0 ); +} +static inline void Rf2_ObjStart( Rf2_Man_t * p, Gia_Obj_t * pObj, int i ) +{ + Vec_Int_t * vVec = Rf2_ObjVec(p, pObj); + int w; + Vec_IntClear( vVec ); + for ( w = 0; w < p->nMapWords; w++ ) + Vec_IntPush( vVec, 0 ); + for ( w = 0; w < p->nMapWords; w++ ) + Vec_IntPush( vVec, ~0 ); + Abc_InfoSetBit( Rf2_ObjA(p, pObj), i ); + Abc_InfoXorBit( Rf2_ObjN(p, pObj), i ); +} +static inline void Rf2_ObjCopy( Rf2_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanin ) +{ + assert( Vec_IntSize(Rf2_ObjVec(p, pObj)) == 2*p->nMapWords ); + memcpy( Rf2_ObjA(p, pObj), Rf2_ObjA(p, pFanin), sizeof(unsigned) * 2 * p->nMapWords ); +} +static inline void Rf2_ObjDeriveAnd( Rf2_Man_t * p, Gia_Obj_t * pObj, int One ) +{ + unsigned * pInfo, * pInfo0, * pInfo1; + int i; + assert( Gia_ObjIsAnd(pObj) ); + assert( One == (int)pObj->fMark0 ); + assert( One == (int)(Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) ); + assert( One == (int)(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) ); + assert( Vec_IntSize(Rf2_ObjVec(p, pObj)) == 2*p->nMapWords ); + + pInfo = Rf2_ObjA( p, pObj ); + pInfo0 = Rf2_ObjA( p, Gia_ObjFanin0(pObj) ); + pInfo1 = Rf2_ObjA( p, Gia_ObjFanin1(pObj) ); + for ( i = 0; i < p->nMapWords; i++ ) + pInfo[i] = One ? (pInfo0[i] & pInfo1[i]) : (pInfo0[i] | pInfo1[i]); + + pInfo = Rf2_ObjN( p, pObj ); + pInfo0 = Rf2_ObjN( p, Gia_ObjFanin0(pObj) ); + pInfo1 = Rf2_ObjN( p, Gia_ObjFanin1(pObj) ); + for ( i = 0; i < p->nMapWords; i++ ) + pInfo[i] = One ? (pInfo0[i] | pInfo1[i]) : (pInfo0[i] & pInfo1[i]); +} +static inline void Rf2_ObjPrint( Rf2_Man_t * p, Gia_Obj_t * pRoot ) +{ + Gia_Obj_t * pObj; + unsigned * pInfo; + int i; + pInfo = Rf2_ObjA( p, pRoot ); + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + if ( !Gia_ObjIsPi(p->pGia, pObj) ) + printf( "%d", Abc_InfoHasBit(pInfo, i) ); + printf( "\n" ); + pInfo = Rf2_ObjN( p, pRoot ); + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + if ( !Gia_ObjIsPi(p->pGia, pObj) ) + printf( "%d", !Abc_InfoHasBit(pInfo, i) ); + printf( "\n" ); + +} + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -146,7 +217,7 @@ Rf2_Man_t * Rf2_ManStart( Gia_Man_t * pGia ) p->vObjs = Vec_IntAlloc( 1000 ); p->vFanins = Vec_IntAlloc( 1000 ); p->pvVecs = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(pGia) ); - p->vNod2Ppi = Vec_VecStart( 100 ); + p->vGrp2Ppi = Vec_VecStart( 100 ); Gia_ManCleanMark0(pGia); Gia_ManCleanMark1(pGia); return p; @@ -171,7 +242,7 @@ void Rf2_ManStop( Rf2_Man_t * p, int fProfile ) } Vec_IntFree( p->vObjs ); Vec_IntFree( p->vFanins ); - Vec_VecFree( p->vNod2Ppi ); + Vec_VecFree( p->vGrp2Ppi ); ABC_FREE( p->pvVecs ); ABC_FREE( p ); } @@ -471,9 +542,14 @@ void Rf2_ManGatherFanins( Rf2_Man_t * p, int Depth ) SeeAlso [] ***********************************************************************/ -int Rf2_ManCountPis( Rf2_Man_t * p ) +static inline int Rf2_ManCountPpis( Rf2_Man_t * p ) { - return 0; + Gia_Obj_t * pObj; + int i, Counter = 0; + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI + Counter++; + return Counter; } /**Function************************************************************* @@ -487,9 +563,40 @@ int Rf2_ManCountPis( Rf2_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Rf2_ManProcessVector( Vec_Int_t * p, int Limit ) +static inline void Rf2_ManPrintVector( Vec_Int_t * p, int Num ) { + int i, k, Entry; + Vec_IntForEachEntry( p, Entry, i ) + { + for ( k = 0; k < Num; k++ ) + printf( "%c", '0' + ((Entry>>k) & 1) ); + printf( "\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Sort, make dup- and containment-free, and filter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Rf2_ManProcessVector( Vec_Int_t * p, int Limit ) +{ +// int Start = Vec_IntSize(p); + int Start = 0; int i, j, k, Entry, Entry2; +// printf( "%d", Vec_IntSize(p) ); + if ( Start > 5 ) + { + printf( "Before: \n" ); + Rf2_ManPrintVector( p, 31 ); + } + k = 0; Vec_IntForEachEntry( p, Entry, i ) if ( Gia_WordCountOnes((unsigned)Entry) <= Limit ) @@ -506,11 +613,18 @@ void Rf2_ManProcessVector( Vec_Int_t * p, int Limit ) Vec_IntWriteEntry( p, k++, Entry ); } Vec_IntShrink( p, k ); +// printf( "->%d ", Vec_IntSize(p) ); + if ( Start > 5 ) + { + printf( "After: \n" ); + Rf2_ManPrintVector( p, 31 ); + k = 0; + } } /**Function************************************************************* - Synopsis [Sort, make dup- and containment-free, and filter.] + Synopsis [Assigns a unique justifification ID for each PPI.] Description [] @@ -519,18 +633,23 @@ void Rf2_ManProcessVector( Vec_Int_t * p, int Limit ) SeeAlso [] ***********************************************************************/ -void Rf2_ManPrintVector( Vec_Int_t * p, int Num ) +int Rf2_ManAssignJustIds( Rf2_Man_t * p ) { - extern void Extra_PrintBinary( FILE * pFile, unsigned * p, int nBits ); - int i, Entry; - printf( "Justification containing %d subsets.\n", Vec_IntSize(p) ); - Vec_IntForEachEntry( p, Entry, i ) - Extra_PrintBinary( stdout, (unsigned *)&Entry, Num ), printf( "\n" ); + Gia_Obj_t * pObj; + int nPpis = Rf2_ManCountPpis( p ); + int nGroupSize = (nPpis / 30) + (nPpis % 30 > 0); + int i, k = 0; + Vec_VecClear( p->vGrp2Ppi ); + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI + Vec_VecPushInt( p->vGrp2Ppi, (k++ / nGroupSize), i ); + printf( "Considering %d PPIs combined into %d groups of size %d.\n", k, (k-1)/nGroupSize+1, nGroupSize ); + return (k-1)/nGroupSize+1; } /**Function************************************************************* - Synopsis [Assigns a unique justifification ID for each PPI.] + Synopsis [Sort, make dup- and containment-free, and filter.] Description [] @@ -539,15 +658,31 @@ void Rf2_ManPrintVector( Vec_Int_t * p, int Num ) SeeAlso [] ***********************************************************************/ -void Rf2_ManAssignJustIds( Rf2_Man_t * p ) +static inline void Rf2_ManPrintVectorSpecial( Rf2_Man_t * p, Vec_Int_t * vVec ) { Gia_Obj_t * pObj; - int i, k = 0; - Vec_VecClear( p->vNod2Ppi ); - Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) - if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI - Vec_VecPushInt( p->vNod2Ppi, k++, i ); - printf( "Considering %d PPIs with unique justification IDs.\n", k ); + int nPpis = Rf2_ManCountPpis( p ); + int nGroupSize = (nPpis / 30) + (nPpis % 30 > 0); + int s, i, k, Entry, Counter; + + Vec_IntForEachEntry( vVec, Entry, s ) + { + k = 0; + Counter = 0; + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + { + if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI + { + if ( (Entry >> (k++ / nGroupSize)) & 1 ) + printf( "1" ), Counter++; + else + printf( "0" ); + } + else + printf( "-" ); + } + printf( " %3d \n", Counter ); + } } /**Function************************************************************* @@ -581,7 +716,7 @@ Vec_Int_t * Rf2_ManPropagate( Rf2_Man_t * p, int Limit ) Vec_IntFill( Rf2_ObjVec(p, pObj), 1, 0 ); } // assign justification sets for PPis - Vec_VecForEachLevelInt( p->vNod2Ppi, vVec, i ) + Vec_VecForEachLevelInt( p->vGrp2Ppi, vVec, i ) Vec_IntForEachEntry( vVec, Entry, k ) { assert( i < 31 ); @@ -615,11 +750,11 @@ Vec_Int_t * Rf2_ManPropagate( Rf2_Man_t * p, int Limit ) continue; } assert( Gia_ObjIsAnd(pObj) ); + vVec0 = Rf2_ObjVec(p, Gia_ObjFanin0(pObj)); + vVec1 = Rf2_ObjVec(p, Gia_ObjFanin1(pObj)); pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); if ( pObj->fMark0 == 1 ) { - vVec0 = Rf2_ObjVec(p, Gia_ObjFanin0(pObj)); - vVec1 = Rf2_ObjVec(p, Gia_ObjFanin1(pObj)); Vec_IntForEachEntry( vVec0, Entry, k ) Vec_IntForEachEntry( vVec1, Entry2, j ) Vec_IntPush( vVec, Entry | Entry2 ); @@ -643,6 +778,77 @@ Vec_Int_t * Rf2_ManPropagate( Rf2_Man_t * p, int Limit ) return Rf2_ObjVec(p, Gia_ManPo(p->pGia, 0)); } +/**Function************************************************************* + + Synopsis [Performs justification propagation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rf2_ManBounds( Rf2_Man_t * p ) +{ + Gia_Obj_t * pObj; + int f, i, iBit = p->pCex->nRegs; + // init constant + pObj = Gia_ManConst0(p->pGia); + pObj->fMark0 = 0; + Rf2_ObjStart( p, pObj, Vec_IntSize(p->vMap) + Vec_IntSize(p->vObjs) ); + // iterate through the timeframes + for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis ) + { + // initialize frontier values and init justification sets + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + { + assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ); + pObj->fMark0 = Abc_InfoHasBit( p->pCex->pData, iBit + i ); + Rf2_ObjStart( p, pObj, i ); + } + // propagate internal nodes + Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i ) + { + pObj->fMark0 = 0; + Rf2_ObjClear( p, pObj ); + if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + if ( f == 0 ) + { + Rf2_ObjStart( p, pObj, Vec_IntSize(p->vMap) + i ); + continue; + } + pObj->fMark0 = Gia_ObjRoToRi(p->pGia, pObj)->fMark0; + Rf2_ObjCopy( p, pObj, Gia_ObjRoToRi(p->pGia, pObj) ); + continue; + } + if ( Gia_ObjIsCo(pObj) ) + { + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)); + Rf2_ObjCopy( p, pObj, Gia_ObjFanin0(pObj) ); + continue; + } + assert( Gia_ObjIsAnd(pObj) ); + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + if ( pObj->fMark0 == 1 ) + Rf2_ObjDeriveAnd( p, pObj, 1 ); + else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 ) + Rf2_ObjDeriveAnd( p, pObj, 0 ); + else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 ) + Rf2_ObjCopy( p, pObj, Gia_ObjFanin0(pObj) ); + else + Rf2_ObjCopy( p, pObj, Gia_ObjFanin1(pObj) ); + } + } + assert( iBit == p->pCex->nBits ); + if ( Gia_ManPo(p->pGia, 0)->fMark0 != 1 ) + printf( "Output value is incorrect.\n" ); + + printf( "Bounds: \n" ); + Rf2_ObjPrint( p, Gia_ManPo(p->pGia, 0) ); +} + /**Function************************************************************* Synopsis [Computes the refinement for a given counter-example.] @@ -657,8 +863,10 @@ Vec_Int_t * Rf2_ManPropagate( Rf2_Man_t * p, int Limit ) Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose ) { Vec_Int_t * vJusts; - Vec_Int_t * vSelected = Vec_IntAlloc( 100 ); +// Vec_Int_t * vSelected = Vec_IntAlloc( 100 ); + Vec_Int_t * vSelected = NULL; clock_t clk, clk2 = clock(); + int nGroups; p->nCalls++; // initialize p->pCex = pCex; @@ -670,15 +878,23 @@ Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in // collect reconvergence points // Rf2_ManGatherFanins( p, 2 ); // propagate justification IDs - Rf2_ManAssignJustIds( p ); - vJusts = Rf2_ManPropagate( p, 100 ); - Rf2_ManPrintVector( vJusts, Rf2_ManCountPis(p) ); + nGroups = Rf2_ManAssignJustIds( p ); + vJusts = Rf2_ManPropagate( p, 32 ); + +// printf( "\n" ); +// Rf2_ManPrintVector( vJusts, nGroups ); + Rf2_ManPrintVectorSpecial( p, vJusts ); if ( Vec_IntSize(vJusts) == 0 ) { printf( "Empty set of justifying subsets.\n" ); return NULL; } + +// p->nMapWords = Abc_BitWordNum( Vec_IntSize(p->vMap) + Vec_IntSize(p->vObjs) + 1 ); // Map + Flops + Const +// Rf2_ManBounds( p ); + // select the result +// Abc_PrintTime( 1, "Time", clock() - clk2 ); // verify (empty) refinement clk = clock(); @@ -687,7 +903,7 @@ Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in // Vec_IntReverseOrder( vSelected ); p->timeVer += clock() - clk; p->timeTotal += clock() - clk2; - p->nRefines += Vec_IntSize(vSelected); +// p->nRefines += Vec_IntSize(vSelected); return vSelected; } diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 6988c8ea..a7722866 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -1170,23 +1170,25 @@ static inline void Vec_IntSort( Vec_Int_t * p, int fReverse ) Synopsis [Leaves only unique entries.] - Description [] + Description [Returns the number of duplicated entried found.] SideEffects [] SeeAlso [] ***********************************************************************/ -static inline void Vec_IntUniqify( Vec_Int_t * p ) +static inline int Vec_IntUniqify( Vec_Int_t * p ) { - int i, k; + int i, k, RetValue; if ( p->nSize < 2 ) - return; + return 0; Vec_IntSort( p, 0 ); for ( i = k = 1; i < p->nSize; i++ ) if ( p->pArray[i] != p->pArray[i-1] ) p->pArray[k++] = p->pArray[i]; + RetValue = p->nSize - k; p->nSize = k; + return RetValue; } /**Function************************************************************* -- cgit v1.2.3