Major restructuring of the code.

1 files changed, 0 insertions, 477 deletions

diff --git a/src/aig/ssw/sswPairs.c b/src/aig/ssw/sswPairs.c
deleted file mode 100644
index 0aba942f..00000000
--- a/src/aig/ssw/sswPairs.c
+++ /dev/null
@@ -1,477 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [sswPairs.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Inductive prover with constraints.]
-
-  Synopsis    [Calls to the SAT solver.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - September 1, 2008.]
-
-  Revision    [$Id: sswPairs.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "sswInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Reports the status of the miter.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ssw_MiterStatus( Aig_Man_t * p, int fVerbose )
-{
-    Aig_Obj_t * pObj, * pChild;
-    int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
-//    if ( p->pData )
-//        return 0;
-    Saig_ManForEachPo( p, pObj, i )
-    {
-        pChild = Aig_ObjChild0(pObj);
-        // check if the output is constant 0
-        if ( pChild == Aig_ManConst0(p) )
-        {
-            CountConst0++;
-            continue;
-        }
-        // check if the output is constant 1
-        if ( pChild == Aig_ManConst1(p) )
-        {
-            CountNonConst0++;
-            continue;
-        }
-        // check if the output is a primary input
-        if ( p->nRegs == 0 && Aig_ObjIsPi(Aig_Regular(pChild)) )
-        {
-            CountNonConst0++;
-            continue;
-        }
-        // check if the output can be not constant 0
-        if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
-        {
-            CountNonConst0++;
-            continue;
-        }
-        CountUndecided++;
-    }
-
-    if ( fVerbose )
-    {
-        printf( "Miter has %d outputs. ", Saig_ManPoNum(p) );
-        printf( "Const0 = %d.  ", CountConst0 );
-        printf( "NonConst0 = %d.  ", CountNonConst0 );
-        printf( "Undecided = %d.  ", CountUndecided );
-        printf( "\n" );
-    }
-
-    if ( CountNonConst0 )
-        return 0;
-    if ( CountUndecided )
-        return -1;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transfer equivalent pairs to the miter.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Ssw_TransferSignalPairs( Aig_Man_t * pMiter, Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2 )
-{
-    Vec_Int_t * vIds;
-    Aig_Obj_t * pObj1, * pObj2;
-    Aig_Obj_t * pObj1m, * pObj2m;
-    int i;
-    vIds = Vec_IntAlloc( 2 * Vec_IntSize(vIds1) );
-    for ( i = 0; i < Vec_IntSize(vIds1); i++ )
-    {
-        pObj1 = Aig_ManObj( pAig1, Vec_IntEntry(vIds1, i) );
-        pObj2 = Aig_ManObj( pAig2, Vec_IntEntry(vIds2, i) );
-        pObj1m = Aig_Regular((Aig_Obj_t *)pObj1->pData);
-        pObj2m = Aig_Regular((Aig_Obj_t *)pObj2->pData);
-        assert( pObj1m && pObj2m );
-        if ( pObj1m == pObj2m )
-            continue;
-        if ( pObj1m->Id < pObj2m->Id )
-        {
-            Vec_IntPush( vIds, pObj1m->Id );
-            Vec_IntPush( vIds, pObj2m->Id );
-        }
-        else
-        {
-            Vec_IntPush( vIds, pObj2m->Id );
-            Vec_IntPush( vIds, pObj1m->Id );
-        }
-    }
-    return vIds;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transform pairs into class representation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t ** Ssw_TransformPairsIntoTempClasses( Vec_Int_t * vPairs, int nObjNumMax )
-{
-    Vec_Int_t ** pvClasses;   // vector of classes
-    int * pReprs;             // mapping nodes into their representatives
-    int Entry, idObj, idRepr, idReprObj, idReprRepr, i;
-    // allocate data-structures
-    pvClasses = ABC_CALLOC( Vec_Int_t *, nObjNumMax );
-    pReprs    = ABC_ALLOC( int, nObjNumMax );
-    for ( i = 0; i < nObjNumMax; i++ )
-        pReprs[i] = -1;
-    // consider pairs
-    for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
-    {
-        // get both objects
-        idRepr = Vec_IntEntry( vPairs, i   );
-        idObj  = Vec_IntEntry( vPairs, i+1 );
-        assert( idObj > 0 );
-        assert( (pReprs[idRepr] == -1) || (pvClasses[pReprs[idRepr]] != NULL) );
-        assert( (pReprs[idObj]  == -1) || (pvClasses[pReprs[idObj] ] != NULL) );
-        // get representatives of both objects
-        idReprRepr = pReprs[idRepr];
-        idReprObj  = pReprs[idObj];
-        // check different situations
-        if ( idReprRepr == -1 && idReprObj == -1 )
-        {   // they do not have classes
-            // create a class
-            pvClasses[idRepr] = Vec_IntAlloc( 4 );
-            Vec_IntPush( pvClasses[idRepr], idRepr );
-            Vec_IntPush( pvClasses[idRepr], idObj );
-            pReprs[ idRepr ] = idRepr;
-            pReprs[ idObj  ] = idRepr;
-        }
-        else if ( idReprRepr >= 0 && idReprObj == -1 )
-        {   // representative has a class
-            // add iObj to the same class
-            Vec_IntPushUniqueOrder( pvClasses[idReprRepr], idObj );
-            pReprs[ idObj ] = idReprRepr;
-        }
-        else if ( idReprRepr == -1 && idReprObj >= 0 )
-        {   // object has a class
-            assert( idReprObj != idRepr );
-            if ( idReprObj < idRepr ) 
-            { // add idRepr to the same class
-                Vec_IntPushUniqueOrder( pvClasses[idReprObj], idRepr );
-                pReprs[ idRepr ] = idReprObj;
-            }
-            else // if ( idReprObj > idRepr ) 
-            { // make idRepr new representative
-                Vec_IntPushFirst( pvClasses[idReprObj], idRepr );
-                pvClasses[idRepr] = pvClasses[idReprObj];
-                pvClasses[idReprObj] = NULL;
-                // set correct representatives of each node
-                Vec_IntForEachEntry( pvClasses[idRepr], Entry, i )
-                    pReprs[ Entry ] = idRepr;
-            }
-        }
-        else // if ( idReprRepr >= 0 && idReprObj >= 0 )
-        {   // both have classes
-            if ( idReprRepr == idReprObj )
-            {  // the classes are the same
-                // nothing to do
-            }
-            else
-            {  // the classes are different
-                // find the repr of the new class
-                if ( idReprRepr < idReprObj )
-                {
-                    Vec_IntForEachEntry( pvClasses[idReprObj], Entry, i )
-                    {
-                        Vec_IntPushUniqueOrder( pvClasses[idReprRepr], Entry );
-                        pReprs[ Entry ] = idReprRepr;
-                    }
-                    Vec_IntFree( pvClasses[idReprObj] );
-                    pvClasses[idReprObj] = NULL;
-                }
-                else // if ( idReprRepr > idReprObj )
-                {
-                    Vec_IntForEachEntry( pvClasses[idReprRepr], Entry, i )
-                    {
-                        Vec_IntPushUniqueOrder( pvClasses[idReprObj], Entry );
-                        pReprs[ Entry ] = idReprObj;
-                    }
-                    Vec_IntFree( pvClasses[idReprRepr] );
-                    pvClasses[idReprRepr] = NULL;
-                }
-            }
-        }
-    }
-    ABC_FREE( pReprs );
-    return pvClasses;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ssw_FreeTempClasses( Vec_Int_t ** pvClasses, int nObjNumMax )
-{
-    int i;
-    for ( i = 0; i < nObjNumMax; i++ )
-        if ( pvClasses[i] ) 
-            Vec_IntFree( pvClasses[i] );
-    ABC_FREE( pvClasses );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs signal correspondence for the miter of two AIGs with node pairs defined.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars )
-{
-    Ssw_Man_t * p; 
-    Aig_Man_t * pAigNew, * pMiter;
-    Ssw_Pars_t Pars;
-    Vec_Int_t * vPairs;
-    Vec_Int_t ** pvClasses;
-    assert( Vec_IntSize(vIds1) == Vec_IntSize(vIds2) );
-    // create sequential miter
-    pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
-    Aig_ManCleanup( pMiter );
-    // transfer information to the miter
-    vPairs = Ssw_TransferSignalPairs( pMiter, pAig1, pAig2, vIds1, vIds2 );
-    // create representation of the classes
-    pvClasses = Ssw_TransformPairsIntoTempClasses( vPairs, Aig_ManObjNumMax(pMiter) );
-    Vec_IntFree( vPairs );
-    // if parameters are not given, create them
-    if ( pPars == NULL )
-        Ssw_ManSetDefaultParams( pPars = &Pars );
-    // start the induction manager
-    p = Ssw_ManCreate( pMiter, pPars );
-    // create equivalence classes using these IDs
-    p->ppClasses = Ssw_ClassesPreparePairs( pMiter, pvClasses );
-    p->pSml = Ssw_SmlStart( pMiter, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
-    Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
-    // perform refinement of classes
-    pAigNew = Ssw_SignalCorrespondenceRefine( p );
-    // cleanup
-    Ssw_FreeTempClasses( pvClasses, Aig_ManObjNumMax(pMiter) );
-    Ssw_ManStop( p );
-    Aig_ManStop( pMiter );
-    return pAigNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Runs inductive SEC for the miter of two AIGs with node pairs defined.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig )
-{
-    Aig_Man_t * pAigNew, * pAigRes;
-    Ssw_Pars_t Pars, * pPars = &Pars;
-    Vec_Int_t * vIds1, * vIds2;
-    Aig_Obj_t * pObj, * pRepr;
-    int RetValue, i, clk = clock();
-    Ssw_ManSetDefaultParams( pPars );
-    pPars->fVerbose = 1;
-    pAigNew = Ssw_SignalCorrespondence( pAig, pPars );
-    // record pairs of equivalent nodes
-    vIds1 = Vec_IntAlloc( Aig_ManObjNumMax(pAig) );
-    vIds2 = Vec_IntAlloc( Aig_ManObjNumMax(pAig) );
-    Aig_ManForEachObj( pAig, pObj, i )
-    {
-        pRepr = Aig_Regular((Aig_Obj_t *)pObj->pData);
-        if ( pRepr == NULL )
-            continue;
-        if ( Aig_ManObj(pAigNew, pRepr->Id) == NULL )
-            continue;
-/*
-        if ( Aig_ObjIsNode(pObj) )
-            printf( "n " );
-        else if ( Saig_ObjIsPi(pAig, pObj) )
-            printf( "pi " );
-        else if ( Saig_ObjIsLo(pAig, pObj) )
-            printf( "lo " );
-*/
-        Vec_IntPush( vIds1, Aig_ObjId(pObj) );
-        Vec_IntPush( vIds2, Aig_ObjId(pRepr) );
-    }
-    printf( "Recorded %d pairs (before: %d  after: %d).\n", Vec_IntSize(vIds1), Aig_ManObjNumMax(pAig), Aig_ManObjNumMax(pAigNew) );
-    // try the new AIGs
-    pAigRes = Ssw_SignalCorrespondenceWithPairs( pAig, pAigNew, vIds1, vIds2, pPars );
-    Vec_IntFree( vIds1 );
-    Vec_IntFree( vIds2 );
-    // report the results
-    RetValue = Ssw_MiterStatus( pAigRes, 1 );
-    if ( RetValue == 1 )
-        printf( "Verification successful.  " );
-    else if ( RetValue == 0 )
-        printf( "Verification failed with the counter-example.  " );
-    else
-        printf( "Verification UNDECIDED. Remaining registers %d (total %d).  ", 
-            Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig) + Aig_ManRegNum(pAigNew) );
-    ABC_PRT( "Time", clock() - clk );
-    // cleanup
-    Aig_ManStop( pAigNew );
-    return pAigRes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Runs inductive SEC for the miter of two AIGs with node pairs defined.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars )
-{
-    Aig_Man_t * pAigRes;
-    int RetValue, clk = clock();
-    assert( vIds1 != NULL && vIds2 != NULL );
-    // try the new AIGs
-    printf( "Performing specialized verification with node pairs.\n" );
-    pAigRes = Ssw_SignalCorrespondenceWithPairs( pAig1, pAig2, vIds1, vIds2, pPars );
-    // report the results
-    RetValue = Ssw_MiterStatus( pAigRes, 1 );
-    if ( RetValue == 1 )
-        printf( "Verification successful.  " );
-    else if ( RetValue == 0 )
-        printf( "Verification failed with a counter-example.  " );
-    else
-        printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ", 
-            Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
-    ABC_PRT( "Time", clock() - clk );
-    // cleanup
-    Aig_ManStop( pAigRes );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Runs inductive SEC for the miter of two AIGs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
-{
-    Aig_Man_t * pAigRes, * pMiter;
-    int RetValue, clk = clock();
-    // try the new AIGs
-    printf( "Performing general verification without node pairs.\n" );
-    pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
-    Aig_ManCleanup( pMiter );
-    pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
-    Aig_ManStop( pMiter );
-    // report the results
-    RetValue = Ssw_MiterStatus( pAigRes, 1 );
-    if ( RetValue == 1 )
-        printf( "Verification successful.  " );
-    else if ( RetValue == 0 )
-        printf( "Verification failed with a counter-example.  " );
-    else
-        printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ", 
-            Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
-    ABC_PRT( "Time", clock() - clk );
-    // cleanup
-    Aig_ManStop( pAigRes );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Runs inductive SEC for the miter of two AIGs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars )
-{
-    Aig_Man_t * pAigRes;
-    int RetValue, clk = clock();
-    // try the new AIGs
-//    printf( "Performing general verification without node pairs.\n" );
-    pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
-    // report the results
-    RetValue = Ssw_MiterStatus( pAigRes, 1 );
-    if ( RetValue == 1 )
-        printf( "Verification successful.  " );
-    else if ( RetValue == 0 )
-        printf( "Verification failed with a counter-example.  " );
-    else
-        printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ", 
-            Aig_ManRegNum(pAigRes), Aig_ManRegNum(pMiter) );
-    ABC_PRT( "Time", clock() - clk );
-    // cleanup
-    Aig_ManStop( pAigRes );
-    return RetValue;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-