Version abc50904

16 files changed, 235 insertions, 1144 deletions

diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index 946ed56b..39c6fae8 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -50,6 +50,7 @@ struct Fraig_ParamsStruct_t_
     int  fTryProve;     // tries to solve the final miter
     int  fVerbose;      // the verbosiness flag
     int  fVerboseP;     // the verbosiness flag (for proof reporting)
+    int  fInternal;     // is set to 1 for internal fraig calls
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c
index 0194f3b4..c9e6960c 100644
--- a/src/sat/fraig/fraigApi.c
+++ b/src/sat/fraig/fraigApi.c
@@ -164,10 +164,9 @@ Fraig_Node_t * Fraig_ManReadIthVar( Fraig_Man_t * p, int i )
 
 /**Function*************************************************************
 
-  Synopsis    [Creates a new node.]
+  Synopsis    [Creates a new PO node.]
 
-  Description [This procedure should be called to create the constant
-  node and the PI nodes first.]
+  Description [This procedure may take a complemented node.]
                
   SideEffects []
 
@@ -176,9 +175,8 @@ Fraig_Node_t * Fraig_ManReadIthVar( Fraig_Man_t * p, int i )
 ***********************************************************************/
 void Fraig_ManSetPo( Fraig_Man_t * p, Fraig_Node_t * pNode )
 {
-//    assert( pNode->fNodePo == 0 ); 
     // internal node may be a PO two times
-    pNode->fNodePo = 1;
+    Fraig_Regular(pNode)->fNodePo = 1;
     Fraig_NodeVecPush( p->vOutputs, pNode );
 }
 
diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c
index b46f6c41..73640387 100644
--- a/src/sat/fraig/fraigFeed.c
+++ b/src/sat/fraig/fraigFeed.c
@@ -768,7 +768,80 @@ void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Doubles the size of simulation info.]
+  Synopsis    [Generated trivial counter example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Fraig_ManAllocCounterExample( Fraig_Man_t * p )
+{
+    int * pModel;
+    pModel = ALLOC( int, p->vInputs->nSize );
+    memset( pModel, 0, sizeof(int) * p->vInputs->nSize );
+    return pModel;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Saves the counter example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_ManSimulateBitNode_rec( Fraig_Man_t * p, Fraig_Node_t * pNode )
+{
+    int Value0, Value1;
+    if ( Fraig_NodeIsTravIdCurrent( p, pNode ) )
+        return pNode->fMark3;
+    Fraig_NodeSetTravIdCurrent( p, pNode );
+    Value0 = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode->p1) );
+    Value1 = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode->p2) );
+    Value0 ^= Fraig_IsComplement(pNode->p1);
+    Value1 ^= Fraig_IsComplement(pNode->p2);
+    pNode->fMark3 = Value0 & Value1;
+    return pNode->fMark3;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one bit.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_ManSimulateBitNode( Fraig_Man_t * p, Fraig_Node_t * pNode, int * pModel )
+{
+    int fCompl, RetValue, i;
+    // set the PI values
+    Fraig_ManIncrementTravId( p );
+    for ( i = 0; i < p->vInputs->nSize; i++ )
+    {
+        Fraig_NodeSetTravIdCurrent( p, p->vInputs->pArray[i] );
+        p->vInputs->pArray[i]->fMark3 = pModel[i];
+    }
+    // perform the traversal
+    fCompl = Fraig_IsComplement(pNode);
+    RetValue = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode) );
+    return fCompl ^ RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Saves the counter example.]
 
   Description []
                
@@ -779,33 +852,52 @@ void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p )
 ***********************************************************************/
 int * Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode )
 {
-    int * pModel = NULL;
+    int * pModel;
     int iPattern;
-    int i;
+    int i, fCompl;
 
-    iPattern = Fraig_FindFirstDiff( p->pConst1, pNode, p->nWordsDyna, 0 );
+    // the node can be complemented
+    fCompl = Fraig_IsComplement(pNode);
+    // because we compare with constant 0, p->pConst1 should also be complemented
+    fCompl = !fCompl;
+
+    // derive the model
+    pModel = Fraig_ManAllocCounterExample( p );
+    iPattern = Fraig_FindFirstDiff( p->pConst1, Fraig_Regular(pNode), fCompl, p->nWordsRand, 1 );
     if ( iPattern >= 0 )
     {
-        pModel = ALLOC( int, p->vInputs->nSize );
-        memset( pModel, 0, sizeof(int) * p->vInputs->nSize );
         for ( i = 0; i < p->vInputs->nSize; i++ )
-            if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimD, iPattern ) )
+            if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimR, iPattern ) )
                 pModel[i] = 1;
+/*
+printf( "SAT solver's pattern:\n" );
+for ( i = 0; i < p->vInputs->nSize; i++ )
+    printf( "%d", pModel[i] );
+printf( "\n" );
+*/
+        assert( Fraig_ManSimulateBitNode( p, pNode, pModel ) );
         return pModel;
     }
-    iPattern = Fraig_FindFirstDiff( p->pConst1, pNode, p->nWordsRand, 1 );
+    iPattern = Fraig_FindFirstDiff( p->pConst1, Fraig_Regular(pNode), fCompl, p->iWordStart, 0 );
     if ( iPattern >= 0 )
     {
-        pModel = ALLOC( int, p->vInputs->nSize );
-        memset( pModel, 0, sizeof(int) * p->vInputs->nSize );
         for ( i = 0; i < p->vInputs->nSize; i++ )
-            if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimR, iPattern ) )
+            if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimD, iPattern ) )
                 pModel[i] = 1;
+/*
+printf( "SAT solver's pattern:\n" );
+for ( i = 0; i < p->vInputs->nSize; i++ )
+    printf( "%d", pModel[i] );
+printf( "\n" );
+*/
+        assert( Fraig_ManSimulateBitNode( p, pNode, pModel ) );
         return pModel;
     }
-    return pModel;
+    FREE( pModel );
+    return NULL;
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index 5f8b3496..1c765c12 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -239,10 +239,11 @@ struct Fraig_NodeStruct_t_
     unsigned              fMark0   :  1; // the mark used for traversals
     unsigned              fMark1   :  1; // the mark used for traversals
     unsigned              fMark2   :  1; // the mark used for traversals
+    unsigned              fMark3   :  1; // the mark used for traversals
     unsigned              fFeedUse :  1; // the presence of the variable in the feedback
     unsigned              fFeedVal :  1; // the value of the variable in the feedback
     unsigned              nFanouts :  2; // the indicator of fanouts (none, one, or many)
-    unsigned              nOnes    : 22; // the number of 1's in the random sim info
+    unsigned              nOnes    : 21; // the number of 1's in the random sim info
  
     // the children of the node
     Fraig_Node_t *        p1;            // the first child
@@ -379,6 +380,7 @@ extern void                Fraig_FeedBackInit( Fraig_Man_t * p );
 extern void                Fraig_FeedBack( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
 extern void                Fraig_FeedBackTest( Fraig_Man_t * p );
 extern int                 Fraig_FeedBackCompress( Fraig_Man_t * p );
+extern int *               Fraig_ManAllocCounterExample( Fraig_Man_t * p );
 extern int *               Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode );
 /*=== fraigMem.c =============================================================*/
 extern Fraig_MemFixed_t *  Fraig_MemFixedStart( int nEntrySize );
@@ -406,7 +408,7 @@ extern Fraig_Node_t *      Fraig_HashTableLookupF0( Fraig_Man_t * pMan, Fraig_No
 extern void                Fraig_HashTableInsertF0( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
 extern int                 Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand );
 extern int                 Fraig_CompareSimInfoUnderMask( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask );
-extern int                 Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand );
+extern int                 Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int fCompl, int iWordLast, int fUseRand );
 extern void                Fraig_CollectXors( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask );
 extern void                Fraig_TablePrintStatsS( Fraig_Man_t * pMan );
 extern void                Fraig_TablePrintStatsF( Fraig_Man_t * pMan );
@@ -416,10 +418,6 @@ extern int                 Fraig_TableRehashF0( Fraig_Man_t * pMan, int fLinkEqu
 extern int                 Fraig_NodeCountPis( Msat_IntVec_t * vVars, int nVarsPi );
 extern int                 Fraig_NodeCountSuppVars( Fraig_Man_t * p, Fraig_Node_t * pNode, int fSuppStr );
 extern int                 Fraig_NodesCompareSupps( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
-extern void                Fraig_ManIncrementTravId( Fraig_Man_t * pMan );
-extern void                Fraig_NodeSetTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
-extern int                 Fraig_NodeIsTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
-extern int                 Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
 extern int                 Fraig_NodeAndSimpleCase_rec( Fraig_Node_t * pOld, Fraig_Node_t * pNew );
 extern int                 Fraig_NodeIsExorType( Fraig_Node_t * pNode );
 extern void                Fraig_ManSelectBestChoice( Fraig_Man_t * p );
@@ -435,6 +433,10 @@ extern int                 Fraig_NodeSimsContained( Fraig_Man_t * pMan, Fraig_No
 extern int                 Fraig_NodeIsInSupergate( Fraig_Node_t * pOld, Fraig_Node_t * pNew );
 extern Fraig_NodeVec_t *   Fraig_CollectSupergate( Fraig_Node_t * pNode, int fStopAtMux );
 extern int                 Fraig_CountPis( Fraig_Man_t * p, Msat_IntVec_t * vVarNums );
+extern void                Fraig_ManIncrementTravId( Fraig_Man_t * pMan );
+extern void                Fraig_NodeSetTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
+extern int                 Fraig_NodeIsTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
+extern int                 Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
 /*=== fraigVec.c ===============================================================*/
 extern void                Fraig_NodeVecSortByRefCount( Fraig_NodeVec_t * p );
 
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index 65716340..cfdba619 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -42,6 +42,7 @@ int timeAssign;
 ***********************************************************************/
 void Fraig_ParamsSetDefault( Fraig_Params_t * pParams )
 {
+    memset( pParams, 0, sizeof(Fraig_Params_t) );
     pParams->nPatsRand  = FRAIG_PATTERNS_RANDOM;  // the number of words of random simulation info
     pParams->nPatsDyna  = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info
     pParams->nBTLimit   = 99;                     // the max number of backtracks to perform
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index da9e8e2b..17201e58 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -122,11 +122,23 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
 ***********************************************************************/
 int Fraig_ManCheckMiter( Fraig_Man_t * p )
 {
-    if ( p->vOutputs->pArray[0] == Fraig_Not(p->pConst1) )
+    Fraig_Node_t * pNode;
+    FREE( p->pModel );
+    // get the output node (it can be complemented!)
+    pNode = p->vOutputs->pArray[0];
+    // if the miter is constant 0, the problem is UNSAT
+    if ( pNode == Fraig_Not(p->pConst1) )
         return 1;
+    // consider the special case when the miter is constant 1
+    if ( pNode == p->pConst1 )
+    {
+        // in this case, any counter example will do to distinquish it from constant 0
+        // here we pick the counter example composed of all zeros
+        p->pModel = Fraig_ManAllocCounterExample( p );
+        return 0;
+    }
     // save the counter example
-    FREE( p->pModel );
-    p->pModel = Fraig_ManSaveCounterExample( p, Fraig_Regular(p->vOutputs->pArray[0]) );
+    p->pModel = Fraig_ManSaveCounterExample( p, pNode );
     // if the model is not found, return undecided
     if ( p->pModel == NULL )
         return -1;
diff --git a/src/sat/fraig/fraigTable.c b/src/sat/fraig/fraigTable.c
index 4dc6afdc..7a8af749 100644
--- a/src/sat/fraig/fraigTable.c
+++ b/src/sat/fraig/fraigTable.c
@@ -382,28 +382,52 @@ int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWor
   SeeAlso     []
 
 ***********************************************************************/
-int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand )
+int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int fCompl, int iWordLast, int fUseRand )
 {
     int i, v;
     assert( !Fraig_IsComplement(pNode1) );
     assert( !Fraig_IsComplement(pNode2) );
-    if ( fUseRand )
+    // take into account possible internal complementation
+    fCompl ^= pNode1->fInv;
+    fCompl ^= pNode2->fInv;
+    // find the pattern
+    if ( fCompl )
     {
-        // check the simulation info
-        for ( i = 0; i < iWordLast; i++ )
-            if ( pNode1->puSimR[i] !=  pNode2->puSimR[i] )
-                for ( v = 0; v < 32; v++ )
-                    if ( (pNode1->puSimR[i] ^ pNode2->puSimR[i]) & (1 << v) )
-                        return i * 32 + v;
+        if ( fUseRand )
+        {
+            for ( i = 0; i < iWordLast; i++ )
+                if ( pNode1->puSimR[i] != ~pNode2->puSimR[i] )
+                    for ( v = 0; v < 32; v++ )
+                        if ( (pNode1->puSimR[i] ^ ~pNode2->puSimR[i]) & (1 << v) )
+                            return i * 32 + v;
+        }
+        else
+        {
+            for ( i = 0; i < iWordLast; i++ )
+                if ( pNode1->puSimD[i] !=  ~pNode2->puSimD[i] )
+                    for ( v = 0; v < 32; v++ )
+                        if ( (pNode1->puSimD[i] ^ ~pNode2->puSimD[i]) & (1 << v) )
+                            return i * 32 + v;
+        }
     }
     else
     {
-        // check the simulation info
-        for ( i = 0; i < iWordLast; i++ )
-            if ( pNode1->puSimD[i] !=  pNode2->puSimD[i] )
-                for ( v = 0; v < 32; v++ )
-                    if ( (pNode1->puSimD[i] ^ pNode2->puSimD[i]) & (1 << v) )
-                        return i * 32 + v;
+        if ( fUseRand )
+        {
+            for ( i = 0; i < iWordLast; i++ )
+                if ( pNode1->puSimR[i] != pNode2->puSimR[i] )
+                    for ( v = 0; v < 32; v++ )
+                        if ( (pNode1->puSimR[i] ^ pNode2->puSimR[i]) & (1 << v) )
+                            return i * 32 + v;
+        }
+        else
+        {
+            for ( i = 0; i < iWordLast; i++ )
+                if ( pNode1->puSimD[i] !=  pNode2->puSimD[i] )
+                    for ( v = 0; v < 32; v++ )
+                        if ( (pNode1->puSimD[i] ^ pNode2->puSimD[i]) & (1 << v) )
+                            return i * 32 + v;
+        }
     }
     return -1;
 }
diff --git a/src/sat/fraig/fraigUtil.c b/src/sat/fraig/fraigUtil.c
index 6b7431f2..2155c4a3 100644
--- a/src/sat/fraig/fraigUtil.c
+++ b/src/sat/fraig/fraigUtil.c
@@ -962,6 +962,71 @@ Fraig_NodeVec_t * Fraig_CollectSupergate( Fraig_Node_t * pNode, int fStopAtMux )
     return vSuper;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_ManIncrementTravId( Fraig_Man_t * pMan )
+{
+    pMan->nTravIds2++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_NodeSetTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
+{
+    pNode->TravId2 = pMan->nTravIds2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_NodeIsTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
+{
+    return pNode->TravId2 == pMan->nTravIds2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
+{
+    return pNode->TravId2 == pMan->nTravIds2 - 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/sim/module.make b/src/sat/sim/module.make
deleted file mode 100644
index ac887acf..00000000
--- a/src/sat/sim/module.make
+++ /dev/null
@@ -1,6 +0,0 @@
-SRC +=  src/sat/sim/simMan.c \
-    src/sat/sim/simSat.c \
-    src/sat/sim/simSupp.c \
-    src/sat/sim/simSym.c \
-    src/sat/sim/simUnate.c \
-    src/sat/sim/simUtils.c
diff --git a/src/sat/sim/sim.h b/src/sat/sim/sim.h
deleted file mode 100644
index 7c4c50e3..00000000
--- a/src/sat/sim/sim.h
+++ /dev/null
@@ -1,136 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [sim.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Simulation package.]
-
-  Synopsis    [External declarations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: sim.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#ifndef __SIM_H__
-#define __SIM_H__
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Sim_Man_t_ Sim_Man_t;
-struct Sim_Man_t_
-{
-    // user specified parameters
-    Abc_Ntk_t *       pNtk;
-    // 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
-    // unateness info
-    Vec_Ptr_t *       vUnateVarsP;   // unate variables
-    Vec_Ptr_t *       vUnateVarsN;   // unate variables
-    // symmtry info
-    Extra_BitMat_t *  pMatSym;       // symmetric pairs
-    Extra_BitMat_t *  pMatNonSym;    // non-symmetric pairs
-    // simulation targets
-    Vec_Ptr_t *       vSuppTargs;    // support targets
-    Vec_Ptr_t *       vUnateTargs;   // unateness targets
-    Vec_Ptr_t *       vSymmTargs;    // symmetry targets
-    // internal data structures
-    Extra_MmFixed_t * pMmPat;   
-    Vec_Ptr_t *       vFifo;
-    Vec_Int_t *       vDiffs;
-    // runtime statistics
-    int               time1;
-    int               time2;
-    int               time3;
-    int               time4;
-};
-
-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 DEFITIONS                             ///
-////////////////////////////////////////////////////////////////////////
-
-#define SIM_NUM_WORDS(n)      ((n)/32 + (((n)%32) > 0))
-#define SIM_LAST_BITS(n)      ((((n)%32) > 0)? (n)%32 : 32)
-
-// 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(pMan,pNode,v)     Sim_SetBit((unsigned*)pMan->vSuppStr->pArray[(pNode)->Id],(v))
-#define Sim_SuppStrHasVar(pMan,pNode,v)     Sim_HasBit((unsigned*)pMan->vSuppStr->pArray[(pNode)->Id],(v))
-#define Sim_SuppFunSetVar(pMan,Output,v)    Sim_SetBit((unsigned*)pMan->vSuppFun->pArray[Output],(v))
-#define Sim_SuppFunHasVar(pMan,Output,v)    Sim_HasBit((unsigned*)pMan->vSuppFun->pArray[Output],(v))
-#define Sim_SimInfoSetVar(pMan,pNode,v)     Sim_SetBit((unsigned*)pMan->vSim0->pArray[(pNode)->Id],(v))
-#define Sim_SimInfoHasVar(pMan,pNode,v)     Sim_HasBit((unsigned*)pMan->vSim0->pArray[(pNode)->Id],(v))
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DECLARATIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== simMan.c ==========================================================*/
-extern Sim_Man_t *     Sim_ManStart( Abc_Ntk_t * pNtk );
-extern void            Sim_ManStop( 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 );
-extern void            Sim_ManPrintStats( Sim_Man_t * p );
-
-/*=== simSupp.c ==========================================================*/
-extern Sim_Man_t *     Sim_ComputeSupp( Abc_Ntk_t * pNtk );
-
-/*=== 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_UtilComputeStrSupp( Sim_Man_t * p );
-extern void            Sim_UtilAssignRandom( Sim_Man_t * p );
-extern void            Sim_UtilFlipSimInfo( Sim_Man_t * p, Abc_Obj_t * pNode );
-extern bool            Sim_UtilCompareSimInfo( 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 int             Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct );
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-#endif
-
diff --git a/src/sat/sim/simMan.c b/src/sat/sim/simMan.c
deleted file mode 100644
index 1dd4053c..00000000
--- a/src/sat/sim/simMan.c
+++ /dev/null
@@ -1,166 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [simMan.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Simulation manager.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: simMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "sim.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the simulatin manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk )
-{
-    Sim_Man_t * p;
-    int i;
-    // start the manager
-    p = ALLOC( Sim_Man_t, 1 );
-    memset( p, 0, sizeof(Sim_Man_t) );
-    p->pNtk = 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->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_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSuppWords, 1 );
-    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
-    p->vSuppTargs = Vec_PtrAlloc( p->nSuppBits );
-    p->vSuppTargs->nSize = p->nSuppBits;
-    for ( i = 0; i < p->nSuppBits; i++ )
-        p->vSuppTargs->pArray[i] = Vec_IntAlloc( 8 );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the simulatin 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->vUnateVarsP )  Sim_UtilInfoFree( p->vUnateVarsP ); 
-    if ( p->vUnateVarsN )  Sim_UtilInfoFree( p->vUnateVarsN ); 
-    if ( p->pMatSym )      Extra_BitMatrixStop( p->pMatSym );
-    if ( p->pMatNonSym )   Extra_BitMatrixStop( p->pMatNonSym );
-    if ( p->vSuppTargs )   Vec_PtrFreeFree( p->vSuppTargs );
-    if ( p->vUnateTargs )  Vec_PtrFree( p->vUnateTargs );
-    if ( p->vSymmTargs )   Vec_PtrFree( p->vSymmTargs );
-    if ( p->pMmPat )       Extra_MmFixedStop( p->pMmPat, 0 );
-    if ( p->vFifo )        Vec_PtrFree( p->vFifo );
-    if ( p->vDiffs )       Vec_IntFree( p->vDiffs );
-    free( p );
-}
-
-/**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 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints the manager statisticis.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_ManPrintStats( Sim_Man_t * p )
-{
-    printf( "Inputs = %d. Outputs = %d. Sim words = %d.\n", 
-        Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
-    printf( "Total struct supps = %6d.\n", Sim_UtilCountSuppSizes(p, 1) );
-    printf( "Total func supps   = %6d.\n", Sim_UtilCountSuppSizes(p, 0) );
-    printf( "Total targets      = %6d.\n", Vec_PtrSizeSize(p->vSuppTargs) );
-    printf( "Total sim patterns = %6d.\n", Vec_PtrSize(p->vFifo) );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/sim/simSat.c b/src/sat/sim/simSat.c
deleted file mode 100644
index b4e080fe..00000000
--- a/src/sat/sim/simSat.c
+++ /dev/null
@@ -1,48 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [simSat.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Simulation to determine functional support.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: simSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "sim.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
- 
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/sim/simSupp.c b/src/sat/sim/simSupp.c
deleted file mode 100644
index 570e8dc6..00000000
--- a/src/sat/sim/simSupp.c
+++ /dev/null
@@ -1,273 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [simSupp.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Simulation to determine functional support.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: simSupp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "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_UtilAssignFromFifo( Sim_Man_t * p );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Compute functional supports of the primary outputs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Sim_Man_t * Sim_ComputeSupp( Abc_Ntk_t * pNtk )
-{
-    Sim_Man_t * p;
-    int i, nSolved;
-
-//    srand( time(NULL) );
-    srand( 0xedfeedfe );
-
-    // start the simulation manager
-    p = Sim_ManStart( pNtk );
-    Sim_UtilComputeStrSupp( p );
-
-    // compute functional support using one round of random simulation
-    Sim_UtilAssignRandom( p );
-    Sim_ComputeSuppRound( p, 0 );
-
-    // set the support targets 
-    Sim_ComputeSuppSetTargets( p );
-printf( "Initial targets    = %5d.\n", Vec_PtrSizeSize(p->vSuppTargs) );
-    if ( Vec_PtrSizeSize(p->vSuppTargs) == 0 )
-        goto exit;
-
-    // compute patterns using one round of random simulation
-    Sim_UtilAssignRandom( p );
-    nSolved = Sim_ComputeSuppRound( p, 1 );
-printf( "First step targets = %5d.   Solved = %5d.\n", Vec_PtrSizeSize(p->vSuppTargs), nSolved );
-    if ( Vec_PtrSizeSize(p->vSuppTargs) == 0 )
-        goto exit;
-
-    // simulate until saturation
-    for ( i = 0; i < 10; i++ )
-    {
-        // compute additional functional support
-//         Sim_UtilAssignFromFifo( p );
-        Sim_UtilAssignRandom( p );
-        nSolved = Sim_ComputeSuppRound( p, 1 );
-printf( "Next step targets  = %5d.   Solved = %5d.\n", Vec_PtrSizeSize(p->vSuppTargs), nSolved );
-        if ( Vec_PtrSizeSize(p->vSuppTargs) == 0 )
-            goto exit;
-    }
-
-exit:
-//    return p;
-    Sim_ManStop( p );
-    return NULL;
-}
-
-/**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;
-    Abc_Obj_t * pNode;
-    int i, Counter = 0;
-    // perform one round of random simulation
-    Sim_UtilSimulate( p, 0 );
-    // iterate through the CIs and detect COs that depend on them
-    Abc_NtkForEachCi( p->pNtk, pNode, 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 )
-{
-    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;
-    // collect nodes by level in the TFO of the CI 
-    // (this procedure increments TravId of the collected nodes)
-    pNodeCi       = Abc_NtkCi( p->pNtk, iNumCi );
-    vNodesByLevel = Abc_DfsLevelized( pNodeCi, 0 );
-    // complement the simulation info of the selected CI
-    Sim_UtilFlipSimInfo( 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) );
-        Sim_UtilSimulateNode( p, pNode, 1, fType0, fType1 );
-    }
-    // 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_NtkCo( p->pNtk, Output );
-            // the output should be in the cone
-            assert( Abc_NodeIsTravIdCurrent(pNode) );
-
-            // simulate the node
-            Sim_UtilSimulateNode( p, pNode, 1, 1, 1 );
-
-            // skip if the simulation info is equal
-            if ( Sim_UtilCompareSimInfo( p, pNode ) )
-                continue;
-
-            // otherwise, we solved a new target
-            Vec_IntRemove( vTargets, Output );
-            Counter++;
-            // make sure this variable is not yet detected
-            assert( !Sim_SuppFunHasVar(p, Output, iNumCi) );
-            // set this variable
-            Sim_SuppFunSetVar( p, 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
-            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, pNodeCi, LuckyPat ) )
-                        Sim_SetBit( pPat->pData, v );
-                Vec_PtrPush( p->vFifo, pPat );
-                break;
-            }
-        }
-    }
-    else
-    {
-        Abc_NtkForEachCo( p->pNtk, pNode, Output )
-        {
-            if ( !Abc_NodeIsTravIdCurrent( pNode ) )
-                continue;
-            Sim_UtilSimulateNode( p, pNode, 1, 1, 1 );
-            if ( !Sim_UtilCompareSimInfo( p, pNode ) )
-            {
-                if ( !Sim_SuppFunHasVar(p, Output, iNumCi) )
-                    Counter++;
-                Sim_SuppFunSetVar( p, 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_IntPush( p->vSuppTargs->pArray[Num], i );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the new patterns from fifo.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilAssignFromFifo( Sim_Man_t * p )
-{
-    Sim_Pat_t * pPat;
-    int i;
-    for ( i = 0; i < p->nSimBits; i++ )
-    {
-        pPat = Vec_PtrPop( p->vFifo );
-
-    }
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/sim/simSym.c b/src/sat/sim/simSym.c
deleted file mode 100644
index 6b8bdaa3..00000000
--- a/src/sat/sim/simSym.c
+++ /dev/null
@@ -1,48 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [simSym.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Simulation to determine two-variable symmetries.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: simSym.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "sim.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
- 
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/sim/simUnate.c b/src/sat/sim/simUnate.c
deleted file mode 100644
index f7ad3557..00000000
--- a/src/sat/sim/simUnate.c
+++ /dev/null
@@ -1,48 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [simUnate.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Simulation to determine unateness of variables.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: simUnate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "sim.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
- 
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/sim/simUtils.c b/src/sat/sim/simUtils.c
deleted file mode 100644
index 5f5708f2..00000000
--- a/src/sat/sim/simUtils.c
+++ /dev/null
@@ -1,379 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [simUtils.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Various simulation utilities.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: simUtils.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "sim.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
- 
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**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;
-    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    [Computes structural supports.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilComputeStrSupp( Sim_Man_t * p )
-{
-    Abc_Obj_t * pNode;
-    unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
-    int i, k;
-    // assign the structural support to the PIs
-    Abc_NtkForEachCi( p->pNtk, pNode, i )
-        Sim_SuppStrSetVar( p, pNode, i );
-    // derive the structural supports of the internal nodes
-    Abc_NtkForEachNode( p->pNtk, pNode, i )
-    {
-        if ( Abc_NodeIsConst(pNode) )
-            continue;
-        pSimmNode  = p->vSuppStr->pArray[ pNode->Id ];
-        pSimmNode1 = p->vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
-        pSimmNode2 = p->vSuppStr->pArray[ Abc_ObjFaninId1(pNode) ];
-        for ( k = 0; k < p->nSuppWords; k++ )
-            pSimmNode[k] = pSimmNode1[k] | pSimmNode2[k];
-    }
-    // set the structural supports of the PO nodes
-    Abc_NtkForEachCo( p->pNtk, pNode, i )
-    {
-        pSimmNode  = p->vSuppStr->pArray[ pNode->Id ];
-        pSimmNode1 = p->vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
-        for ( k = 0; k < p->nSuppWords; k++ )
-            pSimmNode[k] = pSimmNode1[k];
-    }
-}
-
-/**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    [Flips the simulation info of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilFlipSimInfo( Sim_Man_t * p, Abc_Obj_t * pNode )
-{
-    unsigned * pSimInfo1, * pSimInfo2;
-    int k;
-    pSimInfo1 = p->vSim1->pArray[pNode->Id];
-    pSimInfo2 = p->vSim0->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_UtilCompareSimInfo( Sim_Man_t * p, Abc_Obj_t * pNode )
-{
-    unsigned * pSimInfo1, * pSimInfo2;
-    int k;
-    pSimInfo1 = p->vSim1->pArray[pNode->Id];
-    pSimInfo2 = p->vSim0->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 ( Abc_NodeIsConst(pNode) )
-            return;
-
-        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    [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, pNode, v );
-    }
-    else
-    {
-        Abc_NtkForEachCo( p->pNtk, pNode, i )
-            Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
-                Counter += Sim_SuppFunHasVar( p, i, v );
-    }
-    return Counter;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-