Version abc70822

abc.dsp

@@ -2814,6 +2814,10 @@ SOURCE=.\src\aig\aig\aigTruth.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\aig\aigTsim.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\aig\aigUtil.c
 # End Source File
 # Begin Source File

src/aig/aig/aig.h

@@ -359,6 +359,7 @@ extern Vec_Ptr_t *     Aig_ManDfsChoices( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfsReverse( Aig_Man_t * p );
 extern int             Aig_ManCountLevels( Aig_Man_t * p );
 extern int             Aig_DagSize( Aig_Obj_t * pObj );
+extern int             Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern void            Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
 extern Aig_Obj_t *     Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars );
 extern Aig_Obj_t *     Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
@@ -434,10 +435,9 @@ extern Aig_Man_t *     Aig_ManDupRepr( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManRehash( Aig_Man_t * p );
 extern void            Aig_ManCreateChoices( Aig_Man_t * p );
 /*=== aigRet.c ========================================================*/
-extern Aig_Man_t *     Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose );
+extern Aig_Man_t *     Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose );
 /*=== aigSeq.c ========================================================*/
 extern int             Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits );
-extern Aig_Man_t *     Aig_ManConstReduce( Aig_Man_t * p, int fVerbose );
 /*=== aigShow.c ========================================================*/
 extern void            Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold );
 /*=== aigTable.c ========================================================*/
@@ -458,6 +458,8 @@ extern void            Aig_ManVerifyLevel( Aig_Man_t * p );
 extern void            Aig_ManVerifyReverseLevel( Aig_Man_t * p );
 /*=== aigTruth.c ========================================================*/
 extern unsigned *      Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore );
+/*=== aigTsim.c ========================================================*/
+extern Aig_Man_t *     Aig_ManConstReduce( Aig_Man_t * p, int fVerbose );
 /*=== aigUtil.c =========================================================*/
 extern unsigned        Aig_PrimeCudd( unsigned p );
 extern void            Aig_ManIncrementTravId( Aig_Man_t * p );

src/aig/aig/aigDfs.c

@@ -380,6 +380,54 @@ int Aig_DagSize( Aig_Obj_t * pObj )
 
 /**Function*************************************************************
 
+  Synopsis    [Counts the support size of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_SupportSize_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int * pCounter )
+{
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        (*pCounter)++;
+        return;
+    }
+    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
+    Aig_SupportSize_rec( p, Aig_ObjFanin0(pObj), pCounter );
+    if ( Aig_ObjFanin1(pObj) )
+        Aig_SupportSize_rec( p, Aig_ObjFanin1(pObj), pCounter );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the support size of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    int Counter = 0;
+    assert( !Aig_IsComplement(pObj) );
+    assert( !Aig_ObjIsPo(pObj) );
+    Aig_ManIncrementTravId( p );
+    Aig_SupportSize_rec( p, pObj, &Counter );
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Transfers the AIG from one manager into another.]
 
   Description []

src/aig/aig/aigRepr.c

@@ -130,7 +130,7 @@ static inline Aig_Obj_t * Aig_ObjFindRepr( Aig_Man_t * p, Aig_Obj_t * pNode )
     assert( p->pReprs != NULL );
     assert( !Aig_IsComplement(pNode) );
     assert( pNode->Id < p->nReprsAlloc );
-    assert( !p->pReprs[pNode->Id] || p->pReprs[pNode->Id]->Id < pNode->Id );
+//    assert( !p->pReprs[pNode->Id] || p->pReprs[pNode->Id]->Id < pNode->Id );
     return p->pReprs[pNode->Id];
 }
 
@@ -210,12 +210,38 @@ void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p )
     assert( pNew->pReprs != NULL );
     // go through the nodes which have representatives
     Aig_ManForEachObj( p, pObj, k )
-        if ( pRepr = Aig_ObjFindRepr(p, pObj) )
+        if ( (pRepr = Aig_ObjFindRepr(p, pObj)) )
             Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) ); 
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG manager recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManDupRepr_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pRepr;
+    if ( pObj->pData )
+        return pObj->pData;
+    if ( (pRepr = Aig_ObjFindRepr(p, pObj)) )
+    {
+        Aig_ManDupRepr_rec( pNew, p, pRepr );
+        return pObj->pData = Aig_NotCond( pRepr->pData, pRepr->fPhase ^ pObj->fPhase );
+    }
+    Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin0(pObj) );
+    Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin1(pObj) );
+    return pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates AIG while substituting representatives.]
 
   Description []
@@ -227,27 +253,29 @@ void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p )
 ***********************************************************************/
 Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p )
 {
+    int fOrdered = 1;
     Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pRepr;
+    Aig_Obj_t * pObj;
     int i;
     // start the HOP package
     pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
     pNew->nRegs = p->nRegs;
     Aig_ManReprStart( pNew, Aig_ManObjIdMax(p)+1 );
     // map the const and primary inputs
+    Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
     Aig_ManForEachPi( p, pObj, i )
         pObj->pData = Aig_ObjCreatePi(pNew);
     // map the internal nodes
-//printf( "\n" );
-    Aig_ManForEachNode( p, pObj, i )
+    if ( fOrdered )
     {
-        pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) );
-        if ( pRepr = Aig_ObjFindRepr(p, pObj) ) // member of the class
-        {
-//printf( "Using node %d for node %d.\n", pRepr->Id, pObj->Id );
-            Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) );
-        }
+        Aig_ManForEachNode( p, pObj, i )
+            pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) );
+    }
+    else
+    {
+        Aig_ManForEachPo( p, pObj, i )
+            Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin0(pObj) );
     }
     // transfer the POs
     Aig_ManForEachPo( p, pObj, i )

src/aig/aig/aigSeq.c

@@ -24,70 +24,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define AIG_XVS0   1
-#define AIG_XVS1   2
-#define AIG_XVSX   3
-
-static inline void Aig_ObjSetXsim( Aig_Obj_t * pObj, int Value )  { pObj->nCuts = Value;  }
-static inline int  Aig_ObjGetXsim( Aig_Obj_t * pObj )             { return pObj->nCuts;   }
-static inline int  Aig_XsimInv( int Value )   
-{ 
-    if ( Value == AIG_XVS0 )
-        return AIG_XVS1;
-    if ( Value == AIG_XVS1 )
-        return AIG_XVS0;
-    assert( Value == AIG_XVSX );       
-    return AIG_XVSX;
-}
-static inline int  Aig_XsimAnd( int Value0, int Value1 )   
-{ 
-    if ( Value0 == AIG_XVS0 || Value1 == AIG_XVS0 )
-        return AIG_XVS0;
-    if ( Value0 == AIG_XVSX || Value1 == AIG_XVSX )
-        return AIG_XVSX;
-    assert( Value0 == AIG_XVS1 && Value1 == AIG_XVS1 );
-    return AIG_XVS1;
-}
-static inline int  Aig_XsimRand2()   
-{
-    return (rand() & 1) ? AIG_XVS1 : AIG_XVS0;
-}
-static inline int  Aig_XsimRand3()   
-{
-    int RetValue;
-    do { 
-        RetValue = rand() & 3; 
-    } while ( RetValue == 0 );
-    return RetValue;
-}
-static inline int  Aig_ObjGetXsimFanin0( Aig_Obj_t * pObj )       
-{ 
-    int RetValue;
-    RetValue = Aig_ObjGetXsim(Aig_ObjFanin0(pObj));
-    return Aig_ObjFaninC0(pObj)? Aig_XsimInv(RetValue) : RetValue;
-}
-static inline int  Aig_ObjGetXsimFanin1( Aig_Obj_t * pObj )       
-{ 
-    int RetValue;
-    RetValue = Aig_ObjGetXsim(Aig_ObjFanin1(pObj));
-    return Aig_ObjFaninC1(pObj)? Aig_XsimInv(RetValue) : RetValue;
-}
-static inline void Aig_XsimPrint( FILE * pFile, int Value )   
-{ 
-    if ( Value == AIG_XVS0 )
-    {
-        fprintf( pFile, "0" );
-        return;
-    }
-    if ( Value == AIG_XVS1 )
-    {
-        fprintf( pFile, "1" );
-        return;
-    }
-    assert( Value == AIG_XVSX );       
-    fprintf( pFile, "x" );
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -559,161 +495,6 @@ int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits )
 
 
 
-/**Function*************************************************************
-
-  Synopsis    [Cycles the circuit to create a new initial state.]
-
-  Description [Simulates the circuit with random input for the given 
-  number of timeframes to get a better initial state.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
-{
-    int nRounds = 1000; // limit on the number of ternary simulation rounds
-    Vec_Ptr_t * vMap;
-    Vec_Ptr_t * vStates;
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    unsigned * pState, * pPrev;
-    int i, k, f, fConstants, Value, nWords, nCounter;
-    // allocate storage for states
-    nWords  = Aig_BitWordNum( 2*Aig_ManRegNum(p) );
-    vStates = Vec_PtrAllocSimInfo( nRounds, nWords );
-    // initialize the values
-    Aig_ObjSetXsim( Aig_ManConst1(p), AIG_XVS1 );
-    Aig_ManForEachPiSeq( p, pObj, i )
-        Aig_ObjSetXsim( pObj, AIG_XVSX );
-    Aig_ManForEachLoSeq( p, pObj, i )
-        Aig_ObjSetXsim( pObj, AIG_XVS0 );
-    // simulate for the given number of timeframes
-    for ( f = 0; f < nRounds; f++ )
-    {
-        // collect this state
-        pState = Vec_PtrEntry( vStates, f );
-        memset( pState, 0, sizeof(unsigned) * nWords );
-        Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
-        {
-            Value = Aig_ObjGetXsim(pObjLo);
-            if ( Value & 1 )
-                Aig_InfoSetBit( pState, 2 * i );
-            if ( Value & 2 )
-                Aig_InfoSetBit( pState, 2 * i + 1 );
-//            Aig_XsimPrint( stdout, Value );
-        }
-//        printf( "\n" );
-        // check if this state exists
-        for ( i = f - 1; i >= 0; i-- )
-        {
-            pPrev = Vec_PtrEntry( vStates, i );
-            if ( !memcmp( pPrev, pState, sizeof(unsigned) * nWords ) )
-                break;
-        }
-        if ( i >= 0 )
-            break;
-        // simulate internal nodes
-        Aig_ManForEachNode( p, pObj, i )
-            Aig_ObjSetXsim( pObj, Aig_XsimAnd(Aig_ObjGetXsimFanin0(pObj), Aig_ObjGetXsimFanin1(pObj)) );
-        // transfer the latch values
-        Aig_ManForEachLiSeq( p, pObj, i )
-            Aig_ObjSetXsim( pObj, Aig_ObjGetXsimFanin0(pObj) );
-        Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
-            Aig_ObjSetXsim( pObjLo, Aig_ObjGetXsim(pObjLi) );
-    }
-    if ( f == nRounds )
-    {
-        printf( "Aig_ManTernarySimulate(): Did not reach a fixed point.\n" );
-        Vec_PtrFree( vStates );
-        return NULL;
-    }
-    // OR all the states
-    pState = Vec_PtrEntry( vStates, 0 );
-    for ( i = 1; i <= f; i++ )
-    {
-        pPrev = Vec_PtrEntry( vStates, i );
-        for ( k = 0; k < nWords; k++ )
-            pState[k] |= pPrev[k];
-    }
-    // check if there are constants
-    fConstants = 0;
-    if ( 2*Aig_ManRegNum(p) == 32*nWords )
-    {
-        for ( i = 0; i < nWords; i++ )
-            if ( pState[i] != ~0 )
-                fConstants = 1;
-    }
-    else
-    {
-        for ( i = 0; i < nWords - 1; i++ )
-            if ( pState[i] != ~0 )
-                fConstants = 1;
-        if ( pState[i] != Aig_InfoMask( 2*Aig_ManRegNum(p) - 32*(nWords-1) ) )
-            fConstants = 1;
-    }
-    if ( fConstants == 0 )
-    {
-        Vec_PtrFree( vStates );
-        return NULL;
-    }
-
-    // start mapping by adding the true PIs
-    vMap = Vec_PtrAlloc( Aig_ManPiNum(p) );
-    Aig_ManForEachPiSeq( p, pObj, i )
-        Vec_PtrPush( vMap, pObj );
-    // find constant registers
-    nCounter = 0;
-    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
-    {
-        Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
-        nCounter += (Value == 1 || Value == 2);
-        if ( Value == 1 )
-            Vec_PtrPush( vMap, Aig_ManConst0(p) );
-        else if ( Value == 2 )
-            Vec_PtrPush( vMap, Aig_ManConst1(p) );
-        else if ( Value == 3 )
-            Vec_PtrPush( vMap, pObjLo );
-        else
-            assert( 0 );
-//        Aig_XsimPrint( stdout, Value );
-    }
-//    printf( "\n" );
-    Vec_PtrFree( vStates );
-    if ( fVerbose )
-    printf( "Detected %d constants after %d iterations.\n", nCounter, f );
-    return vMap;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reduces the circuit using ternary simulation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose )
-{
-    Aig_Man_t * pTemp;
-    Vec_Ptr_t * vMap;
-    while ( vMap = Aig_ManTernarySimulate( p, fVerbose ) )
-    {
-        if ( fVerbose )
-        printf( "RBeg = %5d. NBeg = %6d.   ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
-        p = Aig_ManRemap( pTemp = p, vMap );
-        Aig_ManStop( pTemp );
-        Vec_PtrFree( vMap );
-        Aig_ManSeqCleanup( p );
-        if ( fVerbose )
-        printf( "REnd = %5d. NEnd = %6d.  \n", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
-    }
-    return p;
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/aig/module.make

@@ -13,5 +13,6 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigTable.c \
     src/aig/aig/aigTiming.c \
     src/aig/aig/aigTruth.c \
+    src/aig/aig/aigTsim.c \
     src/aig/aig/aigUtil.c \
     src/aig/aig/aigWin.c
\ No newline at end of file

src/aig/fra/fra.h

@@ -73,6 +73,7 @@ struct Fra_Par_t_
     int              nBTLimitMiter;     // conflict limit at an output
     int              nFramesP;          // the number of timeframes to in the prefix
     int              nFramesK;          // the number of timeframes to unroll
+    int              nMaxImps;          // the maximum number of implications to consider
     int              fRewrite;          // use rewriting for constraint reduction
     int              fLatchCorr;        // computes latch correspondence only
     int              fUseImps;          // use implications
@@ -133,6 +134,7 @@ struct Fra_Man_t_
     // counter example storage
     int              nPatWords;         // the number of words in the counter example
     unsigned *       pPatWords;         // the counter example
+    Vec_Int_t *      vCex;
     // satisfiability solving
     sat_solver *     pSat;              // SAT solver
     int              nSatVars;          // the number of variables currently used
@@ -226,6 +228,8 @@ extern int                 Fra_ClassesCountPairs( Fra_Cla_t * p );
 extern void                Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
 extern void                Fra_ClassesLatchCorr( Fra_Man_t * p );
 extern void                Fra_ClassesPostprocess( Fra_Cla_t * p );
+extern void                Fra_ClassesSelectRepr( Fra_Cla_t * p );
+extern Aig_Man_t *         Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK );
 /*=== fraCnf.c ========================================================*/
 extern void                Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 /*=== fraCore.c ========================================================*/
@@ -240,7 +244,7 @@ extern int                 Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps
 extern int                 Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps );
 extern void                Fra_ImpCompactArray( Vec_Int_t * vImps );
 /*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter );
+extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );

src/aig/fra/fraClass.c

@@ -114,9 +114,18 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed )
     int i;
     Aig_ManReprStart( p->pAig, Aig_ManObjIdMax(p->pAig) + 1 );
     memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p->pAig) + 1) );
+    if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 )
+    {
+        Aig_ManForEachObj( p->pAig, pObj, i )
+        {
+            if ( p->pAig->pReprs[i] != NULL )
+                printf( "Classes are not cleared!\n" );
+            assert( p->pAig->pReprs[i] == NULL );
+        }
+    }
     if ( vFailed )
-    Vec_PtrForEachEntry( vFailed, pObj, i )
-        p->pAig->pReprs[pObj->Id] = NULL;
+        Vec_PtrForEachEntry( vFailed, pObj, i )
+            p->pAig->pReprs[pObj->Id] = NULL;
 }
 
 /**Function*************************************************************
@@ -206,7 +215,7 @@ void Fra_PrintClass( Aig_Obj_t ** pClass )
         assert( Fra_ClassObjRepr(pTemp) == pClass[0] );
     printf( "{ " );
     for ( i = 0; pTemp = pClass[i]; i++ )
-        printf( "%d ", pTemp->Id, Fra_ClassObjRepr(pTemp)? Fra_ClassObjRepr(pTemp)->Id : -1 );
+        printf( "%d(%d) ", pTemp->Id, pTemp->Level );
     printf( "}\n" );
 }
 
@@ -227,8 +236,11 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
     Aig_Obj_t * pObj;
     int i;
 
-    printf( "Const = %5d. Class = %5d. Lit = %5d.\n", 
+    printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
         Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) );
+    if ( p->vImps && Vec_IntSize(p->vImps) > 0 )
+        printf( "Imp = %5d. ", Vec_IntSize(p->vImps) );
+    printf( "\n" );
 
     if ( fVeryVerbose )
     {
@@ -283,10 +295,10 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
         {
             if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
                 continue;
+            // skip the node with more that the given number of levels
+//            if ( pObj->Level > 3 )
+//                continue;
         }
-//printf( "%3d : ", pObj->Id );
-//Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 32 );
-//printf( "\n" );
         // hash the node by its simulation info
         iEntry = p->pFuncNodeHash( pObj, nTableSize );
         // check if the node belongs to the class of constant 1
@@ -494,7 +506,6 @@ int Fra_ClassesRefine( Fra_Cla_t * p )
     vTemp = p->vClassesTemp;
     p->vClassesTemp = p->vClasses;
     p->vClasses = vTemp;
-    p->fRefinement = (nRefis > 0);
     return nRefis;
 }
 
@@ -531,7 +542,6 @@ int Fra_ClassesRefine1( Fra_Cla_t * p )
     Vec_PtrShrink( p->vClasses1, k );
     if ( Vec_PtrSize(p->vClassNew) == 0 )
         return 0;
-    p->fRefinement = 1;
 /*
     printf( "Refined const-1 class: {" );
     Vec_PtrForEachEntry( p->vClassNew, pObj, i )
@@ -677,6 +687,95 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Postprocesses the classes by selecting representative lowest in top order.]
+
+  Description []
+               
+  SideEffects [] 
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClassesSelectRepr( Fra_Cla_t * p )
+{
+    Aig_Obj_t ** pClass, * pNodeMin;
+    int i, c, cMinSupp, nSuppSizeMin, nSuppSizeCur;
+    // reassign representatives in each class
+    Vec_PtrForEachEntry( p->vClasses, pClass, i )
+    {
+        // collect support sizes and find the min-support node
+        pNodeMin = NULL;
+        nSuppSizeMin = AIG_INFINITY;
+        for ( c = 0; pClass[c]; c++ )
+        {
+            nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] );
+//            nSuppSizeCur = 1;
+            if ( nSuppSizeMin > nSuppSizeCur || 
+                (nSuppSizeMin == nSuppSizeCur && pNodeMin->Level > pClass[c]->Level) )
+            {
+                nSuppSizeMin = nSuppSizeCur;
+                pNodeMin = pClass[c];
+                cMinSupp = c; 
+            }
+        }
+        // skip the case when the repr did not change
+        if ( cMinSupp == 0 )
+            continue;
+        // make the new node the representative of the class
+        pClass[cMinSupp] = pClass[0];
+        pClass[0] = pNodeMin;
+        // set the representative
+        for ( c = 0; pClass[c]; c++ )
+            Fra_ClassObjSetRepr( pClass[c], c? pClass[0] : NULL );
+    }
+}
+
+
+
+static inline Aig_Obj_t * Fra_ObjEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj )                       { return ppEquivs[pObj->Id];  }
+static inline void        Fra_ObjSetEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ppEquivs[pObj->Id] = pNode; }
+
+static inline Aig_Obj_t * Fra_ObjChild0Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj));  }
+static inline Aig_Obj_t * Fra_ObjChild1Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj));  }
+
+/**Function*************************************************************
+
+  Synopsis    [Add the node and its constraints to the new AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fra_ClassesDeriveNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, Aig_Obj_t ** ppEquivs )
+{
+    Aig_Obj_t * pObjNew, * pObjRepr, * pObjReprNew, * pMiter;//, * pObjNew2;
+    // skip nodes without representative
+    if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
+        return;
+    assert( pObjRepr->Id < pObj->Id );
+    // get the new node 
+    pObjNew = Fra_ObjEqu( ppEquivs, pObj );
+    // get the new node of the representative
+    pObjReprNew = Fra_ObjEqu( ppEquivs, pObjRepr );
+    // if this is the same node, no need to add constraints
+    if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
+        return;
+    // these are different nodes - perform speculative reduction
+//    pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
+    // set the new node
+//    Fra_ObjSetEqu( ppEquivs, pObj, pObjNew2 );
+    // add the constraint
+    pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
+    pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
+    pMiter = Aig_Not( pMiter );
+    Aig_ObjCreatePo( pManFraig, pMiter );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Derives AIG for the partitioned problem.]
 
   Description []
@@ -688,7 +787,60 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
 ***********************************************************************/
 Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
 {
-
+    Aig_Man_t * pManFraig;
+    Aig_Obj_t * pObj, * pObjNew;
+    Aig_Obj_t ** pLatches, ** ppEquivs;
+    int i, k, f, nFramesAll = nFramesK + 1;
+    assert( Aig_ManRegNum(p->pAig) > 0 );
+    assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+    assert( nFramesK > 0 );
+    // start the fraig package
+    pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pAig) + 1) * nFramesAll );
+    // allocate place for the node mapping
+    ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjIdMax(p->pAig) + 1 );
+    Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
+    // create latches for the first frame
+    Aig_ManForEachLoSeq( p->pAig, pObj, i )
+        Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
+    // add timeframes
+    pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
+    for ( f = 0; f < nFramesAll; f++ )
+    {
+        // create PIs for this frame
+        Aig_ManForEachPiSeq( p->pAig, pObj, i )
+            Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
+        // set the constraints on the latch outputs
+        Aig_ManForEachLoSeq( p->pAig, pObj, i )
+            Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( p->pAig, pObj, i )
+        {
+            pObjNew = Aig_And( pManFraig, Fra_ObjChild0Equ(ppEquivs, pObj), Fra_ObjChild1Equ(ppEquivs, pObj) );
+            Fra_ObjSetEqu( ppEquivs, pObj, pObjNew );
+            Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
+        }
+        if ( f == nFramesAll - 1 )
+            break;
+        if ( f == nFramesAll - 2 )
+            pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
+        // save the latch input values
+        k = 0;
+        Aig_ManForEachLiSeq( p->pAig, pObj, i )
+            pLatches[k++] = Fra_ObjChild0Equ( ppEquivs, pObj );
+        // insert them to the latch output values
+        k = 0;
+        Aig_ManForEachLoSeq( p->pAig, pObj, i )
+            Fra_ObjSetEqu( ppEquivs, pObj, pLatches[k++] );
+    }
+    free( pLatches );
+    free( ppEquivs );
+    // mark the asserts
+    assert( Aig_ManPoNum(pManFraig) % nFramesAll == 0 );
+printf( "Assert miters = %6d. Output miters = %6d.\n", 
+       pManFraig->nAsserts, Aig_ManPoNum(pManFraig) - pManFraig->nAsserts );
+    // remove dangling nodes
+    Aig_ManCleanup( pManFraig );
+    return pManFraig;
 }
 
 ////////////////////////////////////////////////////////////////////////

src/aig/fra/fraCore.c

@@ -24,6 +24,23 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+/* 
+    Speculating reduction in the sequential case leads to an interesting 
+    situation when a counter-ex may not refine any classes. This happens
+    for non-constant equivalence classes. In such cases the representative
+    of the class (proved by simulation to be non-constant) may be reduced 
+    to a constant during the speculative reduction. The fraig-representative 
+    of this representative node is a constant node, even though this is a 
+    non-constant class. Experiments have shown that this situation happens 
+    very often at the beginning of the refinement iteration when there are 
+    many spurious candidate equivalence classes (especially if heavy-duty 
+    simulatation of BMC was node used at the beginning). As a result, the 
+    SAT solver run may return a counter-ex that  distinguishes the given 
+    representative node from the constant-1 node but this counter-ex
+    does not distinguish the nodes in the non-costant class... This is why 
+    there is no check of refinment after a counter-ex in the sequential case.
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -117,6 +134,54 @@ static inline void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_
 
 /**Function*************************************************************
 
+  Synopsis    [Verifies the generated counter-ex.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_FraigVerifyCounterEx( Fra_Man_t * p, Vec_Int_t * vCex )
+{
+    Aig_Obj_t * pObj, ** ppClass;
+    int i, c;
+    assert( Aig_ManPiNum(p->pManAig) == Vec_IntSize(vCex) );
+    // make sure the input pattern is not used
+    Aig_ManForEachObj( p->pManAig, pObj, i )
+        assert( !pObj->fMarkB );
+    // simulate the cex through the AIG
+    Aig_ManConst1(p->pManAig)->fMarkB = 1;
+    Aig_ManForEachPi( p->pManAig, pObj, i )
+        pObj->fMarkB = Vec_IntEntry(vCex, i);
+    Aig_ManForEachNode( p->pManAig, pObj, i )
+        pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
+                       (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
+    Aig_ManForEachPo( p->pManAig, pObj, i )
+        pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
+    // check if the classes hold
+    Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
+    {
+        if ( pObj->fPhase != pObj->fMarkB )
+            printf( "The node %d is not constant under cex!\n", pObj->Id );
+    }
+    Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
+    {
+        for ( c = 1; ppClass[c]; c++ )
+            if ( (ppClass[0]->fPhase ^ ppClass[c]->fPhase) != (ppClass[0]->fMarkB ^ ppClass[c]->fMarkB) )
+                printf( "The nodes %d and %d are not equal under cex!\n", ppClass[0]->Id, ppClass[c]->Id );
+//        for ( c = 0; ppClass[c]; c++ )
+//            if ( Fra_ObjFraig(ppClass[c],p->pPars->nFramesK) == Aig_ManConst1(p->pManFraig) )
+//                printf( "A member of non-constant class has a constant repr!\n" );
+    }
+    // clean the simulation pattern
+    Aig_ManForEachObj( p->pManAig, pObj, i )
+        pObj->fMarkB = 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs fraiging for one node.]
 
   Description [Returns the fraiged node.]
@@ -173,47 +238,20 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
         Fra_FraigNodeSpeculate( p, pObj, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
         return;
     }
-//printf( "Disproved %d and %d.\n", pObj->Id, pObjRepr->Id );
     // disprove the nodes
+    p->pCla->fRefinement = 1;
     // if we do not include the node into those disproved, we may end up 
     // merging this node with another representative, for which proof has timed out
     if ( p->vTimeouts )
         Vec_PtrPush( p->vTimeouts, pObj );
+    // verify that the counter-example satisfies all the constraints
+//    if ( p->vCex )
+//    Fra_FraigVerifyCounterEx( p, p->vCex );
     // simulate the counter-example and return the Fraig node
     Fra_SmlResimulate( p );
-/*
-printf( "%d -> %d.\n", pObj->Id, pObjRepr->Id );
-Fra_ClassesPrint( p->pCla, 1 );
-printf( "%3d : ", 19 );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 19), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-printf( "%3d : ", 27 );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 27), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-printf( "%3d : ", 30 );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 30), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-printf( "\n\n" );
-*/
-    if ( Fra_ClassObjRepr(pObj) == pObjRepr )
-    {
-/*
-//Fra_ClassesPrint( p->pCla, 1 );
-//printf( "\n\n" );
-printf( "%3d : ", pObj->Id );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObj->Id), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-printf( "%3d : ", pObjRepr->Id );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObjRepr->Id), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-*/
-        if ( Aig_ObjIsPi(pObj) )
-            printf( "primary input\n" );
-        else
-            printf( "NOT primary input\n" );
+    if ( !p->pPars->nFramesK && Fra_ClassObjRepr(pObj) == pObjRepr )
         printf( "Fra_FraigNode(): Error in class refinement!\n" );
-    }
-    assert( Fra_ClassObjRepr(pObj) != pObjRepr );
+    assert( p->pPars->nFramesK || Fra_ClassObjRepr(pObj) != pObjRepr );
 }
 
 /**Function*************************************************************

src/aig/fra/fraImp.c

@@ -205,7 +205,7 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit )
+Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit, int * pCostRange )
 {
     Vec_Int_t * vImpsNew;
     int * pCostCount, nImpCount, Imp, i, c;
@@ -239,6 +239,8 @@ Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax,
             break;
     }
     free( pCostCount );
+    if ( pCostRange )
+        *pCostRange = c;
     return vImpsNew;
 }
 
@@ -290,7 +292,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
     int * pImpCosts, * pNodesI, * pNodesK;
     int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
     int CostMin = AIG_INFINITY, CostMax = 0;
-    int i, k, Imp, clk = clock();
+    int i, k, Imp, CostRange, clk = clock();
     assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
     // normalize both managers
     pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
@@ -350,9 +352,10 @@ finish:
     Fra_SmlStop( pSeq );
 
     // select implications with the highest cost
+    CostRange = CostMin;
     if ( Vec_IntSize(vImps) > nImpUseLimit )
     {
-        vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit );
+        vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit, &CostRange );
         Vec_IntFree( vTemp );  
     }
 
@@ -365,8 +368,8 @@ finish:
             (int (*)(const void *, const void *)) Sml_CompareMaxId );
 if ( p->pPars->fVerbose )
 {
-printf( "Tot = %d. Try = %d. NonS = %d. C = %d. Found = %d.  Cost = [%d - %d]  ", 
-    nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected, CostMin, CostMax );
+printf( "Tot = %d. Try = %d. NonS = %d. C = %d. Found = %d.  Cost = [%d < %d < %d] ", 
+    nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected, CostMin, CostRange, CostMax );
 PRT( "Time", clock() - clk );
 }
     return vImps;
@@ -381,7 +384,7 @@ PRT( "Time", clock() - clk );
 
   Synopsis    [Add implication clauses to the SAT solver.]
 
-  Description []
+  Description [Note that implications should be checked in the first frame!]
                
   SideEffects []
 
@@ -540,7 +543,6 @@ int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps )
         {
             Vec_IntWriteEntry( vImps, i, 0 );
             RetValue = 1;
-            p->pCla->fRefinement = 1;
         }
     }
     return RetValue;

src/aig/fra/fraInd.c

@@ -50,11 +50,9 @@ void Fra_FraigInductionRewrite( Fra_Man_t * p )
     pTemp = Aig_ManDup( p->pManFraig, 0 );
 //    pTemp = Dar_ManRwsat( pTemp, 1, 0 );
     pTemp = Dar_ManRewriteDefault( pTemp );
-
 //    printf( "Before = %6d.  After = %6d.\n", Aig_ManNodeNum(p->pManFraig), Aig_ManNodeNum(pTemp) ); 
 //Aig_ManDumpBlif( p->pManFraig, "1.blif" );
 //Aig_ManDumpBlif( pTemp, "2.blif" );
-
 //    Fra_FramesWriteCone( pTemp );
 //    Aig_ManStop( pTemp );
     // transfer PI/register pointers
@@ -128,8 +126,7 @@ static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * p
 Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
 {
     Aig_Man_t * pManFraig;
-    Aig_Obj_t * pObj, * pObjNew;
-    Aig_Obj_t ** pLatches;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
     int i, k, f;
     assert( p->pManFraig == NULL );
     assert( Aig_ManRegNum(p->pManAig) > 0 );
@@ -149,7 +146,6 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
         Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) );
 
     // add timeframes
-    pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pManAig) );
     for ( f = 0; f < p->nFramesAll - 1; f++ )
     {
         // set the constraints on the latch outputs
@@ -162,23 +158,15 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
             Fra_ObjSetFraig( pObj, f, pObjNew );
             Fra_FramesConstrainNode( pManFraig, pObj, f );
         }
-        // save the latch input values
-        k = 0;
-        Aig_ManForEachLiSeq( p->pManAig, pObj, i )
-            pLatches[k++] = Fra_ObjChild0Fra(pObj,f);
-        assert( k == Aig_ManRegNum(p->pManAig) );
-        // insert them to the latch output values
-        k = 0;
-        Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-            Fra_ObjSetFraig( pObj, f+1, pLatches[k++] );
-        assert( k == Aig_ManRegNum(p->pManAig) );
+        // transfer latch input to the latch outputs 
+        Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, k )
+            Fra_ObjSetFraig( pObjLo, f+1, Fra_ObjChild0Fra(pObjLi,f) );
     }
-    free( pLatches );
     // mark the asserts
     pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
-    // add the POs for the latch inputs
-    Aig_ManForEachLiSeq( p->pManAig, pObj, i )
-        Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f-1) );
+    // add the POs for the latch outputs of the last frame
+    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+        Aig_ObjCreatePo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) );
 
     // remove dangling nodes
     Aig_ManCleanup( pManFraig );
@@ -198,7 +186,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter )
 {
     int fUseSimpleCnf = 0;
     int fUseOldSimulation = 0;
@@ -229,6 +217,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
     Fra_ParamsDefaultSeq( pPars );
     pPars->nFramesP   = nFramesP;
     pPars->nFramesK   = nFramesK;
+    pPars->nMaxImps   = nMaxImps;
     pPars->fVerbose   = fVerbose;
     pPars->fRewrite   = fRewrite;
     pPars->fLatchCorr = fLatchCorr;
@@ -249,9 +238,16 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
     }
     else
     {
+        // bug:  r iscas/blif/s5378.blif    ; st; ssw -v
         // bug:  r iscas/blif/s1238.blif    ; st; ssw -v
         // refine the classes with more simulation rounds
-        p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 2 ); //pPars->nFramesK + 1, 6 );  // 32, 2 );
+if ( fVerbose )
+printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
+        p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1 ); //pPars->nFramesK + 1, 1 );  
+if ( fVerbose ) 
+{
+PRT( "Time", clock() - clk );
+}
         Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
 //        Fra_ClassesPostprocess( p->pCla );
         // allocate new simulation manager for simulating counter-examples
@@ -259,19 +255,26 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
         p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
     }
 
-    // perform BMC
-    Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK + 1 );
+    // perform BMC (for the min number of frames)
+    Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK );
 //Fra_ClassesPrint( p->pCla, 1 );
+//    p->vCex = Vec_IntAlloc( 1000 );
 
     // select the most expressive implications
     if ( pPars->fUseImps )
-        p->pCla->vImps = Fra_ImpDerive( p, 5000000, 5000, pPars->fLatchCorr );
+        p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr );
  
     p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
     p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
     p->nNodesBeg = Aig_ManNodeNum(pManAig);
     p->nRegsBeg  = Aig_ManRegNum(pManAig);
 
+    // dump AIG of the timeframes
+//    pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK );
+//    Aig_ManDumpBlif( pManAigNew, "frame_aig.blif" );
+//    Fra_ManPartitionTest2( pManAigNew );
+//    Aig_ManStop( pManAigNew );
+
     // iterate the inductive case
     p->pCla->fRefinement = 1;
     for ( nIter = 0; p->pCla->fRefinement; nIter++ )
@@ -341,7 +344,11 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
 
         // cleanup
         Fra_ManClean( p );
+//        if ( nIter == 3 )
+//            break;
     }
+//    Fra_ClassesPrint( p->pCla, 1 );
+//    Fra_ClassesSelectRepr( p->pCla );
     // move the classes into representatives and reduce AIG
 clk2 = clock();
     Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );

src/aig/fra/fraMan.c

@@ -248,6 +248,7 @@ void Fra_ManStop( Fra_Man_t * p )
     if ( p->pSat )      sat_solver_delete( p->pSat );
     if ( p->pCla  )     Fra_ClassesStop( p->pCla );
     if ( p->pSml )      Fra_SmlStop( p->pSml );
+    if ( p->vCex )      Vec_IntFree( p->vCex );
     FREE( p->pMemFraig );
     FREE( p->pMemFanins );
     FREE( p->pMemSatNums );

src/aig/fra/fraPart.c

@@ -170,6 +170,92 @@ PRT( "Scanning", clock() - clk );
 
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ManPartitionTest2( Aig_Man_t * p )
+{
+    Vec_Vec_t * vSupps, * vSuppsIn;
+    Vec_Int_t * vSup, * vSup2, * vSup3;
+    Aig_Obj_t * pObj;
+    int Entry, Entry2, Entry3, Counter;
+    int i, k, m, n, clk;
+    char * pSupp;
+ 
+    // compute supports
+clk = clock();
+    vSupps = Aig_ManSupports( p );
+PRT( "Supports", clock() - clk );
+    // remove last entry
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        vSup = Vec_VecEntry( vSupps, i );
+        Vec_IntPop( vSup );
+        // remember support
+//        pObj->pNext = (Aig_Obj_t *)vSup;
+    }
+
+    // create reverse supports
+clk = clock();
+    vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) );
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        if ( i == p->nAsserts )
+            break;
+        vSup = Vec_VecEntry( vSupps, i );
+        Vec_IntForEachEntry( vSup, Entry, k )
+            Vec_VecPush( vSuppsIn, Entry, (void *)i );
+    }
+PRT( "Inverse ", clock() - clk );
+
+    // create affective supports
+clk = clock();
+    pSupp = ALLOC( char, Aig_ManPiNum(p) );
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        if ( i % 50 != 0 )
+            continue;
+        vSup = Vec_VecEntry( vSupps, i );
+        memset( pSupp, 0, sizeof(char) * Aig_ManPiNum(p) );
+        // go through each input of this output
+        Vec_IntForEachEntry( vSup, Entry, k )
+        {
+            pSupp[Entry] = 1;
+            vSup2 = Vec_VecEntry( vSuppsIn, Entry );
+            // go though each assert of this input
+            Vec_IntForEachEntry( vSup2, Entry2, m )
+            {
+                vSup3 = Vec_VecEntry( vSupps, Entry2 );
+                // go through each input of this assert
+                Vec_IntForEachEntry( vSup3, Entry3, n )
+                {
+                    pSupp[Entry3] = 1;
+                }
+            }
+        }
+        // count the entries
+        Counter = 0;
+        for ( m = 0; m < Aig_ManPiNum(p); m++ )
+            Counter += pSupp[m];
+        printf( "%d(%d) ", Vec_IntSize(vSup), Counter );
+    }
+    printf( "\n" );
+PRT( "Extension ", clock() - clk );
+
+    free( pSupp );
+    Vec_VecFree( vSupps );
+    Vec_VecFree( vSuppsIn );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/fra/fraSec.c

@@ -43,11 +43,12 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
 {
     Aig_Man_t * pNew;
     int nFrames, RetValue, nIter, clk, clkTotal = clock();
+    int fLatchCorr = 0;
     if ( nFramesFix )
     {
         nFrames = nFramesFix;
         // perform seq sweeping for one frame number
-        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
+        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter );
     }
     else
     {
@@ -55,7 +56,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
         for ( nFrames = 1; ; nFrames++ )
         {
 clk = clock();
-            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
+            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter );
             RetValue = Fra_FraigMiterStatus( pNew );
             if ( fVerbose )
             {

src/aig/fra/fraSim.c

@@ -200,6 +200,17 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
         if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
             Aig_InfoSetBit( p->pPatWords, i );
 /*
+    if ( p->vCex )
+    {
+        Vec_IntClear( p->vCex );
+        for ( i = 0; i < Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ )
+            Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
+        for ( i = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManPiNum(p->pManFraig); i++ )
+            Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
+    }
+*/
+
+/*
     printf( "Pattern: " );
     Aig_ManForEachPi( p->pManFraig, pObj, i )
         printf( "%d", Aig_InfoHasBit( p->pPatWords, i ) );
@@ -601,7 +612,7 @@ clk = clock();
     if ( p->pCla->vImps )
         nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps );
 p->timeRef += clock() - clk;
-    if ( nChanges < 1 )
+    if ( !p->pPars->nFramesK && nChanges < 1 )
         printf( "Error: A counter-example did not refine classes!\n" );
 //    assert( nChanges >= 1 );
 //printf( "Refined classes = %5d.   Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges );

src/aig/ivy/ivyMan.c

@@ -411,7 +411,7 @@ int Ivy_ManLatchIsSelfFeed( Ivy_Obj_t * pLatch )
 int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel )
 {
     Ivy_Obj_t * pNode;
-    int LimitFactor = 10;
+    int LimitFactor = 100;
     int NodeBeg = Ivy_ManNodeNum(p);
     int nSteps;
     for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ )

src/base/abci/abc.c

@@ -6293,7 +6293,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
 //    pNtkRes = Abc_NtkDar( pNtk );
-    pNtkRes = Abc_NtkDarRetime( pNtk, 100, 1 );
+    pNtkRes = Abc_NtkDarRetime( pNtk, 1000, 1 );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -10974,12 +10974,13 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int nFramesP;
     int nFramesK;
+    int nMaxImps;
     int fExdc;
     int fUseImps;
     int fRewrite;
     int fLatchCorr;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -10988,13 +10989,14 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     nFramesP   = 0;
     nFramesK   = 1;
+    nMaxImps   = 5000;
     fExdc      = 1;
     fUseImps   = 0;
     fRewrite   = 0;
     fLatchCorr = 0;
     fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PFeirlvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PFIeirlvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -11020,6 +11022,17 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nFramesK <= 0 ) 
                 goto usage;
             break;
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nMaxImps = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nMaxImps <= 0 ) 
+                goto usage;
+            break;
         case 'e':
             fExdc ^= 1;
             break;
@@ -11061,7 +11074,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose );
+    pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -11072,10 +11085,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ssweep [-P num] [-F num] [-ilrvh]\n" );
+    fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrvh]\n" );
     fprintf( pErr, "\t         performs sequential sweep using K-step induction\n" );
     fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
     fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
+    fprintf( pErr, "\t-I num : max number of implications to consider [default = %d]\n", nMaxImps );
 //    fprintf( pErr, "\t-e     : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
     fprintf( pErr, "\t-i     : toggle using implications [default = %s]\n", fUseImps? "yes": "no" );
     fprintf( pErr, "\t-l     : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" );

src/base/abci/abcDar.c

@@ -892,11 +892,12 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose )
 {
     Fraig_Params_t Params;
     Abc_Ntk_t * pNtkAig, * pNtkFraig;
     Aig_Man_t * pMan, * pTemp;
+    int clk = clock();
 
     // preprocess the miter by fraiging it
     // (note that for each functional class, fraiging leaves one representative;
@@ -905,13 +906,17 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, in
     Params.nBTLimit = 100000;
     pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
 //    pNtkFraig = Abc_NtkDup( pNtk );
+if ( fVerbose ) 
+{
+PRT( "Initial fraiging time", clock() - clk );
+}
 
     pMan = Abc_NtkToDar( pNtkFraig, 1 );
     Abc_NtkDelete( pNtkFraig );
     if ( pMan == NULL )
         return NULL;
 
-    pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL );
+    pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL );
     Aig_ManStop( pTemp );
 
     if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
@@ -1033,7 +1038,7 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
     pMan = Abc_NtkToDar( pNtk, 1 );
     if ( pMan == NULL )
         return NULL;
-    pMan = Rtm_ManRetimeFwd( pTemp = pMan, nStepsMax, fVerbose );
+    pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, 0 );
     Aig_ManStop( pTemp );
 
 //    pMan = Aig_ManReduceLaches( pMan, 1 );

src/base/abci/abcPrint.c

@@ -127,13 +127,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
 /*
     {
         FILE * pTable;
-        pTable = fopen( "iscas/seqmap__stats.txt", "a+" );
+        pTable = fopen( "xs/reg_stats.txt", "a+" );
         fprintf( pTable, "%s ",  pNtk->pName );
-        fprintf( pTable, "%d ", Abc_NtkPiNum(pNtk) );
-        fprintf( pTable, "%d ", Abc_NtkPoNum(pNtk) );
         fprintf( pTable, "%d ", Abc_NtkLatchNum(pNtk) );
         fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) );
-        fprintf( pTable, "%d ", Abc_NtkLevel(pNtk) );
         fprintf( pTable, "\n" );
         fclose( pTable );
     }

todo.txt

@@ -21,3 +21,6 @@
 - comparing tts of differently derived the same cut
 - area flow based AIG rewriting
 - cut frontier adjustment
+
+
+