summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h4
-rw-r--r--src/aig/gia/giaAbsGla.c44
-rw-r--r--src/aig/gia/giaAbsVta.c270
-rw-r--r--src/aig/gia/giaMan.c7
-rw-r--r--src/base/abci/abc.c120
5 files changed, 257 insertions, 188 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 40c74d8a..0d1c6ff1 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -213,6 +213,7 @@ struct Gia_ParVta_t_
int fUseTermVars; // use terminal variables
int fUseRollback; // use rollback to the starting number of frames
int fPropFanout; // propagate fanout implications
+ int fAddLayer; // refinement strategy by adding layers
int fDumpVabs; // dumps the abstracted model
char * pFileVabs; // dumps the abstracted model into this file
int fVerbose; // verbose flag
@@ -704,7 +705,8 @@ extern int Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars,
extern void Gia_VtaSetDefaultParams( Gia_ParVta_t * p );
extern Vec_Ptr_t * Gia_VtaAbsToFrames( Vec_Int_t * vAbs );
extern Vec_Int_t * Gia_VtaFramesToAbs( Vec_Vec_t * vFrames );
-extern Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs );
+extern Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta );
+extern Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames );
extern int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars );
/*=== giaAiger.c ===========================================================*/
extern int Gia_FileSize( char * pFileName );
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 53c95650..f6ada0c8 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -445,7 +445,7 @@ void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int
***********************************************************************/
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);
+ 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;
@@ -506,7 +506,7 @@ void Gia_ManRefSetAndPropFanout_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec
***********************************************************************/
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);
+ 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 )
@@ -1100,6 +1100,8 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
// other
p->vCla2Obj = Vec_IntAlloc( 1000 ); Vec_IntPush( p->vCla2Obj, -1 );
p->pSat = sat_solver2_new();
+// p->pSat->fVerbose = p->pPars->fVerbose;
+ sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
p->nSatVars = 1;
return p;
}
@@ -1214,7 +1216,7 @@ void Gla_ManStop( Gla_Man_t * p )
Gla_Obj_t * pGla;
int i;
// if ( p->pPars->fVerbose )
- Abc_Print( 1, "SAT solver: Vars = %d. Clauses = %d. Confs = %d. Cexes = %d. ObjAdded = %d\n",
+ Abc_Print( 1, "SAT solver: Vars = %d Clauses = %d Confs = %d Cexes = %d ObjsAdded = %d\n",
sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes, p->nObjAdded );
for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
ABC_FREE( p->pvRefis[i].pArray );
@@ -1754,8 +1756,6 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
clk = clock();
p = Gla_ManStart( pAig, pPars );
p->timeInit = clock() - clk;
- p->pSat->fVerbose = p->pPars->fVerbose;
- sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
// set runtime limit
if ( p->pPars->nTimeOut )
sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 );
@@ -1763,21 +1763,23 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
if ( p->pPars->fVerbose )
{
Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" );
- Abc_Print( 1, "FrameStart = %d FrameMax = %d Conf = %d Timeout = %d. RatioMin = %d %%.\n",
- p->pPars->nFramesStart, p->pPars->nFramesMax, p->pPars->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin );
- Abc_Print( 1, "Frame %% Abs PPI FF AND Confl Cex SatVar Core Time\n" );
+ Abc_Print( 1, "FrameMax = %d ConfMax = %d LearnMax = %d Timeout = %d RatioMin = %d %%.\n",
+ pPars->nFramesMax, pPars->nConfLimit, pPars->nLearntMax, pPars->nTimeOut, pPars->nRatioMin );
+ Abc_Print( 1, "Frame %% Abs PPI FF LUT Confl Cex SatVar Core Time\n" );
}
for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
{
int nConflsBeg = sat_solver2_nconflicts(p->pSat);
p->pPars->iFrame = f;
+
// load timeframe
Gia_GlaAddTimeFrame( p, f );
+
// create bookmark to be used for rollback
-// sat_solver2_reducedb( p->pSat );
sat_solver2_bookmark( p->pSat );
Vec_IntClear( p->vAddedNew );
p->nAbsOld = Vec_IntSize( p->vAbs );
+
// iterate as long as there are counter-examples
for ( i = 0; ; i++ )
{
@@ -1805,17 +1807,20 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
p->nCexes++;
// perform the refinement
clk2 = clock();
-
- vPPis = Gla_ManRefinement( p );
- if ( vPPis == NULL )
+ if ( pPars->fAddLayer )
{
- pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
- break;
+ vPPis = Gla_ManCollectPPis( p, NULL );
+// Gla_ManExplorePPis( p, vPPis );
+ }
+ else
+ {
+ vPPis = Gla_ManRefinement( p );
+ if ( vPPis == NULL )
+ {
+ pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
+ break;
+ }
}
-
-// vPPis = Gla_ManCollectPPis( p, NULL );
-// Gla_ManExplorePPis( p, vPPis );
-
Gia_GlaAddToAbs( p, vPPis, 1 );
Gia_GlaAddOneSlice( p, f, vPPis );
Vec_IntFree( vPPis );
@@ -1905,7 +1910,10 @@ finish:
Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f );
}
else
+ {
+ p->pPars->iFrame++;
Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f );
+ }
}
else
{
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index c6f5e238..1a442a79 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -61,6 +61,7 @@ struct Vta_Man_t_
Vec_Ptr_t * vFrames; // start abstraction for each frame
int nWords; // the number of words in the record
int nCexes; // the number of CEXes
+ int nObjAdded; // objects added to the abstraction
Vec_Int_t * vSeens; // seen objects
Vec_Bit_t * vSeenGla; // seen objects in all frames
int nSeenGla; // seen objects in all frames
@@ -149,10 +150,10 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
{
memset( p, 0, sizeof(Gia_ParVta_t) );
p->nFramesMax = 0; // maximum frames
- p->nFramesStart = 5; // starting frame
+ p->nFramesStart = 0; // starting frame
p->nFramesPast = 4; // overlap frames
p->nConfLimit = 0; // conflict limit
- p->nLearntMax = 15000; // max number of learned clauses
+ p->nLearntMax = 1000; // max number of learned clauses
p->nTimeOut = 0; // timeout in seconds
p->nRatioMin = 10; // stop when less than this % of object is abstracted
p->fUseTermVars = 1; // use terminal variables
@@ -236,31 +237,31 @@ Vec_Int_t * Gia_VtaFramesToAbs( Vec_Vec_t * vFrames )
SeeAlso []
***********************************************************************/
-Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs )
+Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta )
{
Gia_Obj_t * pObj;
- Vec_Int_t * vPresent;
+ Vec_Int_t * vGla;
int nObjMask, nObjs = Gia_ManObjNum(p);
- int i, Entry, nFrames = Vec_IntEntry( vAbs, 0 );
- assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) );
+ int i, Entry, nFrames = Vec_IntEntry( vVta, 0 );
+ assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
// get the bitmask
nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
assert( nObjs <= nObjMask );
// go through objects
- vPresent = Vec_IntStart( nObjs );
- Vec_IntWriteEntry( vPresent, 0, 1 );
- Vec_IntForEachEntryStart( vAbs, Entry, i, nFrames+2 )
+ vGla = Vec_IntStart( nObjs );
+ Vec_IntWriteEntry( vGla, 0, 1 );
+ Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 )
{
pObj = Gia_ManObj( p, (Entry & nObjMask) );
assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) );
- Vec_IntWriteEntry( vPresent, (Entry & nObjMask), 1 );
+ Vec_IntWriteEntry( vGla, (Entry & nObjMask), 1 );
}
- return vPresent;
+ return vGla;
}
/**Function*************************************************************
- Synopsis [Detects how many frames are completed.]
+ Synopsis [Converting GLA vector to VTA vector.]
Description []
@@ -269,26 +270,31 @@ Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs )
SeeAlso []
***********************************************************************/
-static inline int Vta_ManReadFrameStart( Vec_Int_t * p, int nWords )
+Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames )
{
- unsigned * pTotal, * pThis;
- int i, w, nObjs = Vec_IntSize(p) / nWords;
- assert( Vec_IntSize(p) % nWords == 0 );
- pTotal = ABC_CALLOC( unsigned, nWords );
- for ( i = 0; i < nObjs; i++ )
- {
- pThis = (unsigned *)Vec_IntEntryP( p, nWords * i );
- for ( w = 0; w < nWords; w++ )
- pTotal[w] |= pThis[i];
- }
- for ( i = nWords * 32 - 1; i >= 0; i-- )
- if ( Abc_InfoHasBit(pTotal, i) )
- {
- ABC_FREE( pTotal );
- return i+1;
- }
- ABC_FREE( pTotal );
- return -1;
+ Vec_Int_t * vVta;
+ int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p);
+ int i, k, j, Entry, Counter, nGlaSize;
+ //. get the GLA size
+ nGlaSize = Vec_IntSum(vGla);
+ // get the bitmask
+ nObjBits = Abc_Base2Log(nObjs);
+ nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
+ assert( nObjs <= nObjMask );
+ // go through objects
+ vVta = Vec_IntAlloc( 1000 );
+ Vec_IntPush( vVta, nFrames );
+ Counter = nFrames + 2;
+ for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize )
+ Vec_IntPush( vVta, Counter );
+ for ( i = 0; i < nFrames; i++ )
+ for ( k = 0; k <= i; k++ )
+ Vec_IntForEachEntry( vGla, Entry, j )
+ if ( Entry )
+ Vec_IntPush( vVta, (k << nObjBits) | j );
+ Counter = Vec_IntEntry(vVta, nFrames+1);
+ assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
+ return vVta;
}
/**Function*************************************************************
@@ -949,25 +955,28 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
assert( 0 );
}
- // mark those currently included
- Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
- {
- assert( pThis->fVisit == 0 );
- pThis->fVisit = 1;
- }
- // add used terms, which have close relationship
- Counter = Vec_IntSize(vTermsToAdd);
- Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
+ if ( p->pPars->fAddLayer )
{
- if ( pThis->fVisit )
- continue;
-// Vta_ObjPreds( p, pThis, Gia_ManObj(p->pGia, pThis->iObj), &pThis0, &pThis1 );
-// if ( (pThis0 && (pThis0->fAdded || pThis0->fVisit)) || (pThis1 && (pThis1->fAdded || pThis1->fVisit)) )
- Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
+ // mark those currently included
+ Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
+ {
+ assert( pThis->fVisit == 0 );
+ pThis->fVisit = 1;
+ }
+ // add used terms, which have close relationship
+ Counter = Vec_IntSize(vTermsToAdd);
+ Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
+ {
+ if ( pThis->fVisit )
+ continue;
+ // Vta_ObjPreds( p, pThis, Gia_ManObj(p->pGia, pThis->iObj), &pThis0, &pThis1 );
+ // if ( (pThis0 && (pThis0->fAdded || pThis0->fVisit)) || (pThis1 && (pThis1->fAdded || pThis1->fVisit)) )
+ Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
+ }
+ // remove those currenty included
+ Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
+ pThis->fVisit = 0;
}
- // remove those currenty included
- Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
- pThis->fVisit = 0;
// printf( "\n%d -> %d\n", Counter, Vec_IntSize(vTermsToAdd) );
//Vec_IntReverseOrder( vTermsToAdd );
//Vec_IntSort( vTermsToAdd, 1 );
@@ -1054,6 +1063,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
sat_solver2_simplify( p->pSat );
}
+ p->nObjAdded += Vec_IntSize(vTermsToAdd);
Vec_IntFree( vTermsToAdd );
return pCex;
}
@@ -1091,28 +1101,15 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p->vSeenGla = Vec_BitStart( Gia_ManObjNum(pGia) );
p->nSeenGla = 1;
p->nSeenAll = 1;
- // start the abstraction
- if ( pGia->vObjClasses == NULL )
- p->vFrames = Gia_ManUnrollAbs( pGia, pPars->nFramesStart );
- else
- {
- p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses );
- // update parameters
- if ( pPars->nFramesStart != Vec_PtrSize(p->vFrames) )
- {
- Abc_Print( 1, "Starting frame count is changed to match the abstraction (from %d to %d).\n", pPars->nFramesStart, Vec_PtrSize(p->vFrames) );
- pPars->nFramesStart = Vec_PtrSize(p->vFrames);
- }
- if ( pPars->nFramesMax && pPars->nFramesMax < pPars->nFramesStart )
- {
- Abc_Print( 1, "Maximum frame count is changed to match the starting frames (from %d to %d).\n", pPars->nFramesMax, pPars->nFramesStart );
- pPars->nFramesMax = Abc_MaxInt( pPars->nFramesMax, pPars->nFramesStart );
- }
- }
// other data
p->vCla2Var = Vec_IntAlloc( 1000 ); Vec_IntPush( p->vCla2Var, -1 );
p->vCores = Vec_PtrAlloc( 100 );
p->pSat = sat_solver2_new();
+// p->pSat->fVerbose = p->pPars->fVerbose;
+ sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
+ // start the abstraction
+ assert( pGia->vObjClasses != NULL );
+ p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses );
p->vAddedNew = Vec_IntAlloc( 1000 );
return p;
}
@@ -1131,9 +1128,8 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
void Vga_ManStop( Vta_Man_t * p )
{
// if ( p->pPars->fVerbose )
- Abc_Print( 1, "SAT solver: Variables = %d. Clauses = %d. Conflicts = %d. Cexes = %d.\n",
- sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes );
-
+ Abc_Print( 1, "SAT solver: Vars = %d Clauses = %d Confs = %d Cexes = %d ObjsAdded = %d\n",
+ sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes, p->nObjAdded );
Vec_VecFreeP( (Vec_Vec_t **)&p->vCores );
Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames );
Vec_BitFreeP( &p->vSeenGla );
@@ -1624,8 +1620,6 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// preconditions
assert( Gia_ManPoNum(pAig) == 1 );
assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
-
-/*
// compute intial abstraction
if ( pAig->vObjClasses == NULL )
{
@@ -1635,11 +1629,8 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Vec_IntPush( pAig->vObjClasses, 4 );
Vec_IntPush( pAig->vObjClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) );
}
-*/
// start the manager
p = Vga_ManStart( pAig, pPars );
- p->pSat->fVerbose = p->pPars->fVerbose;
- sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
// set runtime limit
if ( p->pPars->nTimeOut )
sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 );
@@ -1647,11 +1638,11 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
if ( p->pPars->fVerbose )
{
Abc_Print( 1, "Running variable-timeframe abstraction (VTA) with the following parameters:\n" );
- Abc_Print( 1, "FrameStart = %d FramePast = %d FrameMax = %d Conf = %d Timeout = %d. RatioMin = %d %%.\n",
- p->pPars->nFramesStart, p->pPars->nFramesPast, p->pPars->nFramesMax,
- p->pPars->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin );
+ Abc_Print( 1, "FramePast = %d FrameMax = %d ConfMax = %d LearnMax = %d Timeout = %d RatioMin = %d %%\n",
+ pPars->nFramesPast, pPars->nFramesMax, pPars->nConfLimit, pPars->nLearntMax, pPars->nTimeOut, pPars->nRatioMin );
Abc_Print( 1, "Frame %% Abs %% Confl Cex SatVar Core F0 F1 F2 ...\n" );
}
+ assert( Vec_PtrSize(p->vFrames) > 0 );
for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
{
int nConflsBeg = sat_solver2_nconflicts(p->pSat);
@@ -1659,72 +1650,72 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// realloc storage for abstraction marks
if ( f == p->nWords * 32 )
p->nWords = Vec_IntDoubleWidth( p->vSeens, p->nWords );
- // check this timeframe
- if ( f < p->pPars->nFramesStart )
- {
- Vga_ManAddClausesOne( p, 0, f );
+
+ // create bookmark to be used for rollback
+ nObjOld = p->nObjs;
+ sat_solver2_bookmark( p->pSat );
+ Vec_IntClear( p->vAddedNew );
+
+ // load new timeframe
+ Vga_ManAddClausesOne( p, 0, f );
+ if ( f < Vec_PtrSize(p->vFrames) )
Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
- }
else
{
- // create bookmark to be used for rollback
- nObjOld = p->nObjs;
-// sat_solver2_reducedb( p->pSat );
- sat_solver2_bookmark( p->pSat );
- Vec_IntClear( p->vAddedNew );
- // load the time frame
- for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesPast, p->pPars->nFramesStart); i++ )
+ for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesPast, f); i++ )
Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
- // iterate as long as there are counter-examples
- for ( i = 0; ; i++ )
- {
- clk2 = clock();
- vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
- assert( (vCore != NULL) == (Status == 1) );
- if ( Status == -1 ) // resource limit is reached
- {
- Vga_ManRollBack( p, nObjOld );
- goto finish;
- }
- // check timeout
- if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit )
- {
- Vga_ManRollBack( p, nObjOld );
- goto finish;
- }
- if ( vCore != NULL )
- {
- p->timeUnsat += clock() - clk2;
- break;
- }
- p->timeSat += clock() - clk2;
- assert( Status == 0 );
- p->nCexes++;
- // perform the refinement
- clk2 = clock();
- pCex = Vta_ManRefineAbstraction( p, f );
- p->timeCex += clock() - clk2;
- if ( pCex != NULL )
- {
- RetValue = 0;
- goto finish;
- }
- // print the result (do not count it towards change)
- Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk, p->pPars->fVerbose );
+ }
+
+ // iterate as long as there are counter-examples
+ for ( i = 0; ; i++ )
+ {
+ clk2 = clock();
+ vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
+ assert( (vCore != NULL) == (Status == 1) );
+ if ( Status == -1 ) // resource limit is reached
+ {
+ Vga_ManRollBack( p, nObjOld );
+ goto finish;
+ }
+ // check timeout
+ if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit )
+ {
+ Vga_ManRollBack( p, nObjOld );
+ goto finish;
+ }
+ if ( vCore != NULL )
+ {
+ p->timeUnsat += clock() - clk2;
+ break;
+ }
+ p->timeSat += clock() - clk2;
+ assert( Status == 0 );
+ p->nCexes++;
+ // perform the refinement
+ clk2 = clock();
+ pCex = Vta_ManRefineAbstraction( p, f );
+ p->timeCex += clock() - clk2;
+ if ( pCex != NULL )
+ {
+ RetValue = 0;
+ goto finish;
}
- assert( Status == 1 );
- // valid core is obtained
- Vta_ManUnsatCoreRemap( p, vCore );
- Vec_IntSort( vCore, 1 );
- // update the SAT solver
- sat_solver2_rollback( p->pSat );
- // update storage
- Vga_ManRollBack( p, nObjOld );
- Vec_IntShrink( p->vCla2Var, (int)p->pSat->stats.clauses+1 );
- // load this timeframe
- Vga_ManLoadSlice( p, vCore, 0 );
- Vec_IntFree( vCore );
- }
+ // print the result (do not count it towards change)
+ Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk, p->pPars->fVerbose );
+ }
+ assert( Status == 1 );
+ // valid core is obtained
+ Vta_ManUnsatCoreRemap( p, vCore );
+ Vec_IntSort( vCore, 1 );
+ // update the SAT solver
+ sat_solver2_rollback( p->pSat );
+ // update storage
+ Vga_ManRollBack( p, nObjOld );
+ Vec_IntShrink( p->vCla2Var, (int)p->pSat->stats.clauses+1 );
+ // load this timeframe
+ Vga_ManLoadSlice( p, vCore, 0 );
+ Vec_IntFree( vCore );
+
// run SAT solver
clk2 = clock();
vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
@@ -1808,7 +1799,10 @@ finish:
Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f );
}
else
+ {
+ p->pPars->iFrame++;
Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f );
+ }
}
}
else
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index c116f5e7..0ab6c091 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -202,6 +202,7 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p )
void Gia_ManPrintGateClasses( Gia_Man_t * p )
{
Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes;
+ int nTotal;
if ( p->vGateClasses == NULL )
return;
if ( Vec_IntSize(p->vGateClasses) != Gia_ManObjNum(p) )
@@ -211,10 +212,12 @@ void Gia_ManPrintGateClasses( Gia_Man_t * p )
}
// create additional arrays
Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, &vFlops, &vNodes );
- printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d (%.2f %%) AND = %d (%.2f %%)\n",
+ nTotal = 1 + Vec_IntSize(vFlops) + Vec_IntSize(vNodes);
+ printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d (%.2f %%) AND = %d (%.2f %%) Obj = %d (%.2f %%)\n",
Vec_IntSize(vPis), Vec_IntSize(vPPis),
Vec_IntSize(vFlops), 100.0*Vec_IntSize(vFlops)/(Gia_ManRegNum(p)+1),
- Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1) );
+ Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1),
+ nTotal, 100.0*nTotal /(Gia_ManRegNum(p)+Gia_ManAndNum(p)+1) );
Vec_IntFree( vPis );
Vec_IntFree( vPPis );
Vec_IntFree( vFlops );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d1c1e5a9..8983ba39 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -352,6 +352,7 @@ static int Abc_CommandAbc9GlaPba ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Gla ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Vta ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Vta2Gla ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Gla2Vta ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Reparam ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9BackReach ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Posplit ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -797,6 +798,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&gla", Abc_CommandAbc9Gla, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&vta", Abc_CommandAbc9Vta, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&vta_gla", Abc_CommandAbc9Vta2Gla, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&gla_vta", Abc_CommandAbc9Gla2Vta, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&reparam", Abc_CommandAbc9Reparam, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&back_reach", Abc_CommandAbc9BackReach, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&posplit", Abc_CommandAbc9Posplit, 0 );
@@ -27384,10 +27386,8 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_ParVta_t Pars, * pPars = &Pars;
int c, fStartVta = 0;
Gia_VtaSetDefaultParams( pPars );
- pPars->nFramesStart = 30;
- pPars->nLearntMax = 100000;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrfdavh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrfkadvh" ) ) != EOF )
{
switch ( c )
{
@@ -27486,11 +27486,14 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'f':
pPars->fPropFanout ^= 1;
break;
- case 'd':
- pPars->fDumpVabs ^= 1;
+ case 'k':
+ fStartVta ^= 1;
break;
case 'a':
- fStartVta ^= 1;
+ pPars->fAddLayer ^= 1;
+ break;
+ case 'd':
+ pPars->fDumpVabs ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
@@ -27526,32 +27529,25 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" );
return 0;
}
- if ( pPars->nFramesStart < 1 )
- {
- Abc_Print( 1, "The starting frame should be 1 or larger.\n" );
- return 0;
- }
pAbc->Status = Gia_GlaPerform( pAbc->pGia, pPars, fStartVta );
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
- Abc_Print( -2, "usage: &gla [-FSCLTR num] [-A file] [-fdavh]\n" );
- Abc_Print( -2, "\t performs gate-level abstraction of a sequential miter\n" );
+ Abc_Print( -2, "usage: &gla [-FSCLTR num] [-A file] [-fkadvh]\n" );
+ Abc_Print( -2, "\t fixed-time-frame gate-level proof- and cex-based abstraction\n" );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
-// Abc_Print( -2, "\t-P num : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesPast );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-L num : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearntMax );
Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-R num : minimum percentage of abstracted objects (0<=num<=100) [default = %d]\n", pPars->nRatioMin );
Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" );
-// Abc_Print( -2, "\t-t : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" );
-// Abc_Print( -2, "\t-r : toggle using rollback after the starting frames [default = %s]\n", pPars->fUseRollback? "yes": "no" );
Abc_Print( -2, "\t-f : toggle propagating fanout implications [default = %s]\n", pPars->fPropFanout? "yes": "no" );
+ Abc_Print( -2, "\t-k : toggle using VTA to kick start GLA for starting frames [default = %s]\n", fStartVta? "yes": "no" );
+ Abc_Print( -2, "\t-a : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping abstracted model into a file [default = %s]\n", pPars->fDumpVabs? "yes": "no" );
- Abc_Print( -2, "\t-a : toggle using VTA to kick start GLA [default = %s]\n", fStartVta? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@@ -27574,7 +27570,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Gia_VtaSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrdvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtradvh" ) ) != EOF )
{
switch ( c )
{
@@ -27670,6 +27666,9 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
pPars->fUseRollback ^= 1;
break;
+ case 'a':
+ pPars->fAddLayer ^= 1;
+ break;
case 'd':
pPars->fDumpVabs ^= 1;
break;
@@ -27707,21 +27706,14 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" );
return 0;
}
- if ( pPars->nFramesStart < 1 )
- {
- Abc_Print( 1, "The starting frame should be 1 or larger.\n" );
- return 0;
- }
-// if ( argc == globalUtilOptind + 1 )
-// pPars->pFileVabs = argv[globalUtilOptind];
pAbc->Status = Gia_VtaPerform( pAbc->pGia, pPars );
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
- Abc_Print( -2, "usage: &vta [-FSPCLTR num] [-A file] [-trdvh]\n" );
- Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" );
+ Abc_Print( -2, "usage: &vta [-FSPCLTR num] [-A file] [-tradvh]\n" );
+ Abc_Print( -2, "\t variable-time-frame gate-level proof- and cex-based abstraction\n" );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
Abc_Print( -2, "\t-P num : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesPast );
@@ -27732,6 +27724,7 @@ usage:
Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"vabs.aig\"]\n" );
Abc_Print( -2, "\t-t : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" );
Abc_Print( -2, "\t-r : toggle using rollback after the starting frames [default = %s]\n", pPars->fUseRollback? "yes": "no" );
+ Abc_Print( -2, "\t-a : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping abstracted model into a file [default = %s]\n", pPars->fDumpVabs? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@@ -27773,7 +27766,7 @@ int Abc_CommandAbc9Vta2Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pGia->vObjClasses == NULL )
{
- Abc_Print( -1, "Abc_CommandAbc9Vta2Gla(): There is no variable-time-frame abstraction defines.\n" );
+ Abc_Print( -1, "Abc_CommandAbc9Vta2Gla(): There is no variable-time-frame abstraction is defined.\n" );
return 1;
}
Vec_IntFreeP( &pAbc->pGia->vGateClasses );
@@ -27783,7 +27776,7 @@ int Abc_CommandAbc9Vta2Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: &vta_gla [-vh]\n" );
- Abc_Print( -2, "\t maps variable- into fixed-time-frame abstraction\n" );
+ Abc_Print( -2, "\t maps variable- into fixed-time-frame gate-level abstraction\n" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@@ -27800,6 +27793,75 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9Gla2Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ int c, fVerbose = 0;
+ int nFrames = pAbc->nFrames;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nFrames = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nFrames < 0 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): There is no AIG.\n" );
+ return 1;
+ }
+ if ( pAbc->pGia->vGateClasses == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): There is no gate-level abstraction is defined.\n" );
+ return 1;
+ }
+ if ( pAbc->nFrames < 1 )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): The number of timeframes (%d) should be a positive integer.\n", nFrames );
+ return 1;
+ }
+ Vec_IntFreeP( &pAbc->pGia->vObjClasses );
+ pAbc->pGia->vObjClasses = Gia_VtaConvertFromGla( pAbc->pGia, pAbc->pGia->vGateClasses, nFrames );
+ Vec_IntFreeP( &pAbc->pGia->vGateClasses );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &gla_vta [-F num] [-vh]\n" );
+ Abc_Print( -2, "\t maps fixed- into variable-time-frame gate-level abstraction\n" );
+ Abc_Print( -2, "\t-F num : timeframes in the resulting variable-time-frame abstraction [default = %d]\n", nFrames );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9Reparam( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp = NULL;
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 04:07:02 +0000