diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-31 00:00:34 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-31 00:00:34 -0700 |
commit | b20ca62e0020ab5f48e34d00ab6fed341a59921b (patch) | |
tree | 26a790aa45b971fa845cc077236012e4891f2897 | |
parent | 51d5055e68f5eb0e4ee222c8ffe20c00e1cd1b0f (diff) | |
download | abc-b20ca62e0020ab5f48e34d00ab6fed341a59921b.tar.gz abc-b20ca62e0020ab5f48e34d00ab6fed341a59921b.tar.bz2 abc-b20ca62e0020ab5f48e34d00ab6fed341a59921b.zip |
Scalable gate-level abstraction.
-rw-r--r-- | src/aig/gia/giaAbsGla2.c | 211 |
1 files changed, 160 insertions, 51 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index cf2dfb95..c2ecef8d 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -46,7 +46,7 @@ struct Ga2_Man_t_ Vec_Int_t * vIds; // abstraction ID for each GIA object Vec_Int_t * vAbs; // array of abstracted objects Vec_Int_t * vValues; // array of objects with abstraction ID assigned - Vec_Int_t * vProofIds; // proof IDs for these objects (1-to-1 with vValues) + Vec_Int_t * vProofIds; // mapping of GIA objects into their proof IDs int nProofIds; // the counter of proof IDs int LimAbs; // limit value for starting abstraction objects int LimPpi; // limit value for starting PPI objects @@ -82,8 +82,8 @@ static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj ) static inline int Ga2_ObjId( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vIds, Gia_ObjId(p->pGia, pObj)); } static inline void Ga2_ObjSetId( Ga2_Man_t * p, Gia_Obj_t * pObj, int i ) { Vec_IntWriteEntry(p->vIds, Gia_ObjId(p->pGia, pObj), i); } -static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Vec_PtrEntry(p->vCnfs, (Ga2_ObjId(p,pObj) << 1) ); } -static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Vec_PtrEntry(p->vCnfs, (Ga2_ObjId(p,pObj) << 1)+1); } +static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj) ); } +static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)+1 ); } static inline int Ga2_ObjIsAbs( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Ga2_ObjId(p,pObj) < p->LimAbs; } static inline int Ga2_ObjIsPpi( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Ga2_ObjId(p,pObj) >= p->LimAbs && Ga2_ObjId(p,pObj) < p->LimPpi; } @@ -93,6 +93,7 @@ static inline Vec_Int_t * Ga2_MapFrameMap( Ga2_Man_t * p, int f ) // returns literal of this object, or -1 if SAT variable of the object is not assigned static inline int Ga2_ObjFindLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) { + int Id = Ga2_ObjId(p,pObj); assert( Ga2_ObjId(p,pObj) && Ga2_ObjId(p,pObj) < Vec_IntSize(p->vValues) ); if ( f == Vec_PtrSize(p->vId2Lit) ) Vec_PtrPush( p->vId2Lit, Vec_IntStartFull(Vec_IntSize(p->vValues)) ); @@ -357,9 +358,8 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) p->vIds = Vec_IntStart( Gia_ManObjNum(pGia) ); p->vAbs = Vec_IntAlloc( 1000 ); p->vValues = Vec_IntAlloc( 1000 ); - p->vProofIds = Vec_IntAlloc( 1000 ); + p->vProofIds = Vec_IntAlloc(0); Vec_IntPush( p->vValues, -1 ); - Vec_IntPush( p->vProofIds, -1 ); // refinement p->pRnm = Rnm_ManStart( pGia ); // SAT solver and variables @@ -401,8 +401,10 @@ void Ga2_ManStop( Ga2_Man_t * p ) Vec_IntFreeP( &p->pGia->vMapping ); Gia_ManSetPhase( p->pGia ); // if ( p->pPars->fVerbose ) - Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Reduce = %d Cex = %d ObjsAdded = %d\n", - sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded ); + Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d ObjsAdded = %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 ); if( p->pSat ) sat_solver2_delete( p->pSat ); Vec_VecFree( (Vec_Vec_t *)p->vCnfs ); Vec_VecFree( (Vec_Vec_t *)p->vId2Lit ); @@ -615,35 +617,33 @@ static inline void Ga2_ManCnfAddStatic( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_In SeeAlso [] ***********************************************************************/ -void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs, int ProofId ) +void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs ) { unsigned uTruth; int nLeaves; assert( pObj->fPhase ); assert( Vec_PtrSize(p->vCnfs) == 2 * Vec_IntSize(p->vValues) ); - assert( Vec_IntSize(p->vProofIds) == Vec_IntSize(p->vValues) ); // assign abstraction ID to the node if ( Ga2_ObjId(p,pObj) == 0 ) { Ga2_ObjSetId( p, pObj, Vec_IntSize(p->vValues) ); Vec_IntPush( p->vValues, Gia_ObjId(p->pGia, pObj) ); - Vec_IntPush( p->vProofIds, ProofId ); Vec_PtrPush( p->vCnfs, NULL ); Vec_PtrPush( p->vCnfs, NULL ); } assert( Ga2_ObjCnf0(p, pObj) == NULL ); - if ( !fAbs ) + if ( !fAbs || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsConst0(pObj) ) return; + assert( Gia_ObjIsAnd(pObj) ); // compute parameters nLeaves = Ga2_ObjLeaveNum(p->pGia, pObj); - // create CNF for pos/neg phases uTruth = Ga2_ObjTruth( p->pGia, pObj ); - Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj), Ga2_ManCnfCompute(uTruth, nLeaves, p->vIsopMem) ); - uTruth = (~uTruth) & Abc_InfoMask( (1 << nLeaves) ); - Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, Ga2_ManCnfCompute(uTruth, nLeaves, p->vIsopMem) ); + // create CNF for pos/neg phases + Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj), Ga2_ManCnfCompute( uTruth, nLeaves, p->vIsopMem) ); + Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, Ga2_ManCnfCompute(~uTruth, nLeaves, p->vIsopMem) ); } -void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd, int ProofId ) +void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd ) { Vec_Int_t * vLeaves, * vMap; Gia_Obj_t * pObj, * pFanin; @@ -651,16 +651,25 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd, int ProofId ) // add abstraction objects Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i ) { - Ga2_ManSetupNode( p, pObj, 1, ProofId ); + Ga2_ManSetupNode( p, pObj, 1 ); Vec_IntPush( p->vAbs, Gia_ObjId(p->pGia, pObj) ); - Vec_IntPush( p->vProofIds, ProofId ); + if ( p->pSat->pPrf2 ) + Vec_IntWriteEntry( p->vProofIds, Gia_ObjId(p->pGia, pObj), p->nProofIds++ ); } // add PPI objects Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i ) { + if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + pFanin = Gia_ObjRoToRi(p->pGia, pObj); + if ( !Ga2_ObjId( p, Gia_ObjFanin0(pFanin) ) ) + Ga2_ManSetupNode( p, Gia_ObjFanin0(pFanin), 0 ); + continue; + } vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) - Ga2_ManSetupNode( p, pObj, 0, -1 ); + if ( !Ga2_ObjId( p, pFanin ) ) + Ga2_ManSetupNode( p, pFanin, 0 ); } // clean mapping in the timeframes Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i ) @@ -674,12 +683,8 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd, int ProofId ) Vec_IntClear( p->vLits ); Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f ) ); - Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Vec_IntEntry(p->vProofIds, Ga2_ObjId(p, pObj)) ); + Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj) ); } - // verify -- if ProofId == -1, all proof IDs should be the same - if ( ProofId == -1 ) - Vec_IntForEachEntry( p->vProofIds, k, i ) - assert( k == -1 ); } void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f ) @@ -696,7 +701,7 @@ void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f ) Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f ) ); iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f ); - Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, i - p->LimAbs ); + Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj) ); } } @@ -723,13 +728,13 @@ void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues ) // shrink values Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i ) { + if ( !i ) continue; assert( Ga2_ObjId(p,pObj) ); if ( i < nValues ) continue; Ga2_ObjSetId( p, pObj, 0 ); } Vec_IntShrink( p->vValues, nValues ); - Vec_IntShrink( p->vProofIds, nValues ); Vec_PtrShrink( p->vCnfs, 2 * nValues ); // clean mapping into timeframes Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i ) @@ -763,8 +768,20 @@ Vec_Int_t * Ga2_ManAbsTranslate( Ga2_Man_t * p ) Gia_Obj_t * pObj; int i; vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) ); + Vec_IntWriteEntry( vGateClasses, 0, 1 ); Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i ) - Ga2_ManAbsTranslate_rec( p->pGia, pObj, vGateClasses, 1 ); + { + if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + Vec_IntWriteEntry( vGateClasses, Gia_ObjId(p->pGia, pObj), 1 ); + pObj = Gia_ObjRoToRi( p->pGia, pObj ); + Vec_IntWriteEntry( vGateClasses, Gia_ObjFaninId0p(p->pGia, pObj), 1 ); + } + else if ( Gia_ObjIsAnd(pObj) ) + Ga2_ManAbsTranslate_rec( p->pGia, pObj, vGateClasses, 1 ); + else if ( !Gia_ObjIsConst0(pObj) ) + assert( 0 ); + } return vGateClasses; } @@ -774,9 +791,10 @@ Vec_Int_t * Ga2_ManAbsDerive( Gia_Man_t * p ) Gia_Obj_t * pObj; int i; vToAdd = Vec_IntAlloc( 1000 ); + Vec_IntPush( vToAdd, 0 ); // const 0 Gia_ManForEachRo( p, pObj, i ) - if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, i) ) - Vec_IntPush( vToAdd, i ); + if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, Gia_ObjId(p, pObj)) ) + Vec_IntPush( vToAdd, Gia_ObjId(p, pObj) ); Gia_ManForEachAnd( p, pObj, i ) if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, i) ) Vec_IntPush( vToAdd, i ); @@ -788,7 +806,6 @@ void Ga2_ManRestart( Ga2_Man_t * p ) Vec_Int_t * vToAdd; assert( p->pGia != NULL && p->pGia->vGateClasses != NULL ); assert( Gia_ManPi(p->pGia, 0)->fPhase ); // marks are set - p->nProofIds = 0; // clear mappings from objects Ga2_ManShrinkAbs( p, 0, 1 ); // clear SAT variable numbers (begin with 1) @@ -797,7 +814,7 @@ void Ga2_ManRestart( Ga2_Man_t * p ) p->nSatVars = 1; // start abstraction vToAdd = Ga2_ManAbsDerive( p->pGia ); - Ga2_ManAddToAbs( p, vToAdd, -1 ); + Ga2_ManAddToAbs( p, vToAdd ); Vec_IntFree( vToAdd ); p->LimAbs = Vec_IntSize(p->vAbs) + 1; p->LimPpi = Vec_IntSize(p->vValues); @@ -820,6 +837,7 @@ void Ga2_ManRestart( Ga2_Man_t * p ) int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) { int fSimple = 1; + int Id = Gia_ObjId(p->pGia, pObj); unsigned uTruth; Gia_Obj_t * pLeaf; int nLeaves, * pLeaves; @@ -839,11 +857,11 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) return 0; } assert( pObj->fPhase ); + if ( Gia_ObjIsPi(p->pGia, pObj) || Ga2_ObjIsPpi(p, pObj) ) + return Ga2_ObjFindOrAddLit( p, pObj, f ); Lit = Ga2_ObjFindLit( p, pObj, f ); if ( Lit >= 0 ) return Lit; - if ( Gia_ObjIsPi(p->pGia, pObj) ) - return Ga2_ObjFindOrAddLit( p, pObj, f ); if ( Gia_ObjIsRo(p->pGia, pObj) ) { assert( f > 0 ); @@ -851,6 +869,7 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) Ga2_ObjAddLit( p, pObj, f, Lit ); return Lit; } + assert( Gia_ObjIsAnd(pObj) ); nLeaves = Ga2_ObjLeaveNum( p->pGia, pObj ); pLeaves = Ga2_ObjLeavePtr( p->pGia, pObj ); if ( fSimple ) @@ -864,7 +883,7 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) // create fanout literal Lit = Ga2_ObjFindOrAddLit( p, pObj, f ); // create clauses - Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), pLits, Lit, -1 ); + Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), pLits, Lit, Gia_ObjId(p->pGia, pObj) ); return Lit; } // collect fanin literals @@ -901,7 +920,7 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) // add new node Lit = Ga2_ObjFindOrAddLit(p, pObj, f); - Ga2_ManCnfAddDynamic( p, uTruth, Vec_IntArray(p->vLits), Lit, -1 ); + Ga2_ManCnfAddDynamic( p, uTruth, Vec_IntArray(p->vLits), Lit, Gia_ObjId(p->pGia, pObj) ); } Ga2_ObjAddLit( p, pObj, f, Lit ); return Lit; @@ -956,6 +975,7 @@ void Ga2_GlaPrepareCexAndMap( Ga2_Man_t * p, Abc_Cex_t ** ppCex, Vec_Int_t ** pv vMap = Vec_IntAlloc( 1000 ); Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i ) { + if ( !i ) continue; if ( Ga2_ObjIsAbs(p, pObj) ) continue; assert( Ga2_ObjIsPpi(p, pObj) ); @@ -1018,6 +1038,66 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p ) /**Function************************************************************* + Synopsis [Creates a new manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ga2_GlaAbsCount( Ga2_Man_t * p, int fRo, int fAnd ) +{ + Gia_Obj_t * pObj; + int i, Counter = 0; + if ( fRo ) + Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i ) + Counter += Gia_ObjIsRo(p->pGia, pObj); + else if ( fAnd ) + Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i ) + Counter += Gia_ObjIsAnd(pObj); + else assert( 0 ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ga2_ManAbsPrintFrame( Ga2_Man_t * p, int nFrames, int nConfls, int nCexes, clock_t Time, int fFinal ) +{ + if ( Abc_FrameIsBatchMode() && !fFinal ) + return; + Abc_Print( 1, "%4d :", nFrames ); + Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * Vec_IntSize(p->vAbs) / p->nMarked) ); + Abc_Print( 1, "%6d", Vec_IntSize(p->vAbs) ); + Abc_Print( 1, "%5d", Vec_IntSize(p->vValues)-Vec_IntSize(p->vAbs)-1 ); + Abc_Print( 1, "%5d", Ga2_GlaAbsCount(p, 1, 0) ); + Abc_Print( 1, "%6d", Ga2_GlaAbsCount(p, 0, 1) ); + Abc_Print( 1, "%8d", nConfls ); + if ( nCexes == 0 ) + Abc_Print( 1, "%5c", '-' ); + else + Abc_Print( 1, "%5d", nCexes ); + Abc_PrintInt( sat_solver2_nvars(p->pSat) ); + Abc_PrintInt( sat_solver2_nclauses(p->pSat) ); + Abc_PrintInt( sat_solver2_nlearnts(p->pSat) ); + Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC ); + Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) ); + Abc_Print( 1, "%s", fFinal ? "\n" : "\r" ); + fflush( stdout ); +} + +/**Function************************************************************* + Synopsis [Performs gate-level abstraction.] Description [] @@ -1031,13 +1111,11 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) { Ga2_Man_t * p; Vec_Int_t * vCore, * vPPis; - clock_t clk = clock(); + clock_t clk2, clk = clock(); int nAbs, nValues, Status, RetValue = -1; int i, c, f, Lit; - // start the manager - p = Ga2_ManStart( pAig, pPars ); // check trivial case - assert( Gia_ManPoNum(pAig) == 1 ); + assert( Gia_ManPoNum(pAig) == 1 ); ABC_FREE( pAig->pCexSeq ); if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) ) { @@ -1068,7 +1146,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) 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" ); + Abc_Print( 1, " Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" ); } // iterate unrolling for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ ) @@ -1081,6 +1159,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) // unroll the circuit for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ ) { + int nConflsBeg = sat_solver2_nconflicts(p->pSat); p->pPars->iFrame = f; // add static clauses to this timeframe Ga2_ManAddAbsClauses( p, f ); @@ -1090,35 +1169,62 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) for ( c = 0; ; c++ ) { // perform SAT solving - clk = clock(); + clk2 = clock(); Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( Status == l_True ) // perform refinement { - p->timeSat += clock() - clk; - clk = clock(); + p->timeSat += clock() - clk2; + + clk2 = clock(); vPPis = Ga2_ManRefine( p ); - p->timeCex += clock() - clk; + p->timeCex += clock() - clk2; if ( vPPis == NULL ) goto finish; - Ga2_ManAddToAbs( p, vPPis, p->nProofIds++ ); + + if ( c == 0 ) + { + // start incremental proof manager + assert( p->pSat->pPrf2 == 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) ); + } + + Ga2_ManAddToAbs( p, vPPis ); Vec_IntFree( vPPis ); + if ( pPars->fVerbose ) + Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 0 ); // verify if ( Vec_IntCheckUnique(p->vAbs) ) printf( "Vector has %d duplicated entries.\n", Vec_IntCheckUnique(p->vAbs) ); continue; } - p->timeUnsat += clock() - clk; - if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit ) // timeout - goto finish; + p->timeUnsat += clock() - clk2; if ( Status == l_Undef ) // ran out of resources goto finish; + if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit ) // timeout + goto finish; assert( RetValue == l_False ); + if ( c == 0 ) + break; + // reduce abstraction + Ga2_ManShrinkAbs( p, nAbs, nValues ); // derive UNSAT core vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat ); - Ga2_ManShrinkAbs( p, nAbs, nValues ); - Ga2_ManAddToAbs( p, vCore, -1 ); + Prf_ManStopP( &p->pSat->pPrf2 ); + // use UNSAT core + Ga2_ManAddToAbs( p, vCore ); Vec_IntFree( vCore ); - p->nProofIds = 0; // remember current limits nAbs = Vec_IntSize(p->vAbs); nValues = Vec_IntSize(p->vValues); @@ -1127,6 +1233,8 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) printf( "Vector has %d duplicated entries.\n", Vec_IntCheckUnique(p->vAbs) ); break; } + if ( pPars->fVerbose ) + Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 ); if ( c > 0 ) { Vec_IntFreeP( &pAig->vGateClasses ); @@ -1142,6 +1250,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) } } finish: + Prf_ManStopP( &p->pSat->pPrf2 ); // analize the results if ( pAig->pCexSeq == NULL ) { |