Version abc71001

12 files changed, 3167 insertions, 0 deletions

diff --git a/src/opt/sim/module.make b/src/opt/sim/module.make
new file mode 100644
index 00000000..54058402
--- /dev/null
+++ b/src/opt/sim/module.make
@@ -0,0 +1,10 @@
+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
new file mode 100644
index 00000000..7fcf5ae6
--- /dev/null
+++ b/src/opt/sim/sim.h
@@ -0,0 +1,233 @@
+/**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
new file mode 100644
index 00000000..3b50ad84
--- /dev/null
+++ b/src/opt/sim/simMan.c
@@ -0,0 +1,288 @@
+/**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
new file mode 100644
index 00000000..d514f7f2
--- /dev/null
+++ b/src/opt/sim/simSat.c
@@ -0,0 +1,48 @@
+/**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
new file mode 100644
index 00000000..49fb939f
--- /dev/null
+++ b/src/opt/sim/simSeq.c
@@ -0,0 +1,171 @@
+/**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
new file mode 100644
index 00000000..f7048f4a
--- /dev/null
+++ b/src/opt/sim/simSupp.c
@@ -0,0 +1,597 @@
+/**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
new file mode 100644
index 00000000..218d4d59
--- /dev/null
+++ b/src/opt/sim/simSwitch.c
@@ -0,0 +1,107 @@
+/**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
new file mode 100644
index 00000000..71de5b05
--- /dev/null
+++ b/src/opt/sim/simSym.c
@@ -0,0 +1,142 @@
+/**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
new file mode 100644
index 00000000..7690a891
--- /dev/null
+++ b/src/opt/sim/simSymSat.c
@@ -0,0 +1,199 @@
+/**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
new file mode 100644
index 00000000..2282825b
--- /dev/null
+++ b/src/opt/sim/simSymSim.c
@@ -0,0 +1,173 @@
+/**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
new file mode 100644
index 00000000..d52c4328
--- /dev/null
+++ b/src/opt/sim/simSymStr.c
@@ -0,0 +1,488 @@
+/**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
new file mode 100644
index 00000000..b0660001
--- /dev/null
+++ b/src/opt/sim/simUtils.c
@@ -0,0 +1,711 @@
+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+
+