Version abc70930

1 files changed, 0 insertions, 721 deletions

diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
deleted file mode 100644
index a5fc7d58..00000000
--- a/src/aig/fra/fraImp.c
+++ /dev/null
@@ -1,721 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraImp.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    [Detecting and proving implications.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraImp.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of 1s in each siminfo of each node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Fra_SmlCountOnesOne( Fra_Sml_t * p, int Node )
-{
-    unsigned * pSim;
-    int k, Counter = 0;
-    pSim = Fra_ObjSim( p, Node );
-    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
-        Counter += Aig_WordCountOnes( pSim[k] );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of 1s in each siminfo of each node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i, * pnBits; 
-    pnBits = ALLOC( int, Aig_ManObjNumMax(p->pAig) );  
-    memset( pnBits, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
-    Aig_ManForEachObj( p->pAig, pObj, i )
-        pnBits[i] = Fra_SmlCountOnesOne( p, i );
-    return pnBits;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if implications holds.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right )
-{
-    unsigned * pSimL, * pSimR;
-    int k;
-    pSimL = Fra_ObjSim( p, Left );
-    pSimR = Fra_ObjSim( p, Right );
-    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
-        if ( pSimL[k] & ~pSimR[k] )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of 1s in the complement of the implication.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
-{
-    unsigned * pSimL, * pSimR;
-    int k, Counter = 0;
-    pSimL = Fra_ObjSim( p, Left );
-    pSimR = Fra_ObjSim( p, Right );
-    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
-        Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the complement of the implication.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Sml_NodeSaveNotImpPatterns( Fra_Sml_t * p, int Left, int Right, unsigned * pResult )
-{
-    unsigned * pSimL, * pSimR;
-    int k;
-    pSimL = Fra_ObjSim( p, Left );
-    pSimR = Fra_ObjSim( p, Right );
-    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
-        pResult[k] |= pSimL[k] & ~pSimR[k];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the array of nodes sorted by the number of 1s.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
-{
-    Aig_Obj_t * pObj;
-    Vec_Ptr_t * vNodes;
-    int i, nNodes, nTotal, nBits, * pnNodes, * pnBits, * pMemory;
-    assert( p->nWordsTotal > 0 );
-    // count 1s in each node's siminfo
-    pnBits = Fra_SmlCountOnes( p );
-    // count number of nodes having that many 1s
-    nNodes = 0;
-    nBits = p->nWordsTotal * 32;
-    pnNodes = ALLOC( int, nBits + 1 );
-    memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
-    Aig_ManForEachObj( p->pAig, pObj, i )
-    {
-        if ( i == 0 ) continue;
-        // skip non-PI and non-internal nodes
-        if ( fLatchCorr )
-        {
-            if ( !Aig_ObjIsPi(pObj) )
-                continue;
-        }
-        else
-        {
-            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
-                continue;
-        }
-        // skip nodes participating in the classes
-//        if ( Fra_ClassObjRepr(pObj) )
-//            continue;
-        assert( pnBits[i] <= nBits ); // "<" because of normalized info
-        pnNodes[pnBits[i]]++;
-        nNodes++;
-    }
-    // allocate memory for all the nodes
-    pMemory = ALLOC( int, nNodes + nBits + 1 );  
-    // markup the memory for each node
-    vNodes = Vec_PtrAlloc( nBits + 1 );
-    Vec_PtrPush( vNodes, pMemory );
-    for ( i = 1; i <= nBits; i++ )
-    {
-        pMemory += pnNodes[i-1] + 1;
-        Vec_PtrPush( vNodes, pMemory );
-    }
-    // add the nodes
-    memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
-    Aig_ManForEachObj( p->pAig, pObj, i )
-    {
-        if ( i == 0 ) continue;
-        // skip non-PI and non-internal nodes
-        if ( fLatchCorr )
-        {
-            if ( !Aig_ObjIsPi(pObj) )
-                continue;
-        }
-        else
-        {
-            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
-                continue;
-        }
-        // skip nodes participating in the classes
-//        if ( Fra_ClassObjRepr(pObj) )
-//            continue;
-        pMemory = Vec_PtrEntry( vNodes, pnBits[i] );
-        pMemory[ pnNodes[pnBits[i]]++ ] = i;
-    }
-    // add 0s in the end
-    nTotal = 0;
-    Vec_PtrForEachEntry( vNodes, pMemory, i )
-    {
-        pMemory[ pnNodes[i]++ ] = 0;
-        nTotal += pnNodes[i];
-    }
-    assert( nTotal == nNodes + nBits + 1 );
-    free( pnNodes );
-    free( pnBits );
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the array of implications with the highest cost.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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;
-    assert( Vec_IntSize(vImps) >= nImpLimit );
-    // count how many implications have each cost
-    pCostCount = ALLOC( int, nCostMax + 1 );
-    memset( pCostCount, 0, sizeof(int) * (nCostMax + 1) );
-    for ( i = 0; i < Vec_IntSize(vImps); i++ )
-    {
-        assert( pCosts[i] <= nCostMax );
-        pCostCount[ pCosts[i] ]++;
-    }
-    assert( pCostCount[0] == 0 );
-    // select the bound on the cost (above this bound, implication will be included)
-    nImpCount = 0;
-    for ( c = nCostMax; c > 0; c-- )
-    {
-        nImpCount += pCostCount[c];
-        if ( nImpCount >= nImpLimit )
-            break;
-    }
-//    printf( "Cost range >= %d.\n", c );
-    // collect implications with the given costs
-    vImpsNew = Vec_IntAlloc( nImpLimit );
-    Vec_IntForEachEntry( vImps, Imp, i )
-    {
-        if ( pCosts[i] < c )
-            continue;
-        Vec_IntPush( vImpsNew, Imp );
-        if ( Vec_IntSize( vImpsNew ) == nImpLimit )
-            break;
-    }
-    free( pCostCount );
-    if ( pCostRange )
-        *pCostRange = c;
-    return vImpsNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compares two implications using their largest ID.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 )
-{
-    int Max1 = AIG_MAX( pImp1[0], pImp1[1] );
-    int Max2 = AIG_MAX( pImp2[0], pImp2[1] );
-    if ( Max1 < Max2 )
-        return -1;
-    if ( Max1 > Max2  )
-        return 1;
-    return 0; 
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives implication candidates.]
-
-  Description [Implication candidates have the property that 
-  (1) they hold using sequential simulation information
-  (2) they do not hold using combinational simulation information
-  (3) they have as high expressive power as possible (heuristically)
-      that is, they are easy to disprove combinationally
-      meaning they cover relatively larger sequential subspace.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr )
-{
-    int nSimWords = 64;
-    Fra_Sml_t * pSeq, * pComb;
-    Vec_Int_t * vImps, * vTemp;
-    Vec_Ptr_t * vNodes;
-    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, CostRange, clk = clock();
-    assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
-    assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
-    // normalize both managers
-    pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
-    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1 );
-    // get the nodes sorted by the number of 1s
-    vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr );
-    // count the total number of implications
-    for ( k = nSimWords * 32; k > 0; k-- )
-    for ( i = k - 1; i > 0; i-- )
-    for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
-    for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
-        nImpsTotal++;
-
-    // compute implications and their costs
-    pImpCosts = ALLOC( int, nImpMaxLimit );
-    vImps = Vec_IntAlloc( nImpMaxLimit );
-    for ( k = pSeq->nWordsTotal * 32; k > 0; k-- )
-        for ( i = k - 1; i > 0; i-- )
-        {
-            for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
-            for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
-            {
-                nImpsTried++;
-                if ( !Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) )
-                {
-                    nImpsNonSeq++;
-                    continue;
-                }
-                if ( Sml_NodeCheckImp(pComb, *pNodesI, *pNodesK) )
-                {
-                    nImpsComb++;
-                    continue;
-                }
-                nImpsCollected++;
-                Imp = Fra_ImpCreate( *pNodesI, *pNodesK );
-                pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK);
-                CostMin = AIG_MIN( CostMin, pImpCosts[ Vec_IntSize(vImps) ] );
-                CostMax = AIG_MAX( CostMax, pImpCosts[ Vec_IntSize(vImps) ] );
-                Vec_IntPush( vImps, Imp );
-                if ( Vec_IntSize(vImps) == nImpMaxLimit )
-                    goto finish;
-            } 
-        }
-finish:
-    Fra_SmlStop( pComb );
-    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, &CostRange );
-        Vec_IntFree( vTemp );  
-    }
-
-    // dealloc
-    free( pImpCosts ); 
-    free( Vec_PtrEntry(vNodes, 0) );
-    Vec_PtrFree( vNodes );
-    // reorder implications topologically
-    qsort( (void *)Vec_IntArray(vImps), Vec_IntSize(vImps), sizeof(int), 
-            (int (*)(const void *, const void *)) Sml_CompareMaxId );
-if ( p->pPars->fVerbose )
-{
-printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n", 
-    nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected );
-printf( "Implication weight: Min = %d. Pivot = %d. Max = %d.   ", 
-       CostMin, CostRange, CostMax );
-PRT( "Time", clock() - clk );
-}
-    return vImps;
-}
-
-
-// the following three procedures are called to 
-// - add implications to the SAT solver
-// - check implications using the SAT solver
-// - refine implications using after a cex is generated
-
-/**Function*************************************************************
-
-  Synopsis    [Add implication clauses to the SAT solver.]
-
-  Description [Note that implications should be checked in the first frame!]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums )
-{
-    sat_solver * pSat = p->pSat;
-    Aig_Obj_t * pLeft, * pRight;
-    Aig_Obj_t * pLeftF, * pRightF;
-    int pLits[2], Imp, Left, Right, i, f, status;
-    int fComplL, fComplR;
-    Vec_IntForEachEntry( vImps, Imp, i )
-    {
-        // get the corresponding nodes
-        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
-        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
-        // check if all the nodes are present
-        for ( f = 0; f < p->pPars->nFramesK; f++ )
-        {
-            // map these info fraig
-            pLeftF = Fra_ObjFraig( pLeft, f );
-            pRightF = Fra_ObjFraig( pRight, f );
-            if ( Aig_ObjIsNone(Aig_Regular(pLeftF)) || Aig_ObjIsNone(Aig_Regular(pRightF)) )
-            {
-                Vec_IntWriteEntry( vImps, i, 0 );
-                break;
-            }
-        }
-        if ( f < p->pPars->nFramesK )
-            continue;
-        // add constraints in each timeframe
-        for ( f = 0; f < p->pPars->nFramesK; f++ )
-        {
-            // map these info fraig
-            pLeftF = Fra_ObjFraig( pLeft, f );
-            pRightF = Fra_ObjFraig( pRight, f );
-            // get the corresponding SAT numbers
-            Left = pSatVarNums[ Aig_Regular(pLeftF)->Id ];
-            Right = pSatVarNums[ Aig_Regular(pRightF)->Id ];
-            assert( Left > 0  && Left < p->nSatVars );
-            assert( Right > 0 && Right < p->nSatVars );
-            // get the complemented attributes
-            fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
-            fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
-            // get the constraint
-            // L => R      L' v R     (complement = L & R')
-            pLits[0] = 2 * Left  + !fComplL;
-            pLits[1] = 2 * Right +  fComplR;
-            // add contraint to solver
-            if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) )
-            {
-                sat_solver_delete( pSat );
-                p->pSat = NULL;
-                return;
-            }
-        }
-    }
-    status = sat_solver_simplify(pSat);
-    if ( status == 0 )
-    {
-        sat_solver_delete( pSat );
-        p->pSat = NULL;
-    }
-//    printf( "Total imps = %d. ", Vec_IntSize(vImps) );
-    Fra_ImpCompactArray( vImps );
-//    printf( "Valid imps = %d. \n", Vec_IntSize(vImps) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Check implications for the node (if they are present).]
-
-  Description [Returns the new position in the array.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos )
-{
-    Aig_Obj_t * pLeft, * pRight;
-    Aig_Obj_t * pLeftF, * pRightF;
-    int i, Imp, Left, Right, Max, RetValue;
-    int fComplL, fComplR;
-    Vec_IntForEachEntryStart( vImps, Imp, i, Pos )
-    {
-        if ( Imp == 0 )
-            continue;
-        Left = Fra_ImpLeft(Imp);
-        Right = Fra_ImpRight(Imp);
-        Max = AIG_MAX( Left, Right );
-        assert( Max >= pNode->Id );
-        if ( Max > pNode->Id )
-            return i;
-        // get the corresponding nodes
-        pLeft  = Aig_ManObj( p->pManAig, Left );
-        pRight = Aig_ManObj( p->pManAig, Right );
-        // get the corresponding FRAIG nodes
-        pLeftF  = Fra_ObjFraig( pLeft, p->pPars->nFramesK );
-        pRightF = Fra_ObjFraig( pRight, p->pPars->nFramesK );
-        // get the complemented attributes
-        fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
-        fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
-        // check equality
-        if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
-        {
-            if ( fComplL == fComplR ) // x => x  - always true
-                continue;
-            assert( fComplL != fComplR );
-            // consider 4 possibilities:
-            // NOT(1) => 1    or   0 => 1  - always true
-            // 1 => NOT(1)    or   1 => 0  - never true
-            // NOT(x) => x    or   x       - not always true
-            // x => NOT(x)    or   NOT(x)  - not always true
-            if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
-                continue;
-            // disproved implication
-            p->pCla->fRefinement = 1;
-            Vec_IntWriteEntry( vImps, i, 0 );
-            continue;
-        }
-        // check the implication 
-        // - if true, a clause is added
-        // - if false, a cex is simulated
-        // make sure the implication is refined
-        RetValue = Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR );
-        if ( RetValue != 1 )
-        {
-            p->pCla->fRefinement = 1;
-            if ( RetValue == 0 )
-                Fra_SmlResimulate( p );
-            if ( Vec_IntEntry(vImps, i) != 0 )
-                printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" );
-            assert( Vec_IntEntry(vImps, i) == 0 );
-        }
-    }
-    return i;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Removes those implications that no longer hold.]
-
-  Description [Returns 1 if refinement has happened.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps )
-{
-    Aig_Obj_t * pLeft, * pRight;
-    int Imp, i, RetValue = 0;
-    Vec_IntForEachEntry( vImps, Imp, i )
-    {
-        if ( Imp == 0 )
-            continue;
-        // get the corresponding nodes
-        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
-        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
-        // check if implication holds using this simulation info
-        if ( !Sml_NodeCheckImp(p->pSml, pLeft->Id, pRight->Id) )
-        {
-            Vec_IntWriteEntry( vImps, i, 0 );
-            RetValue = 1;
-        }
-    }
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Removes empty implications.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ImpCompactArray( Vec_Int_t * vImps )
-{
-    int i, k, Imp;
-    k = 0;
-    Vec_IntForEachEntry( vImps, Imp, i )
-        if ( Imp )
-            Vec_IntWriteEntry( vImps, k++, Imp );
-    Vec_IntShrink( vImps, k );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Determines the ratio of the state space by computed implications.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p )
-{
-    int nSimWords = 64;
-    Fra_Sml_t * pComb;
-    unsigned * pResult;
-    double Ratio = 0.0;
-    int Left, Right, Imp, i;
-    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
-        return Ratio;
-    // simulate the AIG manager with combinational patterns
-    pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
-    // go through the implications and collect where they do not hold
-    pResult = Fra_ObjSim( pComb, 0 );
-    assert( pResult[0] == 0 );
-    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
-    {
-        Left = Fra_ImpLeft(Imp);
-        Right = Fra_ImpRight(Imp);
-        Sml_NodeSaveNotImpPatterns( pComb, Left, Right, pResult );
-    }
-    // count the number of ones in this area
-    Ratio = 100.0 * Fra_SmlCountOnesOne( pComb, 0 ) / (32*(pComb->nWordsTotal-pComb->nWordsPref));
-    Fra_SmlStop( pComb );
-    return Ratio;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the number of failed implications.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
-{
-    int nFrames = 2000;
-    int nSimWords = 8;
-    Fra_Sml_t * pSeq;
-    char * pfFails;
-    int Left, Right, Imp, i, Counter;
-    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
-        return 0;
-    // simulate the AIG manager with combinational patterns
-    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords );
-    // go through the implications and check how many of them do not hold
-    pfFails = ALLOC( char, Vec_IntSize(p->pCla->vImps) );
-    memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) );
-    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
-    {
-        Left = Fra_ImpLeft(Imp);
-        Right = Fra_ImpRight(Imp);
-        pfFails[i] = !Sml_NodeCheckImp( pSeq, Left, Right );
-    }
-    // count how many has failed
-    Counter = 0;
-    for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ )
-        Counter += pfFails[i];
-    free( pfFails );
-    Fra_SmlStop( pSeq );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Record proven implications in the AIG manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew )
-{
-    Aig_Obj_t * pLeft, * pRight, * pMiter;
-    int nPosOld, Imp, i;
-    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
-        return;
-    // go through the implication
-    nPosOld = Aig_ManPoNum(pNew);
-    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
-    {
-        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
-        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
-        // record the implication: L' + R
-        pMiter = Aig_Or( pNew, 
-            Aig_NotCond(pLeft->pData, !pLeft->fPhase), 
-            Aig_NotCond(pRight->pData, pRight->fPhase) ); 
-        Aig_ObjCreatePo( pNew, pMiter );
-    }
-    pNew->nAsserts = Aig_ManPoNum(pNew) - nPosOld;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-