diff options
Diffstat (limited to 'src/aig/gia/giaGiarf.c')
| -rw-r--r-- | src/aig/gia/giaGiarf.c | 1077 |
1 files changed, 1077 insertions, 0 deletions
diff --git a/src/aig/gia/giaGiarf.c b/src/aig/gia/giaGiarf.c new file mode 100644 index 00000000..501f9bb3 --- /dev/null +++ b/src/aig/gia/giaGiarf.c @@ -0,0 +1,1077 @@ +/**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 = Gia_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 = Gia_UtilStrsav( p->pName ); + 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 = Gia_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, Gia_Lit2Var(pLits[i])); + pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); + if ( Gia_InfoHasBit( pPres, iBit ) && + Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) + return 0; + } + for ( i = 0; i < nLits; i++ ) + { + pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); + pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); + Gia_InfoSetBit( pPres, iBit ); + if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) + Gia_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, Gia_Lit2Var(Lit) ); + pInfo = Hcd_ObjSimP( p, Gia_ObjId( p->pGia, pObj ) ); + if ( Gia_InfoHasBit( pInfo, k ) == Gia_LitIsCompl(Lit) ) + Gia_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 "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; + int 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 = Gia_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 = Gia_LitNotCond( pMemberPrev->Value, pMemberPrev->fPhase ); + iMember = Gia_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, 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 + |