Skip to content

Add dynamic SRM and incremental simulation into &scorr -i ; Fix a bug of &scorr -i ; #529

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
alanminko merged 1 commit into from
Jul 2, 2026
Merged

Add dynamic SRM and incremental simulation into &scorr -i ; Fix a bug of &scorr -i ; #529

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions abclib.dsp
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 4 additions & 0 deletions src/aig/gia/gia.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1312,10 +1312,14 @@ extern void Cbs_ManStop( Cbs_Man_t * p );
extern int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj );
extern int Cbs_ManSolve2( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
extern Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int f0Proved, int fVerbose );
extern Vec_Int_t * Cbs_ManSolveMiterNcOutVals( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int f0Proved, int fVerbose, Vec_Int_t * vOutLits, Vec_Int_t ** pvOutVals );
extern void Cbs_ManSyncCore( Cbs_Man_t * p );
extern Vec_Int_t * Cbs_ManSolveRoots( Cbs_Man_t * p, Vec_Int_t * vRootLits, Vec_Str_t ** pvStatus, int fVerbose );
extern void Cbs_ManSetConflictNum( Cbs_Man_t * p, int Num );
extern Vec_Int_t * Cbs_ReadModel( Cbs_Man_t * p );
/*=== giaCTas.c ============================================================*/
extern Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
extern Vec_Int_t * Tas_ManSolveMiterNcOutVals( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose, Vec_Int_t * vOutLits, Vec_Int_t ** pvOutVals );
/*=== giaCof.c =============================================================*/
extern void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes );
extern Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar );
Expand Down
181 changes: 176 additions & 5 deletions src/aig/gia/giaCSat.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,13 +64,17 @@ struct Cbs_Man_t_
{
Cbs_Par_t Pars; // parameters
Gia_Man_t * pAig; // AIG manager
int nSyncedObjs; // pAig objects already prepped (Value/marks/refs) for resident reuse
Cbs_Que_t pProp; // propagation queue
Cbs_Que_t pJust; // justification queue
Cbs_Que_t pClauses; // clause queue
Gia_Obj_t ** pIter; // iterator through clause vars
Vec_Int_t * vLevReas; // levels and decisions
Vec_Int_t * vModel; // satisfying assignment
Vec_Ptr_t * vTemp; // temporary storage
Vec_Int_t * vOutLits; // optional endpoint literals to sample before cancel
Vec_Int_t * vOutVals; // optional endpoint values by output
int iOutVal; // current output whose endpoints are sampled
// SAT calls statistics
int nSatUnsat; // the number of proofs
int nSatSat; // the number of failure
Expand Down Expand Up @@ -256,6 +260,29 @@ static inline void Cbs_ManSaveModelAll( Cbs_Man_t * p, Vec_Int_t * vCex )
Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) );
}

static inline int Cbs_ManLitValue( Cbs_Man_t * p, int iLit )
{
Gia_Obj_t * pObj;
if ( iLit < 0 )
return -1;
if ( Abc_Lit2Var(iLit) == 0 )
return Abc_LitIsCompl(iLit);
pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(iLit) );
if ( !Cbs_VarIsAssigned(pObj) )
return -1;
return Cbs_VarValue(pObj) ^ Abc_LitIsCompl(iLit);
}

static inline void Cbs_ManSaveOutVals( Cbs_Man_t * p, Vec_Int_t * vOutLits, Vec_Int_t * vOutVals, int Out )
{
if ( vOutLits == NULL || vOutVals == NULL )
return;
if ( 2*Out + 1 >= Vec_IntSize(vOutLits) )
return;
Vec_IntWriteEntry( vOutVals, 2*Out, Cbs_ManLitValue( p, Vec_IntEntry(vOutLits, 2*Out) ) );
Vec_IntWriteEntry( vOutVals, 2*Out + 1, Cbs_ManLitValue( p, Vec_IntEntry(vOutLits, 2*Out + 1) ) );
}

/**Function*************************************************************

Synopsis []
Expand Down Expand Up @@ -954,7 +981,10 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
Cbs_ManAssign( p, pObj, 0, NULL, NULL );
if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) )
{
Cbs_ManSaveModel( p, p->vModel );
Cbs_ManSaveOutVals( p, p->vOutLits, p->vOutVals, p->iOutVal );
}
else
RetValue = 1;
Cbs_ManCancelUntil( p, 0 );
Expand Down Expand Up @@ -1034,14 +1064,14 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p )
SeeAlso []

***********************************************************************/
Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int f0Proved, int fVerbose )
Vec_Int_t * Cbs_ManSolveMiterNcOutVals( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int f0Proved, int fVerbose, Vec_Int_t * vOutLits, Vec_Int_t ** pvOutVals )
{
extern void Gia_ManCollectTest( Gia_Man_t * pAig );
extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
Cbs_Man_t * p;
Vec_Int_t * vCex, * vVisit, * vCexStore;
Cbs_Man_t * p;
Vec_Int_t * vCex, * vVisit, * vCexStore, * vOutVals = NULL;
Vec_Str_t * vStatus;
Gia_Obj_t * pRoot;
Gia_Obj_t * pRoot;
int i, status;
abctime clk, clkTotal = Abc_Clock();
assert( Gia_ManRegNum(pAig) == 0 );
Expand All @@ -1058,6 +1088,12 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
// create resulting data-structures
vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
vCexStore = Vec_IntAlloc( 10000 );
if ( pvOutVals )
{
*pvOutVals = NULL;
if ( vOutLits )
vOutVals = Vec_IntStartFull( 2 * Gia_ManPoNum(pAig) );
}
vVisit = Vec_IntAlloc( 100 );
vCex = Cbs_ReadModel( p );
// solve for each output
Expand All @@ -1084,7 +1120,13 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
clk = Abc_Clock();
p->Pars.fUseHighest = 1;
p->Pars.fUseLowest = 0;
p->vOutLits = vOutLits;
p->vOutVals = vOutVals;
p->iOutVal = i;
status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
p->vOutLits = NULL;
p->vOutVals = NULL;
p->iOutVal = -1;
// printf( "\n" );
/*
if ( status == -1 )
Expand Down Expand Up @@ -1126,18 +1168,147 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
// printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );
Cbs_ManStop( p );
*pvStatus = vStatus;
if ( pvOutVals )
*pvOutVals = vOutVals;
else
Vec_IntFreeP( &vOutVals );

// printf( "Total number of cex literals = %d. (Ave = %d)\n",
// Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat,
// (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat );
return vCexStore;
}

Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int f0Proved, int fVerbose )
{
return Cbs_ManSolveMiterNcOutVals( pAig, nConfs, pvStatus, f0Proved, fVerbose, NULL, NULL );
}

/**Function*************************************************************

Synopsis [Incrementally prepares newly appended objects of a persistent AIG.]

Description [The pAig of a resident manager is append-only across solve calls.
Cbs needs every unassigned object to carry Value=~0 and clean marks, and reads
Gia_ObjRefNum during branching. After a clean solve Cbs restores Value/marks
of the nodes it touched, and freshly appended nodes are zero-initialized, so we
only have to prep the suffix [nSyncedObjs, ObjNum): set Value=~0, clear marks,
grow pRefs and bump each new AND's fanin refs (= the global fanout counts that
Gia_ManCreateRefs would produce, computed incrementally). This replaces the
per-round O(|pAig|) refs/marks/value rebuild with O(newly appended).]

SideEffects [Allocates/grows pAig->pRefs (freed by Gia_ManStop).]

SeeAlso []

***********************************************************************/
void Cbs_ManSyncCore( Cbs_Man_t * p )
{
Gia_Man_t * pAig = p->pAig;
Gia_Obj_t * pObj;
int i, nObjs = Gia_ManObjNum( pAig );
assert( p->nSyncedObjs <= nObjs );
if ( p->nSyncedObjs == nObjs )
return;
pAig->pRefs = ABC_REALLOC( int, pAig->pRefs, nObjs );
memset( pAig->pRefs + p->nSyncedObjs, 0, sizeof(int) * (nObjs - p->nSyncedObjs) );
for ( i = p->nSyncedObjs; i < nObjs; i++ )
{
pObj = Gia_ManObj( pAig, i );
pObj->fMark0 = pObj->fMark1 = 0;
pObj->Value = ~0;
if ( Gia_ObjIsAnd(pObj) )
{
pAig->pRefs[Gia_ObjFaninId0(pObj, i)]++;
pAig->pRefs[Gia_ObjFaninId1(pObj, i)]++;
}
}
p->nSyncedObjs = nObjs;
}

/**Function*************************************************************

Synopsis [Solves a set of root literals directly on a persistent AIG.]

Description [Same prover as Cbs_ManSolveMiterNc, but each problem is a root
literal of p->pAig (no CO needed) instead of a CO of a freshly built view, and
the manager is resident: it is allocated once on the persistent COless pCore
and reused across rounds, only Cbs_ManSyncCore-ing the objects appended since
the last call - so neither the throwaway view (alloc + copy-all-CIs + cone
copy) nor the per-round whole-AIG prep is paid. Output index i corresponds to
vRootLits[i]; vCexStore / vStatus format matches Cbs_ManSolveMiterNc. CEX is
saved by CioId, which on pCore equals the view's CI numbering.]

SideEffects [Prepares newly appended objects via Cbs_ManSyncCore.]

SeeAlso []

***********************************************************************/
Vec_Int_t * Cbs_ManSolveRoots( Cbs_Man_t * p, Vec_Int_t * vRootLits, Vec_Str_t ** pvStatus, int fVerbose )
{
extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
Gia_Man_t * pAig = p->pAig;
Vec_Int_t * vCex, * vCexStore;
Vec_Str_t * vStatus;
int i, iLit, status;
abctime clk, clkTotal = Abc_Clock();
assert( Gia_ManRegNum(pAig) == 0 );
Cbs_ManSyncCore( p ); // prep only objects appended since the last solve
vStatus = Vec_StrAlloc( Vec_IntSize(vRootLits) );
vCexStore = Vec_IntAlloc( 10000 );
vCex = Cbs_ReadModel( p );
Vec_IntForEachEntry( vRootLits, iLit, i )
{
Vec_IntClear( vCex );
if ( Abc_Lit2Var(iLit) == 0 ) // structural constant root
{
if ( Abc_LitIsCompl(iLit) ) // const 1: trivial counter-example
{
Cec_ManSatAddToStore( vCexStore, vCex, i );
Vec_StrPush( vStatus, 0 );
}
else // const 0: proved
Vec_StrPush( vStatus, 1 );
continue;
}
clk = Abc_Clock();
p->Pars.fUseHighest = 1;
p->Pars.fUseLowest = 0;
status = Cbs_ManSolve( p, Gia_ObjFromLit(pAig, iLit) );
Vec_StrPush( vStatus, (char)status );
if ( status == -1 )
{
p->nSatUndec++;
p->nConfUndec += p->Pars.nBTThis;
Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
p->timeSatUndec += Abc_Clock() - clk;
continue;
}
if ( status == 1 )
{
p->nSatUnsat++;
p->nConfUnsat += p->Pars.nBTThis;
p->timeSatUnsat += Abc_Clock() - clk;
continue;
}
p->nSatSat++;
p->nConfSat += p->Pars.nBTThis;
Cec_ManSatAddToStore( vCexStore, vCex, i );
p->timeSatSat += Abc_Clock() - clk;
}
p->nSatTotal = Vec_IntSize( vRootLits );
p->timeTotal = Abc_Clock() - clkTotal;
if ( fVerbose )
Cbs_ManSatPrintStats( p );
// manager is resident: caller (Cec_DynSrm) owns its lifetime
*pvStatus = vStatus;
return vCexStore;
}


////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END

9 changes: 8 additions & 1 deletion src/base/abci/abc.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41924,6 +41924,13 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
if ( pPars->fIncremental )
{
//preserve for incremental mode, maybe should be a separate command
pPars->fDynSrm = 1; //dynamic SRM
pPars->fIncrSim = 1; //incremental simulation
pPars->fSkipFailResim = 1; //skip resimulation of failed flops
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Scorr(): There is no AIG.\n" );
Expand Down Expand Up @@ -41999,7 +42006,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-i : toggle integrated incremental SRM/re-proof/resimulation [default = %s]\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" );
Expand Down
5 changes: 4 additions & 1 deletion src/proof/cec/cec.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -167,7 +167,10 @@ 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 fIncremental; // integrated incremental mode for &scorr
int fIncrSim; // persistent CEX-TFO-only resimulation after SAT
int fDynSrm; // persistent dynamic SRM and true-unroll resimulation
int fSkipFailResim;// skip resim in rounds with no real CEX (only timeout/fail)
int fVerboseFlops; // verbose stats
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
Expand Down
Loading
Loading