| /**CFile**************************************************************** |
| |
| FileName [gia.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Scalable AIG package.] |
| |
| Synopsis [] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "gia.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| // combinational simulation manager |
| typedef struct Hcd_Man_t_ Hcd_Man_t; |
| struct Hcd_Man_t_ |
| { |
| // parameters |
| Gia_Man_t * pGia; // the AIG to be used for simulation |
| int nBTLimit; // internal backtrack limit |
| int fVerbose; // internal verbose flag |
| // internal variables |
| unsigned * pSimInfo; // simulation info for each object |
| Vec_Ptr_t * vSimInfo; // pointers to the CI simulation info |
| Vec_Ptr_t * vSimPres; // pointers to the presense of simulation info |
| // temporaries |
| Vec_Int_t * vClassOld; // old class numbers |
| Vec_Int_t * vClassNew; // new class numbers |
| Vec_Int_t * vClassTemp; // temporary storage |
| Vec_Int_t * vRefinedC; // refined const reprs |
| }; |
| |
| static inline unsigned Hcd_ObjSim( Hcd_Man_t * p, int Id ) { return p->pSimInfo[Id]; } |
| static inline unsigned * Hcd_ObjSimP( Hcd_Man_t * p, int Id ) { return p->pSimInfo + Id; } |
| static inline unsigned Hcd_ObjSetSim( Hcd_Man_t * p, int Id, unsigned n ) { return p->pSimInfo[Id] = n; } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Starts the fraiging manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Hcd_Man_t * Gia_ManEquivStart( Gia_Man_t * pGia, int nBTLimit, int fVerbose ) |
| { |
| Hcd_Man_t * p; |
| Gia_Obj_t * pObj; |
| int i; |
| p = ABC_CALLOC( Hcd_Man_t, 1 ); |
| p->pGia = pGia; |
| p->nBTLimit = nBTLimit; |
| p->fVerbose = fVerbose; |
| p->pSimInfo = ABC_ALLOC( unsigned, Gia_ManObjNum(pGia) ); |
| p->vClassOld = Vec_IntAlloc( 100 ); |
| p->vClassNew = Vec_IntAlloc( 100 ); |
| p->vClassTemp = Vec_IntAlloc( 100 ); |
| p->vRefinedC = Vec_IntAlloc( 100 ); |
| // collect simulation info |
| p->vSimInfo = Vec_PtrAlloc( 1000 ); |
| Gia_ManForEachCi( pGia, pObj, i ) |
| Vec_PtrPush( p->vSimInfo, Hcd_ObjSimP(p, Gia_ObjId(pGia,pObj)) ); |
| p->vSimPres = Vec_PtrAllocSimInfo( Gia_ManCiNum(pGia), 1 ); |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Starts the fraiging manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManEquivStop( Hcd_Man_t * p ) |
| { |
| Vec_PtrFree( p->vSimInfo ); |
| Vec_PtrFree( p->vSimPres ); |
| Vec_IntFree( p->vClassOld ); |
| Vec_IntFree( p->vClassNew ); |
| Vec_IntFree( p->vClassTemp ); |
| Vec_IntFree( p->vRefinedC ); |
| ABC_FREE( p->pSimInfo ); |
| ABC_FREE( p ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Compared two simulation infos.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Hcd_ManCompareEqual( unsigned s0, unsigned s1 ) |
| { |
| if ( (s0 & 1) == (s1 & 1) ) |
| return s0 == s1; |
| else |
| return s0 ==~s1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Compares one simulation info.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Hcd_ManCompareConst( unsigned s ) |
| { |
| if ( s & 1 ) |
| return s ==~0; |
| else |
| return s == 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates one equivalence class.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Hcd_ManClassCreate( Gia_Man_t * pGia, Vec_Int_t * vClass ) |
| { |
| int Repr = -1, EntPrev = -1, Ent, i; |
| assert( Vec_IntSize(vClass) > 0 ); |
| Vec_IntForEachEntry( vClass, Ent, i ) |
| { |
| if ( i == 0 ) |
| { |
| Repr = Ent; |
| Gia_ObjSetRepr( pGia, Ent, -1 ); |
| EntPrev = Ent; |
| } |
| else |
| { |
| Gia_ObjSetRepr( pGia, Ent, Repr ); |
| Gia_ObjSetNext( pGia, EntPrev, Ent ); |
| EntPrev = Ent; |
| } |
| } |
| Gia_ObjSetNext( pGia, EntPrev, 0 ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Refines one equivalence class.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Hcd_ManClassClassRemoveOne( Hcd_Man_t * p, int i ) |
| { |
| int iRepr, Ent; |
| if ( Gia_ObjIsConst(p->pGia, i) ) |
| { |
| Gia_ObjSetRepr( p->pGia, i, GIA_VOID ); |
| return 1; |
| } |
| if ( !Gia_ObjIsClass(p->pGia, i) ) |
| return 0; |
| assert( Gia_ObjIsClass(p->pGia, i) ); |
| iRepr = Gia_ObjRepr( p->pGia, i ); |
| if ( iRepr == GIA_VOID ) |
| iRepr = i; |
| // collect nodes |
| Vec_IntClear( p->vClassOld ); |
| Vec_IntClear( p->vClassNew ); |
| Gia_ClassForEachObj( p->pGia, iRepr, Ent ) |
| { |
| if ( Ent == i ) |
| Vec_IntPush( p->vClassNew, Ent ); |
| else |
| Vec_IntPush( p->vClassOld, Ent ); |
| } |
| assert( Vec_IntSize( p->vClassNew ) == 1 ); |
| Hcd_ManClassCreate( p->pGia, p->vClassOld ); |
| Hcd_ManClassCreate( p->pGia, p->vClassNew ); |
| assert( !Gia_ObjIsClass(p->pGia, i) ); |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Refines one equivalence class.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Hcd_ManClassRefineOne( Hcd_Man_t * p, int i ) |
| { |
| unsigned Sim0, Sim1; |
| int Ent; |
| Vec_IntClear( p->vClassOld ); |
| Vec_IntClear( p->vClassNew ); |
| Vec_IntPush( p->vClassOld, i ); |
| Sim0 = Hcd_ObjSim(p, i); |
| Gia_ClassForEachObj1( p->pGia, i, Ent ) |
| { |
| Sim1 = Hcd_ObjSim(p, Ent); |
| if ( Hcd_ManCompareEqual( Sim0, Sim1 ) ) |
| Vec_IntPush( p->vClassOld, Ent ); |
| else |
| Vec_IntPush( p->vClassNew, Ent ); |
| } |
| if ( Vec_IntSize( p->vClassNew ) == 0 ) |
| return 0; |
| Hcd_ManClassCreate( p->pGia, p->vClassOld ); |
| Hcd_ManClassCreate( p->pGia, p->vClassNew ); |
| if ( Vec_IntSize(p->vClassNew) > 1 ) |
| return 1 + Hcd_ManClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) ); |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes hash key of the simulation info.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Hcd_ManHashKey( unsigned * pSim, int nWords, int nTableSize ) |
| { |
| static int s_Primes[16] = { |
| 1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, |
| 4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 }; |
| unsigned uHash = 0; |
| int i; |
| if ( pSim[0] & 1 ) |
| for ( i = 0; i < nWords; i++ ) |
| uHash ^= ~pSim[i] * s_Primes[i & 0xf]; |
| else |
| for ( i = 0; i < nWords; i++ ) |
| uHash ^= pSim[i] * s_Primes[i & 0xf]; |
| return (int)(uHash % nTableSize); |
| |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Rehashes the refined classes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Hcd_ManClassesRehash( Hcd_Man_t * p, Vec_Int_t * vRefined ) |
| { |
| int * pTable, nTableSize, Key, i, k; |
| nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 ); |
| pTable = ABC_CALLOC( int, nTableSize ); |
| Vec_IntForEachEntry( vRefined, i, k ) |
| { |
| assert( !Hcd_ManCompareConst( Hcd_ObjSim(p, i) ) ); |
| Key = Hcd_ManHashKey( Hcd_ObjSimP(p, i), 1, nTableSize ); |
| if ( pTable[Key] == 0 ) |
| Gia_ObjSetRepr( p->pGia, i, GIA_VOID ); |
| else |
| { |
| Gia_ObjSetNext( p->pGia, pTable[Key], i ); |
| Gia_ObjSetRepr( p->pGia, i, Gia_ObjRepr(p->pGia, pTable[Key]) ); |
| if ( Gia_ObjRepr(p->pGia, i) == GIA_VOID ) |
| Gia_ObjSetRepr( p->pGia, i, pTable[Key] ); |
| } |
| pTable[Key] = i; |
| } |
| ABC_FREE( pTable ); |
| // Gia_ManEquivPrintClasses( p->pGia, 0, 0.0 ); |
| // refine classes in the table |
| Vec_IntForEachEntry( vRefined, i, k ) |
| { |
| if ( Gia_ObjIsHead( p->pGia, i ) ) |
| Hcd_ManClassRefineOne( p, i ); |
| } |
| Gia_ManEquivPrintClasses( p->pGia, 0, 0.0 ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Refines equivalence classes after simulation.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Hcd_ManClassesRefine( Hcd_Man_t * p ) |
| { |
| Gia_Obj_t * pObj; |
| int i; |
| Vec_IntClear( p->vRefinedC ); |
| Gia_ManForEachAnd( p->pGia, pObj, i ) |
| { |
| if ( Gia_ObjIsTail(p->pGia, i) ) // add check for the class level |
| { |
| Hcd_ManClassRefineOne( p, Gia_ObjRepr(p->pGia, i) ); |
| } |
| else if ( Gia_ObjIsConst(p->pGia, i) ) |
| { |
| if ( !Hcd_ManCompareConst( Hcd_ObjSim(p, i) ) ) |
| Vec_IntPush( p->vRefinedC, i ); |
| } |
| } |
| Hcd_ManClassesRehash( p, p->vRefinedC ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates equivalence classes for the first time.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Hcd_ManClassesCreate( Hcd_Man_t * p ) |
| { |
| Gia_Obj_t * pObj; |
| int i; |
| assert( p->pGia->pReprs == NULL ); |
| p->pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pGia) ); |
| p->pGia->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pGia) ); |
| Gia_ManForEachObj( p->pGia, pObj, i ) |
| Gia_ObjSetRepr( p->pGia, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Initializes simulation info.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Hcd_ManSimulationInit( Hcd_Man_t * p ) |
| { |
| Gia_Obj_t * pObj; |
| int i; |
| Gia_ManForEachCi( p->pGia, pObj, i ) |
| Hcd_ObjSetSim( p, i, (Gia_ManRandom(0) << 1) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs one round of simple combinational simulation.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Hcd_ManSimulateSimple( Hcd_Man_t * p ) |
| { |
| Gia_Obj_t * pObj; |
| unsigned Res0, Res1; |
| int i; |
| Gia_ManForEachAnd( p->pGia, pObj, i ) |
| { |
| Res0 = Hcd_ObjSim( p, Gia_ObjFaninId0(pObj, i) ); |
| Res1 = Hcd_ObjSim( p, Gia_ObjFaninId1(pObj, i) ); |
| Hcd_ObjSetSim( p, i, (Gia_ObjFaninC0(pObj)? ~Res0: Res0) & |
| (Gia_ObjFaninC1(pObj)? ~Res1: Res1) ); |
| } |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Resimulate and refine one equivalence class.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| unsigned Gia_Resimulate_rec( Hcd_Man_t * p, int iObj ) |
| { |
| Gia_Obj_t * pObj; |
| unsigned Res0, Res1; |
| if ( Gia_ObjIsTravIdCurrentId( p->pGia, iObj ) ) |
| return Hcd_ObjSim( p, iObj ); |
| Gia_ObjSetTravIdCurrentId( p->pGia, iObj ); |
| pObj = Gia_ManObj(p->pGia, iObj); |
| if ( Gia_ObjIsCi(pObj) ) |
| return Hcd_ObjSim( p, iObj ); |
| assert( Gia_ObjIsAnd(pObj) ); |
| Res0 = Gia_Resimulate_rec( p, Gia_ObjFaninId0(pObj, iObj) ); |
| Res1 = Gia_Resimulate_rec( p, Gia_ObjFaninId1(pObj, iObj) ); |
| return Hcd_ObjSetSim( p, iObj, (Gia_ObjFaninC0(pObj)? ~Res0: Res0) & |
| (Gia_ObjFaninC1(pObj)? ~Res1: Res1) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Resimulate and refine one equivalence class.] |
| |
| Description [Assumes that the counter-example is assigned at the PIs. |
| The counter-example should have the first bit set to 0 at each PI.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ResimulateAndRefine( Hcd_Man_t * p, int i ) |
| { |
| int RetValue, iObj; |
| Gia_ManIncrementTravId( p->pGia ); |
| Gia_ClassForEachObj( p->pGia, i, iObj ) |
| Gia_Resimulate_rec( p, iObj ); |
| RetValue = Hcd_ManClassRefineOne( p, i ); |
| if ( RetValue == 0 ) |
| printf( "!!! no refinement !!!\n" ); |
| // assert( RetValue ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns temporary representative of the node.] |
| |
| Description [The temp repr is the first node among the nodes in the class that |
| (a) precedes the given node, and (b) whose level is lower than the given node.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline Gia_Obj_t * Gia_ObjTempRepr( Gia_Man_t * p, int i, int Level ) |
| { |
| int iRepr, iMember; |
| iRepr = Gia_ObjRepr( p, i ); |
| if ( !Gia_ObjProved(p, i) ) |
| return NULL; |
| if ( Gia_ObjFailed(p, i) ) |
| return NULL; |
| if ( iRepr == GIA_VOID ) |
| return NULL; |
| if ( iRepr == 0 ) |
| return Gia_ManConst0( p ); |
| // if ( p->pLevels[iRepr] < Level ) |
| // return Gia_ManObj( p, iRepr ); |
| Gia_ClassForEachObj( p, iRepr, iMember ) |
| { |
| if ( Gia_ObjFailed(p, iMember) ) |
| continue; |
| if ( iMember >= i ) |
| return NULL; |
| if ( Gia_ObjLevelId(p, iMember) < Level ) |
| return Gia_ManObj( p, iMember ); |
| } |
| assert( 0 ); |
| return NULL; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Generates reduced AIG for the given level.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_GenerateReducedLevel( Gia_Man_t * p, int Level, Vec_Ptr_t ** pvRoots ) |
| { |
| Gia_Man_t * pNew; |
| Gia_Obj_t * pObj, * pRepr; |
| Vec_Ptr_t * vRoots; |
| int i; |
| vRoots = Vec_PtrAlloc( 100 ); |
| // copy unmarked nodes |
| pNew = Gia_ManStart( Gia_ManObjNum(p) ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| Gia_ManConst0(p)->Value = 0; |
| Gia_ManForEachCi( p, pObj, i ) |
| pObj->Value = Gia_ManAppendCi(pNew); |
| Gia_ManHashAlloc( pNew ); |
| Gia_ManForEachAnd( p, pObj, i ) |
| { |
| if ( Gia_ObjLevelId(p, i) > Level ) |
| continue; |
| if ( Gia_ObjLevelId(p, i) == Level ) |
| Vec_PtrPush( vRoots, pObj ); |
| if ( Gia_ObjLevelId(p, i) < Level && (pRepr = Gia_ObjTempRepr(p, i, Level)) ) |
| { |
| // printf( "Substituting %d <--- %d\n", Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj) ); |
| assert( pRepr < pObj ); |
| pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); |
| continue; |
| } |
| pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| } |
| *pvRoots = vRoots; |
| // required by SAT solving |
| Gia_ManCreateRefs( pNew ); |
| Gia_ManFillValue( pNew ); |
| Gia_ManIncrementTravId( pNew ); // needed for MiniSat to record cexes |
| // Gia_ManSetPhase( pNew ); // needed if MiniSat is using polarity -- should not be enabled for TAS because fPhase is used to label |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collects relevant classes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Ptr_t * Gia_CollectRelatedClasses( Gia_Man_t * pGia, Vec_Ptr_t * vRoots ) |
| { |
| Vec_Ptr_t * vClasses; |
| Gia_Obj_t * pRoot, * pRepr; |
| int i; |
| vClasses = Vec_PtrAlloc( 100 ); |
| Gia_ManConst0( pGia )->fMark0 = 1; |
| Vec_PtrForEachEntry( Gia_Obj_t *, vRoots, pRoot, i ) |
| { |
| pRepr = Gia_ObjReprObj( pGia, Gia_ObjId(pGia, pRoot) ); |
| if ( pRepr == NULL || pRepr->fMark0 ) |
| continue; |
| pRepr->fMark0 = 1; |
| Vec_PtrPush( vClasses, pRepr ); |
| } |
| Gia_ManConst0( pGia )->fMark0 = 0; |
| Vec_PtrForEachEntry( Gia_Obj_t *, vClasses, pRepr, i ) |
| pRepr->fMark0 = 0; |
| return vClasses; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collects class members.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Obj_t * Gia_CollectClassMembers( Gia_Man_t * p, Gia_Obj_t * pRepr, Vec_Ptr_t * vMembers, int Level ) |
| { |
| Gia_Obj_t * pTempRepr = NULL; |
| int iRepr, iMember; |
| iRepr = Gia_ObjId( p, pRepr ); |
| Vec_PtrClear( vMembers ); |
| Gia_ClassForEachObj( p, iRepr, iMember ) |
| { |
| if ( Gia_ObjLevelId(p, iMember) == Level ) |
| Vec_PtrPush( vMembers, Gia_ManObj( p, iMember ) ); |
| if ( pTempRepr == NULL && Gia_ObjLevelId(p, iMember) < Level ) |
| pTempRepr = Gia_ManObj( p, iMember ); |
| } |
| return pTempRepr; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Packs patterns into array of simulation info.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| *************************************`**********************************/ |
| int Gia_GiarfStorePatternTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits ) |
| { |
| unsigned * pInfo, * pPres; |
| int i; |
| for ( i = 0; i < nLits; i++ ) |
| { |
| pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i])); |
| pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i])); |
| if ( Abc_InfoHasBit( pPres, iBit ) && |
| Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) ) |
| return 0; |
| } |
| for ( i = 0; i < nLits; i++ ) |
| { |
| pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i])); |
| pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i])); |
| Abc_InfoSetBit( pPres, iBit ); |
| if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) ) |
| Abc_InfoXorBit( pInfo, iBit ); |
| } |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Procedure to test the new SAT solver.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_GiarfStorePattern( Vec_Ptr_t * vSimInfo, Vec_Ptr_t * vPres, Vec_Int_t * vCex ) |
| { |
| int k; |
| for ( k = 1; k < 32; k++ ) |
| if ( Gia_GiarfStorePatternTry( vSimInfo, vPres, k, (int *)Vec_IntArray(vCex), Vec_IntSize(vCex) ) ) |
| break; |
| return (int)(k < 32); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Inserts pattern into simulation info for the PIs.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_GiarfInsertPattern( Hcd_Man_t * p, Vec_Int_t * vCex, int k ) |
| { |
| Gia_Obj_t * pObj; |
| unsigned * pInfo; |
| int Lit, i; |
| Vec_IntForEachEntry( vCex, Lit, i ) |
| { |
| pObj = Gia_ManCi( p->pGia, Abc_Lit2Var(Lit) ); |
| pInfo = Hcd_ObjSimP( p, Gia_ObjId( p->pGia, pObj ) ); |
| if ( Abc_InfoHasBit( pInfo, k ) == Abc_LitIsCompl(Lit) ) |
| Abc_InfoXorBit( pInfo, k ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Inserts pattern into simulation info for the PIs.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_GiarfPrintClasses( Gia_Man_t * pGia ) |
| { |
| int nFails = 0; |
| int nProves = 0; |
| int nTotal = 0; |
| int nBoth = 0; |
| int i; |
| for ( i = 0; i < Gia_ManObjNum(pGia); i++ ) |
| { |
| nFails += Gia_ObjFailed(pGia, i); |
| nProves += Gia_ObjProved(pGia, i); |
| nTotal += Gia_ObjReprObj(pGia, i) != NULL; |
| nBoth += Gia_ObjFailed(pGia, i) && Gia_ObjProved(pGia, i); |
| } |
| printf( "nFails = %7d. nProves = %7d. nBoth = %7d. nTotal = %7d.\n", |
| nFails, nProves, nBoth, nTotal ); |
| } |
| |
| ABC_NAMESPACE_IMPL_END |
| |
| #include "proof/cec/cecInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs computation of AIGs with choices.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ComputeEquivalencesLevel( Hcd_Man_t * p, Gia_Man_t * pGiaLev, Vec_Ptr_t * vOldRoots, int Level, int fUseMiniSat ) |
| { |
| int fUse2Solver = 0; |
| Cec_ManSat_t * pSat; |
| Cec_ParSat_t Pars; |
| Tas_Man_t * pTas; |
| Vec_Int_t * vCex; |
| Vec_Ptr_t * vClasses, * vMembers, * vOldRootsNew; |
| Gia_Obj_t * pRoot, * pMember, * pMemberPrev, * pRepr, * pTempRepr; |
| int i, k, nIter, iRoot, iRootNew, iMember, iMemberPrev, status, fOneFailed;//, iRepr;//, fTwoMember; |
| int nSaved = 0, nRecords = 0, nUndec = 0, nClassRefs = 0, nTsat = 0, nMiniSat = 0; |
| clock_t clk, timeTsat = 0, timeMiniSat = 0, timeSim = 0, timeTotal = clock(); |
| if ( Vec_PtrSize(vOldRoots) == 0 ) |
| return 0; |
| // start SAT solvers |
| Cec_ManSatSetDefaultParams( &Pars ); |
| Pars.fPolarFlip = 0; |
| Pars.nBTLimit = p->nBTLimit; |
| pSat = Cec_ManSatCreate( pGiaLev, &Pars ); |
| pTas = Tas_ManAlloc( pGiaLev, p->nBTLimit ); |
| if ( fUseMiniSat ) |
| vCex = Cec_ManSatReadCex( pSat ); |
| else |
| vCex = Tas_ReadModel( pTas ); |
| vMembers = Vec_PtrAlloc( 100 ); |
| Vec_PtrCleanSimInfo( p->vSimPres, 0, 1 ); |
| // resolve constants |
| Vec_PtrForEachEntry( Gia_Obj_t *, vOldRoots, pRoot, i ) |
| { |
| iRoot = Gia_ObjId( p->pGia, pRoot ); |
| if ( !Gia_ObjIsConst( p->pGia, iRoot ) ) |
| continue; |
| iRootNew = Abc_LitNotCond( pRoot->Value, pRoot->fPhase ); |
| assert( iRootNew != 1 ); |
| if ( fUse2Solver ) |
| { |
| nTsat++; |
| clk = clock(); |
| status = Tas_ManSolve( pTas, Gia_ObjFromLit(pGiaLev, iRootNew), NULL ); |
| timeTsat += clock() - clk; |
| if ( status == -1 ) |
| { |
| nMiniSat++; |
| clk = clock(); |
| status = Cec_ManSatCheckNode( pSat, Gia_ObjFromLit(pGiaLev, iRootNew) ); |
| timeMiniSat += clock() - clk; |
| if ( status == 0 ) |
| { |
| Cec_ManSavePattern( pSat, Gia_ObjFromLit(pGiaLev, iRootNew), NULL ); |
| vCex = Cec_ManSatReadCex( pSat ); |
| } |
| } |
| else if ( status == 0 ) |
| vCex = Tas_ReadModel( pTas ); |
| } |
| else if ( fUseMiniSat ) |
| { |
| nMiniSat++; |
| clk = clock(); |
| status = Cec_ManSatCheckNode( pSat, Gia_ObjFromLit(pGiaLev, iRootNew) ); |
| timeMiniSat += clock() - clk; |
| if ( status == 0 ) |
| Cec_ManSavePattern( pSat, Gia_ObjFromLit(pGiaLev, iRootNew), NULL ); |
| } |
| else |
| { |
| nTsat++; |
| clk = clock(); |
| status = Tas_ManSolve( pTas, Gia_ObjFromLit(pGiaLev, iRootNew), NULL ); |
| timeTsat += clock() - clk; |
| } |
| if ( status == -1 ) // undec |
| { |
| // Gia_ObjSetFailed( p->pGia, iRoot ); |
| nUndec++; |
| // Hcd_ManClassClassRemoveOne( p, iRoot ); |
| Gia_ObjSetFailed( p->pGia, iRoot ); |
| } |
| else if ( status == 1 ) // unsat |
| { |
| Gia_ObjSetProved( p->pGia, iRoot ); |
| // printf( "proved constant %d\n", iRoot ); |
| } |
| else // sat |
| { |
| // printf( "Disproved constant %d\n", iRoot ); |
| Gia_ObjUnsetRepr( p->pGia, iRoot ); // do we need this? |
| nRecords++; |
| nSaved += Gia_GiarfStorePattern( p->vSimInfo, p->vSimPres, vCex ); |
| } |
| } |
| |
| vClasses = Vec_PtrAlloc( 100 ); |
| vOldRootsNew = Vec_PtrAlloc( 100 ); |
| for ( nIter = 0; Vec_PtrSize(vOldRoots) > 0; nIter++ ) |
| { |
| // printf( "Iter = %d (Size = %d)\n", nIter, Vec_PtrSize(vOldRoots) ); |
| // resolve equivalences |
| Vec_PtrClear( vClasses ); |
| Vec_PtrClear( vOldRootsNew ); |
| Gia_ManConst0( p->pGia )->fMark0 = 1; |
| Vec_PtrForEachEntry( Gia_Obj_t *, vOldRoots, pRoot, i ) |
| { |
| iRoot = Gia_ObjId( p->pGia, pRoot ); |
| if ( Gia_ObjIsHead( p->pGia, iRoot ) ) |
| pRepr = pRoot; |
| else if ( Gia_ObjIsClass( p->pGia, iRoot ) ) |
| pRepr = Gia_ObjReprObj( p->pGia, iRoot ); |
| else |
| continue; |
| if ( pRepr->fMark0 ) |
| continue; |
| pRepr->fMark0 = 1; |
| Vec_PtrPush( vClasses, pRepr ); |
| // iRepr = Gia_ObjId( p->pGia, pRepr ); |
| // fTwoMember = Gia_ClassIsPair(p->pGia, iRepr) |
| // derive temp repr and members on this level |
| pTempRepr = Gia_CollectClassMembers( p->pGia, pRepr, vMembers, Level ); |
| if ( pTempRepr ) |
| Vec_PtrPush( vMembers, pTempRepr ); |
| if ( Vec_PtrSize(vMembers) < 2 ) |
| continue; |
| // try proving the members |
| fOneFailed = 0; |
| pMemberPrev = (Gia_Obj_t *)Vec_PtrEntryLast( vMembers ); |
| Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k ) |
| { |
| iMemberPrev = Abc_LitNotCond( pMemberPrev->Value, pMemberPrev->fPhase ); |
| iMember = Abc_LitNotCond( pMember->Value, !pMember->fPhase ); |
| assert( iMemberPrev != iMember ); |
| if ( fUse2Solver ) |
| { |
| nTsat++; |
| clk = clock(); |
| status = Tas_ManSolve( pTas, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) ); |
| timeTsat += clock() - clk; |
| if ( status == -1 ) |
| { |
| nMiniSat++; |
| clk = clock(); |
| status = Cec_ManSatCheckNodeTwo( pSat, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) ); |
| timeMiniSat += clock() - clk; |
| if ( status == 0 ) |
| { |
| Cec_ManSavePattern( pSat, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) ); |
| vCex = Cec_ManSatReadCex( pSat ); |
| } |
| } |
| else if ( status == 0 ) |
| vCex = Tas_ReadModel( pTas ); |
| } |
| else if ( fUseMiniSat ) |
| { |
| nMiniSat++; |
| clk = clock(); |
| status = Cec_ManSatCheckNodeTwo( pSat, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) ); |
| timeMiniSat += clock() - clk; |
| if ( status == 0 ) |
| Cec_ManSavePattern( pSat, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) ); |
| } |
| else |
| { |
| nTsat++; |
| clk = clock(); |
| status = Tas_ManSolve( pTas, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) ); |
| timeTsat += clock() - clk; |
| } |
| if ( status == -1 ) // undec |
| { |
| // Gia_ObjSetFailed( p->pGia, iRoot ); |
| nUndec++; |
| if ( Gia_ObjLevel(p->pGia, pMemberPrev) > Gia_ObjLevel(p->pGia, pMember) ) |
| { |
| // Hcd_ManClassClassRemoveOne( p, Gia_ObjId(p->pGia, pMemberPrev) ); |
| Gia_ObjSetFailed( p->pGia, Gia_ObjId(p->pGia, pMemberPrev) ); |
| Gia_ObjSetFailed( p->pGia, Gia_ObjId(p->pGia, pMember) ); |
| } |
| else |
| { |
| // Hcd_ManClassClassRemoveOne( p, Gia_ObjId(p->pGia, pMember) ); |
| Gia_ObjSetFailed( p->pGia, Gia_ObjId(p->pGia, pMemberPrev) ); |
| Gia_ObjSetFailed( p->pGia, Gia_ObjId(p->pGia, pMember) ); |
| } |
| } |
| else if ( status == 1 ) // unsat |
| { |
| // Gia_ObjSetProved( p->pGia, iRoot ); |
| } |
| else // sat |
| { |
| // iRepr = Gia_ObjId( p->pGia, pRepr ); |
| // if ( Gia_ClassIsPair(p->pGia, iRepr) ) |
| // Gia_ClassUndoPair(p->pGia, iRepr); |
| // else |
| { |
| fOneFailed = 1; |
| nRecords++; |
| nSaved += Gia_GiarfStorePattern( p->vSimInfo, p->vSimPres, vCex ); |
| Gia_GiarfInsertPattern( p, vCex, (k % 31) + 1 ); |
| } |
| } |
| pMemberPrev = pMember; |
| // if ( fOneFailed ) |
| // k += Vec_PtrSize(vMembers) / 4; |
| } |
| // if fail, quit this class |
| if ( fOneFailed ) |
| { |
| nClassRefs++; |
| Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k ) |
| if ( pMember != pTempRepr && !Gia_ObjFailed(p->pGia, Gia_ObjId(p->pGia, pMember)) ) |
| Vec_PtrPush( vOldRootsNew, pMember ); |
| clk = clock(); |
| Gia_ResimulateAndRefine( p, Gia_ObjId(p->pGia, pRepr) ); |
| timeSim += clock() - clk; |
| } |
| else |
| { |
| Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k ) |
| Gia_ObjSetProved( p->pGia, Gia_ObjId(p->pGia, pMember) ); |
| /* |
| // } |
| // else |
| // { |
| printf( "Proved equivalent: " ); |
| Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k ) |
| printf( "%d(L=%d) ", Gia_ObjId(p->pGia, pMember), p->pGia->pLevels[Gia_ObjId(p->pGia, pMember)] ); |
| printf( "\n" ); |
| */ |
| } |
| |
| } |
| Vec_PtrClear( vOldRoots ); |
| Vec_PtrForEachEntry( Gia_Obj_t *, vOldRootsNew, pMember, i ) |
| Vec_PtrPush( vOldRoots, pMember ); |
| // clean up |
| Gia_ManConst0( p->pGia )->fMark0 = 0; |
| Vec_PtrForEachEntry( Gia_Obj_t *, vClasses, pRepr, i ) |
| pRepr->fMark0 = 0; |
| } |
| Vec_PtrFree( vClasses ); |
| Vec_PtrFree( vOldRootsNew ); |
| printf( "nSaved = %d nRecords = %d nUndec = %d nClassRefs = %d nMiniSat = %d nTas = %d\n", |
| nSaved, nRecords, nUndec, nClassRefs, nMiniSat, nTsat ); |
| ABC_PRT( "Tas ", timeTsat ); |
| ABC_PRT( "MiniSat", timeMiniSat ); |
| ABC_PRT( "Sim ", timeSim ); |
| ABC_PRT( "Total ", clock() - timeTotal ); |
| |
| // resimulate |
| // clk = clock(); |
| Hcd_ManSimulateSimple( p ); |
| Hcd_ManClassesRefine( p ); |
| // ABC_PRT( "Simulate/refine", clock() - clk ); |
| |
| // verify the results |
| Vec_PtrFree( vMembers ); |
| Tas_ManStop( pTas ); |
| Cec_ManSatStop( pSat ); |
| return nIter; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs computation of AIGs with choices.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ComputeEquivalences( Gia_Man_t * pGia, int nBTLimit, int fUseMiniSat, int fVerbose ) |
| { |
| Hcd_Man_t * p; |
| Vec_Ptr_t * vRoots; |
| Gia_Man_t * pGiaLev; |
| int i, Lev, nLevels, nIters; |
| clock_t clk; |
| Gia_ManRandom( 1 ); |
| Gia_ManSetPhase( pGia ); |
| nLevels = Gia_ManLevelNum( pGia ); |
| Gia_ManIncrementTravId( pGia ); |
| // start the manager |
| p = Gia_ManEquivStart( pGia, nBTLimit, fVerbose ); |
| // create trivial classes |
| Hcd_ManClassesCreate( p ); |
| // refine |
| for ( i = 0; i < 3; i++ ) |
| { |
| clk = clock(); |
| Hcd_ManSimulationInit( p ); |
| Hcd_ManSimulateSimple( p ); |
| ABC_PRT( "Sim", clock() - clk ); |
| clk = clock(); |
| Hcd_ManClassesRefine( p ); |
| ABC_PRT( "Ref", clock() - clk ); |
| } |
| // process in the levelized order |
| for ( Lev = 1; Lev < nLevels; Lev++ ) |
| { |
| clk = clock(); |
| printf( "LEVEL %3d (out of %3d) ", Lev, nLevels ); |
| pGiaLev = Gia_GenerateReducedLevel( pGia, Lev, &vRoots ); |
| nIters = Gia_ComputeEquivalencesLevel( p, pGiaLev, vRoots, Lev, fUseMiniSat ); |
| Gia_ManStop( pGiaLev ); |
| Vec_PtrFree( vRoots ); |
| printf( "Iters = %3d " ); |
| ABC_PRT( "Time", clock() - clk ); |
| } |
| Gia_GiarfPrintClasses( pGia ); |
| // clean up |
| Gia_ManEquivStop( p ); |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
