Version abc81029

1 files changed, 480 insertions, 35 deletions

diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index cfbba7e1..8498f59a 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -28,12 +28,315 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static inline char Saig_AbsVisited( Vec_Str_t * p, int nObjs, Aig_Obj_t * pObj, int i )    { return Vec_StrGetEntry( p, nObjs*i+pObj->Id );    }
+static inline void Saig_AbsSetVisited( Vec_Str_t * p, int nObjs, Aig_Obj_t * pObj, int i ) { Vec_StrSetEntry( p, nObjs*i+pObj->Id, (char)1 );  }
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Finds the set of clauses involved in the UNSAT core.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbose )
+{
+    Vec_Int_t * vCore;
+    void * pSatCnf; 
+    Intp_Man_t * pManProof;
+    int RetValue, clk = clock();
+    // solve the problem
+    RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 );
+    if ( RetValue == l_Undef )
+    {
+        printf( "Conflict limit is reached.\n" );
+        return NULL;
+    }
+    if ( RetValue == l_True )
+    {
+        printf( "The BMC problem is SAT.\n" );
+        return NULL;
+    }
+    if ( fVerbose )
+    {
+        printf( "SAT solver returned UNSAT after %d conflicts.  ", pSat->stats.conflicts );
+        PRT( "Time", clock() - clk );
+    }
+    assert( RetValue == l_False );
+    pSatCnf = sat_solver_store_release( pSat ); 
+    // derive the UNSAT core
+    clk = clock();
+    pManProof = Intp_ManAlloc();
+    vCore = Intp_ManUnsatCore( pManProof, pSatCnf, 0 );
+    Intp_ManFree( pManProof );
+    Sto_ManFree( pSatCnf );
+    if ( fVerbose )
+    {
+        printf( "SAT core contains %d clauses (out of %d).  ", Vec_IntSize(vCore), pSat->stats.clauses );
+        PRT( "Time", clock() - clk );
+    }
+    return vCore;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Mark visited nodes recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_AbsMarkVisited_rec( Aig_Man_t * p, Vec_Str_t * vObj2Visit, Aig_Obj_t * pObj, int i )
+{
+    if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, i ) )
+        return 1;
+    Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, i );
+    if ( Saig_ObjIsPi( p, pObj ) )
+        return 1;
+    if ( Saig_ObjIsLo( p, pObj ) )
+        return Saig_AbsMarkVisited_rec( p, vObj2Visit, Saig_ObjLoToLi(p, pObj), i-1 );
+    if ( Aig_ObjIsPo( pObj ) )
+        return Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin0(pObj), i );
+    Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin0(pObj), i );
+    Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin1(pObj), i );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Mark visited nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Str_t * Saig_AbsMarkVisited( Aig_Man_t * p, int nFramesMax )
+{
+    Vec_Str_t * vObj2Visit;
+    Aig_Obj_t * pObj;
+    int i, f;
+    vObj2Visit = Vec_StrStart( Aig_ManObjNumMax(p) * nFramesMax );
+    Saig_ManForEachLo( p, pObj, i )
+        Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, 0 ); 
+    for ( f = 0; f < nFramesMax; f++ )
+    {
+        Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), Aig_ManConst1(p), f );
+        Saig_ManForEachPo( p, pObj, i )
+            Saig_AbsMarkVisited_rec( p, vObj2Visit, pObj, f );
+    }
+    return vObj2Visit;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs the actual construction of the output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Saig_AbsCreateFrames_rec( Aig_Man_t * pFrame, Aig_Obj_t * pObj )
+{
+    if ( pObj->pData )
+        return pObj->pData;
+    assert( Aig_ObjIsNode(pObj) );
+    Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin0(pObj) );
+    Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin1(pObj) );
+    return pObj->pData = Aig_And( pFrame, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives a vector of AIG managers, one for each frame.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Saig_AbsCreateFrames( Aig_Man_t * p, int nFramesMax, int fVerbose )
+{
+    Vec_Ptr_t * vFrames, * vLoObjs, * vLiObjs;
+    Vec_Str_t * vObj2Visit;
+    Aig_Man_t * pFrame;
+    Aig_Obj_t * pObj;
+    int f, i;
+    vObj2Visit = Saig_AbsMarkVisited( p, nFramesMax );
+    vFrames = Vec_PtrAlloc( nFramesMax );
+    vLoObjs = Vec_PtrAlloc( 100 );
+    vLiObjs = Vec_PtrAlloc( 100 );
+    for ( f = 0; f < nFramesMax; f++ )
+    {
+        Aig_ManCleanData( p );
+        pFrame = Aig_ManStart( 1000 );
+        Aig_ManConst1(p)->pData = Aig_ManConst1(pFrame);
+        // create PIs
+        Vec_PtrClear( vLoObjs );
+        Vec_PtrClear( vLiObjs );
+        Aig_ManForEachPi( p, pObj, i )
+        {
+            if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, f ) )
+            {
+                pObj->pData = Aig_ObjCreatePi(pFrame);
+                if ( i >= Saig_ManPiNum(p) )
+                    Vec_PtrPush( vLoObjs, pObj );
+            }
+        }
+        // remember the number of (implicit) registers in this frame
+        pFrame->nAsserts = Vec_PtrSize(vLoObjs);
+        // create POs
+        Aig_ManForEachPo( p, pObj, i )
+            if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, f ) )
+            {
+                Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin0(pObj) );
+                pObj->pData = Aig_ObjCreatePo( pFrame, Aig_ObjChild0Copy(pObj) );
+                if ( i >= Saig_ManPoNum(p) )
+                    Vec_PtrPush( vLiObjs, pObj );
+            }
+        Vec_PtrPush( vFrames, Cnf_Derive(pFrame, Aig_ManPoNum(pFrame)) );
+        // set the new PIs to point to the recorresponding registers
+        Aig_ManCleanData( pFrame );
+        Vec_PtrForEachEntry( vLoObjs, pObj, i )
+            ((Aig_Obj_t *)pObj->pData)->pData = pObj;
+        Vec_PtrForEachEntry( vLiObjs, pObj, i )
+            ((Aig_Obj_t *)pObj->pData)->pData = pObj;
+        if ( fVerbose )
+            printf( "%3d : PI =%8d. PO =%8d. Flop =%8d. Node =%8d.\n", 
+                f, Aig_ManPiNum(pFrame), Aig_ManPoNum(pFrame), pFrame->nAsserts, Aig_ManNodeNum(pFrame) );
+    }
+    Vec_PtrFree( vLoObjs );
+    Vec_PtrFree( vLiObjs );
+    Vec_StrFree( vObj2Visit );
+    return vFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives a vector of AIG managers, one for each frame.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+sat_solver * Saig_AbsCreateSolverDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames )
+{
+    sat_solver * pSat;
+    Cnf_Dat_t * pCnf, * pCnfPrev;
+    Vec_Int_t * vPoLits;
+    Aig_Obj_t * pObjPo, * pObjLi, * pObjLo;
+    int f, i, Lit, Lits[2], iVarOld, iVarNew, nSatVars, nRegisters;
+    // start array of output literals
+    vPoLits = Vec_IntAlloc( 100 );
+    // count the number of CNF variables
+    nSatVars = 0;
+    Vec_PtrForEachEntry( vFrames, pCnf, f )
+        nSatVars += pCnf->nVars;
+
+    // create the SAT solver
+    pSat = sat_solver_new();
+    sat_solver_store_alloc( pSat ); 
+    sat_solver_setnvars( pSat, nSatVars );
+
+    // add clauses for the timeframes
+    nSatVars = 0;
+//    Vec_PtrForEachEntryReverse( vFrames, pCnf, f )
+    Vec_PtrForEachEntry( vFrames, pCnf, f )
+    {
+        // lift clauses of this CNF
+        Cnf_DataLift( pCnf, nSatVars );
+        nSatVars += pCnf->nVars;
+        // copy clauses into the manager
+        for ( i = 0; i < pCnf->nClauses; i++ )
+        {
+            if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
+            {
+                printf( "The BMC problem is trivially UNSAT.\n" );
+                sat_solver_delete( pSat );
+                Vec_IntFree( vPoLits );
+                return NULL;
+            }
+        }
+        // remember output literal
+        Aig_ManForEachPo( pCnf->pMan, pObjPo, i )
+        {
+            if ( i == Saig_ManPoNum(p) )
+                break;
+            Vec_IntPush( vPoLits, toLit(pCnf->pVarNums[pObjPo->Id]) );
+        }
+    }
+
+    // add auxiliary clauses (output, connectors, initial)
+    // add output clause
+    if ( !sat_solver_addclause( pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ) )
+        assert( 0 );
+    Vec_IntFree( vPoLits );
+
+    // add connecting clauses
+    pCnfPrev = Vec_PtrEntry( vFrames, 0 );
+    Vec_PtrForEachEntryStart( vFrames, pCnf, f, 1 )
+    {
+        nRegisters = pCnf->pMan->nAsserts;
+        assert( nRegisters <= Aig_ManPoNum(pCnfPrev->pMan) );
+        assert( nRegisters <= Aig_ManPiNum(pCnf->pMan) );
+        for ( i = 0; i < nRegisters; i++ )
+        {
+            pObjLi = Aig_ManPo( pCnfPrev->pMan, Aig_ManPoNum(pCnfPrev->pMan) - nRegisters + i );
+            pObjLo = Aig_ManPi( pCnf->pMan,     Aig_ManPiNum(pCnf->pMan) -     nRegisters + i );
+            // get variable numbers
+            iVarOld = pCnfPrev->pVarNums[pObjLi->Id];
+            iVarNew = pCnf->pVarNums[pObjLo->Id];
+            // add clauses connecting existing variables
+            Lits[0] = toLitCond( iVarOld, 0 );
+            Lits[1] = toLitCond( iVarNew, 1 );
+            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+                assert( 0 );
+            Lits[0] = toLitCond( iVarOld, 1 );
+            Lits[1] = toLitCond( iVarNew, 0 );
+            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+                assert( 0 );
+        }
+        pCnfPrev = pCnf;
+    }
+    // add unit clauses
+    pCnf = Vec_PtrEntry( vFrames, 0 );
+    nRegisters = pCnf->pMan->nAsserts;
+    for ( i = 0; i < nRegisters; i++ )
+    {
+        pObjLo = Aig_ManPi( pCnf->pMan, Aig_ManPiNum(pCnf->pMan) - nRegisters + i );
+        assert( pCnf->pVarNums[pObjLo->Id] >= 0 );
+        Lit = toLitCond( pCnf->pVarNums[pObjLo->Id], 1 );
+        if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
+            assert( 0 );
+    }
+    sat_solver_store_mark_roots( pSat ); 
+    return pSat;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Creates SAT solver for BMC.]
 
   Description []
@@ -123,7 +426,7 @@ sat_solver * Saig_AbsCreateSolver( Cnf_Dat_t * pCnf, int nFrames )
 
 /**Function*************************************************************
 
-  Synopsis    [Finds the set of clauses involved in the UNSAT core.]
+  Synopsis    [Performs proof-based abstraction using BMC of the given depth.]
 
   Description []
                
@@ -132,37 +435,78 @@ sat_solver * Saig_AbsCreateSolver( Cnf_Dat_t * pCnf, int nFrames )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbose )
+Vec_Int_t * Saig_AbsCollectRegistersDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames, Vec_Int_t * vCore )
 {
-    Vec_Int_t * vCore;
-    void * pSatCnf; 
-    Intp_Man_t * pManProof;
-    int RetValue;
-    // solve the problem
-    RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 );
-    if ( RetValue == l_Undef )
+    Aig_Obj_t * pObj;
+    Cnf_Dat_t * pCnf;
+    Vec_Int_t * vFlops;
+    int * pVars, * pFlops;
+    int i, f, iClause, iReg, * piLit, nSatVars, nSatClauses;
+    // count the number of CNF variables
+    nSatVars = 0;
+    Vec_PtrForEachEntry( vFrames, pCnf, f )
+        nSatVars += pCnf->nVars;
+    // mark register variables
+    pVars = ALLOC( int, nSatVars );
+    for ( i = 0; i < nSatVars; i++ )
+        pVars[i] = -1;
+    Vec_PtrForEachEntry( vFrames, pCnf, f )
     {
-        printf( "Conflict limit is reached.\n" );
-        return NULL;
+        Aig_ManForEachPi( pCnf->pMan, pObj, i )
+        {
+            assert( pCnf->pVarNums[pObj->Id] >= 0 );
+            assert( pCnf->pVarNums[pObj->Id] < nSatVars );
+            if ( pObj->pData == NULL )
+                continue;
+            iReg = Aig_ObjPioNum(pObj->pData) - Saig_ManPiNum(p);
+            assert( iReg >= 0 && iReg < Aig_ManRegNum(p) );
+            pVars[ pCnf->pVarNums[pObj->Id] ] = iReg;
+        }
+        Aig_ManForEachPo( pCnf->pMan, pObj, i )
+        {
+            assert( pCnf->pVarNums[pObj->Id] >= 0 );
+            assert( pCnf->pVarNums[pObj->Id] < nSatVars );
+            if ( pObj->pData == NULL )
+                continue;
+            iReg = Aig_ObjPioNum(pObj->pData) - Saig_ManPoNum(p);
+            assert( iReg >= 0 && iReg < Aig_ManRegNum(p) );
+            pVars[ pCnf->pVarNums[pObj->Id] ] = iReg;
+        }
     }
-    if ( RetValue == l_True )
+    // mark used registers
+    pFlops = CALLOC( int, Aig_ManRegNum(p) );
+    Vec_IntForEachEntry( vCore, iClause, i )
     {
-        printf( "The BMC problem is SAT.\n" );
-        return NULL;
+        nSatClauses = 0;
+        Vec_PtrForEachEntry( vFrames, pCnf, f )
+        {
+            if ( iClause < nSatClauses + pCnf->nClauses )
+                break;
+            nSatClauses += pCnf->nClauses;
+        }
+        if ( f == Vec_PtrSize(vFrames) )
+            continue;
+        iClause = iClause - nSatClauses;
+        assert( iClause >= 0 );
+        assert( iClause < pCnf->nClauses );
+        // consider the clause
+        for ( piLit = pCnf->pClauses[iClause]; piLit < pCnf->pClauses[iClause+1]; piLit++ )
+        {
+            iReg = pVars[ lit_var(*piLit) ];
+            if ( iReg >= 0 )
+                pFlops[iReg] = 1;
+        }
     }
-    if ( fVerbose )
-        printf( "SAT solver returned UNSAT after %d conflicts.\n", pSat->stats.conflicts );
-    assert( RetValue == l_False );
-    pSatCnf = sat_solver_store_release( pSat ); 
-    // derive the UNSAT core
-    pManProof = Intp_ManAlloc();
-    vCore = Intp_ManUnsatCore( pManProof, pSatCnf, fVerbose );
-    Intp_ManFree( pManProof );
-    Sto_ManFree( pSatCnf );
-    return vCore;
+    // collect registers
+    vFlops = Vec_IntAlloc( Aig_ManRegNum(p) );
+    for ( i = 0; i < Aig_ManRegNum(p); i++ )
+        if ( pFlops[i] )
+            Vec_IntPush( vFlops, i );
+    free( pFlops );
+    free( pVars );
+    return vFlops;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Performs proof-based abstraction using BMC of the given depth.]
@@ -225,39 +569,139 @@ Vec_Int_t * Saig_AbsCollectRegisters( Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t *
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose )
+void Saig_AbsFreeCnfs( Vec_Ptr_t * vFrames )
+{
+    Cnf_Dat_t * pCnf;
+    int i;
+    Vec_PtrForEachEntry( vFrames, pCnf, i )
+    {
+        Aig_ManStop( pCnf->pMan );
+        Cnf_DataFree( pCnf );
+    }
+    Vec_PtrFree( vFrames );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs proof-based abstraction using BMC of the given depth.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_AbsExtendOneStep( Aig_Man_t * p, Vec_Int_t * vFlops )
+{
+    Vec_Ptr_t * vFlopPtrs, * vSupp;
+    Aig_Obj_t * pObj;
+    int i, Entry;
+    // collect latch inputs
+    vFlopPtrs = Vec_PtrAlloc( 1000 );
+    Vec_IntForEachEntry( vFlops, Entry, i )
+    {
+        Vec_PtrPush( vFlopPtrs, Saig_ManLi(p, Entry) );
+        pObj = Saig_ManLo(p, Entry);
+        pObj->fMarkA = 1;
+    }
+    // collect latch outputs
+    vSupp = Vec_PtrAlloc( 1000 );
+    Aig_SupportNodes( p, (Aig_Obj_t **)Vec_PtrArray(vFlopPtrs), Vec_PtrSize(vFlopPtrs), vSupp );
+    Vec_PtrFree( vFlopPtrs );
+    // mark influencing flops
+    Vec_PtrForEachEntry( vSupp, pObj, i )
+        pObj->fMarkA = 1;
+    Vec_PtrFree( vSupp );
+    // reload flops
+    Vec_IntClear( vFlops );
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        if ( pObj->fMarkA == 0 )
+            continue;
+        pObj->fMarkA = 0;
+        if ( Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) >= 0 )
+            Vec_IntPush( vFlops, Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs proof-based abstraction using BMC of the given depth.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fVerbose )
 {
     Aig_Man_t * pResult;
     Cnf_Dat_t * pCnf;
+    Vec_Ptr_t * vFrames;
     sat_solver * pSat;
     Vec_Int_t * vCore;
     Vec_Int_t * vFlops;
-    int clk = clock();
+    int clk = clock(), clk2 = clock();
     assert( Aig_ManRegNum(p) > 0 );
     Aig_ManSetPioNumbers( p );
     if ( fVerbose )
         printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax );
-    // create CNF for the AIG
-    pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) );
-    // create SAT solver for the unrolled AIG
-    pSat = Saig_AbsCreateSolver( pCnf, nFrames );
+    if ( fDynamic )
+    {
+        // create CNF for the frames
+        vFrames = Saig_AbsCreateFrames( p, nFrames, fVerbose );
+        // create dynamic solver
+        pSat = Saig_AbsCreateSolverDyn( p, vFrames );
+    }
+    else
+    {
+        // create CNF for the AIG
+        pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) );
+        // create SAT solver for the unrolled AIG
+        pSat = Saig_AbsCreateSolver( pCnf, nFrames );
+    }
+    if ( fVerbose )
+    {
+        printf( "SAT solver: Vars = %7d. Clauses = %7d.  ", pSat->size, pSat->stats.clauses );
+        PRT( "Time", clock() - clk2 );
+    }
     // compute UNSAT core
     vCore = Saig_AbsSolverUnsatCore( pSat, nConfMax, fVerbose );
     sat_solver_delete( pSat );
     if ( vCore == NULL )
     {
-        Cnf_DataFree( pCnf );
+        Saig_AbsFreeCnfs( vFrames );
         return NULL;
     }
     // collect registers
-    vFlops = Saig_AbsCollectRegisters( pCnf, nFrames, vCore );
-    Cnf_DataFree( pCnf );
+    if ( fDynamic )
+    {
+        vFlops = Saig_AbsCollectRegistersDyn( p, vFrames, vCore );
+        Saig_AbsFreeCnfs( vFrames );
+    }
+    else
+    {
+        vFlops = Saig_AbsCollectRegisters( pCnf, nFrames, vCore );
+        Cnf_DataFree( pCnf );
+    }
     Vec_IntFree( vCore );
     if ( fVerbose )
     {
-        printf( "The number of relevant registers is %d (out of %d).\n", Vec_IntSize(vFlops), Aig_ManRegNum(p) );
+        printf( "The number of relevant registers is %d (out of %d).  ", Vec_IntSize(vFlops), Aig_ManRegNum(p) );
         PRT( "Time", clock() - clk );
     }
+    // extend the abstraction
+    if ( fExtend )
+    {
+        if ( fVerbose )
+            printf( "Support extended from %d flops to", Vec_IntSize(vFlops) );
+        Saig_AbsExtendOneStep( p, vFlops );
+        if ( fVerbose )
+            printf( " %d flops.\n", Vec_IntSize(vFlops) );
+    }
     // create the resulting AIG
     pResult = Saig_ManAbstraction( p, vFlops );
     Vec_IntFree( vFlops );
@@ -265,6 +709,7 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
 }
 
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////