summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/gia/gia.h5
-rw-r--r--src/aig/gia/giaAbsGla.c51
-rw-r--r--src/aig/gia/giaAbsVta.c53
-rw-r--r--src/aig/ivy/ivyFraig.c2
4 files changed, 34 insertions, 77 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 3eda381d..97a7b7b7 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -210,7 +210,10 @@ struct Gia_ParVta_t_
int nFramesStart; // starting frame
int nFramesPast; // overlap frames
int nConfLimit; // conflict limit
- int nLearntMax; // max number of learned clauses
+ int nLearnedMax; // max number of learned clauses
+ int nLearnedStart; // max number of learned clauses
+ int nLearnedDelta; // delta increase of learned clauses
+ int nLearnedPerce; // percentage of clauses to leave
int nTimeOut; // timeout in seconds
int nRatioMin; // stop when less than this % of object is abstracted
int fUseTermVars; // use terminal variables
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 49bcc6a0..c5444119 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -131,36 +131,6 @@ static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) {
/**Function*************************************************************
- Synopsis [Prints integer number using 6 characters.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Abc_PrintInt( int i )
-{
- Abc_Print( 1, " " );
- if ( i > -1000 && i < 1000 )
- Abc_Print( 1, " %4d", i );
- else if ( i > -10000 && i < 10000 )
- Abc_Print( 1, "%4.2fk", (float)i/1000 );
- else if ( i > -100000 && i < 100000 )
- Abc_Print( 1, "%4.1fk", (float)i/1000 );
- else if ( i > -1000000 && i < 1000000 )
- Abc_Print( 1, "%4.0fk", (float)i/1000 );
- else if ( i > -10000000 && i < 10000000 )
- Abc_Print( 1, "%4.2fm", (float)i/1000000 );
- else if ( i > -100000000 && i < 100000000 )
- Abc_Print( 1, "%4.1fm", (float)i/1000000 );
- else if ( i > -1000000000 && i < 1000000000 )
- Abc_Print( 1, "%4.0fm", (float)i/1000000 );
-}
-
-/**Function*************************************************************
-
Synopsis [Derive a new counter-example.]
Description []
@@ -1129,7 +1099,11 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
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 );
+// sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax );
+ p->pSat->nLearntStart = p->pPars->nLearnedStart;
+ p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
+ p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
+ p->pSat->nLearntMax = p->pSat->nLearntStart;
p->nSatVars = 1;
return p;
}
@@ -1243,8 +1217,8 @@ 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 ObjsAdded = %d\n",
- sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes, p->nObjAdded );
+ 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 );
for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
ABC_FREE( p->pvRefis[i].pArray );
Gla_ManForEachObj( p, pGla )
@@ -1660,7 +1634,7 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl
{
if ( Abc_FrameIsBatchMode() && nCoreSize <= 0 )
return;
- Abc_Print( 1, "%3d :", nFrames-1 );
+ Abc_Print( 1, "%4d :", nFrames-1 );
Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * Gia_GlaAbsCount(p, 0, 0) / (p->nObjs - Gia_ManPoNum(p->pGia) + Gia_ManCoNum(p->pGia) + 1)) );
Abc_Print( 1, "%6d", Gia_GlaAbsCount(p, 0, 0) );
Abc_Print( 1, "%5d", Gla_ManCountPPis(p) );
@@ -1794,7 +1768,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
Vec_Int_t * vCore, * vPPis;
Abc_Cex_t * pCex = NULL;
int f, i, iPrev, nConfls, Status, nVarsOld, nCoreSize, fOneIsSent = 0, RetValue = -1;
- clock_t clk = clock(), clk2;
+ clock_t clk2, clk = clock();
// preconditions
assert( Gia_ManPoNum(pAig) == 1 );
assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
@@ -1834,7 +1808,6 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
}
}
// start the manager
- clk = clock();
p = Gla_ManStart( pAig, pPars );
p->timeInit = clock() - clk;
// set runtime limit
@@ -1844,8 +1817,10 @@ 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, "FrameMax = %d ConfMax = %d LearnMax = %d Timeout = %d RatioMin = %d %%.\n",
- pPars->nFramesMax, pPars->nConfLimit, pPars->nLearntMax, pPars->nTimeOut, pPars->nRatioMin );
+ Abc_Print( 1, "FrameMax = %d ConfMax = %d Timeout = %d RatioMin = %d %%.\n",
+ 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" );
}
for ( f = i = iPrev = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++, iPrev = i )
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index e2dfc90d..4e6f3eee 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -137,36 +137,6 @@ extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame );
/**Function*************************************************************
- Synopsis [Prints integer number using 6 characters.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Abc_PrintInt( int i )
-{
- Abc_Print( 1, " " );
- if ( i > -1000 && i < 1000 )
- Abc_Print( 1, " %4d", i );
- else if ( i > -10000 && i < 10000 )
- Abc_Print( 1, "%4.2fk", (float)i/1000 );
- else if ( i > -100000 && i < 100000 )
- Abc_Print( 1, "%4.1fk", (float)i/1000 );
- else if ( i > -1000000 && i < 1000000 )
- Abc_Print( 1, "%4.0fk", (float)i/1000 );
- else if ( i > -10000000 && i < 10000000 )
- Abc_Print( 1, "%4.2fm", (float)i/1000000 );
- else if ( i > -100000000 && i < 100000000 )
- Abc_Print( 1, "%4.1fm", (float)i/1000000 );
- else if ( i > -1000000000 && i < 1000000000 )
- Abc_Print( 1, "%4.0fm", (float)i/1000000 );
-}
-
-/**Function*************************************************************
-
Synopsis [This procedure sets default parameters.]
Description []
@@ -183,7 +153,10 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
p->nFramesStart = 0; // starting frame
p->nFramesPast = 4; // overlap frames
p->nConfLimit = 0; // conflict limit
- p->nLearntMax = 1000; // max number of learned clauses
+ p->nLearnedMax = 1000; // max number of learned clauses
+ p->nLearnedStart = 1000; // max number of learned clauses
+ p->nLearnedDelta = 200; // max number of learned clauses
+ p->nLearnedPerce = 40; // 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 = 0; // use terminal variables
@@ -1065,7 +1038,11 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p->vCores = Vec_PtrAlloc( 100 );
p->pSat = sat_solver2_new();
// p->pSat->fVerbose = p->pPars->fVerbose;
- sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
+// sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax );
+ p->pSat->nLearntStart = p->pPars->nLearnedStart;
+ p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
+ p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
+ p->pSat->nLearntMax = p->pSat->nLearntStart;
// start the abstraction
assert( pGia->vObjClasses != NULL );
p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses );
@@ -1087,8 +1064,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: 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 );
+ 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 );
Vec_VecFreeP( (Vec_Vec_t **)&p->vCores );
Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames );
Vec_BitFreeP( &p->vSeenGla );
@@ -1261,7 +1238,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
return fChanges;
// Abc_Print( 1, "%5d%5d", pCountAll[0], pCountUni[0] );
- Abc_Print( 1, "%3d :", nFrames-1 );
+ Abc_Print( 1, "%4d :", nFrames-1 );
Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenGla / (Gia_ManRegNum(p->pGia) + Gia_ManAndNum(p->pGia) + 1)) );
Abc_Print( 1, "%6d", p->nSeenGla );
Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenAll / (p->nSeenGla * nFrames)) );
@@ -1605,8 +1582,10 @@ 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, "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, "FramePast = %d FrameMax = %d ConfMax = %d Timeout = %d RatioMin = %d %%\n",
+ pPars->nFramesPast, 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 %% Confl Cex SatVar Core F0 F1 F2 ...\n" );
Abc_Print( 1, "Frame %% Abs %% Confl Cex Vars Clas Lrns Core Time Mem\n" );
}
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index 234f403a..776a41b3 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -2923,7 +2923,7 @@ printf( "***************\n" );
***********************************************************************/
int Ivy_FraigCheckCone( Ivy_FraigMan_t * pGlo, Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, int nConfLimit )
{
- extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
+ extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
Vec_Int_t * vLeaves;
Aig_Man_t * pMan;
Aig_Obj_t * pObj;
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-14 11:29:17 +0000