From d55ae1421c7ba4f8b4f936563041fe771454c73a Mon Sep 17 00:00:00 2001 From: xiran Date: Sun, 10 May 2026 12:21:02 -0700 Subject: [PATCH 1/2] New feature: Add incremental refinement to &scorr command --- src/base/abci/abc.c | 8 +- src/proof/cec/cec.h | 1 + src/proof/cec/cecCorr.c | 101 +++++- src/proof/cec/cecCorrIncr.c | 674 ++++++++++++++++++++++++++++++++++++ src/proof/cec/cecInt.h | 33 +- src/proof/cec/module.make | 1 + 6 files changed, 805 insertions(+), 13 deletions(-) create mode 100644 src/proof/cec/cecCorrIncr.c diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 7b760ceb18..682ca67a62 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -41167,7 +41167,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) Cec_ManCorSetDefaultParams( pPars ); pPars->nProcs = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSZpkrecqowvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSZpkrecqiowvh" ) ) != EOF ) { switch ( c ) { @@ -41266,6 +41266,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'q': pPars->fStopWhenGone ^= 1; break; + case 'i': + pPars->fIncremental ^= 1; + break; case 'o': fUseOld ^= 1; break; @@ -41339,7 +41342,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &scorr [-FCGXPSZ num] [-pkrecqowvh]\n" ); + Abc_Print( -2, "usage: &scorr [-FCGXPSZ num] [-pkrecqiowvh]\n" ); Abc_Print( -2, "\t performs signal correpondence computation\n" ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames ); @@ -41354,6 +41357,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -2, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" ); Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" ); Abc_Print( -2, "\t-q : toggle quitting when PO is not a constant candidate [default = %s]\n", pPars->fStopWhenGone? "yes": "no" ); + Abc_Print( -2, "\t-i : toggle incremental TFO-triggered re-proof in main loop [default = %s] by Xiran ZHao at University of Chinese Academy of Sciences\n", pPars->fIncremental? "yes": "no" ); Abc_Print( -2, "\t-o : toggle calling old engine [default = %s]\n", fUseOld? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing verbose info about equivalent flops [default = %s]\n", pPars->fVerboseFlops? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index e360bb99da..eed2cfaf93 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -167,6 +167,7 @@ struct Cec_ParCor_t_ // int fFirstStop; // stop on the first sat output int fUseSmartCnf; // use smart CNF computation int fStopWhenGone; // quit when PO is not a candidate constant + int fIncremental; // active-list/TFO-triggered reproof in main loop int fVerboseFlops; // verbose stats int fVeryVerbose; // verbose stats int fVerbose; // verbose stats diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c index be0b08ba57..d5a0918082 100644 --- a/src/proof/cec/cecCorr.c +++ b/src/proof/cec/cecCorr.c @@ -34,7 +34,10 @@ static inline int Cec_ParCorShouldStop( Cec_ParCor_t * pPars ) /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ); +// Shared with cecCorrIncr.c (declared in cecInt.h). +extern void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ); +extern int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -45,13 +48,13 @@ static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_ Synopsis [Computes the real value of the literal w/o spec reduction.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ) +int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ) { if ( Gia_ObjIsAnd(pObj) ) { @@ -792,7 +795,7 @@ int Cec_ManCountLits( Gia_Man_t * p ) ***********************************************************************/ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPrefs ) -{ +{ Cec_ParSim_t ParsSim, * pParsSim = &ParsSim; Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; Vec_Str_t * vStatus; @@ -801,6 +804,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr Cec_ManSim_t * pSim; Gia_Man_t * pSrm; int fChanges, RetValue, i; + Cec_IncrMgr_t * pBmcMgr = NULL; // prepare simulation manager Cec_ManSimSetDefaultParams( pParsSim ); pParsSim->nWords = pPars->nWords; @@ -813,20 +817,44 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr Cec_ManSatSetDefaultParams( pParsSat ); pParsSat->nBTLimit = pPars->nBTLimit; pParsSat->fVerbose = pPars->fVerbose; + if ( pPars->fIncremental ) + { + pBmcMgr = Cec_IncrMgrAlloc( pAig, pPars->nFrames + nPrefs ); + Cec_IncrMgrSnapshotClasses( pBmcMgr ); + } fChanges = 1; for ( i = 0; fChanges && (!pPars->nLimitMax || i < pPars->nLimitMax); i++ ) { + int * pTfoMask = NULL; + int nReprSeeds = 0, nTotalPairs = 0, nActivePairs = 0, fConverged = 0; if ( Cec_ParCorShouldStop( pPars ) ) break; abctime clkBmc = Abc_Clock(); fChanges = 0; - pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); + // BMC SRM is non-ring (Gia_ManCorrSpecReduceInit ignores fRings); + // the incremental mask filters on pReprs-derived endpoints only. + if ( pBmcMgr && i > 0 ) + { + pTfoMask = Cec_IncrMgrDecideMask( pBmcMgr, 0, &fConverged, + &nReprSeeds, NULL, &nTotalPairs, &nActivePairs ); + if ( fConverged ) + break; + } + if ( pTfoMask ) + pSrm = Gia_ManCorrSpecReduceInit_Active( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pTfoMask ); + else + pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); + if ( pTfoMask && pPars->fVeryVerbose ) + Abc_Print( 1, " [bmc-incr i=%d repr=%d active=%d/%d POs=%d]\n", + i, nReprSeeds, nActivePairs, nTotalPairs, Gia_ManCoNum(pSrm) ); + if ( pBmcMgr ) + Cec_IncrMgrSnapshotClasses( pBmcMgr ); if ( Gia_ManPoNum(pSrm) == 0 ) { Gia_ManStop( pSrm ); Vec_IntFree( vOutputs ); break; - } + } pParsSat->nBTLimit *= 10; if ( pPars->fUseCSat ) vCexStore = Tas_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); @@ -849,6 +877,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr if ( Cec_ParCorShouldStop( pPars ) ) break; } + Cec_IncrMgrFree( pBmcMgr ); Cec_ManSimStop( pSim ); } @@ -949,6 +978,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) abctime clkTotal = Abc_Clock(); abctime clkSat = 0, clkSim = 0, clkSrm = 0; abctime clk2, clk = Abc_Clock(); + Cec_IncrMgr_t * pMgr = NULL; // incremental manager (NULL when -i is off) + abctime clkIncr = 0; + int nIncrSkipped = 0, nIncrFallback = 0; if ( Gia_ManRegNum(pAig) == 0 ) { Abc_Print( 1, "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" ); @@ -999,25 +1031,65 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) Cec_ManSimStop( pSim ); return 1; } + if ( pPars->fIncremental ) + { + pMgr = Cec_IncrMgrAlloc( pAig, pPars->nFrames ); + Cec_IncrMgrSnapshotClasses( pMgr ); + } // perform refinement of equivalence classes for ( r = 0; r < nIterMax; r++ ) - { + { if ( Cec_ParCorShouldStop( pPars ) ) { Cec_ManSimStop( pSim ); + Cec_IncrMgrFree( pMgr ); return 1; } if ( pPars->nStepsMax == r ) { Cec_ManSimStop( pSim ); + Cec_IncrMgrFree( pMgr ); Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", r ); fflush( stdout ); return 1; } clk = Abc_Clock(); - // perform speculative reduction + // perform speculative reduction (with optional active-list filter) clk2 = Abc_Clock(); - pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); + { + int * pTfoMask = NULL; + int nReprSeeds = 0, nNextChanges = 0, nTotalPairs = 0, nActivePairs = 0; + int fConverged = 0; + if ( pMgr && r > 0 ) + { + abctime clkI = Abc_Clock(); + pTfoMask = Cec_IncrMgrDecideMask( pMgr, pPars->fUseRings, &fConverged, + &nReprSeeds, &nNextChanges, + &nTotalPairs, &nActivePairs ); + clkIncr += Abc_Clock() - clkI; + if ( fConverged ) + { + clkSrm += Abc_Clock() - clk2; + break; + } + if ( pTfoMask == NULL ) + nIncrFallback++; + else + nIncrSkipped += nTotalPairs - nActivePairs; + } + if ( pTfoMask ) + pSrm = Gia_ManCorrSpecReduce_Active( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings, pTfoMask, pMgr ); + else + pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); + if ( pTfoMask && pPars->fVeryVerbose ) + Abc_Print( 1, " [incr r=%d repr=%d next=%d tfo=%d active=%d/%d POs=%d]\n", + r, nReprSeeds, nNextChanges, Vec_IntSize(pMgr->vTfoNodes), + nActivePairs, nTotalPairs, Gia_ManCoNum(pSrm) ); + // Snapshot AFTER SRM build: the active builder still reads the + // previous pNexts to recognise newly-created ring edges. + if ( pMgr ) + Cec_IncrMgrSnapshotClasses( pMgr ); + } assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig) ); clkSrm += Abc_Clock() - clk2; if ( Gia_ManCoNum(pSrm) == 0 ) @@ -1058,6 +1130,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) if ( Cec_ParCorShouldStop( pPars ) ) { Cec_ManSimStop( pSim ); + Cec_IncrMgrFree( pMgr ); return 1; } // quit if const is no longer there @@ -1067,6 +1140,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) printf( "because the property output is no longer a candidate constant.\n" ); fflush( stdout ); Cec_ManSimStop( pSim ); + Cec_IncrMgrFree( pMgr ); return 0; } if ( pPars->nLimitMax ) @@ -1078,6 +1152,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) printf( "because refinement does not proceed quickly.\n" ); fflush( stdout ); Cec_ManSimStop( pSim ); + Cec_IncrMgrFree( pMgr ); ABC_FREE( pAig->pReprs ); ABC_FREE( pAig->pNexts ); return 0; @@ -1105,11 +1180,17 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) ABC_PRTP( "Sat ", clkSat, clkTotal ); ABC_PRTP( "Sim ", clkSim, clkTotal ); ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal ); + if ( pMgr ) + { + ABC_PRTP( "Incr ", clkIncr, clkTotal ); + Abc_Print( 1, "Incr: fallback rounds = %d, skipped candidate pairs = %d\n", nIncrFallback, nIncrSkipped ); + } Abc_PrintTime( 1, "TOTAL", clkTotal ); fflush( stdout ); } + Cec_IncrMgrFree( pMgr ); return 1; -} +} /**Function************************************************************* diff --git a/src/proof/cec/cecCorrIncr.c b/src/proof/cec/cecCorrIncr.c new file mode 100644 index 0000000000..fcc61c0b25 --- /dev/null +++ b/src/proof/cec/cecCorrIncr.c @@ -0,0 +1,674 @@ +/**CFile**************************************************************** + + FileName [cecCorrIncr.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinational equivalence checking.] + + Synopsis [Incremental active-list / TFO filter for &scorr.] + + Author [Xiran Zhao] + + Affiliation [University of Chinese Academy of Sciences] + + Date [Ver. 1.0. Started - May 2026.] + +***********************************************************************/ + +#include "cecInt.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates the incremental active-list manager.] + + Description [The manager owns one snapshot of pReprs/pNexts plus the + TFO bookkeeping arrays. pAig must outlive the manager; the manager + never duplicates the AIG, only references it. If the host AIG does + not yet carry a static fanout, this routine builds it and remembers + to tear it down on Free.] + + SideEffects [Builds static fanout on pAig if not already present.] + + SeeAlso [] + +***********************************************************************/ +Cec_IncrMgr_t * Cec_IncrMgrAlloc( Gia_Man_t * pAig, int nFrames ) +{ + Cec_IncrMgr_t * p = ABC_CALLOC( Cec_IncrMgr_t, 1 ); + p->pAig = pAig; + p->nFrames = nFrames; + p->nObjs = Gia_ManObjNum(pAig); + p->vReprPrev = Vec_IntStartFull( p->nObjs ); + p->vNextPrev = Vec_IntStart( p->nObjs ); + p->vSeeds = Vec_IntAlloc( 64 ); + p->vTfoNodes = Vec_IntAlloc( 1024 ); + p->pTfoMark = ABC_CALLOC( int, p->nObjs ); + p->vBfsCur = Vec_IntAlloc( 1024 ); + p->vBfsNext = Vec_IntAlloc( 1024 ); + if ( pAig->vFanout == NULL ) + { + Gia_ManStaticFanoutStart( pAig ); + p->fOwnsFanout = 1; + } + return p; +} + +/**Function************************************************************* + + Synopsis [Frees the incremental manager.] + + Description [Releases all internal vectors and the TFO mark array. + If the manager built the static fanout on Alloc, it is also torn + down here. Safe to call with a NULL pointer.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_IncrMgrFree( Cec_IncrMgr_t * p ) +{ + if ( p == NULL ) return; + if ( p->fOwnsFanout ) + Gia_ManStaticFanoutStop( p->pAig ); + Vec_IntFree( p->vReprPrev ); + Vec_IntFree( p->vNextPrev ); + Vec_IntFree( p->vSeeds ); + Vec_IntFree( p->vTfoNodes ); + Vec_IntFree( p->vBfsCur ); + Vec_IntFree( p->vBfsNext ); + ABC_FREE( p->pTfoMark ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Snapshots the current equivalence-class state.] + + Description [Copies the per-node pReprs and pNexts arrays into the + manager so the next iteration can diff against the class state whose + pairs were just emitted into the SRM. Should be called after SRM + construction and before SAT/sim refinement: the snapshot then reflects + exactly the pairs the SAT solver was asked to prove. O(N).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_IncrMgrSnapshotClasses( Cec_IncrMgr_t * p ) +{ + Gia_Man_t * pAig = p->pAig; + int i; + assert( pAig->pReprs != NULL ); + for ( i = 0; i < p->nObjs; i++ ) + { + Vec_IntWriteEntry( p->vReprPrev, i, Gia_ObjRepr(pAig, i) ); + Vec_IntWriteEntry( p->vNextPrev, i, pAig->pNexts ? Gia_ObjNext(pAig, i) : 0 ); + } +} + +/**Function************************************************************* + + Synopsis [Computes the seed set for the next TFO BFS.] + + Description [Returns the number of nodes whose representative changed + since the last snapshot; the seeds themselves are stored in vSeeds and + consumed by Cec_IncrMgrComputeTfo. Does not update the snapshot -- + the caller decides when to snapshot. pNexts changes are intentionally + excluded here: a ring-link rewrite is an edge-local event that creates + a new ring edge to reprove, not a new fanout cone, so it is handled by + Cec_IncrMgrRingEdgeChanged at SRM emission time.] + + SideEffects [] + + SeeAlso [Cec_IncrMgrComputeTfo Cec_IncrMgrRingEdgeChanged] + +***********************************************************************/ +int Cec_IncrMgrComputeSeeds( Cec_IncrMgr_t * p ) +{ + Gia_Man_t * pAig = p->pAig; + int i, reprNew, reprOld; + Vec_IntClear( p->vSeeds ); + for ( i = 1; i < p->nObjs; i++ ) + { + reprNew = Gia_ObjRepr( pAig, i ); + reprOld = Vec_IntEntry( p->vReprPrev, i ); + if ( reprNew != reprOld ) + Vec_IntPush( p->vSeeds, i ); + } + return Vec_IntSize( p->vSeeds ); +} + +/**Function************************************************************* + + Synopsis [Counts nodes whose ring-list successor changed.] + + Description [Used only for convergence and fallback decisions. These + nodes are NOT TFO seeds, because a pNexts-only change creates a new + ring edge (proved edge-locally by the active SRM builder) rather than + a new fanout cone to re-prove. Returns 0 when pNexts is unallocated, + i.e. when ring mode is off.] + + SideEffects [] + + SeeAlso [Cec_IncrMgrComputeSeeds] + +***********************************************************************/ +int Cec_IncrMgrCountNextChanges( Cec_IncrMgr_t * p ) +{ + Gia_Man_t * pAig = p->pAig; + int i, nChanges = 0; + if ( pAig->pNexts == NULL ) + return 0; + for ( i = 1; i < p->nObjs; i++ ) + nChanges += Gia_ObjNext( pAig, i ) != Vec_IntEntry( p->vNextPrev, i ); + return nChanges; +} + +/**Function************************************************************* + + Synopsis [Detects whether a ring edge is new since the last snapshot.] + + Description [Ring classes store list edges explicitly in pNexts, but + the SRM also proves the implicit closing edge tail -> head. For an + explicit edge, the edge is unchanged iff the predecessor's pNexts slot + still names the same successor. For the closing edge there is no + pNexts slot to compare, so we reconstruct whether the same tail/head + pair already existed in the previous snapshot: the tail must have been + pointing to the head (closing the ring) and the head must still have + been a class root. Returns 1 to mean "must be re-proved". Passing a + NULL manager or a non-ring AIG returns 0 (no edge work needed).] + + SideEffects [] + + SeeAlso [Cec_IncrMgrCountActivePairs] + +***********************************************************************/ +int Cec_IncrMgrRingEdgeChanged( Cec_IncrMgr_t * p, int iPrev, int iObj ) +{ + Gia_Man_t * pAig; + int iNextCur, iNextOld; + if ( p == NULL ) + return 0; + pAig = p->pAig; + if ( pAig->pNexts == NULL ) + return 0; + iNextCur = Gia_ObjNext( pAig, iPrev ); + iNextOld = Vec_IntEntry( p->vNextPrev, iPrev ); + if ( iNextCur == iObj ) + return iNextOld != iObj; + if ( iNextCur > 0 ) + return 1; // conservative: should not happen for callers below + // Closing edge: prove if the previous snapshot did not already contain + // exactly this tail/head pair as a ring's closing edge. + return iNextOld > 0 || + Vec_IntEntry( p->vReprPrev, iPrev ) != iObj || + Vec_IntEntry( p->vReprPrev, iObj ) != GIA_VOID || + Vec_IntEntry( p->vNextPrev, iObj ) <= 0; +} + +/**Function************************************************************* + + Synopsis [Counts total and active candidate pairs before SRM build.] + + Description [Mirrors the PO-emission loops in the active SRM builders + but stops before constructing the unrolled network: it walks every + candidate pair the SRM would emit and tallies how many would survive + the active filter (pTfoMark plus the ring-edge override). The count + is approximate because SRM construction can still simplify a pair + away after the literal it represents collapses; it is used only to + decide whether the active filter saves enough work to be worth the + bookkeeping (the main loop falls back to the full SRM above ~70% + active pairs). When pTfoMark is NULL every pair is counted active.] + + SideEffects [] + + SeeAlso [Gia_ManCorrSpecReduce_Active] + +***********************************************************************/ +void Cec_IncrMgrCountActivePairs( Cec_IncrMgr_t * p, int fRings, int * pTfoMark, + int * pnTotal, int * pnActive ) +{ + Gia_Man_t * pAig = p->pAig; + Gia_Obj_t * pObj, * pRepr; + int i, iPrev, iObj; + *pnTotal = *pnActive = 0; + assert( pAig->pReprs != NULL ); + if ( fRings ) + { + Gia_ManForEachObj1( pAig, pObj, i ) + { + if ( Gia_ObjIsConst( pAig, i ) ) + { + (*pnTotal)++; + (*pnActive) += pTfoMark == NULL || pTfoMark[i]; + } + else if ( Gia_ObjIsHead( pAig, i ) ) + { + iPrev = i; + Gia_ClassForEachObj1( pAig, i, iObj ) + { + (*pnTotal)++; + (*pnActive) += pTfoMark == NULL || pTfoMark[iPrev] || pTfoMark[iObj] || + Cec_IncrMgrRingEdgeChanged( p, iPrev, iObj ); + iPrev = iObj; + } + iObj = i; // closing edge tail -> head + (*pnTotal)++; + (*pnActive) += pTfoMark == NULL || pTfoMark[iPrev] || pTfoMark[iObj] || + Cec_IncrMgrRingEdgeChanged( p, iPrev, iObj ); + } + } + } + else + { + Gia_ManForEachObj1( pAig, pObj, i ) + { + int idR; + pRepr = Gia_ObjReprObj( pAig, Gia_ObjId(pAig,pObj) ); + if ( pRepr == NULL ) + continue; + idR = Gia_ObjId( pAig, pRepr ); + (*pnTotal)++; + (*pnActive) += pTfoMark == NULL || pTfoMark[i] || pTfoMark[idR]; + } + } +} + +/**Function************************************************************* + + Synopsis [Forward TFO BFS from seeds across nFrames unrollings.] + + Description [Marks pTfoMark[id]=1 for every AIG node reachable from + any seed within nFrames combinational+sequential steps. Each frame + performs a combinational fanout BFS; RI fanouts cross to the next + frame by following Gia_ObjRiToRo to the corresponding register output. + After nFrames cross-frame jumps the search stops, since pairs deeper + than that cannot depend on the seeds within an nFrames-deep SRM. + + RI nodes themselves are intentionally not marked: SRM emission is + keyed on AIG candidate nodes (ANDs and CIs) and never on COs, so + marking RIs would only inflate the active set without enabling any + additional pair. + + Mark clearing is amortised: vTfoNodes records every id touched in + the previous round and is iterated to zero only those entries, so + the routine never sweeps the full N-sized array. Cost per call is + O(|TFO_k| * avg_fanout).] + + SideEffects [] + + SeeAlso [Cec_IncrMgrComputeSeeds] + +***********************************************************************/ +void Cec_IncrMgrComputeTfo( Cec_IncrMgr_t * p ) +{ + Gia_Man_t * pAig = p->pAig; + int * pMark = p->pTfoMark; + int f, i, k, Id, FanId, RoId; + + Vec_IntForEachEntry( p->vTfoNodes, Id, i ) + pMark[Id] = 0; + Vec_IntClear( p->vTfoNodes ); + Vec_IntClear( p->vBfsCur ); + Vec_IntClear( p->vBfsNext ); + + Vec_IntForEachEntry( p->vSeeds, Id, i ) + { + if ( !pMark[Id] ) + { + pMark[Id] = 1; + Vec_IntPush( p->vTfoNodes, Id ); + Vec_IntPush( p->vBfsCur, Id ); + } + } + + for ( f = 0; f <= p->nFrames; f++ ) + { + int head = 0; + while ( head < Vec_IntSize(p->vBfsCur) ) + { + Gia_Obj_t * pFan; + Id = Vec_IntEntry( p->vBfsCur, head++ ); + int nFan = Gia_ObjFanoutNumId( pAig, Id ); + for ( k = 0; k < nFan; k++ ) + { + FanId = Gia_ObjFanoutId( pAig, Id, k ); + pFan = Gia_ManObj( pAig, FanId ); + if ( Gia_ObjIsRi(pAig, pFan) ) + { + if ( f < p->nFrames ) + { + RoId = Gia_ObjRiToRoId( pAig, FanId ); + if ( !pMark[RoId] ) + { + pMark[RoId] = 1; + Vec_IntPush( p->vTfoNodes, RoId ); + Vec_IntPush( p->vBfsNext, RoId ); + } + } + } + else if ( Gia_ObjIsCo(pFan) ) + { + // PO: not a candidate, skip + } + else + { + if ( !pMark[FanId] ) + { + pMark[FanId] = 1; + Vec_IntPush( p->vTfoNodes, FanId ); + Vec_IntPush( p->vBfsCur, FanId ); + } + } + } + } + Vec_IntClear( p->vBfsCur ); + Vec_IntAppend( p->vBfsCur, p->vBfsNext ); + Vec_IntClear( p->vBfsNext ); + if ( Vec_IntSize(p->vBfsCur) == 0 ) + break; + } +} + +/**Function************************************************************* + + Synopsis [Active-filter variant of Gia_ManCorrSpecReduce.] + + Description [Identical to Gia_ManCorrSpecReduce in its SRM topology + and speculative reduction; the only difference is the PO emission + filter. A candidate pair (a, b) is emitted iff pTfoMark[a] is set + or pTfoMark[b] is set, i.e. at least one endpoint lies in the TFO of + a recently-changed representative. In ring mode, a ring edge that is + new or rewired since the last snapshot (Cec_IncrMgrRingEdgeChanged) + is also emitted even if neither endpoint is in the TFO -- the edge + has no prior UNSAT result to reuse and must be reproved on its own. + + Walking the full ring is required (rather than skipping unmarked + members) so iPrev stays aligned with the live class order; the active + filter only suppresses the resulting PO when the edge is provably + not new and neither endpoint is reachable from a seed. Passing + pTfoMark == NULL falls back to the unfiltered baseline behaviour.] + + SideEffects [] + + SeeAlso [Gia_ManCorrSpecReduce] + +***********************************************************************/ +Gia_Man_t * Gia_ManCorrSpecReduce_Active( Gia_Man_t * p, int nFrames, int fScorr, + Vec_Int_t ** pvOutputs, int fRings, + int * pTfoMark, Cec_IncrMgr_t * pIncr ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pRepr; + Vec_Int_t * vXorLits; + int f, i, iPrev, iObj, iPrevNew, iObjNew; + assert( nFrames > 0 ); + assert( Gia_ManRegNum(p) > 0 ); + assert( p->pReprs != NULL ); + Vec_IntFill( &p->vCopies, (nFrames+fScorr)*Gia_ManObjNum(p), -1 ); + Gia_ManSetPhase( p ); + pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManHashAlloc( pNew ); + Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 ); + Gia_ManForEachRo( p, pObj, i ) + Gia_ObjSetCopyF( p, 0, pObj, Gia_ManAppendCi(pNew) ); + Gia_ManForEachRo( p, pObj, i ) + if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) + Gia_ObjSetCopyF( p, 0, pObj, Gia_ObjCopyF(p, 0, pRepr) ); + for ( f = 0; f < nFrames+fScorr; f++ ) + { + Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 ); + Gia_ManForEachPi( p, pObj, i ) + Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) ); + } + *pvOutputs = Vec_IntAlloc( 1000 ); + vXorLits = Vec_IntAlloc( 1000 ); + if ( fRings ) + { + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsConst( p, i ) ) + { + if ( pTfoMark && !pTfoMark[i] ) + continue; + iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 ); + iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ); + if ( iObjNew != 0 ) + { + Vec_IntPush( *pvOutputs, 0 ); + Vec_IntPush( *pvOutputs, i ); + Vec_IntPush( vXorLits, iObjNew ); + } + } + else if ( Gia_ObjIsHead( p, i ) ) + { + // Walk every ring edge so iPrev stays aligned with the class + // order; emit only when an endpoint is in TFO or the edge is + // new/rewired since the last snapshot. + iPrev = i; + Gia_ClassForEachObj1( p, i, iObj ) + { + int fEmit = (pTfoMark == NULL) || pTfoMark[iPrev] || pTfoMark[iObj] || + Cec_IncrMgrRingEdgeChanged( pIncr, iPrev, iObj ); + if ( fEmit ) + { + iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); + iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); + iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); + iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); + if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) + { + Vec_IntPush( *pvOutputs, iPrev ); + Vec_IntPush( *pvOutputs, iObj ); + Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) ); + } + } + iPrev = iObj; + } + // Closing edge tail -> head + iObj = i; + { + int fEmit = (pTfoMark == NULL) || pTfoMark[iPrev] || pTfoMark[iObj] || + Cec_IncrMgrRingEdgeChanged( pIncr, iPrev, iObj ); + if ( fEmit ) + { + iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); + iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); + iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); + iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); + if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) + { + Vec_IntPush( *pvOutputs, iPrev ); + Vec_IntPush( *pvOutputs, iObj ); + Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) ); + } + } + } + } + } + } + else + { + Gia_ManForEachObj1( p, pObj, i ) + { + pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); + if ( pRepr == NULL ) + continue; + if ( pTfoMark ) + { + int idR = Gia_ObjId(p, pRepr); + if ( !pTfoMark[i] && !pTfoMark[idR] ) + continue; + } + iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 ); + iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 ); + iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); + if ( iPrevNew != iObjNew ) + { + Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) ); + Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) ); + Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) ); + } + } + } + Vec_IntForEachEntry( vXorLits, iObjNew, i ) + Gia_ManAppendCo( pNew, iObjNew ); + Vec_IntFree( vXorLits ); + Gia_ManHashStop( pNew ); + Vec_IntErase( &p->vCopies ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Active-filter variant of Gia_ManCorrSpecReduceInit (BMC SRM).] + + Description [Mirrors Gia_ManCorrSpecReduceInit but emits a candidate + PO (pRepr, pObj) only when at least one of the two endpoints lies in + pTfoMark. The baseline BMC SRM accepts an fRings flag for symmetry + with the inductive builder but never inspects it -- its topology is + always (head, member) pairs derived from pReprs alone, with no ring + edges to close. Therefore this active variant only needs pReprs- + driven seeds: pNexts changes cannot affect this SRM and there is no + closing edge to reprove. Passing pTfoMark == NULL falls back to the + unfiltered baseline behaviour.] + + SideEffects [] + + SeeAlso [Gia_ManCorrSpecReduceInit] + +***********************************************************************/ +Gia_Man_t * Gia_ManCorrSpecReduceInit_Active( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr, + Vec_Int_t ** pvOutputs, int * pTfoMark ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pRepr; + Vec_Int_t * vXorLits; + int f, i, iPrevNew, iObjNew; + assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix ); + assert( Gia_ManRegNum(p) > 0 ); + assert( p->pReprs != NULL ); + Vec_IntFill( &p->vCopies, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p), -1 ); + Gia_ManSetPhase( p ); + pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManHashAlloc( pNew ); + Gia_ManForEachRo( p, pObj, i ) + { + Gia_ManAppendCi(pNew); + Gia_ObjSetCopyF( p, 0, pObj, 0 ); + } + for ( f = 0; f < nFrames+nPrefix+fScorr; f++ ) + { + Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 ); + Gia_ManForEachPi( p, pObj, i ) + Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) ); + } + *pvOutputs = Vec_IntAlloc( 1000 ); + vXorLits = Vec_IntAlloc( 1000 ); + for ( f = nPrefix; f < nFrames+nPrefix; f++ ) + { + Gia_ManForEachObj1( p, pObj, i ) + { + pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); + if ( pRepr == NULL ) + continue; + if ( pTfoMark ) + { + int idR = Gia_ObjId(p, pRepr); + if ( !pTfoMark[i] && !pTfoMark[idR] ) + continue; + } + iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f, nPrefix ); + iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix ); + iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); + if ( iPrevNew != iObjNew ) + { + Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) ); + Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) ); + Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) ); + } + } + } + Vec_IntForEachEntry( vXorLits, iObjNew, i ) + Gia_ManAppendCo( pNew, iObjNew ); + Vec_IntFree( vXorLits ); + Gia_ManHashStop( pNew ); + Vec_IntErase( &p->vCopies ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [One-shot incremental decision for the refinement loop.] + + Description [Computes seeds, runs the TFO BFS, counts active candidate + pairs, and applies the fallback heuristic. Returns the TFO mask to + pass to the active SRM builder, or NULL when either (a) classes have + converged since the last snapshot (in which case *pfConverged is set + to 1 and the caller should break the refinement loop), or (b) the + active-pair ratio is high enough that the full SRM is cheaper. The + out parameters pnReprSeeds / pnNextChanges / pnTotalPairs / + pnActivePairs are filled when non-NULL and are useful for verbose + printing and progress counters. fUseRings tells the helper whether + to track pNexts changes; the BMC SRM is non-ring and passes 0.] + + SideEffects [] + + SeeAlso [Cec_IncrMgrComputeSeeds Cec_IncrMgrComputeTfo + Cec_IncrMgrCountActivePairs] + +***********************************************************************/ +int * Cec_IncrMgrDecideMask( Cec_IncrMgr_t * p, int fUseRings, int * pfConverged, + int * pnReprSeeds, int * pnNextChanges, + int * pnTotalPairs, int * pnActivePairs ) +{ + int nReprSeeds, nNextChanges = 0, nTotalPairs = 0, nActivePairs = 0; + *pfConverged = 0; + nReprSeeds = Cec_IncrMgrComputeSeeds( p ); + if ( fUseRings ) + nNextChanges = Cec_IncrMgrCountNextChanges( p ); + if ( pnReprSeeds ) *pnReprSeeds = nReprSeeds; + if ( pnNextChanges ) *pnNextChanges = nNextChanges; + if ( nReprSeeds == 0 && nNextChanges == 0 ) + { + *pfConverged = 1; + return NULL; + } + Cec_IncrMgrComputeTfo( p ); + Cec_IncrMgrCountActivePairs( p, fUseRings, p->pTfoMark, &nTotalPairs, &nActivePairs ); + if ( pnTotalPairs ) *pnTotalPairs = nTotalPairs; + if ( pnActivePairs ) *pnActivePairs = nActivePairs; + if ( nActivePairs == 0 ) + { + *pfConverged = 1; + return NULL; + } + // Above ~70% active pairs, the mask plus emission filter costs more + // than just rebuilding the full SRM. Return NULL to signal fallback. + if ( nTotalPairs > 0 && (ABC_INT64_T)10 * nActivePairs > (ABC_INT64_T)7 * nTotalPairs ) + return NULL; + return p->pTfoMark; +} + +ABC_NAMESPACE_IMPL_END + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// diff --git a/src/proof/cec/cecInt.h b/src/proof/cec/cecInt.h index f78e5f25ff..f732565672 100644 --- a/src/proof/cec/cecInt.h +++ b/src/proof/cec/cecInt.h @@ -149,7 +149,7 @@ struct Cec_ManFra_t_ { // parameters Gia_Man_t * pAig; // the AIG to be used for simulation - Cec_ParFra_t * pPars; // SAT sweeping parameters + Cec_ParFra_t * pPars; // SAT sweeping parameters // simulation patterns Vec_Int_t * vXorNodes; // nodes used in speculative reduction int nAllProved; // total number of proved nodes @@ -165,6 +165,23 @@ struct Cec_ManFra_t_ abctime timeTotal; // total runtime }; +// incremental active-list manager for &scorr -i +typedef struct Cec_IncrMgr_t_ Cec_IncrMgr_t; +struct Cec_IncrMgr_t_ +{ + Gia_Man_t * pAig; // host AIG (immutable across iterations) + int nFrames; // unrolling depth used by the SRM builder + int nObjs; // cached Gia_ManObjNum(pAig) + Vec_Int_t * vReprPrev; // snapshot of pReprs from previous round + Vec_Int_t * vNextPrev; // snapshot of pNexts from previous round + Vec_Int_t * vSeeds; // nodes whose pReprs changed since snapshot + Vec_Int_t * vTfoNodes; // ids currently in TFO (for fast clearing) + int * pTfoMark; // dense mark array, size = nObjs + Vec_Int_t * vBfsCur; // BFS frontier for current frame + Vec_Int_t * vBfsNext; // BFS frontier carried to next frame + int fOwnsFanout; // 1 if we built static fanout (must free) +}; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -175,6 +192,20 @@ struct Cec_ManFra_t_ /*=== cecCorr.c ============================================================*/ extern void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, abctime Time ); +extern int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ); +extern void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ); +/*=== cecCorrIncr.c ============================================================*/ +extern Cec_IncrMgr_t * Cec_IncrMgrAlloc( Gia_Man_t * pAig, int nFrames ); +extern void Cec_IncrMgrFree( Cec_IncrMgr_t * p ); +extern void Cec_IncrMgrSnapshotClasses( Cec_IncrMgr_t * p ); +extern int Cec_IncrMgrComputeSeeds( Cec_IncrMgr_t * p ); +extern int Cec_IncrMgrCountNextChanges( Cec_IncrMgr_t * p ); +extern int Cec_IncrMgrRingEdgeChanged( Cec_IncrMgr_t * p, int iPrev, int iObj ); +extern void Cec_IncrMgrCountActivePairs( Cec_IncrMgr_t * p, int fRings, int * pTfoMark, int * pnTotal, int * pnActive ); +extern void Cec_IncrMgrComputeTfo( Cec_IncrMgr_t * p ); +extern Gia_Man_t * Gia_ManCorrSpecReduce_Active( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings, int * pTfoMark, Cec_IncrMgr_t * pIncr ); +extern Gia_Man_t * Gia_ManCorrSpecReduceInit_Active( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int * pTfoMark ); +extern int * Cec_IncrMgrDecideMask( Cec_IncrMgr_t * p, int fUseRings, int * pfConverged, int * pnReprSeeds, int * pnNextChanges, int * pnTotalPairs, int * pnActivePairs ); /*=== cecClass.c ============================================================*/ extern int Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i ); extern int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax ); diff --git a/src/proof/cec/module.make b/src/proof/cec/module.make index ed8deba98d..d9d921e2d2 100644 --- a/src/proof/cec/module.make +++ b/src/proof/cec/module.make @@ -3,6 +3,7 @@ SRC += src/proof/cec/cecCec.c \ src/proof/cec/cecClass.c \ src/proof/cec/cecCore.c \ src/proof/cec/cecCorr.c \ + src/proof/cec/cecCorrIncr.c \ src/proof/cec/cecIso.c \ src/proof/cec/cecMan.c \ src/proof/cec/cecPat.c \ From 97b15a29a067065bc6803739c2a4f0bf4a6879cb Mon Sep 17 00:00:00 2001 From: xiran Date: Mon, 11 May 2026 14:02:23 -0700 Subject: [PATCH 2/2] Fix: fix the build bug in abclib.dsp by registering cecCorrIncr.c --- abclib.dsp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/abclib.dsp b/abclib.dsp index f1d622d2b4..2f16e849ee 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -6681,6 +6681,10 @@ SOURCE=.\src\proof\cec\cecCorr.c # End Source File # Begin Source File +SOURCE=.\src\proof\cec\cecCorrIncr.c +# End Source File +# Begin Source File + SOURCE=.\src\proof\cec\cecInt.h # End Source File # Begin Source File