summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaAbsGla.c4
-rw-r--r--src/aig/gia/giaAbsGla2.c48
-rw-r--r--src/aig/gia/giaAbsVta.c2
3 files changed, 28 insertions, 26 deletions
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index d992aeab..dd9c6b9e 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -1919,7 +1919,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 )
{
@@ -2123,7 +2123,7 @@ finish:
else
{
p->pPars->iFrame++;
- Abc_Print( 1, "Completed %d frames with a %d-stable abstraction. ", f, p->pPars->nFramesNoChange );
+ Abc_Print( 1, "GLA completed %d frames with a %d-stable abstraction. ", f, p->pPars->nFramesNoChange );
}
}
else
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c
index 9504e32d..f0d1b143 100644
--- a/src/aig/gia/giaAbsGla2.c
+++ b/src/aig/gia/giaAbsGla2.c
@@ -1325,8 +1325,8 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
{
char * pFileNameDef = "glabs.aig";
char * pFileName = p->pPars->pFileVabs ? p->pPars->pFileVabs : pFileNameDef;
- if ( fVerbose )
- Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
+// if ( fVerbose )
+// Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
if ( p->pPars->fDumpVabs )
{
// dump absracted model
@@ -1435,7 +1435,11 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin, pPars->nRatioMax );
Abc_Print( 1, "LrnStart = %d LrnDelta = %d LrnRatio = %d %% Skip = %d SimpleCNF = %d Dump = %d\n",
pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs );
- Abc_Print( 1, " Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" );
+ if ( pPars->fDumpVabs )
+ Abc_Print( 1, "Abstracted model will be dumped into file \"%s\".\n", p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig" );
+ else if ( pPars->fDumpMabs )
+ Abc_Print( 1, "Miter with abstraction map will be dumped into file \"%s\".\n", p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig" );
+ Abc_Print( 1, " Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" );
}
// iterate unrolling
for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ )
@@ -1448,7 +1452,6 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// remember abstraction size after the last restart
nAbsOld = Vec_IntSize(p->vAbs);
// unroll the circuit
- p->pPars->nFramesNoChange = -1;
for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ )
{
// remember current limits
@@ -1456,12 +1459,12 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
int nAbs = Vec_IntSize(p->vAbs);
int nValues = Vec_IntSize(p->vValues);
int nVarsOld;
+ // remember the timeframe
+ p->pPars->iFrame = f;
// extend and clear storage
if ( f == Vec_PtrSize(p->vId2Lit) )
Vec_PtrPush( p->vId2Lit, Vec_IntAlloc(0) );
Vec_IntFillExtra( Ga2_MapFrameMap(p, f), Vec_IntSize(p->vValues), -1 );
- // remember the timeframe
- p->pPars->iFrame = f;
// add static clauses to this timeframe
Ga2_ManAddAbsClauses( p, f );
// skip checking if skipcheck is enabled (&gla -s)
@@ -1553,11 +1556,12 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
goto finish;
if ( c == 0 )
{
- if ( p->pPars->nFramesNoChange >= 0 )
+ if ( f > iFrameProved )
p->pPars->nFramesNoChange++;
break;
}
- p->pPars->nFramesNoChange = 0;
+ if ( f > iFrameProved )
+ p->pPars->nFramesNoChange = 0;
// derive the core
assert( p->pSat->pPrf2 != NULL );
@@ -1613,21 +1617,24 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Vec_IntFree( vCore );
break;
}
+ // remember the last proved frame
+ if ( iFrameProved < f )
+ iFrameProved = f;
+ // print statistics
if ( pPars->fVerbose )
Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 );
- // set model
if ( c > 0 )
{
+ // recompute the abstraction
Vec_IntFreeP( &pAig->vGateClasses );
pAig->vGateClasses = Ga2_ManAbsTranslate( p );
-
// check if the number of objects is below limit
if ( Vec_IntSize(p->vAbs) >= p->nMarked * (100 - pPars->nRatioMin) / 100 )
{
Status = l_Undef;
goto finish;
}
-
+ // speak to the bridge
if ( Abc_FrameIsBridgeMode() )
{
// cancel old one if it was sent
@@ -1637,7 +1644,6 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Gia_Ga2SendAbsracted( p, pPars->fVerbose );
fOneIsSent = 1;
}
-
// dump the model into file
if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs )
{
@@ -1649,11 +1655,8 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
Ga2_GlaDumpAbsracted( p, pPars->fVerbose );
}
-
- iFrameProved = f;
if ( p->pPars->fVeryVerbose )
Abc_Print( 1, "\n" );
-
// if abstraction grew more than a certain percentage, force a restart
if ( pPars->nRatioMax == 0 )
break;
@@ -1668,7 +1671,6 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
}
}
finish:
- p->pPars->nFramesNoChange = Abc_MaxInt( p->pPars->nFramesNoChange, 0 );
Prf_ManStopP( &p->pSat->pPrf2 );
if ( p->pPars->fVerbose )
Abc_Print( 1, "\n" );
@@ -1682,18 +1684,18 @@ finish:
if ( Status == l_Undef )
{
if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit )
- Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange );
+ Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, iFrameProved, p->pPars->nFramesNoChange );
else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
- Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, f, p->pPars->nFramesNoChange );
+ Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, iFrameProved, p->pPars->nFramesNoChange );
else if ( Vec_IntSize(p->vAbs) >= p->nMarked * (100 - pPars->nRatioMin) / 100 )
- Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f );
+ Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, iFrameProved );
else
- Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f );
+ Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", iFrameProved );
}
else
{
- p->pPars->iFrame++;
- Abc_Print( 1, "SAT solver completed %d frames and produced a %d-stable abstraction. ", f, p->pPars->nFramesNoChange );
+ p->pPars->iFrame = iFrameProved;
+ Abc_Print( 1, "GLA completed %d frames and produced a %d-stable abstraction. ", iFrameProved, p->pPars->nFramesNoChange );
}
}
else
@@ -1701,7 +1703,7 @@ finish:
if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
Abc_Print( 1, " Gia_GlaPerform(): CEX verification has failed!\n" );
Abc_Print( 1, "Counter-example detected in frame %d. ", f );
- p->pPars->iFrame = pAig->pCexSeq->iFrame - 1;
+ p->pPars->iFrame = f - 1;
Vec_IntFreeP( &pAig->vGateClasses );
RetValue = 0;
}
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 4edbacc4..878903b1 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1727,7 +1727,7 @@ finish:
else
{
p->pPars->iFrame++;
- Abc_Print( 1, "Completed %d frames with a %d-stable abstraction. ", f, p->pPars->nFramesNoChange );
+ Abc_Print( 1, "VTA 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-05 00:46:24 +0000