Several small changes and fixes.

7 files changed, 46 insertions, 31 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 );
             }
         }
     }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 68d0e073..6caf37cb 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27891,7 +27891,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pAbc->pGia == NULL )
     {
         Abc_Print( -1, "There is no AIG.\n" );
-        return 1;
+        return 0;
     } 
     if ( Gia_ManRegNum(pAbc->pGia) == 0 )
     {
@@ -27971,12 +27971,12 @@ int Abc_CommandAbc9Vta2Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pAbc->pGia == NULL )
     {
         Abc_Print( -1, "Abc_CommandAbc9Vta2Gla(): There is no AIG.\n" );
-        return 1;
+        return 0;
     }
     if ( pAbc->pGia->vObjClasses == NULL )
     {
         Abc_Print( -1, "Abc_CommandAbc9Vta2Gla(): There is no variable-time-frame abstraction is defined.\n" );
-        return 1;
+        return 0;
     }
     Vec_IntFreeP( &pAbc->pGia->vGateClasses );
     pAbc->pGia->vGateClasses = Gia_VtaConvertToGla( pAbc->pGia, pAbc->pGia->vObjClasses );
@@ -28034,17 +28034,17 @@ int Abc_CommandAbc9Gla2Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pAbc->pGia == NULL )
     {
         Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): There is no AIG.\n" );
-        return 1;
+        return 0;
     }
     if ( pAbc->pGia->vGateClasses == NULL )
     {
         Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): There is no gate-level abstraction is defined.\n" );
-        return 1;
+        return 0;
     }
     if ( pAbc->nFrames < 1 )
     {
         Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): The number of timeframes (%d) should be a positive integer.\n", nFrames );
-        return 1;
+        return 0;
     }
     Vec_IntFreeP( &pAbc->pGia->vObjClasses );
     pAbc->pGia->vObjClasses = Gia_VtaConvertFromGla( pAbc->pGia, pAbc->pGia->vGateClasses, nFrames );
@@ -28091,12 +28091,12 @@ int Abc_CommandAbc9Fla2Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pAbc->pGia == NULL )
     {
         Abc_Print( -1, "Abc_CommandAbc9Fla2Gla(): There is no AIG.\n" );
-        return 1;
+        return 0;
     }
     if ( pAbc->pGia->vFlopClasses == NULL )
     {
         Abc_Print( -1, "Abc_CommandAbc9Fla2Gla(): There is no gate-level abstraction is defined.\n" );
-        return 1;
+        return 0;
     }
     Vec_IntFreeP( &pAbc->pGia->vGateClasses );
     pAbc->pGia->vGateClasses = Gia_FlaConvertToGla( pAbc->pGia, pAbc->pGia->vFlopClasses );
@@ -28142,12 +28142,12 @@ int Abc_CommandAbc9Gla2Fla( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pAbc->pGia == NULL )
     {
         Abc_Print( -1, "Abc_CommandAbc9Gla2Fla(): There is no AIG.\n" );
-        return 1;
+        return 0;
     }
     if ( pAbc->pGia->vGateClasses == NULL )
     {
         Abc_Print( -1, "Abc_CommandAbc9Gla2Fla(): There is no gate-level abstraction is defined.\n" );
-        return 1;
+        return 0;
     }
     Vec_IntFreeP( &pAbc->pGia->vFlopClasses );
     pAbc->pGia->vFlopClasses = Gia_GlaConvertToFla( pAbc->pGia, pAbc->pGia->vGateClasses );
@@ -28194,7 +28194,7 @@ int Abc_CommandAbc9Reparam( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pAbc->pGia == NULL )
     {
         Abc_Print( -1, "Abc_CommandAbc9Reparam(): There is no AIG.\n" );
-        return 1;
+        return 0;
     } 
     pTemp = Gia_ManReparam( pAbc->pGia, fVerbose );
     Abc_CommandUpdate9( pAbc, pTemp );
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index 680b1996..eeadf09e 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -396,11 +396,15 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
         if ( pNode->Id == 0 ) 
             continue;
         pNode->Id = Vec_SetAppendS( vProof, 2 + pNode->nEnts );
+        assert( pNode->Id > 0 );
         Vec_PtrPush( vUsed, pNode );
         // update fanins
         Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
             if ( (pNode->pEnts[k] & 1) == 0 ) // proof node
+            {
+                assert( pFanin->Id > 0 );
                 pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2);
+            }
 //            else // problem clause
 //                assert( (int*)pFanin >= Vec_IntArray(vClauses) && (int*)pFanin < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) );
     }
@@ -420,7 +424,6 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
         if ( pPivot && pPivot <= pNode )
         {
             RetValue = hTemp;
-//            s->iProofPivot = i;
             pPivot = NULL;
         }
     }
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 520e8284..eace9eea 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -30,7 +30,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "satVec.h"
 #include "satClause.h"
-#include "misc/vec/vecSet.h"
 
 ABC_NAMESPACE_HEADER_START
 
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index cb6199ec..2cd825b7 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -164,7 +164,7 @@ static inline void proof_chain_start( sat_solver2* s, clause* c )
     if ( s->fProofLogging )
     {
         int ProofId = clause2_proofid(s, c, 0);
-        assert( ProofId > 0 );
+        assert( (ProofId >> 2) > 0 );
         veci_resize( &s->temp_proof, 0 );
         veci_push( &s->temp_proof, 0 );
         veci_push( &s->temp_proof, 0 );
@@ -178,7 +178,7 @@ static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var )
     {
         clause* c = cls ? cls : var_unit_clause( s, Var );
         int ProofId = clause2_proofid(s, c, var_is_partA(s,Var));
-        assert( ProofId > 0 );
+        assert( (ProofId >> 2) > 0 );
         veci_push( &s->temp_proof, ProofId );
     }
 }
@@ -1417,7 +1417,10 @@ void sat_solver2_reducedb(sat_solver2* s)
             break;
     }
     if ( j < nLearnedOld / 6 )
+    {
+        ABC_FREE( pSortValues );
         return;
+    }
 
     // mark learned clauses to remove
     Counter = j = 0;
@@ -1439,6 +1442,7 @@ void sat_solver2_reducedb(sat_solver2* s)
             s->stats.learnts--;
         }
     }
+    ABC_FREE( pSortValues );
 //    if ( j == nLearnedOld )
 //        return;
 
@@ -1717,6 +1721,7 @@ void sat_solver2_verify( sat_solver2* s )
 //        Abc_Print(1, "Verification passed.\n" );
 }
 */
+
 // checks how many watched clauses are satisfied by 0-level assignments
 // (this procedure may be called before setting up a new bookmark for rollback)
 int sat_solver2_check_watched( sat_solver2* s )
@@ -1754,7 +1759,6 @@ int sat_solver2_check_watched( sat_solver2* s )
     return 0;
 }
 
-
 int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
 {
     int restart_iter = 0;