From 9cb52998f57d8e46db40ee969ebd1bc6c3155120 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 1 Jul 2012 23:16:23 -0700 Subject: Other improvements to &vta and &gla. --- src/aig/gia/gia.h | 60 +++++ src/aig/gia/giaAbsGla.c | 675 +++++++++++++++++++++++++++++++++++++++++++----- src/aig/gia/giaAbsVta.c | 83 +++++- 3 files changed, 738 insertions(+), 80 deletions(-) (limited to 'src') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index b3584f14..e24ecd26 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -515,6 +515,66 @@ static inline int Gia_XsimAndCond( int Value0, int fCompl0, int Value1, int fCom return GIA_ONE; } + +static inline void Gia_ObjTerSimSetC( Gia_Obj_t * pObj ) { pObj->fMark0 = 0; pObj->fMark1 = 0; } +static inline void Gia_ObjTerSimSet0( Gia_Obj_t * pObj ) { pObj->fMark0 = 1; pObj->fMark1 = 0; } +static inline void Gia_ObjTerSimSet1( Gia_Obj_t * pObj ) { pObj->fMark0 = 0; pObj->fMark1 = 1; } +static inline void Gia_ObjTerSimSetX( Gia_Obj_t * pObj ) { pObj->fMark0 = 1; pObj->fMark1 = 1; } + +static inline int Gia_ObjTerSimGetC( Gia_Obj_t * pObj ) { return !pObj->fMark0 && !pObj->fMark1; } +static inline int Gia_ObjTerSimGet0( Gia_Obj_t * pObj ) { return pObj->fMark0 && !pObj->fMark1; } +static inline int Gia_ObjTerSimGet1( Gia_Obj_t * pObj ) { return !pObj->fMark0 && pObj->fMark1; } +static inline int Gia_ObjTerSimGetX( Gia_Obj_t * pObj ) { return pObj->fMark0 && pObj->fMark1; } + +static inline int Gia_ObjTerSimGet0Fanin0( Gia_Obj_t * pObj ) { return (Gia_ObjTerSimGet1(Gia_ObjFanin0(pObj)) && Gia_ObjFaninC0(pObj)) || (Gia_ObjTerSimGet0(Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj)); } +static inline int Gia_ObjTerSimGet1Fanin0( Gia_Obj_t * pObj ) { return (Gia_ObjTerSimGet0(Gia_ObjFanin0(pObj)) && Gia_ObjFaninC0(pObj)) || (Gia_ObjTerSimGet1(Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj)); } + +static inline int Gia_ObjTerSimGet0Fanin1( Gia_Obj_t * pObj ) { return (Gia_ObjTerSimGet1(Gia_ObjFanin1(pObj)) && Gia_ObjFaninC1(pObj)) || (Gia_ObjTerSimGet0(Gia_ObjFanin1(pObj)) && !Gia_ObjFaninC1(pObj)); } +static inline int Gia_ObjTerSimGet1Fanin1( Gia_Obj_t * pObj ) { return (Gia_ObjTerSimGet0(Gia_ObjFanin1(pObj)) && Gia_ObjFaninC1(pObj)) || (Gia_ObjTerSimGet1(Gia_ObjFanin1(pObj)) && !Gia_ObjFaninC1(pObj)); } + +static inline void Gia_ObjTerSimAnd( Gia_Obj_t * pObj ) +{ + assert( Gia_ObjIsAnd(pObj) ); + assert( !Gia_ObjTerSimGetC( Gia_ObjFanin0(pObj) ) ); + assert( !Gia_ObjTerSimGetC( Gia_ObjFanin1(pObj) ) ); + if ( Gia_ObjTerSimGet0Fanin0(pObj) || Gia_ObjTerSimGet0Fanin1(pObj) ) + Gia_ObjTerSimSet0( pObj ); + else if ( Gia_ObjTerSimGet1Fanin0(pObj) && Gia_ObjTerSimGet1Fanin1(pObj) ) + Gia_ObjTerSimSet1( pObj ); + else + Gia_ObjTerSimSetX( pObj ); +} +static inline void Gia_ObjTerSimCo( Gia_Obj_t * pObj ) +{ + assert( Gia_ObjIsCo(pObj) ); + assert( !Gia_ObjTerSimGetC( Gia_ObjFanin0(pObj) ) ); + if ( Gia_ObjTerSimGet0Fanin0(pObj) ) + Gia_ObjTerSimSet0( pObj ); + else if ( Gia_ObjTerSimGet1Fanin0(pObj) ) + Gia_ObjTerSimSet1( pObj ); + else + Gia_ObjTerSimSetX( pObj ); +} +static inline void Gia_ObjTerSimRo( Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + Gia_Obj_t * pTemp = Gia_ObjRoToRi(p, pObj); + assert( Gia_ObjIsRo(p, pObj) ); + assert( !Gia_ObjTerSimGetC( pTemp ) ); + pObj->fMark0 = pTemp->fMark0; + pObj->fMark1 = pTemp->fMark1; +} + +static inline void Gia_ObjTerSimPrint( Gia_Obj_t * pObj ) +{ + if ( Gia_ObjTerSimGet0(pObj) ) + printf( "0" ); + else if ( Gia_ObjTerSimGet1(pObj) ) + printf( "1" ); + else if ( Gia_ObjTerSimGetX(pObj) ) + printf( "X" ); +} + + static inline Gia_Obj_t * Gia_ObjReprObj( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr == GIA_VOID ? NULL : Gia_ManObj( p, p->pReprs[Id].iRepr ); } static inline int Gia_ObjRepr( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr; } static inline void Gia_ObjSetRepr( Gia_Man_t * p, int Id, int Num ) { assert( Num == GIA_VOID || Num < Id ); p->pReprs[Id].iRepr = Num; } diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 6f3731a1..a9ac56b6 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -26,61 +26,84 @@ ABC_NAMESPACE_IMPL_START - //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -typedef struct Gla_Obj_t_ Gla_Obj_t; // object +typedef struct Rfn_Obj_t_ Rfn_Obj_t; // refinement object +struct Rfn_Obj_t_ +{ + unsigned Value : 1; // value + unsigned fVisit : 1; // visited + unsigned fPPi : 1; // PPI + unsigned Prio : 28; // priority +}; + +typedef struct Gla_Obj_t_ Gla_Obj_t; // abstraction object struct Gla_Obj_t_ { - int iGiaObj; // corresponding GIA obj - unsigned fAbs : 1; // belongs to abstraction - unsigned fCompl0 : 1; // compl bit of the first fanin -// unsigned fCompl1 : 1; // compl bit of the second fanin - unsigned fConst : 1; // object attribute - unsigned fPi : 1; // object attribute - unsigned fPo : 1; // object attribute - unsigned fRo : 1; // object attribute - unsigned fRi : 1; // object attribute - unsigned fAnd : 1; // object attribute - unsigned nFanins : 24; // fanin count - int Fanins[4]; // fanins - Vec_Int_t vFrames; // variables in each timeframe + int iGiaObj; // corresponding GIA obj + unsigned fAbs : 1; // belongs to abstraction + unsigned fCompl0 : 1; // compl bit of the first fanin + unsigned fConst : 1; // object attribute + unsigned fPi : 1; // object attribute + unsigned fPo : 1; // object attribute + unsigned fRo : 1; // object attribute + unsigned fRi : 1; // object attribute + unsigned fAnd : 1; // object attribute + unsigned fMark : 1; // nearby object + unsigned nFanins : 23; // fanin count + int Fanins[4]; // fanins + Vec_Int_t vFrames; // variables in each timeframe }; typedef struct Gla_Man_t_ Gla_Man_t; // manager struct Gla_Man_t_ { // user data - Gia_Man_t * pGia; // AIG manager - Gia_ParVta_t* pPars; // parameters + Gia_Man_t * pGia; // AIG manager + Gia_ParVta_t* pPars; // parameters // internal data - Vec_Int_t * vAbs; // abstracted objects - Gla_Obj_t * pObjRoot; // the primary output - Gla_Obj_t * pObjs; // objects - int nObjs; // the number of objects - int nAbsOld; // previous abstraction + Vec_Int_t * vAbs; // abstracted objects + Gla_Obj_t * pObjRoot; // the primary output + Gla_Obj_t * pObjs; // objects + unsigned * pObj2Obj; // mapping of GIA obj into GLA obj + int nObjs; // the number of objects + int nAbsOld; // previous abstraction // other data - int nCexes; // the number of counter-examples - int nSatVars; // the number of SAT variables - Cnf_Dat_t * pCnf; // CNF derived for the nodes - sat_solver2 * pSat; // incremental SAT solver - Vec_Int_t * vCla2Obj; // mapping of clauses into GLA objs - Vec_Int_t * vTemp; // temporary array - Vec_Int_t * vAddedNew; // temporary array - // statistics - int timeInit; - int timeSat; - int timeUnsat; - int timeCex; - int timeOther; + int nCexes; // the number of counter-examples + int nSatVars; // the number of SAT variables + Cnf_Dat_t * pCnf; // CNF derived for the nodes + sat_solver2 * pSat; // incremental SAT solver + Vec_Int_t * vCla2Obj; // mapping of clauses into GLA objs + Vec_Int_t * vTemp; // temporary array + Vec_Int_t * vAddedNew; // temporary array + Vec_Int_t * vPrevCore; // previous core + // refinement + Vec_Int_t * pvRefis; // vectors of each object + Vec_Int_t * vPrioSels; // selected priorities + // statistics + int timeInit; + int timeSat; + int timeUnsat; + int timeCex; + int timeOther; }; +// declarations +static Vec_Int_t * Gla_ManCollectPPis( Gla_Man_t * p, Vec_Int_t * vPis ); +static int Gla_ManCheckVar( Gla_Man_t * p, int iObj, int iFrame ); +static int Gla_ManGetVar( Gla_Man_t * p, int iObj, int iFrame ); + // object procedures -static inline int Gla_ObjId( Gla_Man_t * p, Gla_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; } -static inline Gla_Obj_t * Gla_ManObj( Gla_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; } -static inline Gia_Obj_t * Gla_ManGiaObj( Gla_Man_t * p, Gla_Obj_t * pObj ) { return Gia_ManObj( p->pGia, pObj->iGiaObj ); } +static inline int Gla_ObjId( Gla_Man_t * p, Gla_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; } +static inline Gla_Obj_t * Gla_ManObj( Gla_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; } +static inline Gia_Obj_t * Gla_ManGiaObj( Gla_Man_t * p, Gla_Obj_t * pObj ) { return Gia_ManObj( p->pGia, pObj->iGiaObj ); } +static inline int Gla_ObjSatValue( Gla_Man_t * p, int iGia, int f ) { return Gla_ManCheckVar(p, p->pObj2Obj[iGia], f) ? sat_solver2_var_value( p->pSat, Gla_ManGetVar(p, p->pObj2Obj[iGia], f) ) : 0; } + +static inline Rfn_Obj_t * Gla_ObjRef( Gla_Man_t * p, int iObj, int f ) { return (Rfn_Obj_t *)Vec_IntGetEntryP( &(p->pvRefis[iObj]), f ); } +static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) { *((int *)p) = 0; } + // iterator through abstracted objects #define Gla_ManForEachObj( p, pObj ) \ @@ -91,7 +114,7 @@ static inline Gia_Obj_t * Gla_ManGiaObj( Gla_Man_t * p, Gla_Obj_t * pObj ) { ret for ( i = 0; i < Vec_IntSize(vVec) && ((pObj = Gla_ManObj(p, Vec_IntEntry(vVec, i))),1); i++) // iterator through fanins of an abstracted object -#define Gla_ObjForEachFanin( p, pObj, pFanin, i ) \ +#define Gla_ObjForEachFanin( p, pObj, pFanin, i ) \ for ( i = 0; (i < (int)pObj->nFanins) && ((pFanin = Gla_ManObj(p, pObj->Fanins[i])),1); i++ ) //////////////////////////////////////////////////////////////////////// @@ -240,6 +263,398 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose +/**Function************************************************************* + + Synopsis [Derives counter-example using current assignments.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Gla_ManDeriveCex( Gla_Man_t * p, Vec_Int_t * vPis ) +{ + Abc_Cex_t * pCex; + Gia_Obj_t * pObj; + int i, f; + pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 ); + pCex->iPo = 0; + pCex->iFrame = p->pPars->iFrame; + Gia_ManForEachObjVec( vPis, p->pGia, pObj, i ) + { + assert( Gia_ObjIsPi(p->pGia, pObj) ); + for ( f = 0; f <= pCex->iFrame; f++ ) + if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) ) + Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Gia_ObjCioId(pObj) ); + } + return pCex; +} + +/**Function************************************************************* + + Synopsis [Collects internal objects in a topo order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gla_ManRefCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vRoAnds, Vec_Int_t * vCos ) +{ + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pObj); + if ( Gia_ObjIsRo(p, pObj) ) + { + Vec_IntPush( vRoAnds, Gia_ObjId(p, pObj) ); + Vec_IntPush( vCos, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) ); + return; + } + assert( Gia_ObjIsAnd(pObj) ); + Gla_ManRefCollect_rec( p, Gia_ObjFanin0(pObj), vRoAnds, vCos ); + Gla_ManRefCollect_rec( p, Gia_ObjFanin1(pObj), vRoAnds, vCos ); + Vec_IntPush( vRoAnds, Gia_ObjId(p, pObj) ); +} + +/**Function************************************************************* + + Synopsis [Selects assignments to be refined.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vRes ) +{ + Rfn_Obj_t * pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); + if ( pRef->fVisit ) + return; + pRef->fVisit = 1; + if ( pRef->fPPi ) + { + assert( (int)pRef->Prio < Vec_IntSize(p->vPrioSels) ); + if ( Vec_IntEntry( p->vPrioSels, pRef->Prio ) == 0 ) // not selected yet + { + Vec_IntWriteEntry( p->vPrioSels, pRef->Prio, 1 ); + Vec_IntPush( vRes, Gia_ObjId(p->pGia, pObj) ); + } + return; + } + if ( Gia_ObjIsPi(p->pGia, pObj) || Gia_ObjIsConst0(pObj) ) + return; + if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + if ( f > 0 ) + Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj)), f-1, vRes ); + return; + } + assert( Gia_ObjIsAnd(pObj) ); + if ( pRef->Value == 1 ) + { + Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes ); + Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes ); + } + else // select one value + { + Rfn_Obj_t * pRef0 = Gla_ObjRef( p, Gia_ObjFaninId0p(p->pGia, pObj), f ); + Rfn_Obj_t * pRef1 = Gla_ObjRef( p, Gia_ObjFaninId1p(p->pGia, pObj), f ); + int fSel0 = Vec_IntEntry( p->vPrioSels, pRef0->Prio ); + int fSel1 = Vec_IntEntry( p->vPrioSels, pRef1->Prio ); + + if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 ) + { + if ( !fSel0 && !fSel1 ) + { + if ( pRef0->Prio <= pRef1->Prio ) // choice + Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes ); + else + Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes ); + } + } + else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 ) + { + if ( !fSel0 ) + Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes ); + } + else + { + if ( !fSel1 ) + Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes ); + } + } +} + +/**Function************************************************************* + + Synopsis [Performs refinement.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p ) +{ + int fVerify = 0; + Vec_Int_t * vPis, * vPPis, * vRoAnds, * vCos, * vRes = NULL; + Rfn_Obj_t * pRef, * pRef0, * pRef1; + Gia_Obj_t * pObj; + Gla_Obj_t * pGla; + int i, f; + + // compute PIs and pseudo-PIs + vPis = Vec_IntAlloc( 100 ); + vPPis = Gla_ManCollectPPis( p, vPis ); + + // remap into GIA + Gla_ManForEachObjAbsVec( vPis, p, pGla, i ) + Vec_IntWriteEntry( vPis, i, pGla->iGiaObj ); + Gla_ManForEachObjAbsVec( vPPis, p, pGla, i ) + Vec_IntWriteEntry( vPPis, i, pGla->iGiaObj ); + + // prepare boundary objects + Gia_ManIncrementTravId( p->pGia ); + Gia_ObjSetTravIdCurrent( p->pGia, Gia_ManConst0(p->pGia) ); + Gia_ManForEachObjVec( vPis, p->pGia, pObj, i ) + Gia_ObjSetTravIdCurrent( p->pGia, pObj ); + Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i ) + Gia_ObjSetTravIdCurrent( p->pGia, pObj ); + + // collect internal objects + vCos = Vec_IntAlloc( 1000 ); + vRoAnds = Vec_IntAlloc( 1000 ); + Vec_IntPush( vCos, Gia_ObjId(p->pGia, Gia_ManPo(p->pGia, 0)) ); + Gia_ManForEachObjVec( vCos, p->pGia, pObj, i ) + Gla_ManRefCollect_rec( p->pGia, Gia_ObjFanin0(pObj), vRoAnds, vCos ); + + // propagate values + for ( f = 0; f <= p->pPars->iFrame; f++ ) + { + // constant + pRef = Gla_ObjRef( p, 0, f ); Gla_ObjClearRef( pRef ); + pRef->Value = 0; + pRef->Prio = 0; + // primary input + Gia_ManForEachObjVec( vPis, p->pGia, pObj, i ) + { + pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef ); + pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ); + pRef->Prio = 0; + } + // primary input + Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i ) + { + assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) ); + pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef ); + pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ); + pRef->Prio = i+1; + pRef->fPPi = 1; + } + // internal nodes + Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i ) + { + pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef ); + if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + if ( f == 0 ) + { + pRef->Value = 0; + pRef->Prio = 0; + } + else + { + pRef0 = Gla_ObjRef( p, Gia_ObjId(p->pGia, Gia_ObjRoToRi(p->pGia, pObj)), f-1 ); + pRef->Value = pRef0->Value; + pRef->Prio = pRef0->Prio; + } + continue; + } + assert( Gia_ObjIsAnd(pObj) ); + pRef0 = Gla_ObjRef( p, Gia_ObjFaninId0p(p->pGia, pObj), f ); + pRef1 = Gla_ObjRef( p, Gia_ObjFaninId1p(p->pGia, pObj), f ); + pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj)) & (pRef1->Value ^ Gia_ObjFaninC1(pObj)); +// if ( p->pCnf->pObj2Count[Gia_ObjId(p->pGia, pObj)] >= 0 ) +// assert( (int)pRef->Value == Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) ); + if ( pRef->Value == 1 ) + pRef->Prio = Abc_MaxInt( pRef0->Prio, pRef1->Prio ); + else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 ) + pRef->Prio = Abc_MinInt( pRef0->Prio, pRef1->Prio ); // choice + else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 ) + pRef->Prio = pRef0->Prio; + else + pRef->Prio = pRef1->Prio; + } + // output nodes + Gia_ManForEachObjVec( vCos, p->pGia, pObj, i ) + { + pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef ); + pRef0 = Gla_ObjRef( p, Gia_ObjFaninId0p(p->pGia, pObj), f ); + pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj)); + pRef->Prio = pRef0->Prio; + } + } + // make sure the output value is 1 + pObj = Gia_ManPo( p->pGia, 0 ); + pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), p->pPars->iFrame ); + assert( pRef->Value == 1 ); + + // check the CEX + if ( pRef->Prio == 0 ) + { + p->pGia->pCexSeq = Gla_ManDeriveCex( p, vPis ); + Vec_IntFree( vPis ); + Vec_IntFree( vPPis ); + Vec_IntFree( vRoAnds ); + Vec_IntFree( vCos ); + return 0; + } + + // select objects + vRes = Vec_IntAlloc( 100 ); + Vec_IntFill( p->vPrioSels, Vec_IntSize(vPPis)+1, 0 ); + Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), p->pPars->iFrame, vRes ); + + if ( fVerify ) + { + Gia_ManForEachObj( p->pGia, pObj, i ) + assert( Gia_ObjTerSimGetC(pObj) ); + for ( f = 0; f <= p->pPars->iFrame; f++ ) + { + Gia_ObjTerSimSet0( Gia_ManConst0(p->pGia) ); + Gia_ManForEachObjVec( vPis, p->pGia, pObj, i ) + { + if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) ) + Gia_ObjTerSimSet1( pObj ); + else + Gia_ObjTerSimSet0( pObj ); + } + Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i ) + { + if ( Vec_IntEntry(p->vPrioSels, i+1) == 0 ) // not selected + Gia_ObjTerSimSetX( pObj ); + else if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) ) + Gia_ObjTerSimSet1( pObj ); + else + Gia_ObjTerSimSet0( pObj ); + } + Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + Gia_ObjTerSimAnd( pObj ); + else if ( f == 0 ) + Gia_ObjTerSimSet0( pObj ); + else + Gia_ObjTerSimRo( p->pGia, pObj ); + } + Gia_ManForEachObjVec( vCos, p->pGia, pObj, i ) + Gia_ObjTerSimCo( pObj ); + } + pObj = Gia_ManPo( p->pGia, 0 ); + if ( !Gia_ObjTerSimGet1(pObj) ) + printf( "Refinement verification has failed!!!" ); + // clear + Gia_ObjTerSimSetC( Gia_ManConst0(p->pGia) ); + Gia_ManForEachObjVec( vPis, p->pGia, pObj, i ) + Gia_ObjTerSimSetC( pObj ); + Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i ) + Gia_ObjTerSimSetC( pObj ); + Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i ) + Gia_ObjTerSimSetC( pObj ); + Gia_ManForEachObjVec( vCos, p->pGia, pObj, i ) + Gia_ObjTerSimSetC( pObj ); + } + + // remap them into GLA objects + Gia_ManForEachObjVec( vRes, p->pGia, pObj, i ) + Vec_IntWriteEntry( vRes, i, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] ); + + Vec_IntFree( vPis ); + Vec_IntFree( vPPis ); + Vec_IntFree( vRoAnds ); + Vec_IntFree( vCos ); + return vRes; +} + + + + + +/**Function************************************************************* + + Synopsis [Selects items that are new in the current abstraction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gla_ManRegionStart( Gla_Man_t * p, Vec_Int_t * vCore ) +{ + Vec_Int_t * vRes; + Gla_Obj_t * pGla; + int i; + vRes = Vec_IntAlloc( 100 ); + Gla_ManForEachObjAbsVec( vCore, p, pGla, i ) + if ( !pGla->fAbs ) + Vec_IntPush( vRes, Gla_ObjId(p, pGla) ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Finds adjacent to previous core among select (or all if NULL).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gla_ManRegionFilter( Gla_Man_t * p, Vec_Int_t * vSelected, Vec_Int_t * vPrevCore ) +{ + Vec_Int_t * vRes; + Gla_Obj_t * pGla, * pFanin; + int i, k; + // mark fanins of previous core + Gla_ManForEachObjAbsVec( vPrevCore, p, pGla, i ) + { + assert( pGla->fMark == 0 ); + Gla_ObjForEachFanin( p, pGla, pFanin, k ) + pFanin->fMark = 1; + } + // select those not marked and included in the abstraction + vRes = Vec_IntAlloc( 100 ); + if ( vSelected == NULL ) + { + Gla_ManForEachObj( p, pGla ) + if ( !pGla->fAbs && pGla->fMark ) + Vec_IntPush( vRes, Gla_ObjId(p, pGla) ); + } + else + { + Gla_ManForEachObjAbsVec( vSelected, p, pGla, i ) + if ( !pGla->fAbs && pGla->fMark ) + Vec_IntPush( vRes, Gla_ObjId(p, pGla) ); + } + // unmark fanins of previous core + Gla_ManForEachObjAbsVec( vPrevCore, p, pGla, i ) + Gla_ObjForEachFanin( p, pGla, pFanin, k ) + pFanin->fMark = 0; + return vRes; +} + /**Function************************************************************* @@ -292,6 +707,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) p->vAbs = Vec_IntAlloc( 100 ); p->vTemp = Vec_IntAlloc( 100 ); p->vAddedNew = Vec_IntAlloc( 100 ); + p->vPrioSels = Vec_IntAlloc( 100 ); // internal data pAig = Gia_ManToAigSimple( p->pGia ); p->pCnf = Cnf_DeriveOther( pAig ); @@ -311,16 +727,18 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) assert( ~pObj->Value ); pLits[i] = toLitCond( pObj->Value, lit_sign(pLits[i]) ); } - // create objects - p->pObjs = ABC_CALLOC( Gla_Obj_t, p->nObjs ); + // create objects + p->pObjs = ABC_CALLOC( Gla_Obj_t, p->nObjs ); + p->pObj2Obj = ABC_FALLOC( unsigned, Gia_ManObjNum(p->pGia) ); + p->pvRefis = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(p->pGia) ); Gia_ManForEachObj( p->pGia, pObj, i ) { + p->pObj2Obj[i] = pObj->Value; if ( !~pObj->Value ) continue; pGla = Gla_ManObj( p, pObj->Value ); pGla->iGiaObj = i; pGla->fCompl0 = Gia_ObjFaninC0(pObj); -// pGla->fCompl1 = Gia_ObjFaninC1(pObj); pGla->fConst = Gia_ObjIsConst0(pObj); pGla->fPi = Gia_ObjIsPi(p->pGia, pObj); pGla->fPo = Gia_ObjIsPo(p->pGia, pObj); @@ -379,10 +797,14 @@ void Gla_ManStop( Gla_Man_t * p ) ABC_FREE( pGla->vFrames.pArray ); Cnf_DataFree( p->pCnf ); sat_solver2_delete( p->pSat ); - Vec_IntFree( p->vCla2Obj ); - Vec_IntFree( p->vAddedNew ); - Vec_IntFree( p->vTemp ); - Vec_IntFree( p->vAbs ); + Vec_IntFreeP( &p->vCla2Obj ); + Vec_IntFreeP( &p->vPrevCore ); + Vec_IntFreeP( &p->vAddedNew ); + Vec_IntFreeP( &p->vPrioSels ); + Vec_IntFreeP( &p->vTemp ); + Vec_IntFreeP( &p->vAbs ); + ABC_FREE( p->pvRefis ); + ABC_FREE( p->pObj2Obj ); ABC_FREE( p->pObjs ); ABC_FREE( p ); } @@ -475,53 +897,53 @@ Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gla_ManCollectPPis( Gla_Man_t * p ) +Vec_Int_t * Gla_ManCollectPPis( Gla_Man_t * p, Vec_Int_t * vPis ) { Vec_Int_t * vPPis; Gla_Obj_t * pObj, * pFanin; int i, k; vPPis = Vec_IntAlloc( 1000 ); + if ( vPis ) + Vec_IntClear( vPis ); Gla_ManForEachObjAbs( p, pObj, i ) { assert( pObj->fConst || pObj->fRo || pObj->fAnd ); Gla_ObjForEachFanin( p, pObj, pFanin, k ) if ( !pFanin->fPi && !pFanin->fAbs ) Vec_IntPush( vPPis, pObj->Fanins[k] ); + else if ( vPis && pFanin->fPi && !pFanin->fAbs ) + Vec_IntPush( vPis, pObj->Fanins[k] ); } Vec_IntUniqify( vPPis ); Vec_IntReverseOrder( vPPis ); + if ( vPis ) + Vec_IntUniqify( vPis ); return vPPis; } int Gla_ManCountPPis( Gla_Man_t * p ) { - Vec_Int_t * vPPis = Gla_ManCollectPPis( p ); + Vec_Int_t * vPPis = Gla_ManCollectPPis( p, NULL ); int RetValue = Vec_IntSize( vPPis ); Vec_IntFree( vPPis ); return RetValue; } + void Gla_ManExplorePPis( Gla_Man_t * p, Vec_Int_t * vPPis ) { static int Round = 0; Gla_Obj_t * pObj, * pFanin; int i, j, k, Count; - if ( (Round++ % 3) == 0 ) + if ( (Round++ % 5) == 0 ) return; -// printf( "\n" ); j = 0; Gla_ManForEachObjAbsVec( vPPis, p, pObj, i ) { assert( pObj->fAbs == 0 ); -// printf( "%6d ", Gla_ObjId(p, pObj) ); -// printf( "Fanins=%d ", pObj->nFanins ); -// Gla_ObjForEachFanin( p, pObj, pFanin, k ) -// printf( "%d", pFanin->fAbs ); -// printf( "\n" ); - Count = 0; Gla_ObjForEachFanin( p, pObj, pFanin, k ) Count += pFanin->fAbs; - if ( Count == 0 ) + if ( Count == 0 || ((Round & 1) && Count == 1) ) continue; Vec_IntWriteEntry( vPPis, j++, Gla_ObjId(p, pObj) ); } @@ -529,6 +951,99 @@ void Gla_ManExplorePPis( Gla_Man_t * p, Vec_Int_t * vPPis ) Vec_IntShrink( vPPis, j ); } +// add those having more than one shared fanin + + +void Gla_ManExplorePPis2( Gla_Man_t * p, Vec_Int_t * vPPis ) +{ + static int Round = 0; + Vec_Int_t * vTemp; + Gla_Obj_t * pGla, * pFanin; + int i, k, Entry, Count; + if ( p->vPrevCore == NULL ) + return; + if ( (Round++ % 10) == 0 ) + { + p->vPrevCore = Gla_ManRegionFilter( p, vPPis, vTemp = p->vPrevCore ); + Vec_IntFree( vTemp ); + } + else + { + p->vPrevCore = Gla_ManRegionFilter( p, NULL, vTemp = p->vPrevCore ); + Vec_IntFree( vTemp ); + // save a copy + vTemp = Vec_IntDup( vPPis ); + // udpate + Vec_IntClear( vPPis ); + Vec_IntForEachEntry( p->vPrevCore, Entry, i ) + Vec_IntPush( vPPis, Entry ); + + + // mark those included as abstracted + Gla_ManForEachObjAbsVec( vPPis, p, pGla, i ) + { + assert( pGla->fAbs == 0 ); + pGla->fAbs = 1; + } + // add those not included but to close to abstracted + Gla_ManForEachObjAbsVec( vTemp, p, pGla, i ) + { + if ( pGla->fAbs ) + continue; + Count = 0; + Gla_ObjForEachFanin( p, pGla, pFanin, k ) + Count += pFanin->fAbs; + if ( Count == 0 || Count == 1 ) + continue; + Vec_IntPush( vPPis, Gla_ObjId(p, pGla) ); + } + // unmark those included + Gla_ManForEachObjAbsVec( vPPis, p, pGla, i ) + pGla->fAbs = 0; + + + // cleanup + Vec_IntFree( vTemp ); + } +} + +/* +void Gla_ManExplorePPis2( Gla_Man_t * p, Vec_Int_t * vPPis, int iIter ) +{ + Gla_Obj_t * pObj, * pFanin; + int i, j, k; + if ( iIter > 10 ) + { + Gla_ManForEachObj( p, pObj ) + pObj->fMark = 0; + return; + } + j = 0; + Gla_ManForEachObjAbsVec( vPPis, p, pObj, i ) + { + assert( pObj->fAbs == 0 ); + if ( pObj->fMark == 0 ) + { + Gla_ObjForEachFanin( p, pObj, pFanin, k ) + if ( pObj->fMark ) + break; + if ( k == (int)pObj->nFanins ) + continue; + } + Vec_IntWriteEntry( vPPis, j++, Gla_ObjId(p, pObj) ); + } +// printf( "\n%d -> %d\n", Vec_IntSize(vPPis), j ); + Vec_IntShrink( vPPis, j ); + + // update + Gla_ManForEachObj( p, pObj ) + pObj->fMark = 0; + Gla_ManForEachObjAbsVec( vPPis, p, pObj, i ) + Gla_ObjForEachFanin( p, pObj, pFanin, k ) + pFanin->fMark = 1; +} +*/ + /**Function************************************************************* @@ -541,6 +1056,13 @@ void Gla_ManExplorePPis( Gla_Man_t * p, Vec_Int_t * vPPis ) SeeAlso [] ***********************************************************************/ +int Gla_ManCheckVar( Gla_Man_t * p, int iObj, int iFrame ) +{ + Gla_Obj_t * pGla = Gla_ManObj( p, iObj ); + int iVar = Vec_IntGetEntry( &pGla->vFrames, iFrame ); + assert( !pGla->fPo && !pGla->fRi ); + return (iVar > 0); +} int Gla_ManGetVar( Gla_Man_t * p, int iObj, int iFrame ) { Gla_Obj_t * pGla = Gla_ManObj( p, iObj ); @@ -772,25 +1294,31 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl void Gla_ManReportMemory( Gla_Man_t * p ) { Gla_Obj_t * pGla; + int i; double memTot = 0; double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t); double memSat = sat_solver2_memory( p->pSat ); double memPro = sat_solver2_memory_proof( p->pSat ); - double memMap = p->nObjs * sizeof(Gla_Obj_t); + double memMap = p->nObjs * sizeof(Gla_Obj_t) + Gia_ManObjNum(p->pGia) * sizeof(int); + double memRef = Gia_ManObjNum(p->pGia) * sizeof(Vec_Int_t) + Vec_IntCap(p->vPrioSels) * sizeof(int); double memOth = sizeof(Gla_Man_t); for ( pGla = p->pObjs; pGla < p->pObjs + p->nObjs; pGla++ ) memMap += Vec_IntCap(&pGla->vFrames) * sizeof(int); + for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ ) + memRef += Vec_IntCap(&p->pvRefis[i]) * sizeof(int); memOth += Vec_IntCap(p->vCla2Obj) * sizeof(int); memOth += Vec_IntCap(p->vAddedNew) * sizeof(int); + memOth += (p->vPrevCore ? Vec_IntCap(p->vPrevCore) : 0) * sizeof(int); memOth += Vec_IntCap(p->vTemp) * sizeof(int); memOth += Vec_IntCap(p->vAbs) * sizeof(int); - memTot = memAig + memSat + memPro + memMap + memOth; - ABC_PRMP( "Memory: AIG ", memAig, memTot ); - ABC_PRMP( "Memory: SAT ", memSat, memTot ); - ABC_PRMP( "Memory: Proof", memPro, memTot ); - ABC_PRMP( "Memory: Map ", memMap, memTot ); - ABC_PRMP( "Memory: Other", memOth, memTot ); - ABC_PRMP( "Memory: TOTAL", memTot, memTot ); + memTot = memAig + memSat + memPro + memMap + memRef + memOth; + ABC_PRMP( "Memory: AIG ", memAig, memTot ); + ABC_PRMP( "Memory: SAT ", memSat, memTot ); + ABC_PRMP( "Memory: Proof ", memPro, memTot ); + ABC_PRMP( "Memory: Map ", memMap, memTot ); + ABC_PRMP( "Memory: Refine", memRef, memTot ); + ABC_PRMP( "Memory: Other ", memOth, memTot ); + ABC_PRMP( "Memory: TOTAL ", memTot, memTot ); } @@ -920,11 +1448,17 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) p->nCexes++; // perform the refinement clk2 = clock(); -// pCex = Vta_ManRefineAbstraction( p, f ); - pCex = NULL; - - vPPis = Gla_ManCollectPPis( p ); +/* + vPPis = Gla_ManRefinement( p ); + if ( vPPis == NULL ) + { + pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL; + break; + } +*/ + vPPis = Gla_ManCollectPPis( p, NULL ); Gla_ManExplorePPis( p, vPPis ); + Gia_GlaAddToAbs( p, vPPis, 1 ); Gia_GlaAddOneSlice( p, f, vPPis ); Vec_IntFree( vPPis ); @@ -952,6 +1486,8 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Gla_ManRollBack( p ); Vec_IntShrink( p->vCla2Obj, (int)p->pSat->stats.clauses+1 ); // load this timeframe + Vec_IntFreeP( &p->vPrevCore ); + p->vPrevCore = Gla_ManRegionStart( p, vCore ); Gia_GlaAddToAbs( p, vCore, 0 ); Gia_GlaAddOneSlice( p, f, vCore ); Vec_IntFree( vCore ); @@ -965,6 +1501,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) break; if ( Status == 0 ) { + assert( 0 ); // Vta_ManSatVerify( p ); // make sure, there was no initial abstraction (otherwise, it was invalid) assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart ); diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 9a9dc56f..44169f23 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -532,8 +532,8 @@ static inline void Vta_ObjPreds( Vta_Man_t * p, Vta_Obj_t * pThis, Gia_Obj_t * p { *ppThis0 = NULL; *ppThis1 = NULL; - if ( !pThis->fAdded ) - return; +// if ( !pThis->fAdded ) +// return; assert( !Gia_ObjIsPi(p->pGia, pObj) ); if ( Gia_ObjIsConst0(pObj) || (Gia_ObjIsCi(pObj) && pThis->iFrame == 0) ) return; @@ -541,13 +541,13 @@ static inline void Vta_ObjPreds( Vta_Man_t * p, Vta_Obj_t * pThis, Gia_Obj_t * p { *ppThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame ); *ppThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame ); - assert( *ppThis0 && *ppThis1 ); +// assert( *ppThis0 && *ppThis1 ); return; } assert( Gia_ObjIsRo(p->pGia, pObj) && pThis->iFrame > 0 ); pObj = Gia_ObjRoToRi( p->pGia, pObj ); *ppThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 ); - assert( *ppThis0 ); +// assert( *ppThis0 ); } /**Function************************************************************* @@ -569,9 +569,12 @@ void Vta_ManCollectNodes_rec( Vta_Man_t * p, Vta_Obj_t * pThis, Vec_Int_t * vOrd return; pThis->fVisit = 1; pObj = Gia_ManObj( p->pGia, pThis->iObj ); - Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 ); - if ( pThis0 ) Vta_ManCollectNodes_rec( p, pThis0, vOrder ); - if ( pThis1 ) Vta_ManCollectNodes_rec( p, pThis1, vOrder ); + if ( pThis->fAdded ) + { + Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 ); + if ( pThis0 ) Vta_ManCollectNodes_rec( p, pThis0, vOrder ); + if ( pThis1 ) Vta_ManCollectNodes_rec( p, pThis1, vOrder ); + } Vec_IntPush( vOrder, Vta_ObjId(p, pThis) ); } Vec_Int_t * Vta_ManCollectNodes( Vta_Man_t * p, int f ) @@ -728,6 +731,41 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f ) if ( pThis1 ) pThis1->Prio = Abc_MinInt( pThis1->Prio, pThis->Prio + 1 ); } + +/* + // update priorities according to reconvergest counters + Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i ) + { + Vta_Obj_t * pThis0, * pThis1; + Gia_Obj_t * pObj = Gia_ManObj( p->pGia, pThis->iObj ); + Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 ); + pThis->Prio += 10000000; + if ( pThis0 ) + pThis->Prio -= 1000000 * pThis0->fAdded; + if ( pThis1 ) + pThis->Prio -= 1000000 * pThis1->fAdded; + } + Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i ) + { + Vta_Obj_t * pThis0, * pThis1; + Gia_Obj_t * pObj = Gia_ManObj( p->pGia, pThis->iObj ); + Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 ); + pThis->Prio += 10000000; + if ( pThis0 ) + pThis->Prio -= 1000000 * pThis0->fAdded; + if ( pThis1 ) + pThis->Prio -= 1000000 * pThis1->fAdded; + } +*/ + +/* + // update priorities according to reconvergest counters + Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i ) + pThis->Prio = pThis->iObj; + Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i ) + pThis->Prio = pThis->iObj; +*/ + // objects with equal distance should receive priority based on number // those objects whose prototypes have been added in other timeframes // should have higher priority than the current object @@ -747,9 +785,6 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f ) pThis->Prio = Counter++; // Abc_Print( 1, "Used %d Unused %d\n", Vec_PtrSize(vTermsUsed), Vec_PtrSize(vTermsUnused) ); - Vec_PtrFree( vTermsUsed ); - Vec_PtrFree( vTermsUnused ); - // propagate in the direct order Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i ) @@ -885,6 +920,33 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f ) assert( 0 ); } + // mark those currently included + Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i ) + { + assert( pThis->fVisit == 0 ); + pThis->fVisit = 1; + } + // add used terms, which have close relationship + Counter = Vec_IntSize(vTermsToAdd); + Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i ) + { + if ( pThis->fVisit ) + continue; +// Vta_ObjPreds( p, pThis, Gia_ManObj(p->pGia, pThis->iObj), &pThis0, &pThis1 ); +// if ( (pThis0 && (pThis0->fAdded || pThis0->fVisit)) || (pThis1 && (pThis1->fAdded || pThis1->fVisit)) ) + Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) ); + } + // remove those currenty included + Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i ) + pThis->fVisit = 0; +// printf( "\n%d -> %d\n", Counter, Vec_IntSize(vTermsToAdd) ); +//Vec_IntReverseOrder( vTermsToAdd ); +//Vec_IntSort( vTermsToAdd, 1 ); + + // cleanup + Vec_PtrFree( vTermsUsed ); + Vec_PtrFree( vTermsUnused ); + if ( fVerify ) { @@ -955,7 +1017,6 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f ) pCex = Vga_ManDeriveCex( p ); else { -// int nObjOld = p->nObjs; Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i ) if ( !Gia_ObjIsPi(p->pGia, pObj) ) Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame ); -- cgit v1.2.3