summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/gia/gia.h3
-rw-r--r--src/aig/gia/giaAbsGla.c19
-rw-r--r--src/aig/gia/giaAbsVta.c17
3 files changed, 24 insertions, 15 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 97a7b7b7..c537a31b 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -223,7 +223,8 @@ struct Gia_ParVta_t_
int fDumpVabs; // dumps the abstracted model
char * pFileVabs; // dumps the abstracted model into this file
int fVerbose; // verbose flag
- int iFrame; // the number of frames covered
+ int iFrame; // the number of frames covered
+ int nFramesNoChange; // the number of last frames without changes
};
static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); }
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 6505c2f2..117ad3e0 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -509,7 +509,7 @@ void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * v
{
int i;//, Id = Gia_ObjId(p->pGia, pObj);
Rfn_Obj_t * pRef = Gla_ObjRef( p, pObj, f );
- assert( (int)pRef->Sign == Sign );
+// assert( (int)pRef->Sign == Sign );
if ( pRef->fVisit )
return;
if ( p->pPars->fPropFanout )
@@ -1214,8 +1214,9 @@ void Gla_ManStop( Gla_Man_t * p )
Gla_Obj_t * pGla;
int i;
// if ( p->pPars->fVerbose )
- Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Reduce = %d Cex = %d ObjsAdded = %d\n",
- sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
+ Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d Objs+ = %d\n",
+ sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat),
+ sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
ABC_FREE( p->pvRefis[i].pArray );
Gla_ManForEachObj( p, pGla )
@@ -1805,7 +1806,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin );
Abc_Print( 1, "LearnStart = %d LearnDelta = %d LearnRatio = %d %%.\n",
pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce );
- Abc_Print( 1, "Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" );
+ Abc_Print( 1, " Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" );
}
for ( f = i = iPrev = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++, iPrev = i )
{
@@ -1891,9 +1892,13 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
nCoreSize = Vec_IntSize( vCore );
Gia_GlaAddToCounters( p, vCore );
if ( i == 0 )
+ {
+ p->pPars->nFramesNoChange++;
Vec_IntFree( vCore );
+ }
else
{
+ p->pPars->nFramesNoChange = 0;
// update the SAT solver
sat_solver2_rollback( p->pSat );
// update storage
@@ -1967,9 +1972,9 @@ finish:
if ( Status == -1 )
{
if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit )
- Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d. ", p->pPars->nTimeOut, f );
+ Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange );
else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
- Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f );
+ Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, f, p->pPars->nFramesNoChange );
else if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 )
Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f );
else
@@ -1978,7 +1983,7 @@ finish:
else
{
p->pPars->iFrame++;
- Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f );
+ Abc_Print( 1, "Completed %d frames with a %d-stable abstraction. ", f, p->pPars->nFramesNoChange );
}
}
else
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index f7c1e5a5..85d51a42 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1062,8 +1062,9 @@ 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: Var = %d Cla = %d Conf = %d Reduce = %d Cex = %d ObjsAdded = %d\n",
- sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
+ Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d Objs+ = %d\n",
+ sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat),
+ sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
Vec_VecFreeP( (Vec_Vec_t **)&p->vCores );
Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames );
Vec_BitFreeP( &p->vSeenGla );
@@ -1534,7 +1535,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{
printf( "Sequential miter is trivially UNSAT.\n" );
return 1;
- }
+ }
ABC_FREE( pAig->pCexSeq );
pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 );
printf( "Sequential miter is trivially SAT.\n" );
@@ -1564,7 +1565,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Abc_Print( 1, "LearnStart = %d LearnDelta = %d LearnRatio = %d %%.\n",
pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce );
// Abc_Print( 1, "Frame %% Abs %% Confl Cex SatVar Core F0 F1 F2 ...\n" );
- Abc_Print( 1, "Frame %% Abs %% Confl Cex Vars Clas Lrns Core Time Mem\n" );
+ Abc_Print( 1, " Frame %% Abs %% Confl Cex Vars Clas Lrns Core Time Mem\n" );
}
assert( Vec_PtrSize(p->vFrames) > 0 );
for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
@@ -1665,9 +1666,11 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{
// reset the counter of frames without change
nCountNoChange = 1;
+ p->pPars->nFramesNoChange = 0;
}
else if ( ++nCountNoChange == 2 ) // time to send
{
+ p->pPars->nFramesNoChange++;
if ( Abc_FrameIsBridgeMode() )
{
// cancel old one if it was sent
@@ -1709,9 +1712,9 @@ finish:
if ( Status == -1 )
{
if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit )
- Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d. ", p->pPars->nTimeOut, f );
+ Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange );
else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
- Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f );
+ Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, f, p->pPars->nFramesNoChange );
else if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )
Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f );
else
@@ -1720,7 +1723,7 @@ finish:
else
{
p->pPars->iFrame++;
- Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f );
+ Abc_Print( 1, "Completed %d frames with a %d-stable abstraction. ", f, p->pPars->nFramesNoChange );
}
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 12:39:52 +0000