From 8982bf58cb8c801bdd6e204d73ac6ed36d98adaa Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 29 Jul 2012 22:31:00 -0700 Subject: Reducing memory usage in proof-based abstraction. --- src/aig/gia/giaAbsGla.c | 107 ++++++++++++++++++++++++++++++++++++----------- src/aig/gia/giaAbsGla2.c | 60 ++++++++++++++++---------- src/aig/gia/giaAbsVta.c | 17 ++++---- 3 files changed, 129 insertions(+), 55 deletions(-) (limited to 'src/aig/gia') diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 7654e44f..b8c13e38 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -74,6 +74,9 @@ struct Gla_Man_t_ 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 @@ -84,6 +87,8 @@ struct Gla_Man_t_ 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 @@ -1056,6 +1061,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars ) 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) ); @@ -1318,6 +1324,7 @@ void Gla_ManStop( Gla_Man_t * p ) 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 ); @@ -1567,15 +1574,29 @@ void Gia_GlaAddToCounters( Gla_Man_t * p, Vec_Int_t * vCore ) void Gia_GlaAddToAbs( Gla_Man_t * p, Vec_Int_t * vAbsAdd, int fCheck ) { Gla_Obj_t * pGla; - int i; + int i, Counter = 0; Gla_ManForEachObjAbsVec( vAbsAdd, p, pGla, i ) { - assert( !fCheck || pGla->fAbs == 0 ); + if ( fCheck ) + { + assert( pGla->fAbs == 0 ); + if ( p->pSat->pPrf2 ) + Vec_IntWriteEntry( p->vProofIds, Gla_ObjId(p, pGla), p->nProofIds++ ); + } if ( pGla->fAbs ) continue; + + if ( !fCheck ) + { + Counter++; +// printf( "%d ", Gla_ObjId(p, pGla) ); + } + pGla->fAbs = 1; Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) ); } +// if ( Counter ) +// printf( " Total = %d\n", Counter ); } void Gia_GlaAddTimeFrame( Gla_Man_t * p, int f ) { @@ -1635,7 +1656,7 @@ int Gla_ManGetOutLit( Gla_Man_t * p, int f ) } 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; + Vec_Int_t * vCore = NULL; int nConfPrev = pSat->stats.conflicts; int RetValue, iLit = Gla_ManGetOutLit( p, f ); clock_t clk = clock(); @@ -1675,6 +1696,8 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, sat_solver2 * pSat, int nCon // 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) ); @@ -1717,6 +1740,9 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl // Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 ); 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_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 ? "\n" : "\r" ); fflush( stdout ); } @@ -1740,13 +1766,13 @@ void Gla_ManReportMemory( Gla_Man_t * p ) 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 ); + 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 ); } @@ -1830,7 +1856,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) { extern int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ); Gla_Man_t * p; - Vec_Int_t * vCore, * vPPis; + Vec_Int_t * vPPis, * vCore;//, * vCore2 = NULL; Abc_Cex_t * pCex = NULL; int f, i, iPrev, nConfls, Status, nVarsOld, nCoreSize, fOneIsSent = 0, RetValue = -1; clock_t clk2, clk = clock(); @@ -1913,24 +1939,31 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) Vec_IntClear( p->vAddedNew ); p->nAbsOld = Vec_IntSize( p->vAbs ); nVarsOld = p->nSatVars; + p->nLrnOld = sat_solver2_nlearnts( p->pSat ); // iterate as long as there are counter-examples + p->nAbsNew = 0; + p->nLrnNew = 0; for ( i = 0; ; i++ ) { clk2 = clock(); vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls ); - assert( (vCore != NULL) == (Status == 1) ); +// assert( (vCore != NULL) == (Status == 1) ); if ( Status == -1 || (p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit) ) // resource limit is reached { + if ( p->pSat->pPrf2 ) + Prf_ManStopP( &p->pSat->pPrf2 ); if ( Gia_ManRegNum(p->pGia) > 1 ) // for comb cases, return the abstration Gla_ManRollBack( p ); goto finish; } - if ( vCore != NULL ) + if ( Status == 1 ) { + if ( p->pSat->pPrf2 ) + Prf_ManStopP( &p->pSat->pPrf2 ); p->timeUnsat += clock() - clk2; break; - } + } p->timeSat += clock() - clk2; assert( Status == 0 ); p->nCexes++; @@ -1954,17 +1987,37 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) vPPis = Gla_ManRefinement( p ); if ( vPPis == NULL ) { + if ( p->pSat->pPrf2 ) + Prf_ManStopP( &p->pSat->pPrf2 ); pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL; break; } } + assert( pCex == NULL ); + + // start proof logging + if ( i == 0 ) + { + 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, Vec_IntSize(p->vAbs) - p->nAbsOld + Vec_IntSize(vPPis) ); + } + Gia_GlaAddToAbs( p, vPPis, 1 ); Gia_GlaAddOneSlice( p, f, vPPis ); Vec_IntFree( vPPis ); - p->timeCex += clock() - clk2; - if ( pCex != NULL ) - goto finish; // 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 ); @@ -1972,24 +2025,30 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) if ( pCex != NULL ) break; assert( Status == 1 ); + // valid core is obtained - nCoreSize = Vec_IntSize( vCore ); - Gia_GlaAddToCounters( p, vCore ); + nCoreSize = 1; + if ( vCore ) + { + nCoreSize += Vec_IntSize( vCore ); + Gia_GlaAddToCounters( p, vCore ); + } if ( i == 0 ) { p->pPars->nFramesNoChange++; - Vec_IntFree( vCore ); + 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 - Vec_IntSort( vCore, 1 ); Gia_GlaAddToAbs( p, vCore, 0 ); Gia_GlaAddOneSlice( p, f, vCore ); Vec_IntFree( vCore ); @@ -1997,7 +2056,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) 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) ); +// assert( (vCore != NULL) == (Status == 1) ); Vec_IntFreeP( &vCore ); if ( Status == -1 ) // resource limit is reached break; @@ -2046,10 +2105,10 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) } finish: // analize the results - if ( p->pPars->fVerbose ) - printf( "\n" ); 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 ); diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index 7edacf3c..cf2dfb95 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -41,21 +41,22 @@ struct Ga2_Man_t_ Gia_Man_t * pGia; // working AIG manager Gia_ParVta_t * pPars; // parameters // markings - int nMarked; // total number of marked nodes and flops Vec_Ptr_t * vCnfs; // for each object: CNF0, CNF1 // abstraction - Vec_Int_t * vIds; // abstraction ID for each object + 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 SAT numbers assigned + 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) + int nProofIds; // the counter of proof IDs int LimAbs; // limit value for starting abstraction objects int LimPpi; // limit value for starting PPI objects + int nMarked; // total number of marked nodes and flops // refinement Rnm_Man_t * pRnm; // refinement manager // SAT solver and variables Vec_Ptr_t * vId2Lit; // mapping, for each timeframe, of object ID into SAT literal sat_solver2 * pSat; // incremental SAT solver int nSatVars; // the number of SAT variables - int nProofIds; // the counter of proof IDs // temporaries Vec_Int_t * vLits; Vec_Int_t * vIsopMem; @@ -356,7 +357,9 @@ 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 ); Vec_IntPush( p->vValues, -1 ); + Vec_IntPush( p->vProofIds, -1 ); // refinement p->pRnm = Rnm_ManStart( pGia ); // SAT solver and variables @@ -380,17 +383,18 @@ void Ga2_ManReportMemory( Ga2_Man_t * p ) memOth += Vec_IntMemory( p->vIds ); memOth += Vec_IntMemory( p->vAbs ); memOth += Vec_IntMemory( p->vValues ); + memOth += Vec_IntMemory( p->vProofIds ); memOth += Vec_IntMemory( p->vLits ); memOth += Vec_IntMemory( p->vIsopMem ); memOth += 336450 + (sizeof(char) + sizeof(char*)) * 65536; 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 ); + 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 ); } void Ga2_ManStop( Ga2_Man_t * p ) { @@ -404,6 +408,7 @@ void Ga2_ManStop( Ga2_Man_t * p ) Vec_VecFree( (Vec_Vec_t *)p->vId2Lit ); Vec_IntFree( p->vIds ); Vec_IntFree( p->vAbs ); + Vec_IntFree( p->vProofIds ); Vec_IntFree( p->vValues ); Vec_IntFree( p->vLits ); Vec_IntFree( p->vIsopMem ); @@ -610,17 +615,19 @@ 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 ) +void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs, int ProofId ) { 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 ); } @@ -629,14 +636,14 @@ void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs ) return; // compute parameters nLeaves = Ga2_ObjLeaveNum(p->pGia, pObj); - uTruth = Ga2_ObjTruth( 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) ); } -void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd ) +void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd, int ProofId ) { Vec_Int_t * vLeaves, * vMap; Gia_Obj_t * pObj, * pFanin; @@ -644,15 +651,16 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd ) // add abstraction objects Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i ) { - Ga2_ManSetupNode( p, pObj, 1 ); + Ga2_ManSetupNode( p, pObj, 1, ProofId ); Vec_IntPush( p->vAbs, Gia_ObjId(p->pGia, pObj) ); + Vec_IntPush( p->vProofIds, ProofId ); } // add PPI objects Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i ) { vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) - Ga2_ManSetupNode( p, pObj, 0 ); + Ga2_ManSetupNode( p, pObj, 0, -1 ); } // clean mapping in the timeframes Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i ) @@ -666,8 +674,12 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd ) 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, p->nProofIds + i ); + Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Vec_IntEntry(p->vProofIds, Ga2_ObjId(p, 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 ) @@ -679,11 +691,11 @@ void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f ) { if ( i < p->LimAbs ) continue; - iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f ); vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); Vec_IntClear( p->vLits ); 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 ); } } @@ -717,6 +729,7 @@ void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues ) 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 ) @@ -775,6 +788,7 @@ 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) @@ -783,11 +797,10 @@ void Ga2_ManRestart( Ga2_Man_t * p ) p->nSatVars = 1; // start abstraction vToAdd = Ga2_ManAbsDerive( p->pGia ); - Ga2_ManAddToAbs( p, vToAdd ); + Ga2_ManAddToAbs( p, vToAdd, -1 ); Vec_IntFree( vToAdd ); p->LimAbs = Vec_IntSize(p->vAbs) + 1; p->LimPpi = Vec_IntSize(p->vValues); - p->nProofIds = 0; // set runtime limit if ( p->pPars->nTimeOut ) sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + p->timeStart ); @@ -1069,7 +1082,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ ) { p->pPars->iFrame = f; - // add abstraction clauses + // add static clauses to this timeframe Ga2_ManAddAbsClauses( p, f ); // get the output literal Lit = Ga2_ManUnroll_rec( p, Gia_ManPo(pAig,0), f ); @@ -1087,7 +1100,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) p->timeCex += clock() - clk; if ( vPPis == NULL ) goto finish; - Ga2_ManAddToAbs( p, vPPis ); + Ga2_ManAddToAbs( p, vPPis, p->nProofIds++ ); Vec_IntFree( vPPis ); // verify if ( Vec_IntCheckUnique(p->vAbs) ) @@ -1103,8 +1116,9 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) // derive UNSAT core vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat ); Ga2_ManShrinkAbs( p, nAbs, nValues ); - Ga2_ManAddToAbs( p, vCore ); + Ga2_ManAddToAbs( p, vCore, -1 ); Vec_IntFree( vCore ); + p->nProofIds = 0; // remember current limits nAbs = Vec_IntSize(p->vAbs); nValues = Vec_IntSize(p->vValues); diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 69f40af5..31158e9d 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -1035,6 +1035,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) // other data p->vCores = Vec_PtrAlloc( 100 ); p->pSat = sat_solver2_new(); + 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; @@ -1499,12 +1500,12 @@ void Gia_VtaPrintMemory( Vta_Man_t * p ) memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCores ); memOth += Vec_IntCap(p->vAddedNew) * 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 ); + 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 ); } @@ -1694,10 +1695,10 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) } finish: // analize the results - if ( p->pPars->fVerbose ) - printf( "\n" ); if ( pCex == NULL ) { + if ( p->pPars->fVerbose && Status == -1 ) + printf( "\n" ); if ( Vec_PtrSize(p->vCores) == 0 ) Abc_Print( 1, "Abstraction is not produced because first frame is not solved. " ); else -- cgit v1.2.3