diff options
Diffstat (limited to 'src/proof/abs/absGlaOld.c')
| -rw-r--r-- | src/proof/abs/absGlaOld.c | 1957 |
1 files changed, 1957 insertions, 0 deletions
diff --git a/src/proof/abs/absGlaOld.c b/src/proof/abs/absGlaOld.c new file mode 100644 index 00000000..5ee69739 --- /dev/null +++ b/src/proof/abs/absGlaOld.c @@ -0,0 +1,1957 @@ +/**CFile**************************************************************** + + FileName [absGla.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Abstraction package.] + + Synopsis [Gate-level abstraction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: absGla.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sat/cnf/cnf.h" +#include "sat/bsat/satSolver2.h" +#include "base/main/main.h" +#include "abs.h" +#include "absRef.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +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 : 16; // priority + unsigned Sign : 12; // traversal signature +}; + +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 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 * pGia0; // starting AIG manager + Gia_Man_t * pGia; // working AIG manager + Abs_Par_t * pPars; // parameters + // internal data + 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 +// int nAbsNew; // previous abstraction +// int nLrnOld; // the number of bytes +// int nLrnNew; // the number of bytes + // other data + int nCexes; // the number of counter-examples + int nObjAdded; // total number of objects added + 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 * vTemp; // temporary array + Vec_Int_t * vAddedNew; // temporary array + Vec_Int_t * vObjCounts; // object counters + Vec_Int_t * vCoreCounts; // counts how many times each object appears in the core + Vec_Int_t * vProofIds; // counts how many times each object appears in the core + int nProofIds; // proof ID counter + // refinement + Vec_Int_t * pvRefis; // vectors of each object + // refinement manager + Gia_Man_t * pGia2; + Rnm_Man_t * pRnm; + // statistics + clock_t timeInit; + clock_t timeSat; + clock_t timeUnsat; + clock_t timeCex; + clock_t 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_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, Gia_Obj_t * pObj, int f ) { return (Rfn_Obj_t *)Vec_IntGetEntryP( &(p->pvRefis[Gia_ObjId(p->pGia, pObj)]), f ); } +static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) { *((int *)p) = 0; } + + +// iterator through abstracted objects +#define Gla_ManForEachObj( p, pObj ) \ + for ( pObj = p->pObjs + 1; pObj < p->pObjs + p->nObjs; pObj++ ) +#define Gla_ManForEachObjAbs( p, pObj, i ) \ + for ( i = 0; i < Vec_IntSize(p->vAbs) && ((pObj = Gla_ManObj(p, Vec_IntEntry(p->vAbs, i))),1); i++) +#define Gla_ManForEachObjAbsVec( vVec, p, pObj, i ) \ + 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 ) \ + for ( i = 0; (i < (int)pObj->nFanins) && ((pFanin = Gla_ManObj(p, pObj->Fanins[i])),1); i++ ) + +// some lessons learned from debugging mismatches between GIA and mapped CNF +// - inputs/output of AND-node may be PPIs (have SAT vars), but the node is not included in the abstraction +// - some logic node can be a PPI of one LUT and an internal node of another LUT + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Prepares CEX and vMap for refinement.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_GlaPrepareCexAndMap( Gla_Man_t * p, Abc_Cex_t ** ppCex, Vec_Int_t ** pvMap ) +{ + Abc_Cex_t * pCex; + Vec_Int_t * vMap; + Gla_Obj_t * pObj, * pFanin; + Gia_Obj_t * pGiaObj; + int f, i, k; + // find PIs and PPIs + vMap = Vec_IntAlloc( 1000 ); + Gla_ManForEachObjAbs( p, pObj, i ) + { + assert( pObj->fConst || pObj->fRo || pObj->fAnd ); + Gla_ObjForEachFanin( p, pObj, pFanin, k ) + if ( !pFanin->fAbs ) + Vec_IntPush( vMap, pFanin->iGiaObj ); + } + Vec_IntUniqify( vMap ); + // derive counter-example + pCex = Abc_CexAlloc( 0, Vec_IntSize(vMap), p->pPars->iFrame+1 ); + pCex->iFrame = p->pPars->iFrame; + for ( f = 0; f <= p->pPars->iFrame; f++ ) + Gia_ManForEachObjVec( vMap, p->pGia, pGiaObj, k ) + if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pGiaObj), f ) ) + Abc_InfoSetBit( pCex->pData, f * Vec_IntSize(vMap) + k ); + *pvMap = vMap; + *ppCex = pCex; +} + +/**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 ) + { + if ( !Gia_ObjIsPi(p->pGia, pObj) ) + continue; + 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 GIA abstraction objects.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gla_ManCollectInternal_rec( Gia_Man_t * p, Gia_Obj_t * pGiaObj, Vec_Int_t * vRoAnds ) +{ + if ( Gia_ObjIsTravIdCurrent(p, pGiaObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pGiaObj); + assert( Gia_ObjIsAnd(pGiaObj) ); + Gla_ManCollectInternal_rec( p, Gia_ObjFanin0(pGiaObj), vRoAnds ); + Gla_ManCollectInternal_rec( p, Gia_ObjFanin1(pGiaObj), vRoAnds ); + Vec_IntPush( vRoAnds, Gia_ObjId(p, pGiaObj) ); +} +void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int_t * vCos, Vec_Int_t * vRoAnds ) +{ + Gla_Obj_t * pObj, * pFanin; + Gia_Obj_t * pGiaObj; + int i, k; + + // collect COs + Vec_IntPush( vCos, Gia_ObjId(p->pGia, Gia_ManPo(p->pGia, 0)) ); + // collect fanins of abstracted objects + Gla_ManForEachObjAbs( p, pObj, i ) + { + assert( pObj->fConst || pObj->fRo || pObj->fAnd ); + if ( pObj->fRo ) + { + pGiaObj = Gia_ObjRoToRi( p->pGia, Gia_ManObj(p->pGia, pObj->iGiaObj) ); + Vec_IntPush( vCos, Gia_ObjId(p->pGia, pGiaObj) ); + } + Gla_ObjForEachFanin( p, pObj, pFanin, k ) + if ( !pFanin->fAbs ) + Vec_IntPush( (pFanin->fPi ? vPis : vPPis), pFanin->iGiaObj ); + } + Vec_IntUniqify( vPis ); + Vec_IntUniqify( vPPis ); + Vec_IntSort( vCos, 0 ); + // sorting PIs/PPIs/COs leads to refinements that are more "well-aligned"... + + // mark const/PIs/PPIs + Gia_ManIncrementTravId( p->pGia ); + Gia_ObjSetTravIdCurrent( p->pGia, Gia_ManConst0(p->pGia) ); + Gia_ManForEachObjVec( vPis, p->pGia, pGiaObj, i ) + Gia_ObjSetTravIdCurrent( p->pGia, pGiaObj ); + Gia_ManForEachObjVec( vPPis, p->pGia, pGiaObj, i ) + Gia_ObjSetTravIdCurrent( p->pGia, pGiaObj ); + // mark and add ROs first + Gia_ManForEachObjVec( vCos, p->pGia, pGiaObj, i ) + { + if ( i == 0 ) continue; + pGiaObj = Gia_ObjRiToRo( p->pGia, pGiaObj ); + Gia_ObjSetTravIdCurrent( p->pGia, pGiaObj ); + Vec_IntPush( vRoAnds, Gia_ObjId(p->pGia, pGiaObj) ); + } + // collect nodes between PIs/PPIs/ROs and COs + Gia_ManForEachObjVec( vCos, p->pGia, pGiaObj, i ) + Gla_ManCollectInternal_rec( p->pGia, Gia_ObjFanin0(pGiaObj), vRoAnds ); +} + +/**Function************************************************************* + + Synopsis [Drive implications of the given node towards primary outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManRefSetAndPropFanout_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect, int Sign ) +{ + int i;//, Id = Gia_ObjId(p->pGia, pObj); + Rfn_Obj_t * pRef0, * pRef1, * pRef = Gla_ObjRef( p, pObj, f ); + Gia_Obj_t * pFanout; + int k; + if ( (int)pRef->Sign != Sign ) + return; + assert( pRef->fVisit == 0 ); + pRef->fVisit = 1; + if ( pRef->fPPi ) + { + assert( (int)pRef->Prio > 0 ); + for ( i = p->pPars->iFrame; i >= 0; i-- ) + if ( !Gla_ObjRef(p, pObj, i)->fVisit ) + Gia_ManRefSetAndPropFanout_rec( p, pObj, i, vSelect, Sign ); + Vec_IntPush( vSelect, Gia_ObjId(p->pGia, pObj) ); + return; + } + if ( (Gia_ObjIsCo(pObj) && f == p->pPars->iFrame) || Gia_ObjIsPo(p->pGia, pObj) ) + return; + if ( Gia_ObjIsRi(p->pGia, pObj) ) + { + pFanout = Gia_ObjRiToRo(p->pGia, pObj); + if ( !Gla_ObjRef(p, pFanout, f+1)->fVisit ) + Gia_ManRefSetAndPropFanout_rec( p, pFanout, f+1, vSelect, Sign ); + return; + } + assert( Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) ); + Gia_ObjForEachFanoutStatic( p->pGia, pObj, pFanout, k ) + { +// Rfn_Obj_t * pRefF = Gla_ObjRef(p, pFanout, f); + if ( Gla_ObjRef(p, pFanout, f)->fVisit ) + continue; + if ( Gia_ObjIsCo(pFanout) ) + { + Gia_ManRefSetAndPropFanout_rec( p, pFanout, f, vSelect, Sign ); + continue; + } + assert( Gia_ObjIsAnd(pFanout) ); + pRef0 = Gla_ObjRef( p, Gia_ObjFanin0(pFanout), f ); + pRef1 = Gla_ObjRef( p, Gia_ObjFanin1(pFanout), f ); + if ( ((pRef0->Value ^ Gia_ObjFaninC0(pFanout)) == 0 && pRef0->fVisit) || + ((pRef1->Value ^ Gia_ObjFaninC1(pFanout)) == 0 && pRef1->fVisit) || + ( ((pRef0->Value ^ Gia_ObjFaninC0(pFanout)) == 1 && pRef0->fVisit) && + ((pRef1->Value ^ Gia_ObjFaninC1(pFanout)) == 1 && pRef1->fVisit) ) ) + Gia_ManRefSetAndPropFanout_rec( p, pFanout, f, vSelect, Sign ); + } +} + +/**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 * vSelect, int Sign ) +{ + int i;//, Id = Gia_ObjId(p->pGia, pObj); + Rfn_Obj_t * pRef = Gla_ObjRef( p, pObj, f ); +// assert( (int)pRef->Sign == Sign ); + if ( pRef->fVisit ) + return; + if ( p->pPars->fPropFanout ) + Gia_ManRefSetAndPropFanout_rec( p, pObj, f, vSelect, Sign ); + else + pRef->fVisit = 1; + if ( pRef->fPPi ) + { + assert( (int)pRef->Prio > 0 ); + if ( p->pPars->fPropFanout ) + { + for ( i = p->pPars->iFrame; i >= 0; i-- ) + if ( !Gla_ObjRef(p, pObj, i)->fVisit ) + Gia_ManRefSetAndPropFanout_rec( p, pObj, i, vSelect, Sign ); + } + else + { + Vec_IntPush( vSelect, Gia_ObjId(p->pGia, pObj) ); + Vec_IntAddToEntry( p->vObjCounts, f, 1 ); + } + 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, vSelect, Sign ); + return; + } + if ( Gia_ObjIsAnd(pObj) ) + { + Rfn_Obj_t * pRef0 = Gla_ObjRef( p, Gia_ObjFanin0(pObj), f ); + Rfn_Obj_t * pRef1 = Gla_ObjRef( p, Gia_ObjFanin1(pObj), f ); + if ( pRef->Value == 1 ) + { + if ( pRef0->Prio > 0 ) + Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vSelect, Sign ); + if ( pRef1->Prio > 0 ) + Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vSelect, Sign ); + } + else // select one value + { + if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 ) + { + if ( pRef0->Prio <= pRef1->Prio ) // choice + { + if ( pRef0->Prio > 0 ) + Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vSelect, Sign ); + } + else + { + if ( pRef1->Prio > 0 ) + Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vSelect, Sign ); + } + } + else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 ) + { + if ( pRef0->Prio > 0 ) + Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vSelect, Sign ); + } + else if ( (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 ) + { + if ( pRef1->Prio > 0 ) + Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vSelect, Sign ); + } + else assert( 0 ); + } + } + else assert( 0 ); +} + + +/**Function************************************************************* + + Synopsis [Performs refinement.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gla_ManVerifyUsingTerSim( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int_t * vRoAnds, Vec_Int_t * vCos, Vec_Int_t * vRes ) +{ + Gia_Obj_t * pObj; + int i, f; +// 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 ) + Gia_ObjTerSimSetX( pObj ); + Gia_ManForEachObjVec( vRes, p->pGia, pObj, i ) + 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) ) + Abc_Print( 1, "\nRefinement verification has failed!!!\n" ); + // 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 ); +} + + +/**Function************************************************************* + + Synopsis [Performs refinement.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p ) +{ + Abc_Cex_t * pCex; + Vec_Int_t * vMap, * vVec; + Gia_Obj_t * pObj; + int i; + Gia_GlaPrepareCexAndMap( p, &pCex, &vMap ); + vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 0, 1 ); + Abc_CexFree( pCex ); + if ( Vec_IntSize(vVec) == 0 ) + { + Vec_IntFree( vVec ); + Abc_CexFreeP( &p->pGia->pCexSeq ); + p->pGia->pCexSeq = Gla_ManDeriveCex( p, vMap ); + Vec_IntFree( vMap ); + return NULL; + } + Vec_IntFree( vMap ); + // remap them into GLA objects + Gia_ManForEachObjVec( vVec, p->pGia, pObj, i ) + Vec_IntWriteEntry( vVec, i, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] ); + p->nObjAdded += Vec_IntSize(vVec); + return vVec; +} + +/**Function************************************************************* + + Synopsis [Performs refinement.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gla_ManRefinement2( Gla_Man_t * p ) +{ + int fVerify = 1; + static int Sign = 0; + Vec_Int_t * vPis, * vPPis, * vCos, * vRoAnds, * vSelect = NULL; + Rfn_Obj_t * pRef, * pRef0, * pRef1; + Gia_Obj_t * pObj; + int i, f; + Sign++; + + // compute PIs and pseudo-PIs + vCos = Vec_IntAlloc( 1000 ); + vPis = Vec_IntAlloc( 1000 ); + vPPis = Vec_IntAlloc( 1000 ); + vRoAnds = Vec_IntAlloc( 1000 ); + Gla_ManCollect( p, vPis, vPPis, vCos, vRoAnds ); + +/* + // check how many pseudo PIs have variables + Gla_ManForEachObjAbsVec( vPis, p, pGla, i ) + { + Abc_Print( 1, " %5d : ", Gla_ObjId(p, pGla) ); + for ( f = 0; f <= p->pPars->iFrame; f++ ) + Abc_Print( 1, "%d", Gla_ManCheckVar(p, Gla_ObjId(p, pGla), f) ); + Abc_Print( 1, "\n" ); + } + + // check how many pseudo PIs have variables + Gla_ManForEachObjAbsVec( vPPis, p, pGla, i ) + { + Abc_Print( 1, "%5d : ", Gla_ObjId(p, pGla) ); + for ( f = 0; f <= p->pPars->iFrame; f++ ) + Abc_Print( 1, "%d", Gla_ManCheckVar(p, Gla_ObjId(p, pGla), f) ); + Abc_Print( 1, "\n" ); + } +*/ + // propagate values + for ( f = 0; f <= p->pPars->iFrame; f++ ) + { + // constant + pRef = Gla_ObjRef( p, Gia_ManConst0(p->pGia), f ); Gla_ObjClearRef( pRef ); + pRef->Value = 0; + pRef->Prio = 0; + pRef->Sign = Sign; + // primary input + Gia_ManForEachObjVec( vPis, p->pGia, pObj, i ) + { +// assert( f == p->pPars->iFrame || Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) ); + pRef = Gla_ObjRef( p, pObj, f ); Gla_ObjClearRef( pRef ); + pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ); + pRef->Prio = 0; + pRef->Sign = Sign; + assert( pRef->fVisit == 0 ); + } + // primary input + Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i ) + { +// assert( f == p->pPars->iFrame || Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) ); + assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) ); + pRef = Gla_ObjRef( p, pObj, f ); Gla_ObjClearRef( pRef ); + pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ); + pRef->Prio = i+1; + pRef->fPPi = 1; + pRef->Sign = Sign; + assert( pRef->fVisit == 0 ); + } + // internal nodes + Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i ) + { + assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) ); + pRef = Gla_ObjRef( p, pObj, f ); Gla_ObjClearRef( pRef ); + if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + if ( f == 0 ) + { + pRef->Value = 0; + pRef->Prio = 0; + pRef->Sign = Sign; + } + else + { + pRef0 = Gla_ObjRef( p, Gia_ObjRoToRi(p->pGia, pObj), f-1 ); + pRef->Value = pRef0->Value; + pRef->Prio = pRef0->Prio; + pRef->Sign = Sign; + } + continue; + } + assert( Gia_ObjIsAnd(pObj) ); + pRef0 = Gla_ObjRef( p, Gia_ObjFanin0(pObj), f ); + pRef1 = Gla_ObjRef( p, Gia_ObjFanin1(pObj), f ); + pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj)) & (pRef1->Value ^ Gia_ObjFaninC1(pObj)); + + if ( p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] != ~0 && + Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) && + (int)pRef->Value != Gla_ObjSatValue(p, Gia_ObjId(p->pGia, pObj), f) ) + { + Abc_Print( 1, "Object has value mismatch " ); + Gia_ObjPrint( p->pGia, pObj ); + } + + 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; + assert( pRef->fVisit == 0 ); + pRef->Sign = Sign; + } + // output nodes + Gia_ManForEachObjVec( vCos, p->pGia, pObj, i ) + { + pRef = Gla_ObjRef( p, pObj, f ); Gla_ObjClearRef( pRef ); + pRef0 = Gla_ObjRef( p, Gia_ObjFanin0(pObj), f ); + pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj)); + pRef->Prio = pRef0->Prio; + assert( pRef->fVisit == 0 ); + pRef->Sign = Sign; + } + } + + // make sure the output value is 1 + pObj = Gia_ManPo( p->pGia, 0 ); + pRef = Gla_ObjRef( p, pObj, p->pPars->iFrame ); + if ( pRef->Value != 1 ) + Abc_Print( 1, "\nCounter-example verification has failed!!!\n" ); + + // 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 NULL; + } + + // select objects + vSelect = Vec_IntAlloc( 100 ); + Vec_IntFill( p->vObjCounts, p->pPars->iFrame+1, 0 ); + Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), p->pPars->iFrame, vSelect, Sign ); + Vec_IntUniqify( vSelect ); + +/* + for ( f = 0; f < p->pPars->iFrame; f++ ) + printf( "%2d", Vec_IntEntry(p->vObjCounts, f) ); + printf( "\n" ); +*/ + if ( fVerify ) + Gla_ManVerifyUsingTerSim( p, vPis, vPPis, vRoAnds, vCos, vSelect ); + + // remap them into GLA objects + Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i ) + Vec_IntWriteEntry( vSelect, i, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] ); + + Vec_IntFree( vPis ); + Vec_IntFree( vPPis ); + Vec_IntFree( vRoAnds ); + Vec_IntFree( vCos ); + + p->nObjAdded += Vec_IntSize(vSelect); + return vSelect; +} + + +/**Function************************************************************* + + Synopsis [Adds clauses for the given obj in the given frame.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gla_ManCollectFanins( Gla_Man_t * p, Gla_Obj_t * pGla, int iObj, Vec_Int_t * vFanins ) +{ + int i, nClauses, iFirstClause, * pLit; + nClauses = p->pCnf->pObj2Count[pGla->iGiaObj]; + iFirstClause = p->pCnf->pObj2Clause[pGla->iGiaObj]; + Vec_IntClear( vFanins ); + for ( i = iFirstClause; i < iFirstClause + nClauses; i++ ) + for ( pLit = p->pCnf->pClauses[i]; pLit < p->pCnf->pClauses[i+1]; pLit++ ) + if ( lit_var(*pLit) != iObj ) + Vec_IntPushUnique( vFanins, lit_var(*pLit) ); + assert( Vec_IntSize( vFanins ) <= 4 ); + Vec_IntSort( vFanins, 0 ); +} + + +/**Function************************************************************* + + Synopsis [Duplicates AIG while decoupling nodes duplicated in the mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDupMapped_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew ) +{ + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pObj); + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManDupMapped_rec( p, Gia_ObjFanin0(pObj), pNew ); + Gia_ManDupMapped_rec( p, Gia_ObjFanin1(pObj), pNew ); + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Vec_IntPush( pNew->vLutConfigs, Gia_ObjId(p, pObj) ); +} +Gia_Man_t * Gia_ManDupMapped( Gia_Man_t * p, Vec_Int_t * vMapping ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj, * pFanin; + int i, k, * pMapping, * pObj2Obj; + // start new manager + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + // start mapping + Gia_ManFillValue( p ); + pObj2Obj = ABC_FALLOC( int, Gia_ManObjNum(p) ); + pObj2Obj[0] = 0; + // create reverse mapping and attach it to the node + pNew->vLutConfigs = Vec_IntAlloc( Gia_ManObjNum(p) * 4 / 3 ); + Vec_IntPush( pNew->vLutConfigs, 0 ); + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + { + int Offset = Vec_IntEntry(vMapping, Gia_ObjId(p, pObj)); + if ( Offset == 0 ) + continue; + pMapping = Vec_IntEntryP( vMapping, Offset ); + Gia_ManIncrementTravId( p ); + for ( k = 1; k <= 4; k++ ) + { + if ( pMapping[k] == -1 ) + continue; + pFanin = Gia_ManObj(p, pMapping[k]); + Gia_ObjSetTravIdCurrent( p, pFanin ); + pFanin->Value = pObj2Obj[pMapping[k]]; + assert( ~pFanin->Value ); + } + assert( !Gia_ObjIsTravIdCurrent(p, pObj) ); + assert( !~pObj->Value ); + Gia_ManDupMapped_rec( p, pObj, pNew ); + pObj2Obj[i] = pObj->Value; + assert( ~pObj->Value ); + } + else if ( Gia_ObjIsCi(pObj) ) + { + pObj2Obj[i] = Gia_ManAppendCi( pNew ); + Vec_IntPush( pNew->vLutConfigs, i ); + } + else if ( Gia_ObjIsCo(pObj) ) + { + Gia_ObjFanin0(pObj)->Value = pObj2Obj[Gia_ObjFaninId0p(p, pObj)]; + assert( ~Gia_ObjFanin0(pObj)->Value ); + pObj2Obj[i] = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Vec_IntPush( pNew->vLutConfigs, i ); + } + } + assert( Vec_IntSize(pNew->vLutConfigs) == Gia_ManObjNum(pNew) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + // map original AIG into the new AIG + Gia_ManForEachObj( p, pObj, i ) + pObj->Value = pObj2Obj[i]; + ABC_FREE( pObj2Obj ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Creates a new manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Abs_Par_t * pPars ) +{ + Gla_Man_t * p; + Aig_Man_t * pAig; + Gia_Obj_t * pObj; + Gla_Obj_t * pGla; + Vec_Int_t * vMappingNew; + int i, k, Offset, * pMapping, * pLits, * pObj2Count, * pObj2Clause; + + // start + p = ABC_CALLOC( Gla_Man_t, 1 ); + p->pGia0 = pGia0; + p->pPars = pPars; + p->vAbs = Vec_IntAlloc( 100 ); + p->vTemp = Vec_IntAlloc( 100 ); + p->vAddedNew = Vec_IntAlloc( 100 ); + p->vObjCounts = Vec_IntAlloc( 100 ); + + // internal data + pAig = Gia_ManToAigSimple( pGia0 ); + p->pCnf = Cnf_DeriveOther( pAig, 1 ); + Aig_ManStop( pAig ); + // create working GIA + p->pGia = Gia_ManDupMapped( pGia0, p->pCnf->vMapping ); + if ( pPars->fPropFanout ) + Gia_ManStaticFanoutStart( p->pGia ); + + // derive new gate map + assert( pGia0->vGateClasses != 0 ); + p->pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) ); + p->vCoreCounts = Vec_IntStart( Gia_ManObjNum(p->pGia) ); + p->vProofIds = Vec_IntAlloc(0); + // update p->pCnf->vMapping, p->pCnf->pObj2Count, p->pCnf->pObj2Clause + // (here are not updating p->pCnf->pVarNums because it is not needed) + vMappingNew = Vec_IntStart( Gia_ManObjNum(p->pGia) ); + pObj2Count = ABC_FALLOC( int, Gia_ManObjNum(p->pGia) ); + pObj2Clause = ABC_FALLOC( int, Gia_ManObjNum(p->pGia) ); + Gia_ManForEachObj( pGia0, pObj, i ) + { + // skip internal nodes not used in the mapping + if ( !~pObj->Value ) + continue; + // replace positive literal by variable + assert( !Abc_LitIsCompl(pObj->Value) ); + pObj->Value = Abc_Lit2Var(pObj->Value); + assert( (int)pObj->Value < Gia_ManObjNum(p->pGia) ); + // update arrays + pObj2Count[pObj->Value] = p->pCnf->pObj2Count[i]; + pObj2Clause[pObj->Value] = p->pCnf->pObj2Clause[i]; + if ( Vec_IntEntry(pGia0->vGateClasses, i) ) + Vec_IntWriteEntry( p->pGia->vGateClasses, pObj->Value, 1 ); + // update mappings + Offset = Vec_IntEntry(p->pCnf->vMapping, i); + Vec_IntWriteEntry( vMappingNew, pObj->Value, Vec_IntSize(vMappingNew) ); + pMapping = Vec_IntEntryP(p->pCnf->vMapping, Offset); + Vec_IntPush( vMappingNew, pMapping[0] ); + for ( k = 1; k <= 4; k++ ) + { + if ( pMapping[k] == -1 ) + Vec_IntPush( vMappingNew, -1 ); + else + { + assert( ~Gia_ManObj(pGia0, pMapping[k])->Value ); + Vec_IntPush( vMappingNew, Gia_ManObj(pGia0, pMapping[k])->Value ); + } + } + } + // update mapping after the offset (currently not being done because it is not used) + Vec_IntFree( p->pCnf->vMapping ); p->pCnf->vMapping = vMappingNew; + ABC_FREE( p->pCnf->pObj2Count ); p->pCnf->pObj2Count = pObj2Count; + ABC_FREE( p->pCnf->pObj2Clause ); p->pCnf->pObj2Clause = pObj2Clause; + + + // count the number of variables + p->nObjs = 1; + Gia_ManForEachObj( p->pGia, pObj, i ) + if ( p->pCnf->pObj2Count[i] >= 0 ) + pObj->Value = p->nObjs++; + else + pObj->Value = ~0; + + // re-express CNF using new variable IDs + pLits = p->pCnf->pClauses[0]; + for ( i = 0; i < p->pCnf->nLiterals; i++ ) + { + // find the original AIG object + pObj = Gia_ManObj( pGia0, lit_var(pLits[i]) ); + assert( ~pObj->Value ); + // find the working AIG object + pObj = Gia_ManObj( p->pGia, pObj->Value ); + assert( ~pObj->Value ); + // express literal in terms of LUT variables + pLits[i] = toLitCond( pObj->Value, lit_sign(pLits[i]) ); + } + + // 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->fConst = Gia_ObjIsConst0(pObj); + pGla->fPi = Gia_ObjIsPi(p->pGia, pObj); + pGla->fPo = Gia_ObjIsPo(p->pGia, pObj); + pGla->fRi = Gia_ObjIsRi(p->pGia, pObj); + pGla->fRo = Gia_ObjIsRo(p->pGia, pObj); + pGla->fAnd = Gia_ObjIsAnd(pObj); + if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) ) + continue; + if ( Gia_ObjIsCo(pObj) ) + { + pGla->nFanins = 1; + pGla->Fanins[0] = Gia_ObjFanin0(pObj)->Value; + continue; + } + if ( Gia_ObjIsAnd(pObj) ) + { +// Gla_ManCollectFanins( p, pGla, pObj->Value, p->vTemp ); +// pGla->nFanins = Vec_IntSize( p->vTemp ); +// memcpy( pGla->Fanins, Vec_IntArray(p->vTemp), sizeof(int) * Vec_IntSize(p->vTemp) ); + Offset = Vec_IntEntry( p->pCnf->vMapping, i ); + pMapping = Vec_IntEntryP( p->pCnf->vMapping, Offset ); + pGla->nFanins = 0; + for ( k = 1; k <= 4; k++ ) + if ( pMapping[k] != -1 ) + pGla->Fanins[ pGla->nFanins++ ] = Gia_ManObj(p->pGia, pMapping[k])->Value; + continue; + } + assert( Gia_ObjIsRo(p->pGia, pObj) ); + pGla->nFanins = 1; + pGla->Fanins[0] = Gia_ObjFanin0( Gia_ObjRoToRi(p->pGia, pObj) )->Value; + pGla->fCompl0 = Gia_ObjFaninC0( Gia_ObjRoToRi(p->pGia, pObj) ); + } + p->pObjRoot = Gla_ManObj( p, Gia_ManPo(p->pGia, 0)->Value ); + // abstraction + assert( p->pGia->vGateClasses != NULL ); + Gla_ManForEachObj( p, pGla ) + { + if ( Vec_IntEntry( p->pGia->vGateClasses, pGla->iGiaObj ) == 0 ) + continue; + pGla->fAbs = 1; + Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) ); + } + // other + p->pSat = sat_solver2_new(); + if ( pPars->fUseFullProof ) + p->pSat->pPrf1 = Vec_SetAlloc( 20 ); +// p->pSat->fVerbose = p->pPars->fVerbose; +// sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax ); + p->pSat->nLearntStart = p->pPars->nLearnedStart; + p->pSat->nLearntDelta = p->pPars->nLearnedDelta; + p->pSat->nLearntRatio = p->pPars->nLearnedPerce; + p->pSat->nLearntMax = p->pSat->nLearntStart; + p->nSatVars = 1; + // start the refinement manager +// p->pGia2 = Gia_ManDup( p->pGia ); + p->pRnm = Rnm_ManStart( p->pGia ); + return p; +} + +/**Function************************************************************* + + Synopsis [Creates a new manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia, Abs_Par_t * pPars ) +{ + Gla_Man_t * p; + Aig_Man_t * pAig; + Gia_Obj_t * pObj; + Gla_Obj_t * pGla; + int i, * pLits; + // start + p = ABC_CALLOC( Gla_Man_t, 1 ); + p->pGia = pGia; + p->pPars = pPars; + p->vAbs = Vec_IntAlloc( 100 ); + p->vTemp = Vec_IntAlloc( 100 ); + p->vAddedNew = Vec_IntAlloc( 100 ); + // internal data + pAig = Gia_ManToAigSimple( p->pGia ); + p->pCnf = Cnf_DeriveOther( pAig, 1 ); + Aig_ManStop( pAig ); + // count the number of variables + p->nObjs = 1; + Gia_ManForEachObj( p->pGia, pObj, i ) + if ( p->pCnf->pObj2Count[i] >= 0 ) + pObj->Value = p->nObjs++; + else + pObj->Value = ~0; + // re-express CNF using new variable IDs + pLits = p->pCnf->pClauses[0]; + for ( i = 0; i < p->pCnf->nLiterals; i++ ) + { + pObj = Gia_ManObj( p->pGia, lit_var(pLits[i]) ); + assert( ~pObj->Value ); + pLits[i] = toLitCond( pObj->Value, lit_sign(pLits[i]) ); + } + // 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->fConst = Gia_ObjIsConst0(pObj); + pGla->fPi = Gia_ObjIsPi(p->pGia, pObj); + pGla->fPo = Gia_ObjIsPo(p->pGia, pObj); + pGla->fRi = Gia_ObjIsRi(p->pGia, pObj); + pGla->fRo = Gia_ObjIsRo(p->pGia, pObj); + pGla->fAnd = Gia_ObjIsAnd(pObj); + if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) ) + continue; + if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) ) + { + Gla_ManCollectFanins( p, pGla, pObj->Value, p->vTemp ); + pGla->nFanins = Vec_IntSize( p->vTemp ); + memcpy( pGla->Fanins, Vec_IntArray(p->vTemp), sizeof(int) * Vec_IntSize(p->vTemp) ); + continue; + } + assert( Gia_ObjIsRo(p->pGia, pObj) ); + pGla->nFanins = 1; + pGla->Fanins[0] = Gia_ObjFanin0( Gia_ObjRoToRi(p->pGia, pObj) )->Value; + pGla->fCompl0 = Gia_ObjFaninC0( Gia_ObjRoToRi(p->pGia, pObj) ); + } + p->pObjRoot = Gla_ManObj( p, Gia_ManPo(p->pGia, 0)->Value ); + // abstraction + assert( pGia->vGateClasses != NULL ); + Gla_ManForEachObj( p, pGla ) + { + if ( Vec_IntEntry( pGia->vGateClasses, pGla->iGiaObj ) == 0 ) + continue; + pGla->fAbs = 1; + Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) ); + } + // other + p->pSat = sat_solver2_new(); + p->nSatVars = 1; + return p; +} + +/**Function************************************************************* + + Synopsis [Creates a new manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gla_ManStop( Gla_Man_t * p ) +{ + Gla_Obj_t * pGla; + int i; + + if ( p->pPars->fVerbose ) + Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d Objs+ = %d\n", + sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), + sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded ); + + // stop the refinement manager +// Gia_ManStopP( &p->pGia2 ); + Rnm_ManStop( p->pRnm, 0 ); + + if ( p->pvRefis ) + for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ ) + ABC_FREE( p->pvRefis[i].pArray ); + Gla_ManForEachObj( p, pGla ) + ABC_FREE( pGla->vFrames.pArray ); + Cnf_DataFree( p->pCnf ); + if ( p->pGia0 != NULL ) + Gia_ManStop( p->pGia ); +// Gia_ManStaticFanoutStart( p->pGia0 ); + sat_solver2_delete( p->pSat ); + Vec_IntFreeP( &p->vObjCounts ); + Vec_IntFreeP( &p->vAddedNew ); + Vec_IntFreeP( &p->vCoreCounts ); + Vec_IntFreeP( &p->vProofIds ); + Vec_IntFreeP( &p->vTemp ); + Vec_IntFreeP( &p->vAbs ); + ABC_FREE( p->pvRefis ); + ABC_FREE( p->pObj2Obj ); + ABC_FREE( p->pObjs ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Creates a new manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_GlaAbsCount( Gla_Man_t * p, int fRo, int fAnd ) +{ + Gla_Obj_t * pObj; + int i, Counter = 0; + if ( fRo ) + Gla_ManForEachObjAbs( p, pObj, i ) + Counter += (pObj->fRo && pObj->fAbs); + else if ( fAnd ) + Gla_ManForEachObjAbs( p, pObj, i ) + Counter += (pObj->fAnd && pObj->fAbs); + else + Gla_ManForEachObjAbs( p, pObj, i ) + Counter += (pObj->fAbs); + return Counter; +} + + +/**Function************************************************************* + + Synopsis [Derives new abstraction map.] + + Description [Returns 1 if node contains abstracted leaf on the path.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gla_ManTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vGla, int nUsageCount ) +{ + int Value0, Value1; + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return 1; + Gia_ObjSetTravIdCurrent(p, pObj); + if ( Gia_ObjIsCi(pObj) ) + return 0; + assert( Gia_ObjIsAnd(pObj) ); + Value0 = Gla_ManTranslate_rec( p, Gia_ObjFanin0(pObj), vGla, nUsageCount ); + Value1 = Gla_ManTranslate_rec( p, Gia_ObjFanin1(pObj), vGla, nUsageCount ); + if ( Value0 || Value1 ) + Vec_IntAddToEntry( vGla, Gia_ObjId(p, pObj), nUsageCount ); + return Value0 || Value1; +} +Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p ) +{ + Vec_Int_t * vGla, * vGla2; + Gla_Obj_t * pObj, * pFanin; + Gia_Obj_t * pGiaObj; + int i, k, nUsageCount; + vGla = Vec_IntStart( Gia_ManObjNum(p->pGia) ); + Gla_ManForEachObjAbs( p, pObj, i ) + { + nUsageCount = Vec_IntEntry(p->vCoreCounts, pObj->iGiaObj); + assert( nUsageCount >= 0 ); + if ( nUsageCount == 0 ) + nUsageCount++; + pGiaObj = Gla_ManGiaObj( p, pObj ); + if ( Gia_ObjIsConst0(pGiaObj) || Gia_ObjIsRo(p->pGia, pGiaObj) ) + { + Vec_IntWriteEntry( vGla, pObj->iGiaObj, nUsageCount ); + continue; + } + assert( Gia_ObjIsAnd(pGiaObj) ); + Gia_ManIncrementTravId( p->pGia ); + Gla_ObjForEachFanin( p, pObj, pFanin, k ) + Gia_ObjSetTravIdCurrent( p->pGia, Gla_ManGiaObj(p, pFanin) ); + Gla_ManTranslate_rec( p->pGia, pGiaObj, vGla, nUsageCount ); + } + Vec_IntWriteEntry( vGla, 0, p->pPars->iFrame+1 ); + if ( p->pGia->vLutConfigs ) // use mapping from new to old + { + vGla2 = Vec_IntStart( Gia_ManObjNum(p->pGia0) ); + for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ ) + if ( Vec_IntEntry(vGla, i) ) + Vec_IntWriteEntry( vGla2, Vec_IntEntry(p->pGia->vLutConfigs, i), Vec_IntEntry(vGla, i) ); + Vec_IntFree( vGla ); + return vGla2; + } + return vGla; +} + + +/**Function************************************************************* + + Synopsis [Collect pseudo-PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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, 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++ % 5) == 0 ) + return; + j = 0; + Gla_ManForEachObjAbsVec( vPPis, p, pObj, i ) + { + assert( pObj->fAbs == 0 ); + Count = 0; + Gla_ObjForEachFanin( p, pObj, pFanin, k ) + Count += pFanin->fAbs; + if ( Count == 0 || ((Round & 1) && Count == 1) ) + continue; + Vec_IntWriteEntry( vPPis, j++, Gla_ObjId(p, pObj) ); + } +// printf( "\n%d -> %d\n", Vec_IntSize(vPPis), j ); + Vec_IntShrink( vPPis, j ); +} + + +/**Function************************************************************* + + Synopsis [Adds CNF for the given timeframe.] + + Description [] + + SideEffects [] + + 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 ); + int iVar = Vec_IntGetEntry( &pGla->vFrames, iFrame ); + assert( !pGla->fPo && !pGla->fRi ); + if ( iVar == 0 ) + { + Vec_IntSetEntry( &pGla->vFrames, iFrame, (iVar = p->nSatVars++) ); + // remember the change + Vec_IntPush( p->vAddedNew, iObj ); + Vec_IntPush( p->vAddedNew, iFrame ); + } + return iVar; +} +void Gla_ManAddClauses( Gla_Man_t * p, int iObj, int iFrame, Vec_Int_t * vLits ) +{ + Gla_Obj_t * pGlaObj = Gla_ManObj( p, iObj ); + int iVar, iVar1, iVar2; + if ( pGlaObj->fConst ) + { + iVar = Gla_ManGetVar( p, iObj, iFrame ); + sat_solver2_add_const( p->pSat, iVar, 1, 0, iObj ); + } + else if ( pGlaObj->fRo ) + { + assert( pGlaObj->nFanins == 1 ); + if ( iFrame == 0 ) + { + iVar = Gla_ManGetVar( p, iObj, iFrame ); + sat_solver2_add_const( p->pSat, iVar, 1, 0, iObj ); + } + else + { + iVar1 = Gla_ManGetVar( p, iObj, iFrame ); + iVar2 = Gla_ManGetVar( p, pGlaObj->Fanins[0], iFrame-1 ); + sat_solver2_add_buffer( p->pSat, iVar1, iVar2, pGlaObj->fCompl0, 0, iObj ); + } + } + else if ( pGlaObj->fAnd ) + { + int i, RetValue, nClauses, iFirstClause, * pLit; + nClauses = p->pCnf->pObj2Count[pGlaObj->iGiaObj]; + iFirstClause = p->pCnf->pObj2Clause[pGlaObj->iGiaObj]; + for ( i = iFirstClause; i < iFirstClause + nClauses; i++ ) + { + Vec_IntClear( vLits ); + for ( pLit = p->pCnf->pClauses[i]; pLit < p->pCnf->pClauses[i+1]; pLit++ ) + { + iVar = Gla_ManGetVar( p, lit_var(*pLit), iFrame ); + Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) ); + } + RetValue = sat_solver2_addclause( p->pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits), iObj ); + } + } + else assert( 0 ); +} +void Gia_GlaAddToCounters( Gla_Man_t * p, Vec_Int_t * vCore ) +{ + Gla_Obj_t * pGla; + int i; + Gla_ManForEachObjAbsVec( vCore, p, pGla, i ) + Vec_IntAddToEntry( p->vCoreCounts, pGla->iGiaObj, 1 ); +} +void Gia_GlaAddToAbs( Gla_Man_t * p, Vec_Int_t * vAbsAdd, int fCheck ) +{ + Gla_Obj_t * pGla; + int i, k = 0; + Gla_ManForEachObjAbsVec( vAbsAdd, p, pGla, i ) + { + if ( fCheck ) + { + assert( pGla->fAbs == 0 ); + if ( p->pSat->pPrf2 ) + Vec_IntWriteEntry( p->vProofIds, Gla_ObjId(p, pGla), p->nProofIds++ ); + } + if ( pGla->fAbs ) + continue; + pGla->fAbs = 1; + Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) ); + // filter clauses to remove those contained in the abstraction + Vec_IntWriteEntry( vAbsAdd, k++, Gla_ObjId(p, pGla) ); + } + Vec_IntShrink( vAbsAdd, k ); +} +void Gia_GlaAddTimeFrame( Gla_Man_t * p, int f ) +{ + Gla_Obj_t * pObj; + int i; + Gla_ManForEachObjAbs( p, pObj, i ) + Gla_ManAddClauses( p, Gla_ObjId(p, pObj), f, p->vTemp ); + sat_solver2_simplify( p->pSat ); +} +void Gia_GlaAddOneSlice( Gla_Man_t * p, int fCur, Vec_Int_t * vCore ) +{ + int f, i, iGlaObj; + for ( f = fCur; f >= 0; f-- ) + Vec_IntForEachEntry( vCore, iGlaObj, i ) + Gla_ManAddClauses( p, iGlaObj, f, p->vTemp ); + sat_solver2_simplify( p->pSat ); +} +void Gla_ManRollBack( Gla_Man_t * p ) +{ + int i, iObj, iFrame; + Vec_IntForEachEntryDouble( p->vAddedNew, iObj, iFrame, i ) + { + assert( Vec_IntEntry( &Gla_ManObj(p, iObj)->vFrames, iFrame ) > 0 ); + Vec_IntWriteEntry( &Gla_ManObj(p, iObj)->vFrames, iFrame, 0 ); + } + Vec_IntForEachEntryStart( p->vAbs, iObj, i, p->nAbsOld ) + { + assert( Gla_ManObj( p, iObj )->fAbs == 1 ); + Gla_ManObj( p, iObj )->fAbs = 0; + } + Vec_IntShrink( p->vAbs, p->nAbsOld ); +} + + + + + +/**Function************************************************************* + + Synopsis [Finds the set of clauses involved in the UNSAT core.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gla_ManGetOutLit( Gla_Man_t * p, int f ) +{ + Gla_Obj_t * pFanin = Gla_ManObj( p, p->pObjRoot->Fanins[0] ); + int iSat = Vec_IntEntry( &pFanin->vFrames, f ); + assert( iSat > 0 ); + if ( f == 0 && pFanin->fRo && !p->pObjRoot->fCompl0 ) + return -1; + return Abc_Var2Lit( iSat, p->pObjRoot->fCompl0 ); +} +Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls ) +{ + Vec_Int_t * vCore = NULL; + int nConfPrev = pSat->stats.conflicts; + int RetValue, iLit = Gla_ManGetOutLit( p, f ); + clock_t clk = clock(); + if ( piRetValue ) + *piRetValue = 1; + // consider special case when PO points to the flop + // this leads to immediate conflict in the first timeframe + if ( iLit == -1 ) + { + vCore = Vec_IntAlloc( 1 ); + Vec_IntPush( vCore, p->pObjRoot->Fanins[0] ); + return vCore; + } + // solve the problem + RetValue = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( pnConfls ) + *pnConfls = (int)pSat->stats.conflicts - nConfPrev; + if ( RetValue == l_Undef ) + { + if ( piRetValue ) + *piRetValue = -1; + return NULL; + } + if ( RetValue == l_True ) + { + if ( piRetValue ) + *piRetValue = 0; + return NULL; + } + if ( fVerbose ) + { +// Abc_Print( 1, "%6d", (int)pSat->stats.conflicts - nConfPrev ); +// Abc_Print( 1, "UNSAT after %7d conflicts. ", pSat->stats.conflicts ); +// Abc_PrintTime( 1, "Time", clock() - clk ); + } + assert( RetValue == l_False ); + // derive the UNSAT core + clk = clock(); + vCore = (Vec_Int_t *)Sat_ProofCore( pSat ); + if ( vCore ) + Vec_IntSort( vCore, 1 ); + if ( fVerbose ) + { +// Abc_Print( 1, "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) ); +// Abc_PrintTime( 1, "Time", clock() - clk ); + } + return vCore; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfls, int nCexes, clock_t Time ) +{ + if ( Abc_FrameIsBatchMode() && nCoreSize <= 0 ) + return; + Abc_Print( 1, "%4d :", nFrames-1 ); + Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * Gia_GlaAbsCount(p, 0, 0) / (p->nObjs - Gia_ManPoNum(p->pGia) + Gia_ManCoNum(p->pGia) + 1)) ); + Abc_Print( 1, "%6d", Gia_GlaAbsCount(p, 0, 0) ); + Abc_Print( 1, "%5d", Gla_ManCountPPis(p) ); + Abc_Print( 1, "%5d", Gia_GlaAbsCount(p, 1, 0) ); + Abc_Print( 1, "%6d", Gia_GlaAbsCount(p, 0, 1) ); + Abc_Print( 1, "%8d", nConfls ); + if ( nCexes == 0 ) + Abc_Print( 1, "%5c", '-' ); + else + Abc_Print( 1, "%5d", nCexes ); +// Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) ); + Abc_PrintInt( sat_solver2_nvars(p->pSat) ); + Abc_PrintInt( sat_solver2_nclauses(p->pSat) ); + Abc_PrintInt( sat_solver2_nlearnts(p->pSat) ); +// Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 ); + Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC ); + Abc_Print( 1, "%5.0f MB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<20) ); +// Abc_PrintInt( p->nAbsNew ); +// Abc_PrintInt( p->nLrnNew ); +// Abc_Print( 1, "%4.1f MB", 4.0 * p->nLrnNew * Abc_BitWordNum(p->nAbsNew) / (1<<20) ); + Abc_Print( 1, "%s", (nCoreSize > 0 && nCexes > 0) ? "\n" : "\r" ); + fflush( stdout ); +} +void Gla_ManReportMemory( Gla_Man_t * p ) +{ + Gla_Obj_t * pGla; + double memTot = 0; + double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t); + double memSat = sat_solver2_memory( p->pSat, 1 ); + double memPro = sat_solver2_memory_proof( p->pSat ); + double memMap = p->nObjs * sizeof(Gla_Obj_t) + Gia_ManObjNum(p->pGia) * sizeof(int); + double memRef = Rnm_ManMemoryUsage( p->pRnm ); + double memOth = sizeof(Gla_Man_t); + for ( pGla = p->pObjs; pGla < p->pObjs + p->nObjs; pGla++ ) + memMap += Vec_IntCap(&pGla->vFrames) * sizeof(int); + memOth += Vec_IntCap(p->vAddedNew) * sizeof(int); + memOth += Vec_IntCap(p->vTemp) * sizeof(int); + memOth += Vec_IntCap(p->vAbs) * sizeof(int); + 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 ); +} + + +/**Function************************************************************* + + Synopsis [Send abstracted model or send cancel.] + + Description [Counter-example will be sent automatically when &vta terminates.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_GlaSendAbsracted( Gla_Man_t * p, int fVerbose ) +{ + extern int Gia_ManToBridgeAbsNetlist( FILE * pFile, Gia_Man_t * p ); + Gia_Man_t * pAbs; + Vec_Int_t * vGateClasses; + assert( Abc_FrameIsBridgeMode() ); +// if ( fVerbose ) +// Abc_Print( 1, "Sending abstracted model...\n" ); + // create abstraction (value of p->pGia is not used here) + vGateClasses = Gla_ManTranslate( p ); + pAbs = Gia_ManDupAbsGates( p->pGia0, vGateClasses ); + Vec_IntFreeP( &vGateClasses ); + // send it out + Gia_ManToBridgeAbsNetlist( stdout, pAbs ); + Gia_ManStop( pAbs ); +} +void Gia_GlaSendCancel( Gla_Man_t * p, int fVerbose ) +{ + extern int Gia_ManToBridgeBadAbs( FILE * pFile ); + assert( Abc_FrameIsBridgeMode() ); +// if ( fVerbose ) +// Abc_Print( 1, "Cancelling previously sent model...\n" ); + Gia_ManToBridgeBadAbs( stdout ); +} + +/**Function************************************************************* + + Synopsis [Send abstracted model or send cancel.] + + Description [Counter-example will be sent automatically when &vta terminates.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose ) +{ + char * pFileNameDef = "glabs.aig"; + char * pFileName = p->pPars->pFileVabs ? p->pPars->pFileVabs : pFileNameDef; + Gia_Man_t * pAbs; + Vec_Int_t * vGateClasses; + if ( fVerbose ) + Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName ); + // create abstraction + vGateClasses = Gla_ManTranslate( p ); + pAbs = Gia_ManDupAbsGates( p->pGia0, vGateClasses ); + Vec_IntFreeP( &vGateClasses ); + // write into file + Gia_WriteAiger( pAbs, pFileName, 0, 0 ); + Gia_ManStop( pAbs ); +} + + +/**Function************************************************************* + + Synopsis [Performs gate-level abstraction] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta ) +{ + extern int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars ); + extern void Ga2_ManDumpStats( Gia_Man_t * pGia, Abs_Par_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN ); + Gla_Man_t * p; + Vec_Int_t * vPPis, * vCore;//, * vCore2 = NULL; + Abc_Cex_t * pCex = NULL; + int f, i, iPrev, nConfls, Status, nVarsOld = 0, nCoreSize, fOneIsSent = 0, RetValue = -1; + clock_t clk2, clk = clock(); + // preconditions + assert( Gia_ManPoNum(pAig) == 1 ); + assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax ); + if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) ) + { + if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) ) + { + printf( "Sequential miter is trivially UNSAT.\n" ); + return 1; + } + ABC_FREE( pAig->pCexSeq ); + pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 ); + printf( "Sequential miter is trivially SAT.\n" ); + return 0; + } + + // compute intial abstraction + if ( pAig->vGateClasses == NULL ) + { + if ( fStartVta ) + { + int nFramesMaxOld = pPars->nFramesMax; + int nFramesStartOld = pPars->nFramesStart; + int nTimeOutOld = pPars->nTimeOut; + int nDumpOld = pPars->fDumpVabs; + pPars->nFramesMax = pPars->nFramesStart; + pPars->nFramesStart = Abc_MinInt( pPars->nFramesStart/2 + 1, 3 ); + pPars->nTimeOut = 20; + pPars->fDumpVabs = 0; + RetValue = Gia_VtaPerformInt( pAig, pPars ); + pPars->nFramesMax = nFramesMaxOld; + pPars->nFramesStart = nFramesStartOld; + pPars->nTimeOut = nTimeOutOld; + pPars->fDumpVabs = nDumpOld; + // create gate classes + Vec_IntFreeP( &pAig->vGateClasses ); + if ( pAig->vObjClasses ) + pAig->vGateClasses = Gia_VtaConvertToGla( pAig, pAig->vObjClasses ); + Vec_IntFreeP( &pAig->vObjClasses ); + // return if VTA solve the problem if could not start + if ( RetValue == 0 || pAig->vGateClasses == NULL ) + return RetValue; + } + else + { + pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) ); + Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 ); + Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)), 1 ); + } + } + // start the manager + p = Gla_ManStart( pAig, pPars ); + p->timeInit = clock() - clk; + // set runtime limit + if ( p->pPars->nTimeOut ) + sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + clock() ); + // perform initial abstraction + if ( p->pPars->fVerbose ) + { + Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" ); + Abc_Print( 1, "FrameMax = %d ConfMax = %d Timeout = %d RatioMin = %d %%.\n", + pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin ); + Abc_Print( 1, "LearnStart = %d LearnDelta = %d LearnRatio = %d %%.\n", + pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce ); + Abc_Print( 1, " Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" ); + } + for ( f = i = iPrev = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++, iPrev = i ) + { + int nConflsBeg = sat_solver2_nconflicts(p->pSat); + p->pPars->iFrame = f; + + // load timeframe + Gia_GlaAddTimeFrame( p, f ); + + // iterate as long as there are counter-examples + for ( i = 0; ; i++ ) + { + clk2 = clock(); + vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls ); +// assert( (vCore != NULL) == (Status == 1) ); + if ( Status == -1 || (p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit) ) // resource limit is reached + { + Prf_ManStopP( &p->pSat->pPrf2 ); +// if ( Gia_ManRegNum(p->pGia) > 1 ) // for comb cases, return the abstraction +// Vec_IntShrink( p->vAbs, p->nAbsOld ); + goto finish; + } + if ( Status == 1 ) + { + Prf_ManStopP( &p->pSat->pPrf2 ); + p->timeUnsat += clock() - clk2; + break; + } + p->timeSat += clock() - clk2; + assert( Status == 0 ); + p->nCexes++; + + // cancel old one if it was sent + if ( Abc_FrameIsBridgeMode() && fOneIsSent ) + { + Gia_GlaSendCancel( p, pPars->fVerbose ); + fOneIsSent = 0; + } + + // perform the refinement + clk2 = clock(); + if ( pPars->fAddLayer ) + { + vPPis = Gla_ManCollectPPis( p, NULL ); +// Gla_ManExplorePPis( p, vPPis ); + } + else + { + vPPis = Gla_ManRefinement( p ); + if ( vPPis == NULL ) + { + Prf_ManStopP( &p->pSat->pPrf2 ); + pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL; + break; + } + } + assert( pCex == NULL ); + + // start proof logging + if ( i == 0 ) + { + // create bookmark to be used for rollback + sat_solver2_bookmark( p->pSat ); + Vec_IntClear( p->vAddedNew ); + p->nAbsOld = Vec_IntSize( p->vAbs ); + nVarsOld = p->nSatVars; +// p->nLrnOld = sat_solver2_nlearnts( p->pSat ); +// p->nAbsNew = 0; +// p->nLrnNew = 0; + + // start incremental proof manager + assert( p->pSat->pPrf2 == NULL ); + if ( p->pSat->pPrf1 == NULL ) + p->pSat->pPrf2 = Prf_ManAlloc(); + if ( p->pSat->pPrf2 ) + { + p->nProofIds = 0; + Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 ); + Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vPPis) ); + } + } + else + { + // resize the proof logger + if ( p->pSat->pPrf2 ) + Prf_ManGrow( p->pSat->pPrf2, p->nProofIds + Vec_IntSize(vPPis) ); + } + + Gia_GlaAddToAbs( p, vPPis, 1 ); + Gia_GlaAddOneSlice( p, f, vPPis ); + Vec_IntFree( vPPis ); + + // print the result (do not count it towards change) + if ( p->pPars->fVerbose ) + Gla_ManAbsPrintFrame( p, -1, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk ); + } + if ( pCex != NULL ) + break; + assert( Status == 1 ); + + // valid core is obtained + nCoreSize = 1; + if ( vCore ) + { + nCoreSize += Vec_IntSize( vCore ); + Gia_GlaAddToCounters( p, vCore ); + } + if ( i == 0 ) + { + p->pPars->nFramesNoChange++; + Vec_IntFreeP( &vCore ); + } + else + { + p->pPars->nFramesNoChange = 0; +// p->nAbsNew = Vec_IntSize( p->vAbs ) - p->nAbsOld; +// p->nLrnNew = Abc_AbsInt( sat_solver2_nlearnts( p->pSat ) - p->nLrnOld ); + // update the SAT solver + sat_solver2_rollback( p->pSat ); + // update storage + Gla_ManRollBack( p ); + p->nSatVars = nVarsOld; + // load this timeframe + Gia_GlaAddToAbs( p, vCore, 0 ); + Gia_GlaAddOneSlice( p, f, vCore ); + Vec_IntFree( vCore ); + // run SAT solver + clk2 = clock(); + vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls ); + p->timeUnsat += clock() - clk2; +// assert( (vCore != NULL) == (Status == 1) ); + Vec_IntFreeP( &vCore ); + if ( Status == -1 ) // resource limit is reached + 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 ); + // pCex = Vga_ManDeriveCex( p ); + break; + } + } + // print the result + if ( p->pPars->fVerbose ) + Gla_ManAbsPrintFrame( p, nCoreSize, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk ); + + if ( f > 2 && iPrev > 0 && i == 0 ) // change has happened + { + if ( Abc_FrameIsBridgeMode() ) + { + // cancel old one if it was sent + if ( fOneIsSent ) + Gia_GlaSendCancel( p, pPars->fVerbose ); + // send new one + Gia_GlaSendAbsracted( p, pPars->fVerbose ); + fOneIsSent = 1; + } + + // dump the model into file + if ( p->pPars->fDumpVabs ) + { + char Command[1000]; + Abc_FrameSetStatus( -1 ); + Abc_FrameSetCex( NULL ); + Abc_FrameSetNFrames( f+1 ); + sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status") ); + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ); + Gia_GlaDumpAbsracted( p, pPars->fVerbose ); + } + } + + // check if the number of objects is below limit + if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 ) + { + Status = -1; + break; + } + } +finish: + // analize the results + if ( pCex == NULL ) + { + if ( p->pPars->fVerbose && Status == -1 ) + printf( "\n" ); +// if ( pAig->vGateClasses != NULL ) +// Abc_Print( 1, "Replacing the old abstraction by a new one.\n" ); + Vec_IntFreeP( &pAig->vGateClasses ); + pAig->vGateClasses = Gla_ManTranslate( p ); + if ( Status == -1 ) + { + if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) + Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange ); + else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit ) + Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, f, p->pPars->nFramesNoChange ); + else if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 ) + Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f ); + else + Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f ); + } + else + { + p->pPars->iFrame++; + Abc_Print( 1, "GLA completed %d frames with a %d-stable abstraction. ", f, p->pPars->nFramesNoChange ); + } + } + else + { + if ( p->pPars->fVerbose ) + printf( "\n" ); + ABC_FREE( pAig->pCexSeq ); + pAig->pCexSeq = pCex; + if ( !Gia_ManVerifyCex( pAig, pCex, 0 ) ) + Abc_Print( 1, " Gia_ManPerformGlaOld(): CEX verification has failed!\n" ); + Abc_Print( 1, "Counter-example detected in frame %d. ", f ); + p->pPars->iFrame = pCex->iFrame - 1; + Vec_IntFreeP( &pAig->vGateClasses ); + RetValue = 0; + } + Abc_PrintTime( 1, "Time", clock() - clk ); + if ( p->pPars->fVerbose ) + { + p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit; + ABC_PRTP( "Runtime: Initializing", p->timeInit, clock() - clk ); + ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, clock() - clk ); + ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, clock() - clk ); + ABC_PRTP( "Runtime: Refinement ", p->timeCex, clock() - clk ); + ABC_PRTP( "Runtime: Other ", p->timeOther, clock() - clk ); + ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk ); + Gla_ManReportMemory( p ); + } +// Ga2_ManDumpStats( pAig, p->pPars, p->pSat, p->pPars->iFrame, 1 ); + Gla_ManStop( p ); + fflush( stdout ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |