summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaAbsGla.c30
-rw-r--r--src/aig/gia/giaAbsVta.c37
-rw-r--r--src/sat/bsat/satSolver.c4
-rw-r--r--src/sat/bsat/satSolver2.c1
-rw-r--r--src/sat/bsat/satSolver2.h5
5 files changed, 68 insertions, 9 deletions
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 75aacc7d..944badc4 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -131,6 +131,27 @@ 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 )
+{
+ if ( i > -1000 && i < 1000 )
+ printf( "%6d", i );
+ else if ( i > -1000000 && i < 1000000 )
+ printf( "%5dk", i/1000 );
+ else if ( i > -1000000000 && i < 1000000000 )
+ printf( "%5dm", i/1000000 );
+}
+
+/**Function*************************************************************
+
Synopsis [Derive a new counter-example.]
Description []
@@ -1641,8 +1662,11 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl
Abc_Print( 1, "%5c", '-' );
else
Abc_Print( 1, "%5d", nCexes );
- Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) );
- Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 );
+// Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) );
+ Abc_PrintInt( sat_solver2_nvars(p->pSat) );
+ Abc_PrintInt( sat_solver2_nclauses(p->pSat) );
+ Abc_PrintInt( sat_solver2_nlearnts(p->pSat) );
+// Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 );
Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
Abc_Print( 1, "%s", nCoreSize > 0 ? "\n" : "\r" );
@@ -1813,7 +1837,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
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, "Frame %% Abs PPI FF LUT Confl Cex SatVar Core Time\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 )
{
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index d32c1a2e..98f2b536 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -137,6 +137,27 @@ 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 )
+{
+ if ( i > -1000 && i < 1000 )
+ printf( "%6d", i );
+ else if ( i > -1000000 && i < 1000000 )
+ printf( "%5dk", i/1000 );
+ else if ( i > -1000000000 && i < 1000000000 )
+ printf( "%5dm", i/1000000 );
+}
+
+/**Function*************************************************************
+
Synopsis [This procedure sets default parameters.]
Description []
@@ -1191,7 +1212,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
{
unsigned * pInfo;
int * pCountAll = NULL, * pCountUni = NULL;
- int i, k, iFrame, iObj, Entry, fChanges = 0;
+ int i, iFrame, iObj, Entry, fChanges = 0;
// print info about frames
if ( vCore )
{
@@ -1240,12 +1261,15 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
Abc_Print( 1, "%5c", '-' );
else
Abc_Print( 1, "%5d", nCexes );
- Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) );
+// Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) );
+ Abc_PrintInt( sat_solver2_nvars(p->pSat) );
+ Abc_PrintInt( sat_solver2_nclauses(p->pSat) );
+ Abc_PrintInt( sat_solver2_nlearnts(p->pSat) );
if ( vCore == NULL )
{
Abc_Print( 1, " ..." );
- for ( k = 0; k < 7; k++ )
- Abc_Print( 1, " " );
+// for ( k = 0; k < 7; k++ )
+// Abc_Print( 1, " " );
Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
Abc_Print( 1, "\r" );
@@ -1253,6 +1277,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
else
{
Abc_Print( 1, "%7d", pCountAll[0] );
+/*
if ( nFrames > 7 )
{
for ( k = 0; k < 3; k++ )
@@ -1268,6 +1293,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
for ( k = nFrames; k < 7; k++ )
Abc_Print( 1, " " );
}
+*/
Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
Abc_Print( 1, "\n" );
@@ -1572,7 +1598,8 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
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, "Frame %% Abs %% Confl Cex SatVar Core F0 F1 F2 ...\n" );
+// 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" );
}
assert( Vec_PtrSize(p->vFrames) > 0 );
for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 0a7cb1c7..2e3af2dd 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1502,7 +1502,9 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
lbool status = l_Undef;
lit* i;
-// printf( "Running SAT solver with parameters %d and %d and %d.\n", s->nLearntStart, s->nLearntDelta, s->nLearntRatio );
+ if ( s->fVerbose )
+ printf( "Running SAT solver with parameters %d and %d and %d.\n", s->nLearntStart, s->nLearntDelta, s->nLearntRatio );
+
////////////////////////////////////////////////
if ( s->fSolved )
{
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 0e456f46..58ea531c 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1574,6 +1574,7 @@ void sat_solver2_rollback( sat_solver2* s )
for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
s->wlists[i].size = 0;
+
// initialize other vars
s->size = s->iVarPivot;
if ( s->size == 0 )
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index bca9bc97..cba57638 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -212,6 +212,11 @@ static inline int sat_solver2_nclauses(sat_solver2* s)
return (int)s->stats.clauses;
}
+static inline int sat_solver2_nlearnts(sat_solver2* s)
+{
+ return (int)s->stats.learnts;
+}
+
static inline int sat_solver2_nconflicts(sat_solver2* s)
{
return (int)s->stats.conflicts;
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 14:14:00 +0000