diff options
| -rw-r--r-- | src/aig/gia/giaUtil.c | 1 | ||||
| -rw-r--r-- | src/proof/ssc/sscClass.c | 61 | ||||
| -rw-r--r-- | src/proof/ssc/sscCore.c | 87 | ||||
| -rw-r--r-- | src/proof/ssc/sscInt.h | 2 | ||||
| -rw-r--r-- | src/proof/ssc/sscSim.c | 72 |
5 files changed, 201 insertions, 22 deletions
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index c0a222dd..5288bf35 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -370,6 +370,7 @@ void Gia_ManSetPhasePattern( Gia_Man_t * p, Vec_Int_t * vCiValues ) { Gia_Obj_t * pObj; int i; + assert( Gia_ManCiNum(p) == Vec_IntSize(vCiValues) ); Gia_ManForEachObj( p, pObj, i ) if ( Gia_ObjIsCi(pObj) ) pObj->fPhase = Vec_IntEntry( vCiValues, Gia_ObjCioId(pObj) ); diff --git a/src/proof/ssc/sscClass.c b/src/proof/ssc/sscClass.c index a9904148..c6b96a90 100644 --- a/src/proof/ssc/sscClass.c +++ b/src/proof/ssc/sscClass.c @@ -107,6 +107,12 @@ static inline int Ssc_GiaSimAreEqual( Gia_Man_t * p, int iObj0, int iObj1 ) } return 1; } +static inline int Ssc_GiaSimAreEqualBit( Gia_Man_t * p, int iObj0, int iObj1 ) +{ + Gia_Obj_t * pObj0 = Gia_ManObj( p, iObj0 ); + Gia_Obj_t * pObj1 = Gia_ManObj( p, iObj1 ); + return (pObj0->fPhase ^ pObj0->fMark0) == (pObj1->fPhase ^ pObj1->fMark0); +} /**Function************************************************************* @@ -141,10 +147,58 @@ void Ssc_GiaSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass ) } Gia_ObjSetNext( p, EntPrev, 0 ); } + +/**Function************************************************************* + + Synopsis [Refines one equivalence class using individual bit-pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssc_GiaSimClassRefineOneBit( Gia_Man_t * p, int i ) +{ + Gia_Obj_t * pObj; + int Ent; + assert( Gia_ObjIsHead( p, i ) ); + Vec_IntClear( p->vClassOld ); + Vec_IntClear( p->vClassNew ); + Vec_IntPush( p->vClassOld, i ); + pObj = Gia_ManObj(p, i); + Gia_ClassForEachObj1( p, i, Ent ) + { + if ( Ssc_GiaSimAreEqualBit( p, i, Ent ) ) + Vec_IntPush( p->vClassOld, Ent ); + else + Vec_IntPush( p->vClassNew, Ent ); + } + if ( Vec_IntSize( p->vClassNew ) == 0 ) + return 0; + Ssc_GiaSimClassCreate( p, p->vClassOld ); + Ssc_GiaSimClassCreate( p, p->vClassNew ); + return 1; +} + + +/**Function************************************************************* + + Synopsis [Refines one class using simulation patterns.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Ssc_GiaSimClassRefineOne( Gia_Man_t * p, int i ) { Gia_Obj_t * pObj; int Ent; + assert( Gia_ObjIsHead( p, i ) ); Vec_IntClear( p->vClassOld ); Vec_IntClear( p->vClassNew ); Vec_IntPush( p->vClassOld, i ); @@ -226,17 +280,18 @@ int Ssc_GiaClassesRefine( Gia_Man_t * p ) { Vec_Int_t * vRefinedC; Gia_Obj_t * pObj; - int i; + int i, Counter = 0; if ( p->pReprs != NULL ); vRefinedC = Vec_IntAlloc( 100 ); Gia_ManForEachCand( p, pObj, i ) if ( Gia_ObjIsTail(p, i) ) - Ssc_GiaSimClassRefineOne( p, Gia_ObjRepr(p, i) ); + Counter += Ssc_GiaSimClassRefineOne( p, Gia_ObjRepr(p, i) ); else if ( Gia_ObjIsConst(p, i) && !Ssc_GiaSimIsConst0(p, i) ) Vec_IntPush( vRefinedC, i ); Ssc_GiaSimProcessRefined( p, vRefinedC ); + Counter += Vec_IntSize( vRefinedC ); Vec_IntFree( vRefinedC ); - return 0; + return Counter; } diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c index 55f0e140..43d0e250 100644 --- a/src/proof/ssc/sscCore.c +++ b/src/proof/ssc/sscCore.c @@ -119,6 +119,7 @@ Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPar p->vFanins = Vec_IntAlloc( 100 ); p->vFront = Vec_IntAlloc( 100 ); Ssc_GiaClassesInit( pAig ); + // now it is ready for refinement using simulation return p; } void Ssc_ManPrintStats( Ssc_Man_t * p ) @@ -144,6 +145,65 @@ void Ssc_ManPrintStats( Ssc_Man_t * p ) /**Function************************************************************* + Synopsis [Refine one class by resimulating one pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssc_GiaSimulatePatternFraig_rec( Ssc_Man_t * p, int iFraigObj ) +{ + Gia_Obj_t * pObj; + int Res0, Res1; + if ( Ssc_ObjSatVar(p, iFraigObj) ) + return sat_solver_var_value( p->pSat, Ssc_ObjSatVar(p, iFraigObj) ); + pObj = Gia_ManObj( p->pFraig, iFraigObj ); + assert( Gia_ObjIsAnd(pObj) ); + Res0 = Ssc_GiaSimulatePatternFraig_rec( p, Gia_ObjFaninId0(pObj, iFraigObj) ); + Res1 = Ssc_GiaSimulatePatternFraig_rec( p, Gia_ObjFaninId1(pObj, iFraigObj) ); + pObj->fMark0 = (Res0 ^ Gia_ObjFaninC0(pObj)) & (Res1 ^ Gia_ObjFaninC1(pObj)); + return pObj->fMark0; +} +int Ssc_GiaSimulatePattern_rec( Ssc_Man_t * p, Gia_Obj_t * pObj ) +{ + int Res0, Res1; + if ( Gia_ObjIsTravIdCurrent(p->pAig, pObj) ) + return pObj->fMark0; + Gia_ObjSetTravIdCurrent(p->pAig, pObj); + if ( ~pObj->Value ) // mapping into FRAIG exists - simulate FRAIG + { + Res0 = Ssc_GiaSimulatePatternFraig_rec( p, Abc_Lit2Var(pObj->Value) ); + pObj->fMark0 = Res0 ^ Abc_LitIsCompl(pObj->Value); + } + else // mapping into FRAIG does not exist - simulate AIG + { + Res0 = Ssc_GiaSimulatePattern_rec( p, Gia_ObjFanin0(pObj) ); + Res1 = Ssc_GiaSimulatePattern_rec( p, Gia_ObjFanin1(pObj) ); + pObj->fMark0 = (Res0 ^ Gia_ObjFaninC0(pObj)) & (Res1 ^ Gia_ObjFaninC1(pObj)); + } + return pObj->fMark0; +} +int Ssc_GiaResimulateOneClass( Ssc_Man_t * p, int iRepr, int iObj ) +{ + int Ent, RetValue; + assert( iRepr == Gia_ObjRepr(p->pAig, iObj) ); + assert( Gia_ObjIsHead( p->pAig, iRepr ) ); + // set bit-values at the nodes according to the counter-example + Gia_ManIncrementTravId( p->pAig ); + Gia_ClassForEachObj( p->pAig, iRepr, Ent ) + Ssc_GiaSimulatePattern_rec( p, Gia_ManObj(p->pAig, Ent) ); + // refine one class using these bit-values + RetValue = Ssc_GiaSimClassRefineOneBit( p->pAig, iRepr ); + // check that the candidate equivalence is indeed refined + assert( iRepr != Gia_ObjRepr(p->pAig, iObj) ); + return RetValue; +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -159,7 +219,7 @@ Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t Gia_Man_t * pResult; Gia_Obj_t * pObj, * pRepr; clock_t clk, clkTotal = clock(); - int i, fCompl, status; + int i, fCompl, nRefined, status; clk = clock(); assert( Gia_ManRegNum(pCare) == 0 ); assert( Gia_ManCiNum(pAig) == Gia_ManCiNum(pCare) ); @@ -172,18 +232,23 @@ clk = clock(); if ( p == NULL ) return Gia_ManDup( pAig ); if ( p->pPars->fVerbose ) - printf( "Care set produced %d hits out of %d.\n", Ssc_GiaEstimateCare(p->pFraig, 10), 640 ); + printf( "Care set produced %d hits out of %d.\n", Ssc_GiaEstimateCare(p->pFraig, 5), 640 ); // perform simulation - if ( Gia_ManAndNum(pCare) == 0 ) // no constraints + while ( 1 ) { - for ( i = 0; i < 16; i++ ) - { - Ssc_GiaRandomPiPattern( pAig, 10, NULL ); - Ssc_GiaSimRound( pAig ); - if ( pPars->fVerbose ) - Ssc_GiaClassesRefine( pAig ); + // simulate care set + Ssc_GiaRandomPiPattern( p->pFraig, 5, NULL ); + Ssc_GiaSimRound( p->pFraig ); + // transfer care patterns to user's AIG + if ( !Ssc_GiaTransferPiPattern( pAig, p->pFraig, p->vPivot ) ) + break; + // simulate the main AIG + Ssc_GiaSimRound( pAig ); + nRefined = Ssc_GiaClassesRefine( pAig ); + if ( pPars->fVerbose ) Gia_ManEquivPrintClasses( pAig, 0, 0 ); - } + if ( nRefined <= Gia_ManCandNum(pAig) / 100 ) + break; } p->timeSimInit += clock() - clk; @@ -242,6 +307,8 @@ clk = clock(); Vec_IntPush( p->vDisPairs, i ); // printf( "Try %2d and %2d: ", Gia_ObjRepr(p->pAig, i), i ); // Vec_IntPrint( p->vPattern ); + if ( Gia_ObjRepr(p->pAig, i) > 0 ) + Ssc_GiaResimulateOneClass( p, Gia_ObjRepr(p->pAig, i), i ); } else if ( status == l_Undef ) p->nSatCallsUndec++; diff --git a/src/proof/ssc/sscInt.h b/src/proof/ssc/sscInt.h index 1226f4ee..0be25174 100644 --- a/src/proof/ssc/sscInt.h +++ b/src/proof/ssc/sscInt.h @@ -102,6 +102,7 @@ static inline void Ssc_ObjSetFraig( Gia_Obj_t * pObj, int iNode ) { pObj extern void Ssc_GiaClassesInit( Gia_Man_t * p ); extern int Ssc_GiaClassesRefine( Gia_Man_t * p ); extern void Ssc_GiaClassesCheckPairs( Gia_Man_t * p, Vec_Int_t * vDisPairs ); +extern int Ssc_GiaSimClassRefineOneBit( Gia_Man_t * p, int i ); /*=== sscCnf.c ===================================================*/ extern void Ssc_CnfNodeAddToSolver( Ssc_Man_t * p, Gia_Obj_t * pObj ); /*=== sscCore.c ==================================================*/ @@ -113,6 +114,7 @@ extern int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iObj /*=== sscSim.c ===================================================*/ extern void Ssc_GiaResetPiPattern( Gia_Man_t * p, int nWords ); extern void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot ); +extern int Ssc_GiaTransferPiPattern( Gia_Man_t * pAig, Gia_Man_t * pCare, Vec_Int_t * vPivot ); extern void Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat ); extern void Ssc_GiaSimRound( Gia_Man_t * p ); extern Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p ); diff --git a/src/proof/ssc/sscSim.c b/src/proof/ssc/sscSim.c index d28db432..ae9a3eec 100644 --- a/src/proof/ssc/sscSim.c +++ b/src/proof/ssc/sscSim.c @@ -175,6 +175,56 @@ void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot ) // Extra_PrintBinary( stdout, (unsigned *)pSimPi, 64 ), printf( "\n" ); } } +void Ssc_GiaPrintPiPatterns( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + word * pSimAig; + int i, nWords = Gia_ObjSimWords( p ); + Gia_ManForEachCi( p, pObj, i ) + { + pSimAig = Gia_ObjSimObj( p, pObj ); +// Extra_PrintBinary( stdout, pSimAig, 64 * nWords ); + } +} + +/**Function************************************************************* + + Synopsis [Transfer the simulation pattern from pCare to pAig.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssc_GiaTransferPiPattern( Gia_Man_t * pAig, Gia_Man_t * pCare, Vec_Int_t * vPivot ) +{ + extern word * Ssc_GiaGetCareMask( Gia_Man_t * p ); + Gia_Obj_t * pObj; + int i, w, nWords = Gia_ObjSimWords( pCare ); + word * pCareMask = Ssc_GiaGetCareMask( pCare ); + int Count = Ssc_SimCountBits( pCareMask, nWords ); + word * pSimPiCare, * pSimPiAig; + if ( Count == 0 ) + { + ABC_FREE( pCareMask ); + return 0; + } + Ssc_GiaResetPiPattern( pAig, nWords ); + Gia_ManForEachCi( pCare, pObj, i ) + { + pSimPiAig = Gia_ObjSimPi( pAig, i ); + pSimPiCare = Gia_ObjSimObj( pCare, pObj ); + for ( w = 0; w < nWords; w++ ) + if ( Vec_IntEntry(vPivot, i) ) + pSimPiAig[w] = pSimPiCare[w] | ~pCareMask[w]; + else + pSimPiAig[w] = pSimPiCare[w] & pCareMask[w]; + } + ABC_FREE( pCareMask ); + return Count; +} /**Function************************************************************* @@ -246,14 +296,21 @@ void Ssc_GiaSimRound( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p ) +word * Ssc_GiaGetCareMask( Gia_Man_t * p ) { - Vec_Int_t * vInit; Gia_Obj_t * pObj; - int i, iBit, nWords = Gia_ObjSimWords( p ); + int i, nWords = Gia_ObjSimWords( p ); word * pRes = ABC_FALLOC( word, nWords ); Gia_ManForEachPo( p, pObj, i ) Ssc_SimAnd( pRes, pRes, Gia_ObjSimObj(p, pObj), nWords, 0, 0 ); + return pRes; +} +Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p ) +{ + Vec_Int_t * vInit; + Gia_Obj_t * pObj; + int i, iBit, nWords = Gia_ObjSimWords( p ); + word * pRes = Ssc_GiaGetCareMask( p ); iBit = Ssc_SimFindBit( pRes, nWords ); ABC_FREE( pRes ); if ( iBit == -1 ) @@ -285,12 +342,9 @@ Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p ) ***********************************************************************/ int Ssc_GiaCountCaresSim( Gia_Man_t * p ) { - Gia_Obj_t * pObj; - int i, Count, nWords = Gia_ObjSimWords( p ); - word * pRes = ABC_FALLOC( word, nWords ); - Gia_ManForEachPo( p, pObj, i ) - Ssc_SimAnd( pRes, pRes, Gia_ObjSimObj(p, pObj), nWords, 0, 0 ); - Count = Ssc_SimCountBits( pRes, nWords ); + word * pRes = Ssc_GiaGetCareMask( p ); + int nWords = Gia_ObjSimWords( p ); + int Count = Ssc_SimCountBits( pRes, nWords ); ABC_FREE( pRes ); return Count; } |