Fixing performance bug with old proof-logging (adding clauses multiple times).

src/aig/gia/giaAbsGla.c

@@ -1180,7 +1180,8 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
         Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) );
     }
     // other 
-    p->pSat      = sat_solver2_new();
+    p->pSat        = sat_solver2_new();
+//    p->pSat->pPrf1 = Vec_SetAlloc( 20 );
 //    p->pSat->fVerbose = p->pPars->fVerbose;
 //    sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax );
     p->pSat->nLearntStart = p->pPars->nLearnedStart;
@@ -1574,7 +1575,7 @@ void Gia_GlaAddToCounters( Gla_Man_t * p, Vec_Int_t * vCore )
 void Gia_GlaAddToAbs( Gla_Man_t * p, Vec_Int_t * vAbsAdd, int fCheck )
 {
     Gla_Obj_t * pGla;
-    int i, Counter = 0;
+    int i, k = 0;
     Gla_ManForEachObjAbsVec( vAbsAdd, p, pGla, i )
     {
         if ( fCheck )
@@ -1585,18 +1586,12 @@ void Gia_GlaAddToAbs( Gla_Man_t * p, Vec_Int_t * vAbsAdd, int fCheck )
         }
         if ( pGla->fAbs )
             continue;
-
-        if ( !fCheck )
-        {
-            Counter++;
-//            printf( "%d ", Gla_ObjId(p, pGla) );
-        }
-
         pGla->fAbs = 1;
         Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) );
+        // filter clauses to remove those contained in the abstraction
+        Vec_IntWriteEntry( vAbsAdd, k++, Gla_ObjId(p, pGla) );
     }
-//    if ( Counter )
+    Vec_IntShrink( vAbsAdd, k );
-//    printf( "  Total = %d\n", Counter );
 }
 void Gia_GlaAddTimeFrame( Gla_Man_t * p, int f )
 {
@@ -1951,16 +1946,14 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
 //            assert( (vCore != NULL) == (Status == 1) );
             if ( Status == -1 || (p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit) ) // resource limit is reached
             {
-                if ( p->pSat->pPrf2 )
+                Prf_ManStopP( &p->pSat->pPrf2 );
-                    Prf_ManStopP( &p->pSat->pPrf2 );
                 if ( Gia_ManRegNum(p->pGia) > 1 ) // for comb cases, return the abstration
                     Gla_ManRollBack( p );
                 goto finish;
             }
             if ( Status == 1 )
             {
-                if ( p->pSat->pPrf2 )
+                Prf_ManStopP( &p->pSat->pPrf2 );
-                    Prf_ManStopP( &p->pSat->pPrf2 );
                 p->timeUnsat += clock() - clk2;
                 break;
             } 
@@ -1987,8 +1980,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
                 vPPis = Gla_ManRefinement( p );
                 if ( vPPis == NULL )
                 {
-                    if ( p->pSat->pPrf2 )
+                    Prf_ManStopP( &p->pSat->pPrf2 );
-                        Prf_ManStopP( &p->pSat->pPrf2 );
                     pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
                     break;
                 }

src/misc/vec/vecInt.h

@@ -1053,6 +1053,28 @@ static inline int Vec_IntCountPositive( Vec_Int_t * p )
     return Counter;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Checks if two vectors are equal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntEqual( Vec_Int_t * p1, Vec_Int_t * p2 ) 
+{
+    int i;
+    if ( p1->nSize != p2->nSize )
+        return 0;
+    for ( i = 0; i < p1->nSize; i++ )
+        if ( p1->pArray[i] != p2->pArray[i] )
+            return 0;
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Counts the number of common entries.]

src/sat/bsat/satProof.c

@@ -921,6 +921,7 @@ void * Proof_DeriveCore( Vec_Set_t * vProof, int hRoot )
     // collect core clauses 
     vCore = Sat_ProofCollectCore( vProof, vUsed );
     Vec_IntFree( vUsed );
+    Vec_IntSort( vCore, 1 );
     return vCore;
 }