Version abc70930

12 files changed, 0 insertions, 3167 deletions

diff --git a/src/opt/sim/module.make b/src/opt/sim/module.make
deleted file mode 100644
index 54058402..00000000
--- a/src/opt/sim/module.make
+++ /dev/null
@@ -1,10 +0,0 @@
-SRC +=  src/opt/sim/simMan.c \
-    src/opt/sim/simSat.c \
-    src/opt/sim/simSeq.c \
-    src/opt/sim/simSupp.c \
-    src/opt/sim/simSwitch.c \
-    src/opt/sim/simSym.c \
-    src/opt/sim/simSymSat.c \
-    src/opt/sim/simSymSim.c \
-    src/opt/sim/simSymStr.c \
-    src/opt/sim/simUtils.c
diff --git a/src/opt/sim/sim.h b/src/opt/sim/sim.h
deleted file mode 100644
index 7fcf5ae6..00000000
--- a/src/opt/sim/sim.h
+++ /dev/null
@@ -1,233 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [sim.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Simulation package.]
-
-  Synopsis    [External declarations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: sim.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __SIM_H__
-#define __SIM_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-/*
-    The ideas realized in this package are described in the paper:
-    "Detecting Symmetries in Boolean Functions using Circuit Representation, 
-    Simulation, and Satisfiability".
-*/
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Sym_Man_t_ Sym_Man_t;
-struct Sym_Man_t_
-{
-    // info about the network
-    Abc_Ntk_t *       pNtk;          // the network 
-    Vec_Ptr_t *       vNodes;        // internal nodes in topological order
-    int               nInputs;
-    int               nOutputs;
-    // internal simulation information
-    int               nSimWords;     // the number of bits in simulation info
-    Vec_Ptr_t *       vSim;          // simulation info
-    // support information
-    Vec_Ptr_t *       vSuppFun;      // bit representation
-    Vec_Vec_t *       vSupports;     // integer representation
-    // symmetry info for each output
-    Vec_Ptr_t *       vMatrSymms;    // symmetric pairs
-    Vec_Ptr_t *       vMatrNonSymms; // non-symmetric pairs
-    Vec_Int_t *       vPairsTotal;   // total pairs
-    Vec_Int_t *       vPairsSym;     // symmetric pairs
-    Vec_Int_t *       vPairsNonSym;  // non-symmetric pairs
-    // temporary simulation info
-    unsigned *        uPatRand;
-    unsigned *        uPatCol;
-    unsigned *        uPatRow;
-    // temporary
-    Vec_Int_t *       vVarsU;
-    Vec_Int_t *       vVarsV;
-    int               iOutput;
-    int               iVar1;
-    int               iVar2;
-    int               iVar1Old;
-    int               iVar2Old;
-    // internal data structures
-    int               nSatRuns;
-    int               nSatRunsSat;
-    int               nSatRunsUnsat;
-    // pairs
-    int               nPairsSymm;
-    int               nPairsSymmStr;
-    int               nPairsNonSymm;
-    int               nPairsRem;
-    int               nPairsTotal;
-    // runtime statistics
-    int               timeStruct;
-    int               timeCount;
-    int               timeMatr;
-    int               timeSim;
-    int               timeFraig;
-    int               timeSat;
-    int               timeTotal;
-};
-
-typedef struct Sim_Man_t_ Sim_Man_t;
-struct Sim_Man_t_
-{
-    // info about the network
-    Abc_Ntk_t *       pNtk;
-    int               nInputs;
-    int               nOutputs;
-    int               fLightweight;
-    // internal simulation information
-    int               nSimBits;      // the number of bits in simulation info
-    int               nSimWords;     // the number of words in simulation info
-    Vec_Ptr_t *       vSim0;         // simulation info 1
-    Vec_Ptr_t *       vSim1;         // simulation info 2
-    // support information
-    int               nSuppBits;     // the number of bits in support info
-    int               nSuppWords;    // the number of words in support info
-    Vec_Ptr_t *       vSuppStr;      // structural supports
-    Vec_Ptr_t *       vSuppFun;      // functional supports
-    // simulation targets
-    Vec_Vec_t *       vSuppTargs;    // support targets
-    int               iInput;        // the input current processed
-    // internal data structures
-    Extra_MmFixed_t * pMmPat;   
-    Vec_Ptr_t *       vFifo;
-    Vec_Int_t *       vDiffs;
-    int               nSatRuns;
-    int               nSatRunsSat;
-    int               nSatRunsUnsat;
-    // runtime statistics
-    int               timeSim;
-    int               timeTrav;
-    int               timeFraig;
-    int               timeSat;
-    int               timeTotal;
-};
-
-typedef struct Sim_Pat_t_ Sim_Pat_t;
-struct Sim_Pat_t_
-{
-    int              Input;         // the input which it has detected
-    int              Output;        // the output for which it was collected
-    unsigned *       pData;         // the simulation data
-};
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-#define SIM_NUM_WORDS(n)      (((n)>>5) + (((n)&31) > 0))
-#define SIM_LAST_BITS(n)      ((((n)&31) > 0)? (n)&31 : 32)
-
-#define SIM_MASK_FULL         (0xFFFFFFFF)
-#define SIM_MASK_BEG(n)       (SIM_MASK_FULL >> (32-n))
-#define SIM_MASK_END(n)       (SIM_MASK_FULL << (n))
-#define SIM_SET_0_FROM(m,n)   ((m) & ~SIM_MASK_BEG(n))
-#define SIM_SET_1_FROM(m,n)   ((m) |  SIM_MASK_END(n))
-
-// generating random unsigned (#define RAND_MAX 0x7fff)
-#define SIM_RANDOM_UNSIGNED   ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))
-
-// macros to get hold of bits in a bit string
-#define Sim_SetBit(p,i)       ((p)[(i)>>5] |= (1<<((i) & 31)))
-#define Sim_XorBit(p,i)       ((p)[(i)>>5] ^= (1<<((i) & 31)))
-#define Sim_HasBit(p,i)      (((p)[(i)>>5]  & (1<<((i) & 31))) > 0)
-
-// macros to get hold of the support info
-#define Sim_SuppStrSetVar(vSupps,pNode,v)     Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
-#define Sim_SuppStrHasVar(vSupps,pNode,v)     Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
-#define Sim_SuppFunSetVar(vSupps,Output,v)    Sim_SetBit((unsigned*)(vSupps)->pArray[Output],(v))
-#define Sim_SuppFunHasVar(vSupps,Output,v)    Sim_HasBit((unsigned*)(vSupps)->pArray[Output],(v))
-#define Sim_SimInfoSetVar(vSupps,pNode,v)     Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
-#define Sim_SimInfoHasVar(vSupps,pNode,v)     Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
-#define Sim_SimInfoGet(vInfo,pNode)           ((unsigned *)((vInfo)->pArray[(pNode)->Id]))
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DECLARATIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== simMan.c ==========================================================*/
-extern Sym_Man_t *     Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose );
-extern void            Sym_ManStop( Sym_Man_t * p );
-extern void            Sym_ManPrintStats( Sym_Man_t * p );
-extern Sim_Man_t *     Sim_ManStart( Abc_Ntk_t * pNtk, int fLightweight );
-extern void            Sim_ManStop( Sim_Man_t * p );
-extern void            Sim_ManPrintStats( Sim_Man_t * p );
-extern Sim_Pat_t *     Sim_ManPatAlloc( Sim_Man_t * p );
-extern void            Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat );
-/*=== simSeq.c ==========================================================*/
-extern Vec_Ptr_t *     Sim_SimulateSeqRandom( Abc_Ntk_t * pNtk, int nFrames, int nWords );
-extern Vec_Ptr_t *     Sim_SimulateSeqModel( Abc_Ntk_t * pNtk, int nFrames, int * pModel );
-/*=== simSupp.c ==========================================================*/
-extern Vec_Ptr_t *     Sim_ComputeStrSupp( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t *     Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
-/*=== simSym.c ==========================================================*/
-extern int             Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose );
-/*=== simSymSat.c ==========================================================*/
-extern int             Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern );
-/*=== simSymStr.c ==========================================================*/
-extern void            Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * vSuppFun );
-/*=== simSymSim.c ==========================================================*/
-extern void            Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPatRand, Vec_Ptr_t * vMatrsNonSym );
-/*=== simUtil.c ==========================================================*/
-extern Vec_Ptr_t *     Sim_UtilInfoAlloc( int nSize, int nWords, bool fClean );
-extern void            Sim_UtilInfoFree( Vec_Ptr_t * p );
-extern void            Sim_UtilInfoAdd( unsigned * pInfo1, unsigned * pInfo2, int nWords );
-extern void            Sim_UtilInfoDetectDiffs( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs );
-extern void            Sim_UtilInfoDetectNews( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs );
-extern void            Sim_UtilInfoFlip( Sim_Man_t * p, Abc_Obj_t * pNode );
-extern bool            Sim_UtilInfoCompare( Sim_Man_t * p, Abc_Obj_t * pNode );
-extern void            Sim_UtilSimulate( Sim_Man_t * p, bool fFirst );
-extern void            Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fType1, bool fType2 );
-extern void            Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset );
-extern void            Sim_UtilTransferNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset, int fShift );
-extern int             Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct );
-extern int             Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords );
-extern Vec_Int_t *     Sim_UtilCountOnesArray( Vec_Ptr_t * vInfo, int nSimWords );
-extern void            Sim_UtilSetRandom( unsigned * pPatRand, int nSimWords );
-extern void            Sim_UtilSetCompl( unsigned * pPatRand, int nSimWords );
-extern void            Sim_UtilSetConst( unsigned * pPatRand, int nSimWords, int fConst1 );
-extern int             Sim_UtilInfoIsEqual( unsigned * pPats1, unsigned * pPats2, int nSimWords );
-extern int             Sim_UtilInfoIsImp( unsigned * pPats1, unsigned * pPats2, int nSimWords );
-extern int             Sim_UtilInfoIsClause( unsigned * pPats1, unsigned * pPats2, int nSimWords );
-extern int             Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters );
-extern void            Sim_UtilCountPairsAll( Sym_Man_t * p );
-extern int             Sim_UtilMatrsAreDisjoint( Sym_Man_t * p );
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/opt/sim/simMan.c b/src/opt/sim/simMan.c
deleted file mode 100644
index 3b50ad84..00000000
--- a/src/opt/sim/simMan.c
+++ /dev/null
@@ -1,288 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [simMan.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Simulation manager.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: simMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "sim.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the simulation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose )
-{
-    Sym_Man_t * p;
-    int i, v; 
-    // start the manager
-    p = ALLOC( Sym_Man_t, 1 );
-    memset( p, 0, sizeof(Sym_Man_t) );
-    p->pNtk = pNtk;
-    p->vNodes     = Abc_NtkDfs( pNtk, 0 );
-    p->nInputs    = Abc_NtkCiNum(p->pNtk);
-    p->nOutputs   = Abc_NtkCoNum(p->pNtk);
-    // internal simulation information
-    p->nSimWords  = SIM_NUM_WORDS(p->nInputs);
-    p->vSim       = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 );
-    // symmetry info for each output
-    p->vMatrSymms    = Vec_PtrStart( p->nOutputs );
-    p->vMatrNonSymms = Vec_PtrStart( p->nOutputs );
-    p->vPairsTotal   = Vec_IntStart( p->nOutputs );
-    p->vPairsSym     = Vec_IntStart( p->nOutputs );
-    p->vPairsNonSym  = Vec_IntStart( p->nOutputs );
-    for ( i = 0; i < p->nOutputs; i++ )
-    {
-        p->vMatrSymms->pArray[i]    = Extra_BitMatrixStart( p->nInputs );
-        p->vMatrNonSymms->pArray[i] = Extra_BitMatrixStart( p->nInputs );
-    }
-    // temporary patterns
-    p->uPatRand = ALLOC( unsigned, p->nSimWords );
-    p->uPatCol  = ALLOC( unsigned, p->nSimWords );
-    p->uPatRow  = ALLOC( unsigned, p->nSimWords );
-    p->vVarsU   = Vec_IntStart( 100 );
-    p->vVarsV   = Vec_IntStart( 100 );
-    // compute supports
-    p->vSuppFun  = Sim_ComputeFunSupp( pNtk, fVerbose );
-    p->vSupports = Vec_VecStart( p->nOutputs );
-    for ( i = 0; i < p->nOutputs; i++ )
-        for ( v = 0; v < p->nInputs; v++ )
-            if ( Sim_SuppFunHasVar( p->vSuppFun, i, v ) )
-                Vec_VecPush( p->vSupports, i, (void *)v );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the simulation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sym_ManStop( Sym_Man_t * p )
-{
-    int i;
-    Sym_ManPrintStats( p );
-    if ( p->vSuppFun )     Sim_UtilInfoFree( p->vSuppFun );   
-    if ( p->vSim )         Sim_UtilInfoFree( p->vSim );   
-    if ( p->vNodes )       Vec_PtrFree( p->vNodes );
-    if ( p->vSupports )    Vec_VecFree( p->vSupports );
-    for ( i = 0; i < p->nOutputs; i++ )
-    {
-        Extra_BitMatrixStop( p->vMatrSymms->pArray[i] );
-        Extra_BitMatrixStop( p->vMatrNonSymms->pArray[i] );
-    }
-    Vec_IntFree( p->vVarsU );
-    Vec_IntFree( p->vVarsV );
-    Vec_PtrFree( p->vMatrSymms );
-    Vec_PtrFree( p->vMatrNonSymms );
-    Vec_IntFree( p->vPairsTotal );
-    Vec_IntFree( p->vPairsSym );
-    Vec_IntFree( p->vPairsNonSym );
-    FREE( p->uPatRand );
-    FREE( p->uPatCol );
-    FREE( p->uPatRow );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints the manager statisticis.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sym_ManPrintStats( Sym_Man_t * p )
-{
-//    printf( "Inputs = %5d. Outputs = %5d. Sim words = %5d.\n", 
-//        Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
-    printf( "Total symm         = %8d.\n", p->nPairsSymm );
-    printf( "Structural symm    = %8d.\n", p->nPairsSymmStr );
-    printf( "Total non-sym      = %8d.\n", p->nPairsNonSymm );
-    printf( "Total var pairs    = %8d.\n", p->nPairsTotal );
-    printf( "Sat runs SAT       = %8d.\n", p->nSatRunsSat );
-    printf( "Sat runs UNSAT     = %8d.\n", p->nSatRunsUnsat );
-    PRT( "Structural  ", p->timeStruct );
-    PRT( "Simulation  ", p->timeSim );
-    PRT( "Matrix      ", p->timeMatr );
-    PRT( "Counting    ", p->timeCount );
-    PRT( "Fraiging    ", p->timeFraig );
-    PRT( "SAT         ", p->timeSat );
-    PRT( "TOTAL       ", p->timeTotal );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the simulation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk, int fLightweight )
-{
-    Sim_Man_t * p;
-    // start the manager
-    p = ALLOC( Sim_Man_t, 1 );
-    memset( p, 0, sizeof(Sim_Man_t) );
-    p->pNtk = pNtk;
-    p->nInputs    = Abc_NtkCiNum(p->pNtk);
-    p->nOutputs   = Abc_NtkCoNum(p->pNtk);
-    // internal simulation information
-    p->nSimBits   = 2048;
-    p->nSimWords  = SIM_NUM_WORDS(p->nSimBits);
-    p->vSim0      = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 );
-    p->fLightweight = fLightweight;
-    if (!p->fLightweight) {
-        p->vSim1      = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 );
-        // support information
-        p->nSuppBits  = Abc_NtkCiNum(pNtk);
-        p->nSuppWords = SIM_NUM_WORDS(p->nSuppBits);
-        p->vSuppStr   = Sim_ComputeStrSupp( pNtk );
-        p->vSuppFun   = Sim_UtilInfoAlloc( Abc_NtkCoNum(p->pNtk),  p->nSuppWords, 1 );
-        // other data
-        p->pMmPat     = Extra_MmFixedStart( sizeof(Sim_Pat_t) + p->nSuppWords * sizeof(unsigned) ); 
-        p->vFifo      = Vec_PtrAlloc( 100 );
-        p->vDiffs     = Vec_IntAlloc( 100 );
-        // allocate support targets (array of unresolved outputs for each input)
-        p->vSuppTargs = Vec_VecStart( p->nInputs );
-    }
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the simulation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_ManStop( Sim_Man_t * p )
-{
-    Sim_ManPrintStats( p );
-    if ( p->vSim0 )        Sim_UtilInfoFree( p->vSim0 );       
-    if ( p->vSim1 )        Sim_UtilInfoFree( p->vSim1 );       
-    if ( p->vSuppStr )     Sim_UtilInfoFree( p->vSuppStr );    
-//    if ( p->vSuppFun )     Sim_UtilInfoFree( p->vSuppFun );    
-    if ( p->vSuppTargs )   Vec_VecFree( p->vSuppTargs );
-    if ( p->pMmPat )       Extra_MmFixedStop( p->pMmPat );
-    if ( p->vFifo )        Vec_PtrFree( p->vFifo );
-    if ( p->vDiffs )       Vec_IntFree( p->vDiffs );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints the manager statisticis.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_ManPrintStats( Sim_Man_t * p )
-{
-//    printf( "Inputs = %5d. Outputs = %5d. Sim words = %5d.\n", 
-//        Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
-    printf( "Total func supps   = %8d.\n", Sim_UtilCountSuppSizes(p, 0) );
-    printf( "Total struct supps = %8d.\n", Sim_UtilCountSuppSizes(p, 1) );
-    printf( "Sat runs SAT       = %8d.\n", p->nSatRunsSat );
-    printf( "Sat runs UNSAT     = %8d.\n", p->nSatRunsUnsat );
-    PRT( "Simulation  ", p->timeSim );
-    PRT( "Traversal   ", p->timeTrav );
-    PRT( "Fraiging    ", p->timeFraig );
-    PRT( "SAT         ", p->timeSat );
-    PRT( "TOTAL       ", p->timeTotal );
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Returns one simulation pattern.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Sim_Pat_t * Sim_ManPatAlloc( Sim_Man_t * p )
-{
-    Sim_Pat_t * pPat;
-    pPat = (Sim_Pat_t *)Extra_MmFixedEntryFetch( p->pMmPat );
-    pPat->Output = -1;
-    pPat->pData  = (unsigned *)((char *)pPat + sizeof(Sim_Pat_t));
-    memset( pPat->pData, 0, p->nSuppWords * sizeof(unsigned) );
-    return pPat;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns one simulation pattern.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat )
-{
-    Extra_MmFixedEntryRecycle( p->pMmPat, (char *)pPat );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/sim/simSat.c b/src/opt/sim/simSat.c
deleted file mode 100644
index d514f7f2..00000000
--- a/src/opt/sim/simSat.c
+++ /dev/null
@@ -1,48 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [simSat.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Simulation to determine functional support.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: simSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "sim.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
- 
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/sim/simSeq.c b/src/opt/sim/simSeq.c
deleted file mode 100644
index 49fb939f..00000000
--- a/src/opt/sim/simSeq.c
+++ /dev/null
@@ -1,171 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [simSeq.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Simulation for sequential circuits.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: simUtils.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "sim.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static void Sim_SimulateSeqFrame( Vec_Ptr_t * vInfo, Abc_Ntk_t * pNtk, int iFrames, int nWords, int fTransfer );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates sequential circuit.]
-
-  Description [Takes sequential circuit (pNtk). Simulates the given number
-  (nFrames) of the circuit with the given number of machine words (nWords)
-  of random simulation data, starting from the initial state. If the initial
-  state of some latches is a don't-care, uses random input for that latch.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Sim_SimulateSeqRandom( Abc_Ntk_t * pNtk, int nFrames, int nWords )
-{
-    Vec_Ptr_t * vInfo;
-    Abc_Obj_t * pNode;
-    int i;
-    assert( Abc_NtkIsStrash(pNtk) );
-    vInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nWords * nFrames, 0 );
-    // set the constant data
-    pNode = Abc_AigConst1(pNtk);
-    Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords * nFrames, 1 );
-    // set the random PI data
-    Abc_NtkForEachPi( pNtk, pNode, i )
-        Sim_UtilSetRandom( Sim_SimInfoGet(vInfo,pNode), nWords * nFrames );
-    // set the initial state data
-    Abc_NtkForEachLatch( pNtk, pNode, i )
-        if ( Abc_LatchIsInit0(pNode) )
-            Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords, 0 );
-        else if ( Abc_LatchIsInit1(pNode) )
-            Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords, 1 );
-        else 
-            Sim_UtilSetRandom( Sim_SimInfoGet(vInfo,pNode), nWords );
-    // simulate the nodes for the given number of timeframes
-    for ( i = 0; i < nFrames; i++ )
-        Sim_SimulateSeqFrame( vInfo, pNtk, i, nWords, (int)(i < nFrames-1) );
-    return vInfo;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates sequential circuit.]
-
-  Description [Takes sequential circuit (pNtk). Simulates the given number
-  (nFrames) of the circuit with the given model. The model is assumed to 
-  contain values of PIs for each frame. The latches are initialized to
-  the initial state. One word of data is simulated.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Sim_SimulateSeqModel( Abc_Ntk_t * pNtk, int nFrames, int * pModel )
-{
-    Vec_Ptr_t * vInfo;
-    Abc_Obj_t * pNode;
-    unsigned * pUnsigned;
-    int i, k;
-    vInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nFrames, 0 );
-    // set the constant data
-    pNode = Abc_AigConst1(pNtk);
-    Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nFrames, 1 );
-    // set the random PI data
-    Abc_NtkForEachPi( pNtk, pNode, i )
-    {
-        pUnsigned = Sim_SimInfoGet(vInfo,pNode);
-        for ( k = 0; k < nFrames; k++ )
-            pUnsigned[k] = pModel[k * Abc_NtkPiNum(pNtk) + i] ? ~((unsigned)0) : 0;
-    }
-    // set the initial state data
-    Abc_NtkForEachLatch( pNtk, pNode, i )
-    {
-        pUnsigned = Sim_SimInfoGet(vInfo,pNode);
-        if ( Abc_LatchIsInit0(pNode) )
-            pUnsigned[0] = 0;
-        else if ( Abc_LatchIsInit1(pNode) )
-            pUnsigned[0] = ~((unsigned)0);
-        else 
-            pUnsigned[0] = SIM_RANDOM_UNSIGNED;
-    }
-    // simulate the nodes for the given number of timeframes
-    for ( i = 0; i < nFrames; i++ )
-        Sim_SimulateSeqFrame( vInfo, pNtk, i, 1, (int)(i < nFrames-1) );
-/*
-    // print the simulated values
-    for ( i = 0; i < nFrames; i++ )
-    {
-        printf( "Frame %d : ", i+1 );
-        Abc_NtkForEachPi( pNtk, pNode, k )
-            printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
-        printf( " " );
-        Abc_NtkForEachLatch( pNtk, pNode, k )
-            printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
-        printf( " " );
-        Abc_NtkForEachPo( pNtk, pNode, k )
-            printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
-        printf( "\n" );
-    }
-    printf( "\n" );
-*/
-    return vInfo;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates one frame of sequential circuit.]
-
-  Description [Assumes that the latches and POs are already initialized.
-  In the end transfers the data to the latches of the next frame.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_SimulateSeqFrame( Vec_Ptr_t * vInfo, Abc_Ntk_t * pNtk, int iFrames, int nWords, int fTransfer )
-{
-    Abc_Obj_t * pNode;
-    int i;
-    Abc_NtkForEachNode( pNtk, pNode, i )
-        Sim_UtilSimulateNodeOne( pNode, vInfo, nWords, iFrames * nWords );
-    Abc_NtkForEachPo( pNtk, pNode, i )
-        Sim_UtilTransferNodeOne( pNode, vInfo, nWords, iFrames * nWords, 0 );
-    if ( !fTransfer )
-        return;
-    Abc_NtkForEachLatch( pNtk, pNode, i )
-        Sim_UtilTransferNodeOne( pNode, vInfo, nWords, iFrames * nWords, 1 );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c
deleted file mode 100644
index f7048f4a..00000000
--- a/src/opt/sim/simSupp.c
+++ /dev/null
@@ -1,597 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [simSupp.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Simulation to determine functional support.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: simSupp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "fraig.h"
-#include "sim.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
- 
-static int    Sim_ComputeSuppRound( Sim_Man_t * p, bool fUseTargets );
-static int    Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets );
-static void   Sim_ComputeSuppSetTargets( Sim_Man_t * p );
-
-static void   Sim_UtilAssignRandom( Sim_Man_t * p );
-static void   Sim_UtilAssignFromFifo( Sim_Man_t * p );
-static void   Sim_SolveTargetsUsingSat( Sim_Man_t * p, int nCounters );
-static int    Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Output );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Computes structural supports.]
-
-  Description [Supports are returned as an array of bit strings, one
-  for each CO.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk )
-{
-    Vec_Ptr_t * vSuppStr;
-    Abc_Obj_t * pNode;
-    unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
-    int nSuppWords, i, k;
-    // allocate room for structural supports
-    nSuppWords = SIM_NUM_WORDS( Abc_NtkCiNum(pNtk) );
-    vSuppStr   = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nSuppWords, 1 );
-    // assign the structural support to the PIs
-    Abc_NtkForEachCi( pNtk, pNode, i )
-        Sim_SuppStrSetVar( vSuppStr, pNode, i );
-    // derive the structural supports of the internal nodes
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-//        if ( Abc_NodeIsConst(pNode) )
-//            continue;
-        pSimmNode  = vSuppStr->pArray[ pNode->Id ];
-        pSimmNode1 = vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
-        pSimmNode2 = vSuppStr->pArray[ Abc_ObjFaninId1(pNode) ];
-        for ( k = 0; k < nSuppWords; k++ )
-            pSimmNode[k] = pSimmNode1[k] | pSimmNode2[k];
-    }
-    // set the structural supports of the PO nodes
-    Abc_NtkForEachCo( pNtk, pNode, i )
-    {
-        pSimmNode  = vSuppStr->pArray[ pNode->Id ];
-        pSimmNode1 = vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
-        for ( k = 0; k < nSuppWords; k++ )
-            pSimmNode[k] = pSimmNode1[k];
-    }
-    return vSuppStr;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compute functional supports.]
-
-  Description [Supports are returned as an array of bit strings, one
-  for each CO.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose )
-{
-    Sim_Man_t * p;
-    Vec_Ptr_t * vResult;
-    int nSolved, i, clk = clock();
-
-    srand( 0xABC );
-
-    // start the simulation manager
-    p = Sim_ManStart( pNtk, 0 );
-
-    // compute functional support using one round of random simulation
-    Sim_UtilAssignRandom( p );
-    Sim_ComputeSuppRound( p, 0 );
-
-    // set the support targets 
-    Sim_ComputeSuppSetTargets( p );
-if ( fVerbose )
-    printf( "Number of support targets after simulation = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) );
-    if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
-        goto exit;
-
-    for ( i = 0; i < 1; i++ )
-    {
-        // compute patterns using one round of random simulation
-        Sim_UtilAssignRandom( p );
-        nSolved = Sim_ComputeSuppRound( p, 1 );
-        if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
-            goto exit;
-
-if ( fVerbose )
-    printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.\n", 
-       Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) );
-    }
-
-    // try to solve the support targets
-    while ( Vec_VecSizeSize(p->vSuppTargs) > 0 )
-    {
-        // solve targets until the first disproved one (which gives counter-example)
-        Sim_SolveTargetsUsingSat( p, p->nSimWords/p->nSuppWords );
-        // compute additional functional support
-        Sim_UtilAssignFromFifo( p );
-        nSolved = Sim_ComputeSuppRound( p, 1 );
-
-if ( fVerbose )
-    printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.  SAT runs = %3d.\n", 
-            Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo), p->nSatRuns );
-    }
-
-exit:
-p->timeTotal = clock() - clk;
-    vResult = p->vSuppFun;  
-    //  p->vSuppFun = NULL;
-    Sim_ManStop( p );
-    return vResult;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes functional support using one round of simulation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_ComputeSuppRound( Sim_Man_t * p, bool fUseTargets )
-{
-    Vec_Int_t * vTargets;
-    int i, Counter = 0;
-    int clk;
-    // perform one round of random simulation
-clk = clock();
-    Sim_UtilSimulate( p, 0 );
-p->timeSim += clock() - clk;
-    // iterate through the CIs and detect COs that depend on them
-    for ( i = p->iInput; i < p->nInputs; i++ )
-    {
-        vTargets = p->vSuppTargs->pArray[i];
-        if ( fUseTargets && vTargets->nSize == 0 )
-            continue;
-        Counter += Sim_ComputeSuppRoundNode( p, i, fUseTargets );
-    }
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes functional support for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets )
-{
-    int fVerbose = 0;
-    Sim_Pat_t * pPat;
-    Vec_Int_t * vTargets;
-    Vec_Vec_t * vNodesByLevel;
-    Abc_Obj_t * pNodeCi, * pNode;
-    int i, k, v, Output, LuckyPat, fType0, fType1;
-    int Counter = 0;
-    int fFirst = 1;
-    int clk;
-    // collect nodes by level in the TFO of the CI 
-    // this proceduredoes not collect the CIs and COs
-    // but it increments TravId of the collected nodes and CIs/COs
-clk = clock();
-    pNodeCi       = Abc_NtkCi( p->pNtk, iNumCi );
-    vNodesByLevel = Abc_DfsLevelized( pNodeCi, 0 );
-p->timeTrav += clock() - clk;
-    // complement the simulation info of the selected CI
-    Sim_UtilInfoFlip( p, pNodeCi );
-    // simulate the levelized structure of nodes
-    Vec_VecForEachEntry( vNodesByLevel, pNode, i, k )
-    {
-        fType0 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin0(pNode) );
-        fType1 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin1(pNode) );
-clk = clock();
-        Sim_UtilSimulateNode( p, pNode, 1, fType0, fType1 );
-p->timeSim += clock() - clk;
-    }
-    // set the simulation info of the affected COs
-    if ( fUseTargets )
-    {
-        vTargets = p->vSuppTargs->pArray[iNumCi];
-        for ( i = vTargets->nSize - 1; i >= 0; i-- )
-        {
-            // get the target output
-            Output = vTargets->pArray[i];
-            // get the target node
-            pNode  = Abc_ObjFanin0( Abc_NtkCo(p->pNtk, Output) );
-            // the output should be in the cone
-            assert( Abc_NodeIsTravIdCurrent(pNode) );
-
-            // skip if the simulation info is equal
-            if ( Sim_UtilInfoCompare( p, pNode ) )
-                continue;
-
-            // otherwise, we solved a new target
-            Vec_IntRemove( vTargets, Output );
-if ( fVerbose )
-    printf( "(%d,%d) ", iNumCi, Output );
-            Counter++;
-            // make sure this variable is not yet detected
-            assert( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) );
-            // set this variable
-            Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi );
-            
-            // detect the differences in the simulation info
-            Sim_UtilInfoDetectDiffs( p->vSim0->pArray[pNode->Id], p->vSim1->pArray[pNode->Id], p->nSimWords, p->vDiffs );
-            // create new patterns
-            if ( !fFirst && p->vFifo->nSize > 1000 )
-                continue;
-
-            Vec_IntForEachEntry( p->vDiffs, LuckyPat, k )
-            {
-                // set the new pattern
-                pPat = Sim_ManPatAlloc( p );
-                pPat->Input  = iNumCi;
-                pPat->Output = Output;
-                Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
-                    if ( Sim_SimInfoHasVar( p->vSim0, pNodeCi, LuckyPat ) )
-                        Sim_SetBit( pPat->pData, v );
-                Vec_PtrPush( p->vFifo, pPat );
-
-                fFirst = 0;
-                break;
-            }
-        }
-if ( fVerbose && Counter )
-printf( "\n" );
-    }
-    else
-    {
-        Abc_NtkForEachCo( p->pNtk, pNode, Output )
-        {
-            if ( !Abc_NodeIsTravIdCurrent( pNode ) )
-                continue;
-            if ( !Sim_UtilInfoCompare( p, Abc_ObjFanin0(pNode) ) )
-            {
-                if ( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) )
-                {
-                    Counter++;
-                    Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi );
-                }
-            }
-        }
-    }
-    Vec_VecFree( vNodesByLevel );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the simulation targets.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_ComputeSuppSetTargets( Sim_Man_t * p )
-{
-    Abc_Obj_t * pNode;
-    unsigned * pSuppStr, * pSuppFun;
-    int i, k, Num;
-    Abc_NtkForEachCo( p->pNtk, pNode, i )
-    {
-        pSuppStr = p->vSuppStr->pArray[pNode->Id];
-        pSuppFun = p->vSuppFun->pArray[i];
-        // find vars in the structural support that are not in the functional support
-        Sim_UtilInfoDetectNews( pSuppFun, pSuppStr, p->nSuppWords, p->vDiffs );
-        Vec_IntForEachEntry( p->vDiffs, Num, k )
-            Vec_VecPush( p->vSuppTargs, Num, (void *)i );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Assigns random simulation info to the PIs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilAssignRandom( Sim_Man_t * p )
-{
-    Abc_Obj_t * pNode;
-    unsigned * pSimInfo;
-    int i, k;
-    // assign the random/systematic simulation info to the PIs
-    Abc_NtkForEachCi( p->pNtk, pNode, i )
-    {
-        pSimInfo = p->vSim0->pArray[pNode->Id];
-        for ( k = 0; k < p->nSimWords; k++ )
-            pSimInfo[k] = SIM_RANDOM_UNSIGNED;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the new patterns from fifo.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilAssignFromFifo( Sim_Man_t * p )
-{
-    int fUseOneWord = 0;
-    Abc_Obj_t * pNode;
-    Sim_Pat_t * pPat;
-    unsigned * pSimInfo;
-    int nWordsNew, iWord, iWordLim, i, w;
-    int iBeg, iEnd;
-    int Counter = 0;
-    // go through the patterns and fill in the dist-1 minterms for each
-    for ( iWord = 0; p->vFifo->nSize > 0; iWord = iWordLim )
-    {
-        ++Counter;
-        // get the pattern
-        pPat = Vec_PtrPop( p->vFifo );
-        if ( fUseOneWord )
-        {
-            // get the first word of the next series
-            iWordLim = iWord + 1; 
-            // set the pattern for all PIs from iBit to iWord + p->nInputs
-            iBeg = p->iInput;
-            iEnd = ABC_MIN( iBeg + 32, p->nInputs );
-//            for ( i = iBeg; i < iEnd; i++ )
-            Abc_NtkForEachCi( p->pNtk, pNode, i )
-            {
-                pNode = Abc_NtkCi(p->pNtk,i);
-                pSimInfo = p->vSim0->pArray[pNode->Id];
-                if ( Sim_HasBit(pPat->pData, i) )
-                    pSimInfo[iWord] = SIM_MASK_FULL;
-                else
-                    pSimInfo[iWord] = 0;
-                // flip one bit
-                if ( i >= iBeg && i < iEnd )
-                    Sim_XorBit( pSimInfo + iWord, i-iBeg );
-            }
-        }
-        else
-        {
-            // get the number of words for the remaining inputs
-            nWordsNew = p->nSuppWords;
-//            nWordsNew = SIM_NUM_WORDS( p->nInputs - p->iInput );
-            // get the first word of the next series
-            iWordLim = (iWord + nWordsNew < p->nSimWords)? iWord + nWordsNew : p->nSimWords; 
-            // set the pattern for all CIs from iWord to iWord + nWordsNew
-            Abc_NtkForEachCi( p->pNtk, pNode, i )
-            {
-                pSimInfo = p->vSim0->pArray[pNode->Id];
-                if ( Sim_HasBit(pPat->pData, i) )
-                {
-                    for ( w = iWord; w < iWordLim; w++ )
-                        pSimInfo[w] = SIM_MASK_FULL;
-                }
-                else
-                {
-                    for ( w = iWord; w < iWordLim; w++ )
-                        pSimInfo[w] = 0;
-                }
-                Sim_XorBit( pSimInfo + iWord, i );
-                // flip one bit
-//                if ( i >= p->iInput )
-//                    Sim_XorBit( pSimInfo + iWord, i-p->iInput );
-            }
-        }
-        Sim_ManPatFree( p, pPat );
-        // stop if we ran out of room for patterns
-        if ( iWordLim == p->nSimWords )
-            break;
-//        if ( Counter == 1 )
-//            break;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Get the given number of counter-examples using SAT.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit )
-{
-    Fraig_Params_t Params;
-    Fraig_Man_t * pMan;
-    Abc_Obj_t * pNodeCi;
-    Abc_Ntk_t * pMiter;
-    Sim_Pat_t * pPat;
-    void * pEntry;
-    int * pModel;
-    int RetValue, Output, Input, k, v;
-    int Counter = 0;
-    int clk;
-
-    p->nSatRuns = 0;
-    // put targets into one array
-    Vec_VecForEachEntryReverse( p->vSuppTargs, pEntry, Input, k )
-    {
-        p->nSatRuns++;
-        Output = (int)pEntry;
-
-        // set up the miter for the two cofactors of this output w.r.t. this input
-        pMiter = Abc_NtkMiterForCofactors( p->pNtk, Output, Input, -1 );
-
-        // transform the miter into a fraig
-        Fraig_ParamsSetDefault( &Params );
-        Params.nSeconds = ABC_INFINITY;
-        Params.fInternal = 1;
-clk = clock();
-        pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); 
-p->timeFraig += clock() - clk;
-clk = clock();
-        Fraig_ManProveMiter( pMan );
-p->timeSat += clock() - clk;
-
-        // analyze the result
-        RetValue = Fraig_ManCheckMiter( pMan );
-        assert( RetValue >= 0 );
-        if ( RetValue == 1 ) // unsat
-        {
-            p->nSatRunsUnsat++;
-            pModel = NULL;
-            Vec_PtrRemove( p->vSuppTargs->pArray[Input], pEntry );
-        }
-        else // sat
-        {
-            p->nSatRunsSat++;
-            pModel = Fraig_ManReadModel( pMan );
-            assert( pModel != NULL );
-            assert( Sim_SolveSuppModelVerify( p->pNtk, pModel, Input, Output ) );
-
-//printf( "Solved by SAT (%d,%d).\n", Input, Output );
-            // set the new pattern
-            pPat = Sim_ManPatAlloc( p );
-            pPat->Input  = Input;
-            pPat->Output = Output;
-            Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
-                if ( pModel[v] )
-                    Sim_SetBit( pPat->pData, v );
-            Vec_PtrPush( p->vFifo, pPat );
-/*
-            // set the new pattern
-            pPat = Sim_ManPatAlloc( p );
-            pPat->Input  = Input;
-            pPat->Output = Output;
-            Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
-                if ( pModel[v] )
-                    Sim_SetBit( pPat->pData, v );
-            Sim_XorBit( pPat->pData, Input );  // add this bit in the opposite polarity
-            Vec_PtrPush( p->vFifo, pPat );
-*/
-            Counter++;
-        }
-        // delete the fraig manager
-        Fraig_ManFree( pMan );
-        // delete the miter
-        Abc_NtkDelete( pMiter );
-
-        // makr the input, which we are processing
-        p->iInput = Input;
-
-        // stop when we found enough patterns
-//        if ( Counter == Limit )
-        if ( Counter == 1 )
-            return;
-    }
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Saves the counter example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_NtkSimTwoPats_rec( Abc_Obj_t * pNode )
-{
-    int Value0, Value1;
-    if ( Abc_NodeIsTravIdCurrent( pNode ) )
-        return (int)pNode->pCopy;
-    Abc_NodeSetTravIdCurrent( pNode );
-    Value0 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin0(pNode) );
-    Value1 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin1(pNode) );
-    if ( Abc_ObjFaninC0(pNode) )
-        Value0 = ~Value0;
-    if ( Abc_ObjFaninC1(pNode) )
-        Value1 = ~Value1;
-    pNode->pCopy = (Abc_Obj_t *)(Value0 & Value1);
-    return Value0 & Value1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Verifies that pModel proves the presence of Input in the support of Output.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Output )
-{
-    Abc_Obj_t * pNode;
-    int RetValue, i;
-    // set the PI values
-    Abc_NtkIncrementTravId( pNtk );
-    Abc_NtkForEachCi( pNtk, pNode, i )
-    {
-        Abc_NodeSetTravIdCurrent( pNode );
-        if ( pNode == Abc_NtkCi(pNtk,Input) )
-            pNode->pCopy = (Abc_Obj_t *)1;
-        else if ( pModel[i] == 1 )
-            pNode->pCopy = (Abc_Obj_t *)3;
-        else
-            pNode->pCopy = NULL;
-    }
-    // perform the traversal
-    RetValue = 3 & Sim_NtkSimTwoPats_rec( Abc_ObjFanin0( Abc_NtkCo(pNtk,Output) ) );
-//    assert( RetValue == 1 || RetValue == 2 ); 
-    return RetValue == 1 || RetValue == 2;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/sim/simSwitch.c b/src/opt/sim/simSwitch.c
deleted file mode 100644
index 218d4d59..00000000
--- a/src/opt/sim/simSwitch.c
+++ /dev/null
@@ -1,107 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [simSwitch.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Computes switching activity of nodes in the ABC network.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: simSwitch.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "sim.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static void Sim_NodeSimulate( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords );
-static float Sim_ComputeSwitching( unsigned * pSimInfo, int nSimWords );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Computes switching activity using simulation.]
-
-  Description [Computes switching activity, which is understood as the
-  probability of switching under random simulation. Assigns the
-  random simulation information at the CI and propagates it through
-  the internal nodes of the AIG.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns )
-{
-    Vec_Int_t * vSwitching;
-    float * pSwitching;
-    Vec_Ptr_t * vNodes;
-    Vec_Ptr_t * vSimInfo;
-    Abc_Obj_t * pNode;
-    unsigned * pSimInfo;
-    int nSimWords, i;
-
-    // allocate space for simulation info of all nodes
-    nSimWords = SIM_NUM_WORDS(nPatterns);
-    vSimInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nSimWords, 0 );
-    // assign the random simulation to the CIs
-    vSwitching = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
-    pSwitching = (float *)vSwitching->pArray;
-    Abc_NtkForEachCi( pNtk, pNode, i )
-    {
-        pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
-        Sim_UtilSetRandom( pSimInfo, nSimWords );
-        pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords );
-    }
-    // simulate the internal nodes
-    vNodes  = Abc_AigDfs( pNtk, 1, 0 );
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-    {
-        pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
-        Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords, 0 );
-        pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords );
-    }
-    Vec_PtrFree( vNodes );
-    Sim_UtilInfoFree( vSimInfo );
-    return vSwitching;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes switching activity of one node.]
-
-  Description [Uses the formula: Switching = 2 * nOnes * nZeros / (nTotal ^ 2) ]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float Sim_ComputeSwitching( unsigned * pSimInfo, int nSimWords )
-{
-    int nOnes, nTotal;
-    nTotal = 32 * nSimWords;
-    nOnes = Sim_UtilCountOnes( pSimInfo, nSimWords );
-    return (float)2.0 * nOnes * (nTotal - nOnes) / nTotal / nTotal;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/sim/simSym.c b/src/opt/sim/simSym.c
deleted file mode 100644
index 71de5b05..00000000
--- a/src/opt/sim/simSym.c
+++ /dev/null
@@ -1,142 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [simSym.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Simulation to determine two-variable symmetries.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: simSym.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "sim.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
- 
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Computes two variable symmetries.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose )
-{
-    Sym_Man_t * p;
-    Vec_Ptr_t * vResult;
-    int Result;
-    int i, clk, clkTotal = clock();
-
-    srand( 0xABC );
-
-    // start the simulation manager
-    p = Sym_ManStart( pNtk, fVerbose );
-    p->nPairsTotal = p->nPairsRem = Sim_UtilCountAllPairs( p->vSuppFun, p->nSimWords, p->vPairsTotal );
-    if ( fVerbose )
-        printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
-               p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
-
-    // detect symmetries using circuit structure
-clk = clock();
-    Sim_SymmsStructCompute( pNtk, p->vMatrSymms, p->vSuppFun );
-p->timeStruct = clock() - clk;
-
-    Sim_UtilCountPairsAll( p );
-    p->nPairsSymmStr = p->nPairsSymm;
-    if ( fVerbose )
-        printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
-            p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
-
-    // detect symmetries using simulation
-    for ( i = 1; i <= 1000; i++ )
-    {
-        // simulate this pattern
-        Sim_UtilSetRandom( p->uPatRand, p->nSimWords );
-        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
-        if ( i % 50 != 0 )
-            continue;
-        // check disjointness
-        assert( Sim_UtilMatrsAreDisjoint( p ) );
-        // count the number of pairs
-        Sim_UtilCountPairsAll( p );
-        if ( i % 500 != 0 )
-            continue;
-        if ( fVerbose )
-            printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
-                p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
-    }
-
-    // detect symmetries using SAT
-    for ( i = 1; Sim_SymmsGetPatternUsingSat( p, p->uPatRand ); i++ )
-    {
-        // simulate this pattern in four polarities
-        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
-        Sim_XorBit( p->uPatRand, p->iVar1 );
-        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
-        Sim_XorBit( p->uPatRand, p->iVar2 );
-        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
-        Sim_XorBit( p->uPatRand, p->iVar1 );
-        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
-        Sim_XorBit( p->uPatRand, p->iVar2 );
-/*
-        // try the previuos pair
-        Sim_XorBit( p->uPatRand, p->iVar1Old );
-        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
-        Sim_XorBit( p->uPatRand, p->iVar2Old );
-        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
-        Sim_XorBit( p->uPatRand, p->iVar1Old );
-        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
-*/
-        if ( i % 10 != 0 )
-            continue;
-        // check disjointness
-        assert( Sim_UtilMatrsAreDisjoint( p ) );
-        // count the number of pairs
-        Sim_UtilCountPairsAll( p );
-        if ( i % 50 != 0 )
-            continue;
-        if ( fVerbose )
-            printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
-                p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
-    }
-
-    // count the number of pairs
-    Sim_UtilCountPairsAll( p );
-    if ( fVerbose )
-        printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
-            p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
-//    Sim_UtilCountPairsAllPrint( p );
-
-    Result = p->nPairsSymm;
-    vResult = p->vMatrSymms;  
-p->timeTotal = clock() - clkTotal;
-    //  p->vMatrSymms = NULL;
-    Sym_ManStop( p );
-    return Result;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/sim/simSymSat.c b/src/opt/sim/simSymSat.c
deleted file mode 100644
index 7690a891..00000000
--- a/src/opt/sim/simSymSat.c
+++ /dev/null
@@ -1,199 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [simSymSat.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Satisfiability to determine two variable symmetries.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: simSymSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "sim.h"
-#include "fraig.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Tries to prove the remaining pairs using SAT.]
-
-  Description [Continues to prove as long as it encounters symmetric pairs.
-  Returns 1 if a non-symmetric pair is found (which gives a counter-example).
-  Returns 0 if it finishes considering all pairs for all outputs.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern )
-{
-    Vec_Int_t * vSupport;
-    Extra_BitMat_t * pMatSym, * pMatNonSym;
-    int Index1, Index2, Index3, IndexU, IndexV;
-    int v, u, i, k, b, out;
-
-    // iterate through outputs
-    for ( out = p->iOutput; out < p->nOutputs; out++ )
-    {
-        pMatSym    = Vec_PtrEntry( p->vMatrSymms,    out );
-        pMatNonSym = Vec_PtrEntry( p->vMatrNonSymms, out );
-
-        // go through the remaining variable pairs
-        vSupport = Vec_VecEntry( p->vSupports, out );
-        Vec_IntForEachEntry( vSupport, v, Index1 )
-        Vec_IntForEachEntryStart( vSupport, u, Index2, Index1+1 )
-        {
-            if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
-                continue;
-            p->nSatRuns++;
-
-            // collect the support variables that are symmetric with u and v
-            Vec_IntClear( p->vVarsU );
-            Vec_IntClear( p->vVarsV );
-            Vec_IntForEachEntry( vSupport, b, Index3 )
-            {
-                if ( Extra_BitMatrixLookup1( pMatSym, u, b ) )
-                    Vec_IntPush( p->vVarsU, b );
-                if ( Extra_BitMatrixLookup1( pMatSym, v, b ) )
-                    Vec_IntPush( p->vVarsV, b );
-            }
-
-            if ( Sim_SymmsSatProveOne( p, out, v, u, pPattern ) )
-            { // update the symmetric variable info            
-                p->nSatRunsUnsat++;
-                Vec_IntForEachEntry( p->vVarsU, i, IndexU )
-                Vec_IntForEachEntry( p->vVarsV, k, IndexV )
-                {
-                    Extra_BitMatrixInsert1( pMatSym,  i, k );  // Theorem 1
-                    Extra_BitMatrixInsert2( pMatSym,  i, k );  // Theorem 1
-                    Extra_BitMatrixOrTwo( pMatNonSym, i, k );  // Theorem 2
-                }
-            }
-            else
-            { // update the assymmetric variable info
-                p->nSatRunsSat++;
-                Vec_IntForEachEntry( p->vVarsU, i, IndexU )
-                Vec_IntForEachEntry( p->vVarsV, k, IndexV )
-                {
-                    Extra_BitMatrixInsert1( pMatNonSym, i, k );   // Theorem 3
-                    Extra_BitMatrixInsert2( pMatNonSym, i, k );   // Theorem 3
-                }
-
-                // remember the out
-                p->iOutput = out;
-                p->iVar1Old = p->iVar1;
-                p->iVar2Old = p->iVar2;
-                p->iVar1 = v;
-                p->iVar2 = u;
-                return 1;
-
-            }
-        }
-        // make sure that the symmetry matrix contains only cliques
-        assert( Extra_BitMatrixIsClique( pMatSym ) );
-    }
-
-    // mark that we finished all outputs
-    p->iOutput = p->nOutputs;
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the variables are symmetric; 0 otherwise.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern )
-{
-    Fraig_Params_t Params;
-    Fraig_Man_t * pMan;
-    Abc_Ntk_t * pMiter;
-    int RetValue, i, clk;
-    int * pModel;
-
-    // get the miter for this problem
-    pMiter = Abc_NtkMiterForCofactors( p->pNtk, Out, Var1, Var2 );
-    // transform the miter into a fraig
-    Fraig_ParamsSetDefault( &Params );
-    Params.fInternal = 1;
-    Params.nPatsRand = 512;
-    Params.nPatsDyna = 512;
-    Params.nSeconds = ABC_INFINITY;
-
-clk = clock();
-    pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); 
-p->timeFraig += clock() - clk;
-clk = clock();
-    Fraig_ManProveMiter( pMan );
-p->timeSat += clock() - clk;
-
-    // analyze the result
-    RetValue = Fraig_ManCheckMiter( pMan );
-//    assert( RetValue >= 0 );
-    // save the pattern
-    if ( RetValue == 0 )
-    {
-        // get the pattern
-        pModel = Fraig_ManReadModel( pMan );
-        assert( pModel != NULL );
-//printf( "Disproved by SAT: out = %d  pair = (%d, %d)\n", Out, Var1, Var2 );
-        // transfer the model into the pattern
-        for ( i = 0; i < p->nSimWords; i++ )
-            pPattern[i] = 0;
-        for ( i = 0; i < p->nInputs; i++ )
-            if ( pModel[i] )
-                Sim_SetBit( pPattern, i );
-        // make sure these variables have the same value (1)
-        Sim_SetBit( pPattern, Var1 );
-        Sim_SetBit( pPattern, Var2 );
-    }
-    else if ( RetValue == -1 )
-    {
-        // this should never happen; if it happens, such is life
-        // we are conservative and assume that there is no symmetry
-//printf( "STRANGE THING: out = %d %s  pair = (%d %s, %d %s)\n", 
-//                        Out, Abc_ObjName(Abc_NtkCo(p->pNtk,Out)), 
-//                        Var1, Abc_ObjName(Abc_NtkCi(p->pNtk,Var1)), 
-//                        Var2, Abc_ObjName(Abc_NtkCi(p->pNtk,Var2)) );
-        memset( pPattern, 0, sizeof(unsigned) * p->nSimWords );
-        RetValue = 0;
-    }
-    // delete the fraig manager
-    Fraig_ManFree( pMan );
-    // delete the miter
-    Abc_NtkDelete( pMiter );
-    return RetValue;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/sim/simSymSim.c b/src/opt/sim/simSymSim.c
deleted file mode 100644
index 2282825b..00000000
--- a/src/opt/sim/simSymSim.c
+++ /dev/null
@@ -1,173 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [simSymSim.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Simulation to determine two-variable symmetries.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: simSymSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "sim.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat );
-static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Vec_Ptr_t * vMatrsNonSym, int Output );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Detects non-symmetric pairs using one pattern.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPat, Vec_Ptr_t * vMatrsNonSym )
-{
-    Abc_Obj_t * pNode;
-    int i, nPairsTotal, nPairsSym, nPairsNonSym;
-    int clk;
-
-    // create the simulation matrix
-    Sim_SymmsCreateSquare( p, pPat );
-    // simulate each node in the DFS order
-clk = clock();
-    Vec_PtrForEachEntry( p->vNodes, pNode, i )
-    {
-//        if ( Abc_NodeIsConst(pNode) )
-//            continue;
-        Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords, 0 );
-    }
-p->timeSim += clock() - clk;
-    // collect info into the CO matrices
-clk = clock();
-    Abc_NtkForEachCo( p->pNtk, pNode, i )
-    {
-        pNode = Abc_ObjFanin0(pNode);
-//        if ( Abc_ObjIsCi(pNode) || Abc_AigNodeIsConst(pNode) )
-//            continue;
-        nPairsTotal  = Vec_IntEntry(p->vPairsTotal, i);
-        nPairsSym    = Vec_IntEntry(p->vPairsSym,   i);
-        nPairsNonSym = Vec_IntEntry(p->vPairsNonSym,i);
-        assert( nPairsTotal >= nPairsSym + nPairsNonSym ); 
-        if ( nPairsTotal == nPairsSym + nPairsNonSym )
-            continue;
-        Sim_SymmsDeriveInfo( p, pPat, pNode, vMatrsNonSym, i );
-    }
-p->timeMatr += clock() - clk;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the square matrix of simulation info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat )
-{
-    unsigned * pSimInfo;
-    Abc_Obj_t * pNode;
-    int i, w;
-    // for each PI var copy the pattern
-    Abc_NtkForEachCi( p->pNtk, pNode, i )
-    {
-        pSimInfo = Vec_PtrEntry( p->vSim, pNode->Id );
-        if ( Sim_HasBit(pPat, i) )
-        {
-            for ( w = 0; w < p->nSimWords; w++ )
-                pSimInfo[w] = SIM_MASK_FULL;
-        }
-        else
-        {
-            for ( w = 0; w < p->nSimWords; w++ )
-                pSimInfo[w] = 0;
-        }
-        // flip one bit
-        Sim_XorBit( pSimInfo, i );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transfers the info to the POs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Vec_Ptr_t * vMatrsNonSym, int Output )
-{
-    Extra_BitMat_t * pMat;
-    Vec_Int_t * vSupport;
-    unsigned * pSupport;
-    unsigned * pSimInfo;
-    int i, w, Index;
-    // get the matrix, the support, and the simulation info
-    pMat = Vec_PtrEntry( vMatrsNonSym, Output );
-    vSupport = Vec_VecEntry( p->vSupports, Output );
-    pSupport = Vec_PtrEntry( p->vSuppFun, Output );
-    pSimInfo = Vec_PtrEntry( p->vSim, pNode->Id );
-    // generate vectors A1 and A2
-    for ( w = 0; w < p->nSimWords; w++ )
-    {
-        p->uPatCol[w] = pSupport[w] & pPat[w] &  pSimInfo[w];
-        p->uPatRow[w] = pSupport[w] & pPat[w] & ~pSimInfo[w];
-    }
-    // add two dimensions
-    Vec_IntForEachEntry( vSupport, i, Index )
-        if ( Sim_HasBit( p->uPatCol, i ) )
-            Extra_BitMatrixOr( pMat, i, p->uPatRow );
-    // add two dimensions
-    Vec_IntForEachEntry( vSupport, i, Index )
-        if ( Sim_HasBit( p->uPatRow, i ) )
-            Extra_BitMatrixOr( pMat, i, p->uPatCol );
-    // generate vectors B1 and B2
-    for ( w = 0; w < p->nSimWords; w++ )
-    {
-        p->uPatCol[w] = pSupport[w] & ~pPat[w] &  pSimInfo[w];
-        p->uPatRow[w] = pSupport[w] & ~pPat[w] & ~pSimInfo[w];
-    }
-    // add two dimensions
-    Vec_IntForEachEntry( vSupport, i, Index )
-        if ( Sim_HasBit( p->uPatCol, i ) )
-            Extra_BitMatrixOr( pMat, i, p->uPatRow );
-    // add two dimensions
-    Vec_IntForEachEntry( vSupport, i, Index )
-        if ( Sim_HasBit( p->uPatRow, i ) )
-            Extra_BitMatrixOr( pMat, i, p->uPatCol );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/sim/simSymStr.c b/src/opt/sim/simSymStr.c
deleted file mode 100644
index d52c4328..00000000
--- a/src/opt/sim/simSymStr.c
+++ /dev/null
@@ -1,488 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [simSymStr.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Structural detection of symmetries.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: simSymStr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "sim.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-#define SIM_READ_SYMMS(pNode)       ((Vec_Int_t *)pNode->pCopy) 
-#define SIM_SET_SYMMS(pNode,vVect)  (pNode->pCopy = (Abc_Obj_t *)(vVect)) 
-
-static void  Sim_SymmsStructComputeOne( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int * pMap );
-static void  Sim_SymmsBalanceCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
-static void  Sim_SymmsPartitionNodes( Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesPis0, Vec_Ptr_t * vNodesPis1, Vec_Ptr_t * vNodesOther );
-static void  Sim_SymmsAppendFromGroup( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesPi, Vec_Ptr_t * vNodesOther, Vec_Int_t * vSymms, int * pMap );
-static void  Sim_SymmsAppendFromNode( Abc_Ntk_t * pNtk, Vec_Int_t * vSymms0, Vec_Ptr_t * vNodesOther, Vec_Ptr_t * vNodesPi0, Vec_Ptr_t * vNodesPi1, Vec_Int_t * vSymms, int * pMap );
-static int   Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, Vec_Ptr_t * vNodesOther, int * pMap );
-static int   Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap );
-static void  Sim_SymmsPrint( Vec_Int_t * vSymms );
-static void  Sim_SymmsTrans( Vec_Int_t * vSymms );
-static void  Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport );
-static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Computes symmetries for a single output function.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * vSuppFun )
-{
-    Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pTemp;
-    int * pMap, i;
-
-    assert( Abc_NtkCiNum(pNtk) + 10 < (1<<16) );
-
-    // get the structural support
-    pNtk->vSupps = Sim_ComputeStrSupp( pNtk );
-    // set elementary info for the CIs
-    Abc_NtkForEachCi( pNtk, pTemp, i )
-        SIM_SET_SYMMS( pTemp, Vec_IntAlloc(0) );
-    // create the map of CI ids into their numbers
-    pMap = Sim_SymmsCreateMap( pNtk );
-    // collect the nodes in the TFI cone of this output
-    vNodes = Abc_NtkDfs( pNtk, 0 );
-    Vec_PtrForEachEntry( vNodes, pTemp, i )
-    {
-//        if ( Abc_NodeIsConst(pTemp) )
-//            continue;
-        Sim_SymmsStructComputeOne( pNtk, pTemp, pMap );
-    }
-    // collect the results for the COs;
-    Abc_NtkForEachCo( pNtk, pTemp, i )
-    {
-//printf( "Output %d:\n", i );
-        pTemp = Abc_ObjFanin0(pTemp);
-        if ( Abc_ObjIsCi(pTemp) || Abc_AigNodeIsConst(pTemp) )
-            continue;
-        Sim_SymmsTransferToMatrix( Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp), Vec_PtrEntry(vSuppFun, i) );
-    }
-    // clean the intermediate results
-    Sim_UtilInfoFree( pNtk->vSupps );
-    pNtk->vSupps = NULL;
-    Abc_NtkForEachCi( pNtk, pTemp, i )
-        Vec_IntFree( SIM_READ_SYMMS(pTemp) );
-    Vec_PtrForEachEntry( vNodes, pTemp, i )
-//        if ( !Abc_NodeIsConst(pTemp) )
-            Vec_IntFree( SIM_READ_SYMMS(pTemp) );
-    Vec_PtrFree( vNodes );
-    free( pMap );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively computes symmetries. ]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_SymmsStructComputeOne( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int * pMap )
-{
-    Vec_Ptr_t * vNodes, * vNodesPi0, * vNodesPi1, * vNodesOther;
-    Vec_Int_t * vSymms;
-    Abc_Obj_t * pTemp;
-    int i;
-
-    // allocate the temporary arrays
-    vNodes      = Vec_PtrAlloc( 10 );
-    vNodesPi0   = Vec_PtrAlloc( 10 );
-    vNodesPi1   = Vec_PtrAlloc( 10 );
-    vNodesOther = Vec_PtrAlloc( 10 );  
-
-    // collect the fanins of the implication supergate
-    Sim_SymmsBalanceCollect_rec( pNode, vNodes );
-
-    // sort the nodes in the implication supergate
-    Sim_SymmsPartitionNodes( vNodes, vNodesPi0, vNodesPi1, vNodesOther );
-
-    // start the resulting set
-    vSymms = Vec_IntAlloc( 10 );
-    // generate symmetries from the groups
-    Sim_SymmsAppendFromGroup( pNtk, vNodesPi0, vNodesOther, vSymms, pMap );
-    Sim_SymmsAppendFromGroup( pNtk, vNodesPi1, vNodesOther, vSymms, pMap );
-    // add symmetries from other inputs
-    for ( i = 0; i < vNodesOther->nSize; i++ )
-    {
-        pTemp = Abc_ObjRegular(vNodesOther->pArray[i]);
-        Sim_SymmsAppendFromNode( pNtk, SIM_READ_SYMMS(pTemp), vNodesOther, vNodesPi0, vNodesPi1, vSymms, pMap );
-    }
-    Vec_PtrFree( vNodes );
-    Vec_PtrFree( vNodesPi0 );
-    Vec_PtrFree( vNodesPi1 );
-    Vec_PtrFree( vNodesOther );
-
-    // set the symmetry at the node
-    SIM_SET_SYMMS( pNode, vSymms );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the array of nodes to be combined into one multi-input AND-gate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_SymmsBalanceCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
-{
-    // if the new node is complemented, another gate begins
-    if ( Abc_ObjIsComplement(pNode) )
-    {
-        Vec_PtrPushUnique( vNodes, pNode );
-        return;
-    }
-    // if pNew is the PI node, return
-    if ( Abc_ObjIsCi(pNode) )
-    {
-        Vec_PtrPushUnique( vNodes, pNode );
-        return;    
-    }
-    // go through the branches
-    Sim_SymmsBalanceCollect_rec( Abc_ObjChild0(pNode), vNodes );
-    Sim_SymmsBalanceCollect_rec( Abc_ObjChild1(pNode), vNodes );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Divides PI variables into groups.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_SymmsPartitionNodes( Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesPis0, 
-    Vec_Ptr_t * vNodesPis1, Vec_Ptr_t * vNodesOther )
-{
-    Abc_Obj_t * pNode;
-    int i;
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-    {
-        if ( !Abc_ObjIsCi(Abc_ObjRegular(pNode)) )
-            Vec_PtrPush( vNodesOther, pNode );
-        else if ( Abc_ObjIsComplement(pNode) )
-            Vec_PtrPush( vNodesPis0, pNode );
-        else
-            Vec_PtrPush( vNodesPis1, pNode );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Makes the product of two partitions.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_SymmsAppendFromGroup( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesPi, Vec_Ptr_t * vNodesOther, Vec_Int_t * vSymms, int * pMap )
-{
-    Abc_Obj_t * pNode1, * pNode2;
-    unsigned uSymm;
-    int i, k;
-
-    if ( vNodesPi->nSize == 0 )
-        return;
-
-    // go through the pairs
-    for ( i = 0; i < vNodesPi->nSize; i++ )
-    for ( k = i+1; k < vNodesPi->nSize; k++ )
-    {
-        // get the two PI nodes
-        pNode1 = Abc_ObjRegular(vNodesPi->pArray[i]);
-        pNode2 = Abc_ObjRegular(vNodesPi->pArray[k]);
-        assert( pMap[pNode1->Id] != pMap[pNode2->Id] );
-        assert( pMap[pNode1->Id] >= 0 );
-        assert( pMap[pNode2->Id] >= 0 );
-        // generate symmetry
-        if ( pMap[pNode1->Id] < pMap[pNode2->Id] )
-            uSymm = ((pMap[pNode1->Id] << 16) | pMap[pNode2->Id]);
-        else
-            uSymm = ((pMap[pNode2->Id] << 16) | pMap[pNode1->Id]);
-        // check if symmetry belongs
-        if ( Sim_SymmsIsCompatibleWithNodes( pNtk, uSymm, vNodesOther, pMap ) )
-            Vec_IntPushUnique( vSymms, (int)uSymm );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Add the filters symmetries from the nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_SymmsAppendFromNode( Abc_Ntk_t * pNtk, Vec_Int_t * vSymms0, Vec_Ptr_t * vNodesOther, 
-    Vec_Ptr_t * vNodesPi0, Vec_Ptr_t * vNodesPi1, Vec_Int_t * vSymms, int * pMap )
-{
-    unsigned uSymm;
-    int i;
-
-    if ( vSymms0->nSize == 0 )
-        return;
-
-    // go through the pairs
-    for ( i = 0; i < vSymms0->nSize; i++ )
-    {
-        uSymm = (unsigned)vSymms0->pArray[i];
-        // check if symmetry belongs
-        if ( Sim_SymmsIsCompatibleWithNodes( pNtk, uSymm, vNodesOther, pMap ) &&
-             Sim_SymmsIsCompatibleWithGroup( uSymm, vNodesPi0, pMap ) && 
-             Sim_SymmsIsCompatibleWithGroup( uSymm, vNodesPi1, pMap ) )
-            Vec_IntPushUnique( vSymms, (int)uSymm );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if symmetry is compatible with the group of nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, Vec_Ptr_t * vNodesOther, int * pMap )
-{
-    Vec_Int_t * vSymmsNode;
-    Abc_Obj_t * pNode;
-    int i, s, Ind1, Ind2, fIsVar1, fIsVar2;
-
-    if ( vNodesOther->nSize == 0 )
-        return 1;
-
-    // get the indices of the PI variables
-    Ind1 = (uSymm & 0xffff);
-    Ind2 = (uSymm >> 16);
-
-    // go through the nodes
-    // if they do not belong to a support, it is okay
-    // if one belongs, the other does not belong, quit
-    // if they belong, but are not part of symmetry, quit
-    for ( i = 0; i < vNodesOther->nSize; i++ )
-    {
-        pNode = Abc_ObjRegular(vNodesOther->pArray[i]);
-        fIsVar1 = Sim_SuppStrHasVar( pNtk->vSupps, pNode, Ind1 );
-        fIsVar2 = Sim_SuppStrHasVar( pNtk->vSupps, pNode, Ind2 );
-
-        if ( !fIsVar1 && !fIsVar2 )
-            continue;
-        if ( fIsVar1 ^ fIsVar2 )
-            return 0;
-        // both belong
-        // check if there is a symmetry
-        vSymmsNode = SIM_READ_SYMMS( pNode );
-        for ( s = 0; s < vSymmsNode->nSize; s++ )
-            if ( uSymm == (unsigned)vSymmsNode->pArray[s] )
-                break;
-        if ( s == vSymmsNode->nSize )
-            return 0;
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if symmetry is compatible with the group of PIs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap )
-{
-    Abc_Obj_t * pNode;
-    int i, Ind1, Ind2, fHasVar1, fHasVar2;
-
-    if ( vNodesPi->nSize == 0 )
-        return 1;
-
-    // get the indices of the PI variables
-    Ind1 = (uSymm & 0xffff);
-    Ind2 = (uSymm >> 16);
-
-    // go through the PI nodes
-    fHasVar1 = fHasVar2 = 0;
-    for ( i = 0; i < vNodesPi->nSize; i++ )
-    {
-        pNode = Abc_ObjRegular(vNodesPi->pArray[i]);
-        if ( pMap[pNode->Id] == Ind1 )
-            fHasVar1 = 1;
-        else if ( pMap[pNode->Id] == Ind2 )
-            fHasVar2 = 1;
-    }
-    return fHasVar1 == fHasVar2;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Improvements due to transitivity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_SymmsTrans( Vec_Int_t * vSymms )
-{
-    unsigned uSymm, uSymma, uSymmr;
-    int i, Ind1, Ind2;
-    int k, Ind1a, Ind2a;
-    int j;
-    int nTrans = 0;
-
-    for ( i = 0; i < vSymms->nSize; i++ )
-    {
-        uSymm = (unsigned)vSymms->pArray[i];
-        Ind1 = (uSymm & 0xffff);
-        Ind2 = (uSymm >> 16);
-        // find other symmetries that have Ind1
-        for ( k = i+1; k < vSymms->nSize; k++ )
-        {
-            uSymma = (unsigned)vSymms->pArray[k];
-            if ( uSymma == uSymm )
-                continue;
-            Ind1a = (uSymma & 0xffff);
-            Ind2a = (uSymma >> 16);
-            if ( Ind1a == Ind1 )
-            {
-                // find the symmetry (Ind2,Ind2a)
-                if ( Ind2 < Ind2a )
-                    uSymmr = ((Ind2 << 16) | Ind2a);
-                else
-                    uSymmr = ((Ind2a << 16) | Ind2);
-                for ( j = 0; j < vSymms->nSize; j++ )
-                    if ( uSymmr == (unsigned)vSymms->pArray[j] )
-                        break;
-                if ( j == vSymms->nSize )
-                    nTrans++;
-            }
-        }
-
-    }
-    printf( "Trans = %d.\n", nTrans );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Transfers from the vector to the matrix.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport )
-{
-    int i, Ind1, Ind2, nInputs;
-    unsigned uSymm;
-    // add diagonal elements
-    nInputs = Extra_BitMatrixReadSize( pMatSymm );
-    for ( i = 0; i < nInputs; i++ )
-        Extra_BitMatrixInsert1( pMatSymm, i, i );
-    // add non-diagonal elements
-    for ( i = 0; i < vSymms->nSize; i++ )
-    {
-        uSymm = (unsigned)vSymms->pArray[i];
-        Ind1 = (uSymm & 0xffff);
-        Ind2 = (uSymm >> 16);
-//printf( "%d,%d ", Ind1, Ind2 );
-        // skip variables that are not in the true support
-        assert( Sim_HasBit(pSupport, Ind1) == Sim_HasBit(pSupport, Ind2) );
-        if ( !Sim_HasBit(pSupport, Ind1) || !Sim_HasBit(pSupport, Ind2) )
-            continue;
-        Extra_BitMatrixInsert1( pMatSymm, Ind1, Ind2 );
-        Extra_BitMatrixInsert2( pMatSymm, Ind1, Ind2 );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Mapping of indices into numbers.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk )
-{
-    int * pMap;
-    Abc_Obj_t * pNode;
-    int i;
-    pMap = ALLOC( int, Abc_NtkObjNumMax(pNtk) );
-    for ( i = 0; i < Abc_NtkObjNumMax(pNtk); i++ )
-        pMap[i] = -1;
-    Abc_NtkForEachCi( pNtk, pNode, i )
-        pMap[pNode->Id] = i;
-    return pMap;
-}
-
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/sim/simUtils.c b/src/opt/sim/simUtils.c
deleted file mode 100644
index b0660001..00000000
--- a/src/opt/sim/simUtils.c
+++ /dev/null
@@ -1,711 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [simUtils.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Various simulation utilities.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: simUtils.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "sim.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
- 
-static int bit_count[256] = {
-  0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
-  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
-  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
-  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
-  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
-  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
-  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
-  3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
-};
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates simulation information for all nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Sim_UtilInfoAlloc( int nSize, int nWords, bool fClean )
-{
-    Vec_Ptr_t * vInfo;
-    int i;
-    assert( nSize > 0 && nWords > 0 );
-    vInfo = Vec_PtrAlloc( nSize );
-    vInfo->pArray[0] = ALLOC( unsigned, nSize * nWords );
-    if ( fClean )
-        memset( vInfo->pArray[0], 0, sizeof(unsigned) * nSize * nWords );
-    for ( i = 1; i < nSize; i++ )
-        vInfo->pArray[i] = ((unsigned *)vInfo->pArray[i-1]) + nWords;
-    vInfo->nSize = nSize;
-    return vInfo;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates simulation information for all nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilInfoFree( Vec_Ptr_t * p )
-{
-    free( p->pArray[0] );
-    Vec_PtrFree( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds the second supp-info the first.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilInfoAdd( unsigned * pInfo1, unsigned * pInfo2, int nWords )
-{
-    int w;
-    for ( w = 0; w < nWords; w++ )
-        pInfo1[w] |= pInfo2[w];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the positions where pInfo2 is 1 while pInfo1 is 0.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilInfoDetectDiffs( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs )
-{
-    int w, b;
-    unsigned uMask;
-    vDiffs->nSize = 0;
-    for ( w = 0; w < nWords; w++ )
-        if ( uMask = (pInfo2[w] ^ pInfo1[w]) )
-            for ( b = 0; b < 32; b++ )
-                if ( uMask & (1 << b) )
-                    Vec_IntPush( vDiffs, 32*w + b );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the positions where pInfo2 is 1 while pInfo1 is 0.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilInfoDetectNews( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs )
-{
-    int w, b;
-    unsigned uMask;
-    vDiffs->nSize = 0;
-    for ( w = 0; w < nWords; w++ )
-        if ( uMask = (pInfo2[w] & ~pInfo1[w]) )
-            for ( b = 0; b < 32; b++ )
-                if ( uMask & (1 << b) )
-                    Vec_IntPush( vDiffs, 32*w + b );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Flips the simulation info of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilInfoFlip( Sim_Man_t * p, Abc_Obj_t * pNode )
-{
-    unsigned * pSimInfo1, * pSimInfo2;
-    int k;
-    pSimInfo1 = p->vSim0->pArray[pNode->Id];
-    pSimInfo2 = p->vSim1->pArray[pNode->Id];
-    for ( k = 0; k < p->nSimWords; k++ )
-        pSimInfo2[k] = ~pSimInfo1[k];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the simulation infos are equal.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Sim_UtilInfoCompare( Sim_Man_t * p, Abc_Obj_t * pNode )
-{
-    unsigned * pSimInfo1, * pSimInfo2;
-    int k;
-    pSimInfo1 = p->vSim0->pArray[pNode->Id];
-    pSimInfo2 = p->vSim1->pArray[pNode->Id];
-    for ( k = 0; k < p->nSimWords; k++ )
-        if ( pSimInfo2[k] != pSimInfo1[k] )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates the internal nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilSimulate( Sim_Man_t * p, bool fType )
-{
-    Abc_Obj_t * pNode;
-    int i;
-    // simulate the internal nodes
-    Abc_NtkForEachNode( p->pNtk, pNode, i )
-        Sim_UtilSimulateNode( p, pNode, fType, fType, fType );
-    // assign simulation info of the CO nodes
-    Abc_NtkForEachCo( p->pNtk, pNode, i )
-        Sim_UtilSimulateNode( p, pNode, fType, fType, fType );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fType1, bool fType2 )
-{
-    unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
-    int k, fComp1, fComp2;
-    // simulate the internal nodes
-    if ( Abc_ObjIsNode(pNode) )
-    {
-        if ( fType )
-            pSimmNode  = p->vSim1->pArray[ pNode->Id ];
-        else
-            pSimmNode  = p->vSim0->pArray[ pNode->Id ];
-
-        if ( fType1 )
-            pSimmNode1 = p->vSim1->pArray[ Abc_ObjFaninId0(pNode) ];
-        else
-            pSimmNode1 = p->vSim0->pArray[ Abc_ObjFaninId0(pNode) ];
-
-        if ( fType2 )
-            pSimmNode2 = p->vSim1->pArray[ Abc_ObjFaninId1(pNode) ];
-        else
-            pSimmNode2 = p->vSim0->pArray[ Abc_ObjFaninId1(pNode) ];
-
-        fComp1 = Abc_ObjFaninC0(pNode);
-        fComp2 = Abc_ObjFaninC1(pNode);
-        if ( fComp1 && fComp2 )
-            for ( k = 0; k < p->nSimWords; k++ )
-                pSimmNode[k] = ~pSimmNode1[k] & ~pSimmNode2[k];
-        else if ( fComp1 && !fComp2 )
-            for ( k = 0; k < p->nSimWords; k++ )
-                pSimmNode[k] = ~pSimmNode1[k] &  pSimmNode2[k];
-        else if ( !fComp1 && fComp2 )
-            for ( k = 0; k < p->nSimWords; k++ )
-                pSimmNode[k] =  pSimmNode1[k] & ~pSimmNode2[k];
-        else // if ( fComp1 && fComp2 )
-            for ( k = 0; k < p->nSimWords; k++ )
-                pSimmNode[k] =  pSimmNode1[k] &  pSimmNode2[k];
-    }
-    else 
-    {
-        assert( Abc_ObjFaninNum(pNode) == 1 );
-        if ( fType )
-            pSimmNode  = p->vSim1->pArray[ pNode->Id ];
-        else
-            pSimmNode  = p->vSim0->pArray[ pNode->Id ];
-
-        if ( fType1 )
-            pSimmNode1 = p->vSim1->pArray[ Abc_ObjFaninId0(pNode) ];
-        else
-            pSimmNode1 = p->vSim0->pArray[ Abc_ObjFaninId0(pNode) ];
-
-        fComp1 = Abc_ObjFaninC0(pNode);
-        if ( fComp1 )
-            for ( k = 0; k < p->nSimWords; k++ )
-                pSimmNode[k] = ~pSimmNode1[k];
-        else 
-            for ( k = 0; k < p->nSimWords; k++ )
-                pSimmNode[k] =  pSimmNode1[k];
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset )
-{
-    unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
-    int k, fComp1, fComp2;
-    // simulate the internal nodes
-    assert( Abc_ObjIsNode(pNode) );
-    pSimmNode  = Vec_PtrEntry(vSimInfo, pNode->Id);
-    pSimmNode1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
-    pSimmNode2 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode));
-    pSimmNode  += nOffset;
-    pSimmNode1 += nOffset;
-    pSimmNode2 += nOffset;
-    fComp1 = Abc_ObjFaninC0(pNode);
-    fComp2 = Abc_ObjFaninC1(pNode);
-    if ( fComp1 && fComp2 )
-        for ( k = 0; k < nSimWords; k++ )
-            pSimmNode[k] = ~pSimmNode1[k] & ~pSimmNode2[k];
-    else if ( fComp1 && !fComp2 )
-        for ( k = 0; k < nSimWords; k++ )
-            pSimmNode[k] = ~pSimmNode1[k] &  pSimmNode2[k];
-    else if ( !fComp1 && fComp2 )
-        for ( k = 0; k < nSimWords; k++ )
-            pSimmNode[k] =  pSimmNode1[k] & ~pSimmNode2[k];
-    else // if ( fComp1 && fComp2 )
-        for ( k = 0; k < nSimWords; k++ )
-            pSimmNode[k] =  pSimmNode1[k] &  pSimmNode2[k];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilTransferNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset, int fShift )
-{
-    unsigned * pSimmNode, * pSimmNode1;
-    int k, fComp1;
-    // simulate the internal nodes
-    assert( Abc_ObjIsCo(pNode) );
-    pSimmNode  = Vec_PtrEntry(vSimInfo, pNode->Id);
-    pSimmNode1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
-    pSimmNode  += nOffset + (fShift > 0)*nSimWords;
-    pSimmNode1 += nOffset;
-    fComp1 = Abc_ObjFaninC0(pNode);
-    if ( fComp1 )
-        for ( k = 0; k < nSimWords; k++ )
-            pSimmNode[k] = ~pSimmNode1[k];
-    else 
-        for ( k = 0; k < nSimWords; k++ )
-            pSimmNode[k] =  pSimmNode1[k];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the simulation infos are equal.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct )
-{
-    Abc_Obj_t * pNode, * pNodeCi;
-    int i, v, Counter;
-    Counter = 0;
-    if ( fStruct )
-    {
-        Abc_NtkForEachCo( p->pNtk, pNode, i )
-            Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
-                Counter += Sim_SuppStrHasVar( p->vSuppStr, pNode, v );
-    }
-    else
-    {
-        Abc_NtkForEachCo( p->pNtk, pNode, i )
-            Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
-                Counter += Sim_SuppFunHasVar( p->vSuppFun, i, v );
-    }
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of 1's in the bitstring.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords )
-{
-    unsigned char * pBytes;
-    int nOnes, nBytes, i;
-    pBytes = (unsigned char *)pSimInfo;
-    nBytes = 4 * nSimWords;
-    nOnes  = 0;
-    for ( i = 0; i < nBytes; i++ )
-        nOnes += bit_count[ pBytes[i] ];
-    return nOnes;    
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of 1's in the bitstring.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Sim_UtilCountOnesArray( Vec_Ptr_t * vInfo, int nSimWords )
-{
-    Vec_Int_t * vCounters;
-    unsigned * pSimInfo;
-    int i;
-    vCounters = Vec_IntStart( Vec_PtrSize(vInfo) );
-    Vec_PtrForEachEntry( vInfo, pSimInfo, i )
-        Vec_IntWriteEntry( vCounters, i, Sim_UtilCountOnes(pSimInfo, nSimWords) );
-    return vCounters;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns random patterns.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilSetRandom( unsigned * pPatRand, int nSimWords )
-{
-    int k;
-    for ( k = 0; k < nSimWords; k++ )
-        pPatRand[k] = SIM_RANDOM_UNSIGNED;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns complemented patterns.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilSetCompl( unsigned * pPatRand, int nSimWords )
-{
-    int k;
-    for ( k = 0; k < nSimWords; k++ )
-        pPatRand[k] = ~pPatRand[k];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns constant patterns.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilSetConst( unsigned * pPatRand, int nSimWords, int fConst1 )
-{
-    int k;
-    for ( k = 0; k < nSimWords; k++ )
-        pPatRand[k] = 0;
-    if ( fConst1 )
-        Sim_UtilSetCompl( pPatRand, nSimWords );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if equal.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_UtilInfoIsEqual( unsigned * pPats1, unsigned * pPats2, int nSimWords )
-{
-    int k;
-    for ( k = 0; k < nSimWords; k++ )
-        if ( pPats1[k] != pPats2[k] )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if Node1 implies Node2.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_UtilInfoIsImp( unsigned * pPats1, unsigned * pPats2, int nSimWords )
-{
-    int k;
-    for ( k = 0; k < nSimWords; k++ )
-        if ( pPats1[k] & ~pPats2[k] )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if Node1 v Node2 is always true.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_UtilInfoIsClause( unsigned * pPats1, unsigned * pPats2, int nSimWords )
-{
-    int k;
-    for ( k = 0; k < nSimWords; k++ )
-        if ( ~pPats1[k] & ~pPats2[k] )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the total number of pairs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters )
-{
-    unsigned * pSupp;
-    int Counter, nOnes, nPairs, i;
-    Counter = 0;
-    Vec_PtrForEachEntry( vSuppFun, pSupp, i )
-    {
-        nOnes  = Sim_UtilCountOnes( pSupp, nSimWords );
-        nPairs = nOnes * (nOnes - 1) / 2;
-        Vec_IntWriteEntry( vCounters, i, nPairs );
-        Counter += nPairs;
-    }
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of entries in the array of matrices.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_UtilCountPairsOne( Extra_BitMat_t * pMat, Vec_Int_t * vSupport )
-{
-    int i, k, Index1, Index2;
-    int Counter = 0;
-//    int Counter2;
-    Vec_IntForEachEntry( vSupport, i, Index1 )
-    Vec_IntForEachEntryStart( vSupport, k, Index2, Index1+1 )
-        Counter += Extra_BitMatrixLookup1( pMat, i, k );
-//    Counter2 = Extra_BitMatrixCountOnesUpper(pMat);
-//    assert( Counter == Counter2 );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of entries in the array of matrices.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_UtilCountPairsOnePrint( Extra_BitMat_t * pMat, Vec_Int_t * vSupport )
-{
-    int i, k, Index1, Index2;
-    Vec_IntForEachEntry( vSupport, i, Index1 )
-    Vec_IntForEachEntryStart( vSupport, k, Index2, Index1+1 )
-        if ( Extra_BitMatrixLookup1( pMat, i, k ) )
-            printf( "(%d,%d) ", i, k );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of entries in the array of matrices.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilCountPairsAllPrint( Sym_Man_t * p )
-{
-    int i, clk;
-clk = clock();
-    for ( i = 0; i < p->nOutputs; i++ )
-    {
-        printf( "Output %2d :", i );
-        Sim_UtilCountPairsOnePrint( Vec_PtrEntry(p->vMatrSymms, i), Vec_VecEntry(p->vSupports, i) );
-        printf( "\n" );
-    }
-p->timeCount += clock() - clk;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of entries in the array of matrices.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilCountPairsAll( Sym_Man_t * p )
-{
-    int nPairsTotal, nPairsSym, nPairsNonSym, i, clk;
-clk = clock();
-    p->nPairsSymm    = 0;
-    p->nPairsNonSymm = 0;
-    for ( i = 0; i < p->nOutputs; i++ )
-    {
-        nPairsTotal  = Vec_IntEntry(p->vPairsTotal, i);
-        nPairsSym    = Vec_IntEntry(p->vPairsSym,   i);
-        nPairsNonSym = Vec_IntEntry(p->vPairsNonSym,i);
-        assert( nPairsTotal >= nPairsSym + nPairsNonSym ); 
-        if ( nPairsTotal == nPairsSym + nPairsNonSym )
-        {
-            p->nPairsSymm    += nPairsSym;
-            p->nPairsNonSymm += nPairsNonSym;
-            continue;
-        }
-        nPairsSym    = Sim_UtilCountPairsOne( Vec_PtrEntry(p->vMatrSymms,   i), Vec_VecEntry(p->vSupports, i) );
-        nPairsNonSym = Sim_UtilCountPairsOne( Vec_PtrEntry(p->vMatrNonSymms,i), Vec_VecEntry(p->vSupports, i) );
-        assert( nPairsTotal >= nPairsSym + nPairsNonSym ); 
-        Vec_IntWriteEntry( p->vPairsSym,    i, nPairsSym );
-        Vec_IntWriteEntry( p->vPairsNonSym, i, nPairsNonSym );
-        p->nPairsSymm    += nPairsSym;
-        p->nPairsNonSymm += nPairsNonSym;
-//        printf( "%d ", nPairsTotal - nPairsSym - nPairsNonSym );
-    }
-//printf( "\n" );
-    p->nPairsRem = p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm;
-p->timeCount += clock() - clk;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_UtilMatrsAreDisjoint( Sym_Man_t * p )
-{
-    int i;
-    for ( i = 0; i < p->nOutputs; i++ )
-        if ( !Extra_BitMatrixIsDisjoint( Vec_PtrEntry(p->vMatrSymms,i), Vec_PtrEntry(p->vMatrNonSymms,i) ) )
-            return 0;
-    return 1;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-