Version abc50905

10 files changed, 405 insertions, 239 deletions

diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index e7d6fec6..a21dd520 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -78,13 +78,13 @@ clk = clock();
     if ( fPrecompute )
     {   // precompute subgraphs
         Rwr_ManPrecompute( p );
+//        Rwr_ManPrint( p );
         Rwr_ManWriteToArray( p );
-        Rwr_ManPrint( p );
     }
     else
     {   // load saved subgraphs
         Rwr_ManLoadFromArray( p, 0 );
-        Rwr_ManPrint( p );
+//        Rwr_ManPrint( p );
         Rwr_ManPreprocess( p );
     }
 p->timeStart = clock() - clk;
diff --git a/src/opt/sim/sim.h b/src/opt/sim/sim.h
index 9b4d9699..afed7190 100644
--- a/src/opt/sim/sim.h
+++ b/src/opt/sim/sim.h
@@ -21,6 +21,12 @@
 #ifndef __SIM_H__
 #define __SIM_H__
 
+/*
+    The ideas realized in this package are described in the paper:
+    "Detecting Symmetries in Boolean Functions using Circuit Representation, 
+    Simulation, and Satisfiability".
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -45,7 +51,8 @@ struct Sym_Man_t_
     int               nSimWords;     // the number of bits in simulation info
     Vec_Ptr_t *       vSim;          // simulation info
     // support information
-    Vec_Ptr_t *       vSuppFun;      // functional supports
+    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
@@ -56,6 +63,14 @@ struct Sym_Man_t_
     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;
@@ -64,8 +79,12 @@ struct Sym_Man_t_
     int               nPairsSymm;
     int               nPairsSymmStr;
     int               nPairsNonSymm;
+    int               nPairsRem;
     int               nPairsTotal;
     // runtime statistics
+    int               timeStruct;
+    int               timeCount;
+    int               timeMatr;
     int               timeSim;
     int               timeFraig;
     int               timeSat;
@@ -91,6 +110,7 @@ struct Sim_Man_t_
     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;
@@ -148,7 +168,7 @@ struct Sim_Pat_t_
 ////////////////////////////////////////////////////////////////////////
 
 /*=== simMan.c ==========================================================*/
-extern Sym_Man_t *     Sym_ManStart( Abc_Ntk_t * pNtk );
+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 );
@@ -158,11 +178,13 @@ extern Sim_Pat_t *     Sim_ManPatAlloc( Sim_Man_t * p );
 extern void            Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat );
 /*=== simSupp.c ==========================================================*/
 extern Vec_Ptr_t *     Sim_ComputeStrSupp( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t *     Sim_ComputeFunSupp( 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 );
+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 );
+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 ==========================================================*/
@@ -180,7 +202,8 @@ extern int             Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct );
 extern int             Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords );
 extern void            Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords );
 extern int             Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters );
-extern int             Sim_UtilCountPairs( Vec_Ptr_t * vMatrs, Vec_Int_t * vCounters );
+extern void            Sim_UtilCountPairsAll( Sym_Man_t * p );
+extern int             Sim_UtilMatrsAreDisjoint( Sym_Man_t * p );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/sim/simMan.c b/src/opt/sim/simMan.c
index 02d59343..780ecfd8 100644
--- a/src/opt/sim/simMan.c
+++ b/src/opt/sim/simMan.c
@@ -40,10 +40,10 @@
   SeeAlso     []
 
 ***********************************************************************/
-Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk )
+Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Sym_Man_t * p;
-    int i;
+    int i, v; 
     // start the manager
     p = ALLOC( Sym_Man_t, 1 );
     memset( p, 0, sizeof(Sym_Man_t) );
@@ -69,8 +69,15 @@ Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk )
     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 );
+    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;
 }
 
@@ -92,11 +99,14 @@ void Sym_ManStop( Sym_Man_t * 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 );
@@ -121,17 +131,18 @@ void Sym_ManStop( Sym_Man_t * p )
 ***********************************************************************/
 void Sym_ManPrintStats( Sym_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_VecSizeSize(p->vSuppTargs) );
-    printf( "Total sim patterns = %6d.\n", Vec_PtrSize(p->vFifo) );
-*/
-    printf( "Sat runs SAT       = %6d.\n", p->nSatRunsSat );
-    printf( "Sat runs UNSAT     = %6d.\n", p->nSatRunsUnsat );
+//    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 );
@@ -217,14 +228,12 @@ void Sim_ManStop( Sim_Man_t * p )
 ***********************************************************************/
 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_VecSizeSize(p->vSuppTargs) );
-    printf( "Total sim patterns = %6d.\n", Vec_PtrSize(p->vFifo) );
-    printf( "Sat runs SAT       = %6d.\n", p->nSatRunsSat );
-    printf( "Sat runs UNSAT     = %6d.\n", p->nSatRunsUnsat );
+//    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 );
diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c
index 2f380866..576e19cc 100644
--- a/src/opt/sim/simSupp.c
+++ b/src/opt/sim/simSupp.c
@@ -99,13 +99,12 @@ Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk )
+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( time(NULL) );
     srand( 0xABC );
 
     // start the simulation manager
@@ -117,35 +116,40 @@ Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk )
 
     // set the support targets 
     Sim_ComputeSuppSetTargets( p );
-printf( "Initial targets    = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) );
+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 );
-printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.\n", Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) );
-    if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
-        goto exit;
-    }
+        // 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) );
+    }
 
-    // simulate until saturation
+    // try to solve the support targets
     while ( Vec_VecSizeSize(p->vSuppTargs) > 0 )
     {
-        // solve randomly a given number of targets
+        // solve targets until the first disproved one (which gives counter-example)
         Sim_SolveTargetsUsingSat( p, p->nSimWords/p->nSuppWords );
         // compute additional functional support
-//        Sim_UtilAssignRandom( p );
         Sim_UtilAssignFromFifo( p );
         nSolved = Sim_ComputeSuppRound( p, 1 );
-printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.  SAT runs = %3d.\n", 
+
+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 );
@@ -166,7 +170,6 @@ exit:
 int Sim_ComputeSuppRound( Sim_Man_t * p, bool fUseTargets )
 {
     Vec_Int_t * vTargets;
-    Abc_Obj_t * pNode;
     int i, Counter = 0;
     int clk;
     // perform one round of random simulation
@@ -174,7 +177,7 @@ clk = clock();
     Sim_UtilSimulate( p, 0 );
 p->timeSim += clock() - clk;
     // iterate through the CIs and detect COs that depend on them
-    Abc_NtkForEachCi( p->pNtk, pNode, i )
+    for ( i = p->iInput; i < p->nInputs; i++ )
     {
         vTargets = p->vSuppTargs->pArray[i];
         if ( fUseTargets && vTargets->nSize == 0 )
@@ -207,7 +210,8 @@ int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets )
     int fFirst = 1;
     int clk;
     // collect nodes by level in the TFO of the CI 
-    // (this procedure increments TravId of the collected nodes)
+    // 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 );
@@ -232,13 +236,10 @@ p->timeSim += clock() - clk;
             // get the target output
             Output = vTargets->pArray[i];
             // get the target node
-            pNode  = Abc_NtkCo( p->pNtk, Output );
+            pNode  = Abc_ObjFanin0( 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_UtilInfoCompare( p, pNode ) )
                 continue;
@@ -283,12 +284,13 @@ printf( "\n" );
         {
             if ( !Abc_NodeIsTravIdCurrent( pNode ) )
                 continue;
-            Sim_UtilSimulateNode( p, pNode, 1, 1, 1 );
-            if ( !Sim_UtilInfoCompare( p, pNode ) )
+            if ( !Sim_UtilInfoCompare( p, Abc_ObjFanin0(pNode) ) )
             {
                 if ( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) )
+                {
                     Counter++;
-                Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi );
+                    Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi );
+                }
             }
         }
     }
@@ -365,7 +367,7 @@ void Sim_UtilAssignFromFifo( Sim_Man_t * p )
     Abc_Obj_t * pNode;
     Sim_Pat_t * pPat;
     unsigned * pSimInfo;
-    int iWord, iWordLim, i, w;
+    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
@@ -379,7 +381,7 @@ void Sim_UtilAssignFromFifo( Sim_Man_t * p )
             // get the first word of the next series
             iWordLim = iWord + 1; 
             // set the pattern for all PIs from iBit to iWord + p->nInputs
-            iBeg = ABC_MAX( 0, pPat->Input - 16 );
+            iBeg = p->iInput;
             iEnd = ABC_MIN( iBeg + 32, p->nInputs );
 //            for ( i = iBeg; i < iEnd; i++ )
             Abc_NtkForEachCi( p->pNtk, pNode, i )
@@ -397,9 +399,12 @@ void Sim_UtilAssignFromFifo( Sim_Man_t * p )
         }
         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 + p->nSuppWords < p->nSimWords)? iWord + p->nSuppWords : p->nSimWords; 
-            // set the pattern for all PIs from iBit to iWord + p->nInputs
+            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];
@@ -413,8 +418,10 @@ void Sim_UtilAssignFromFifo( Sim_Man_t * p )
                     for ( w = iWord; w < iWordLim; w++ )
                         pSimInfo[w] = 0;
                 }
-                // flip one bit
                 Sim_XorBit( pSimInfo + iWord, i );
+                // flip one bit
+//                if ( i >= p->iInput )
+//                    Sim_XorBit( pSimInfo + iWord, i-p->iInput );
             }
         }
         Sim_ManPatFree( p, pPat );
@@ -456,10 +463,11 @@ void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit )
     {
         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 target into a fraig
+        // transform the miter into a fraig
         Fraig_ParamsSetDefault( &Params );
         Params.fInternal = 1;
 clk = clock();
@@ -502,23 +510,23 @@ p->timeSat += clock() - clk;
             Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
                 if ( pModel[v] )
                     Sim_SetBit( pPat->pData, v );
-            Sim_XorBit( pPat->pData, Input ); // flip the given bit
+            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 target
+        // 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;
-        // switch to the next input if we found one model
-        if ( pModel )
-            break;
     }
 }
 
diff --git a/src/opt/sim/simSwitch.c b/src/opt/sim/simSwitch.c
index 06b730fc..b43597f3 100644
--- a/src/opt/sim/simSwitch.c
+++ b/src/opt/sim/simSwitch.c
@@ -72,8 +72,8 @@ Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns )
     vNodes  = Abc_AigDfs( pNtk, 1, 0 );
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
-        Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords );
         pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
+        Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords );
         pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords );
     }
     Vec_PtrFree( vNodes );
diff --git a/src/opt/sim/simSym.c b/src/opt/sim/simSym.c
index 706b13dc..c452bb1b 100644
--- a/src/opt/sim/simSym.c
+++ b/src/opt/sim/simSym.c
@@ -40,52 +40,100 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk )
+int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Sym_Man_t * p;
     Vec_Ptr_t * vResult;
     int Result;
-    int i, clk = clock();
+    int i, clk, clkTotal = clock();
 
-//    srand( time(NULL) );
     srand( 0xABC );
 
     // start the simulation manager
-    p = Sym_ManStart( pNtk );
-    p->nPairsTotal = Sim_UtilCountAllPairs( p->vSuppFun, p->nSimWords, p->vPairsTotal );
+    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
-    Sim_SymmsStructCompute( pNtk, p->vMatrSymms );
-    p->nPairsSymm = p->nPairsSymmStr = Sim_UtilCountPairs( p->vMatrSymms, p->vPairsSym );
+clk = clock();
+    Sim_SymmsStructCompute( pNtk, p->vMatrSymms, p->vSuppFun );
+p->timeStruct = clock() - clk;
 
-printf( "Total = %6d.  Sym = %6d.  NonSym = %6d.  Remaining = %6d.\n", 
-       p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm );
+    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++ )
     {
-        // generate random pattern
-        Sim_UtilGetRandom( p->uPatRand, p->nSimWords );
         // simulate this pattern
+        Sim_UtilGetRandom( p->uPatRand, p->nSimWords );
         Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
-        if ( i % 100 != 0 )
+        if ( i % 50 != 0 )
             continue;
+        // check disjointness
+        assert( Sim_UtilMatrsAreDisjoint( p ) );
         // count the number of pairs
-        p->nPairsSymm    = Sim_UtilCountPairs( p->vMatrSymms,    p->vPairsSym );
-        p->nPairsNonSymm = Sim_UtilCountPairs( p->vMatrNonSymms, p->vPairsNonSym );
+        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 );
+    }
 
-printf( "Total = %6d.  Sym = %6d.  NonSym = %6d.  Remaining = %6d.\n", 
-       p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm );
+    // 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 );
+
     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
index 88e33161..db9917b3 100644
--- a/src/opt/sim/simSymSat.c
+++ b/src/opt/sim/simSymSat.c
@@ -20,13 +20,14 @@
 
 #include "abc.h"
 #include "sim.h"
+#include "fraig.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int   Fraig_SymmsSatProveOne( Fraig_Man_t * p, int Var1, int Var2 );
-static int   Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat );
+extern int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern );
+extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -34,95 +35,88 @@ static int   Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat )
 
 /**Function*************************************************************
 
-  Synopsis    [Performs the SAT based check.]
+  Synopsis    [Tries to prove the remaining pairs using SAT.]
 
-  Description [Given two bit matrices, with symm info and non-symm info, 
-  checks the remaining pairs.]
+  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     []
 
 ***********************************************************************/
-void Fraig_SymmsSatComputeOne( Fraig_Man_t * p, Extra_BitMat_t * pMatSym, Extra_BitMat_t * pMatNonSym )
+int Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern )
 {
-    int VarsU[512], VarsV[512];
-    int nVarsU, nVarsV;
-    int v, u, i, k;
-    int Counter = 0;
-    int satCalled = 0;
-    int satProved = 0;
-    double Density;
-    int clk = clock();
-
-    extern int symsSat;
-    extern int Fraig_CountBits( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
-
-
-    // count undecided pairs
-    for ( v = 0; v < p->vInputs->nSize; v++ )
-    for ( u = v+1; u < p->vInputs->nSize; u++ )
-    {
-        if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
-            continue;
-        Counter++;
-    }
-    // compute the density of 1's in the input space of the functions
-    Density = (double)Fraig_CountBits(p, Fraig_Regular(p->vOutputs->pArray[0])) * 100.0 / FRAIG_SIM_ROUNDS / 32;
-
-    printf( "Ins = %3d. Pairs to test = %4d. Dens = %5.2f %%. ", 
-        p->vInputs->nSize, Counter, Density );
+    Vec_Int_t * vSupport;
+    Extra_BitMat_t * pMatSym, * pMatNonSym;
+    int Index1, Index2, Index3, IndexU, IndexV;
+    int v, u, i, k, b, out;
 
-
-    // go through the remaining variable pairs
-    for ( v = 0; v < p->vInputs->nSize; v++ )
-    for ( u = v+1; u < p->vInputs->nSize; u++ )
+    // iterate through outputs
+    for ( out = p->iOutput; out < p->nOutputs; out++ )
     {
-        if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
-            continue;
-        symsSat++;
-        satCalled++;
-
-        // collect the variables that are symmetric with each
-        nVarsU = nVarsV = 0;
-        for ( i = 0; i < p->vInputs->nSize; i++ )
+        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, u, i ) )
-                VarsU[nVarsU++] = i;
-            if ( Extra_BitMatrixLookup1( pMatSym, v, i ) )
-                VarsV[nVarsV++] = i;
-        }
+            if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
+                continue;
+            p->nSatRuns++;
 
-        if ( Fraig_SymmsSatProveOne( p, v, u ) )
-        { // update the symmetric variable info            
-//printf( "%d sym %d\n", v, u );
-            for ( i = 0; i < nVarsU; i++ )
-            for ( k = 0; k < nVarsV; k++ )
+            // collect the support variables that are symmetric with u and v
+            Vec_IntClear( p->vVarsU );
+            Vec_IntClear( p->vVarsV );
+            Vec_IntForEachEntry( vSupport, b, Index3 )
             {
-                Extra_BitMatrixInsert1( pMatSym, VarsU[i], VarsV[k] );   // Theorem 1
-                Extra_BitMatrixInsert2( pMatSym, VarsU[i], VarsV[k] );   // Theorem 1
-                Extra_BitMatrixOrTwo( pMatNonSym, VarsU[i], VarsV[k] );  // Theorem 2
+                if ( Extra_BitMatrixLookup1( pMatSym, u, b ) )
+                    Vec_IntPush( p->vVarsU, b );
+                if ( Extra_BitMatrixLookup1( pMatSym, v, b ) )
+                    Vec_IntPush( p->vVarsV, b );
             }
-            satProved++;
-        }
-        else
-        { // update the assymmetric variable info
-//printf( "%d non-sym %d\n", v, u );
-            for ( i = 0; i < nVarsU; i++ )
-            for ( k = 0; k < nVarsV; k++ )
-            {
-                Extra_BitMatrixInsert1( pMatNonSym, VarsU[i], VarsV[k] );   // Theorem 3
-                Extra_BitMatrixInsert2( pMatNonSym, VarsU[i], VarsV[k] );   // Theorem 3
+
+            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;
+
             }
         }
-//Extra_BitMatrixPrint( pMatSym );
-//Extra_BitMatrixPrint( pMatNonSym );
+        // make sure that the symmetry matrix contains only cliques
+        assert( Extra_BitMatrixIsClique( pMatSym ) );
     }
-printf( "SAT calls = %3d. Proved = %3d. ", satCalled, satProved );
-PRT( "Time", clock() - clk );
 
-    // make sure that the symmetry matrix contains only cliques
-    assert( Fraig_SymmsIsCliqueMatrix( p, pMatSym ) );
+    // mark that we finished all outputs
+    p->iOutput = p->nOutputs;
+    return 0;
 }
 
 /**Function*************************************************************
@@ -136,65 +130,68 @@ PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Fraig_SymmsSatProveOne( Fraig_Man_t * p, int Var1, int Var2 )
-{
-    Fraig_Node_t * pCof01, * pCof10, * pVar1, * pVar2;
-    int RetValue;
-    int nSatRuns = p->nSatCalls;
-    int nSatProof = p->nSatProof;
-
-    p->nBTLimit = 10;  // set the backtrack limit
-
-    pVar1 = p->vInputs->pArray[Var1];
-    pVar2 = p->vInputs->pArray[Var2];
-    pCof01 = Fraig_CofactorTwo( p, p->vOutputs->pArray[0], pVar1, Fraig_Not(pVar2) );
-    pCof10 = Fraig_CofactorTwo( p, p->vOutputs->pArray[0], Fraig_Not(pVar1), pVar2 );
-
-//printf( "(%d,%d)", p->nSatCalls - nSatRuns, p->nSatProof - nSatProof );
-
-//    RetValue = (pCof01 == pCof10);
-//    RetValue = Fraig_NodesAreaEqual( p, pCof01, pCof10 );
-    RetValue = Fraig_NodesAreEqual( p, pCof01, pCof10, -1 );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [A sanity check procedure.]
-
-  Description [Makes sure that the symmetry information in the matrix
-  is closed w.r.t. the relationship of transitivity (that is the symmetry
-  graph is composed of cliques).]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat )
+int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern )
 {
-    int v, u, i;
-    for ( v = 0; v < p->vInputs->nSize; v++ )
-    for ( u = v+1; u < p->vInputs->nSize; u++ )
+    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;
+
+clk = clock();
+    pMan = Abc_NtkToFraig( pMiter, &Params, 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 )
     {
-        if ( !Extra_BitMatrixLookup1( pMat, v, u ) )
-            continue;
-        // v and u are symmetric
-        for ( i = 0; i < p->vInputs->nSize; i++ )
-        {
-            if ( i == v || i == u )
-                continue;
-            // i is neither v nor u
-            // the symmetry status of i is the same w.r.t. to v and u
-            if ( Extra_BitMatrixLookup1( pMat, i, v ) != Extra_BitMatrixLookup1( pMat, i, u ) )
-                return 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 );
     }
-    return 1;
+    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
index 53fc4ac2..94028c47 100644
--- a/src/opt/sim/simSymSim.c
+++ b/src/opt/sim/simSymSim.c
@@ -26,7 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat );
-static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Extra_BitMat_t * pMatrix, int Output );
+static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Vec_Ptr_t * vMatrsNonSym, int Output );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -46,26 +46,36 @@ static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNo
 void Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPat, Vec_Ptr_t * vMatrsNonSym )
 {
     Abc_Obj_t * pNode;
-    int i;
+    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 );
     }
+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_NodeIsConst(pNode) )
             continue;
-        if ( Vec_IntEntry(p->vPairsTotal,i) == Vec_IntEntry(p->vPairsSym,i) + Vec_IntEntry(p->vPairsNonSym,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 )
             continue;
-        Sim_SymmsDeriveInfo( p, pPat, pNode, Vec_PtrEntry(vMatrsNonSym, i), i );
+        Sim_SymmsDeriveInfo( p, pPat, pNode, vMatrsNonSym, i );
     }
+p->timeMatr += clock() - clk;
 }
 
 /**Function*************************************************************
@@ -114,40 +124,44 @@ void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat )
   SeeAlso     []
 
 ***********************************************************************/
-void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Extra_BitMat_t * pMat, int Output )
+void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Vec_Ptr_t * vMatrsNonSym, int Output )
 {
-    unsigned * pSuppInfo;
+    Extra_BitMat_t * pMat;
+    Vec_Int_t * vSupport;
+    unsigned * pSupport;
     unsigned * pSimInfo;
-    int i, w;
-    // get the simuation info for the node
+    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 );
-    pSuppInfo = Vec_PtrEntry( p->vSuppFun, Output );
     // generate vectors A1 and A2
     for ( w = 0; w < p->nSimWords; w++ )
     {
-        p->uPatCol[w] = pSuppInfo[w] & pPat[w] &  pSimInfo[w];
-        p->uPatRow[w] = pSuppInfo[w] & pPat[w] & ~pSimInfo[w];
+        p->uPatCol[w] = pSupport[w] & pPat[w] &  pSimInfo[w];
+        p->uPatRow[w] = pSupport[w] & pPat[w] & ~pSimInfo[w];
     }
     // add two dimensions
-    for ( i = 0; i < p->nInputs; i++ )
+    Vec_IntForEachEntry( vSupport, i, Index )
         if ( Sim_HasBit( p->uPatCol, i ) )
             Extra_BitMatrixOr( pMat, i, p->uPatRow );
     // add two dimensions
-    for ( i = 0; i < p->nInputs; i++ )
+    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] = pSuppInfo[w] & ~pPat[w] &  pSimInfo[w];
-        p->uPatRow[w] = pSuppInfo[w] & ~pPat[w] & ~pSimInfo[w];
+        p->uPatCol[w] = pSupport[w] & ~pPat[w] &  pSimInfo[w];
+        p->uPatRow[w] = pSupport[w] & ~pPat[w] & ~pSimInfo[w];
     }
     // add two dimensions
-    for ( i = 0; i < p->nInputs; i++ )
+    Vec_IntForEachEntry( vSupport, i, Index )
         if ( Sim_HasBit( p->uPatCol, i ) )
             Extra_BitMatrixOr( pMat, i, p->uPatRow );
     // add two dimensions
-    for ( i = 0; i < p->nInputs; i++ )
+    Vec_IntForEachEntry( vSupport, i, Index )
         if ( Sim_HasBit( p->uPatRow, i ) )
             Extra_BitMatrixOr( pMat, i, p->uPatCol );
 }
diff --git a/src/opt/sim/simSymStr.c b/src/opt/sim/simSymStr.c
index c3059d84..ed7e93bf 100644
--- a/src/opt/sim/simSymStr.c
+++ b/src/opt/sim/simSymStr.c
@@ -37,7 +37,7 @@ static int   Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, V
 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 );
+static void  Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport );
 static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk );
 
 ////////////////////////////////////////////////////////////////////////
@@ -55,7 +55,7 @@ static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk );
   SeeAlso     []
 
 ***********************************************************************/
-void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs )
+void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * vSuppFun )
 {
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pTemp;
@@ -84,7 +84,7 @@ void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs )
         pTemp = Abc_ObjFanin0(pTemp);
         if ( Abc_ObjIsCi(pTemp) || Abc_NodeIsConst(pTemp) )
             continue;
-        Sim_SymmsTransferToMatrix( Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp) );
+        Sim_SymmsTransferToMatrix( Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp), Vec_PtrEntry(vSuppFun, i) );
     }
     // clean the intermediate results
     Sim_UtilInfoFree( pNtk->vSupps );
@@ -92,7 +92,8 @@ void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs )
     Abc_NtkForEachCi( pNtk, pTemp, i )
         Vec_IntFree( SIM_READ_SYMMS(pTemp) );
     Vec_PtrForEachEntry( vNodes, pTemp, i )
-        Vec_IntFree( SIM_READ_SYMMS(pTemp) );
+        if ( !Abc_NodeIsConst(pTemp) )
+            Vec_IntFree( SIM_READ_SYMMS(pTemp) );
     Vec_PtrFree( vNodes );
     free( pMap );
 }
@@ -429,7 +430,7 @@ void Sim_SymmsTrans( Vec_Int_t * vSymms )
   SeeAlso     []
 
 ***********************************************************************/
-void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms )
+void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport )
 {
     int i, Ind1, Ind2, nInputs;
     unsigned uSymm;
@@ -443,6 +444,10 @@ void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms )
         uSymm = (unsigned)vSymms->pArray[i];
         Ind1 = (uSymm & 0xffff);
         Ind2 = (uSymm >> 16);
+        // 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 );
     }
diff --git a/src/opt/sim/simUtils.c b/src/opt/sim/simUtils.c
index 5a57ca2d..4b89c650 100644
--- a/src/opt/sim/simUtils.c
+++ b/src/opt/sim/simUtils.c
@@ -436,18 +436,80 @@ int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCou
   SeeAlso     []
 
 ***********************************************************************/
-int Sim_UtilCountPairs( Vec_Ptr_t * vMatrs, Vec_Int_t * vCounters )
+int Sim_UtilCountPairsOne( Extra_BitMat_t * pMat, Vec_Int_t * vSupport )
 {
-    Extra_BitMat_t * vMat;
-    int Counter, nPairs, i;
-    Counter = 0;
-    Vec_PtrForEachEntry( vMatrs, vMat, i )
+    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     []
+
+***********************************************************************/
+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++ )
     {
-        nPairs = Extra_BitMatrixCountOnesUpper( vMat );
-        Vec_IntWriteEntry( vCounters, i, nPairs );
-        Counter += nPairs;
+        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 );
     }
-    return Counter;
+//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;
 }
 
 ////////////////////////////////////////////////////////////////////////