SAT variable profiling.

src/base/abci/abc.c

@@ -21479,7 +21479,7 @@ usage:
     Abc_Print( -2, "\t-I num : the number of PIs to abstract [default = %d]\n",                   pPars->nPisAbstract );
     Abc_Print( -2, "\t-P num : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearnedStart );
     Abc_Print( -2, "\t-Q num : delta value for learned clause removal [default = %d]\n",               pPars->nLearnedDelta );
-    Abc_Print( -2, "\t-R num : ratio percentage for learned clause removal [default = %d]\n",          pPars->nLearnedPerce );
+    Abc_Print( -2, "\t-R num : percentage to keep for learned clause removal [default = %d]\n",          pPars->nLearnedPerce );
     Abc_Print( -2, "\t-L file: the log file name [default = %s]\n",                               pLogFileName ? pLogFileName : "no logging" );
     Abc_Print( -2, "\t-a     : solve all outputs (do not stop when one is SAT) [default = %s]\n", pPars->fSolveAll? "yes": "no" );
     Abc_Print( -2, "\t-x     : toggle storing CEXes when solving all outputs [default = %s]\n",   pPars->fStoreCex? "yes": "no" );

src/sat/bmc/bmcBmc3.c

@@ -761,8 +761,14 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne )
 void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
 {
     if ( p->pPars->fVerbose )
-    printf( "Buffs = %d. Dups = %d.   Hash hits = %d.  Hash misses = %d.  Hash overs = %d.  UniProps = %d.\n", 
-        p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nHashOver, p->nUniProps );
+    {
+        int nUsedVars = sat_solver_count_usedvars(p->pSat);
+        printf( "LStart(P) = %d  LDelta(Q) = %d  LRatio(R) = %d  ReduceDB = %d  Vars = %d  Used = %d (%.2f %%)\n", 
+            p->pSat->nLearntStart, p->pSat->nLearntDelta, p->pSat->nLearntRatio, 
+            p->pSat->nDBreduces, p->pSat->size, nUsedVars, 100.0*nUsedVars/p->pSat->size );
+        printf( "Buffs = %d. Dups = %d.   Hash hits = %d.  Hash misses = %d.  Hash overs = %d.  UniProps = %d.\n", 
+            p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nHashOver, p->nUniProps );
+    }
 //    Aig_ManCleanMarkA( p->pAig );
     if ( p->vCexes )
     {
@@ -1642,7 +1648,7 @@ nTimeUndec += clock() - clk2;
             }
             printf( "%4d %s : ", f, fUnfinished ? "-" : "+" );
             printf( "Var =%8.0f. ", (double)p->nSatVars );
-            printf( "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
+//            printf( "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
             printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
             printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
 //            printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );