New SAT-based optimization package.

2 files changed, 376 insertions, 27 deletions

diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c
index 2120a8f9..6b311e01 100644
--- a/src/opt/sbd/sbdCore.c
+++ b/src/opt/sbd/sbdCore.c
@@ -48,6 +48,7 @@ struct Sbd_Man_t_
     Vec_Int_t *     vTfo;        // TFO (excludes node, includes roots)
     Vec_Int_t *     vLeaves;     // leaves (TFI leaves + extended leaves)
     Vec_Int_t *     vTfi;        // TFI (TFI + node + extended TFI)
+    Vec_Int_t *     vDivs;       // divisors
     Vec_Int_t *     vCounts[2];  // counters of zeros and ones
 };
 
@@ -76,7 +77,7 @@ void Sbd_ParSetDefault( Sbd_Par_t * pPars )
 {
     memset( pPars, 0, sizeof(Sbd_Par_t) );
     pPars->nLutSize     = 4;  // target LUT size
-    pPars->nTfoLevels   = 4;  // the number of TFO levels (windowing)
+    pPars->nTfoLevels   = 3;  // the number of TFO levels (windowing)
     pPars->nTfoFanMax   = 4;  // the max number of fanouts (windowing)
     pPars->nWinSizeMax  = 0;  // maximum window size (windowing)
     pPars->nBTLimit     = 0;  // maximum number of SAT conflicts 
@@ -102,6 +103,7 @@ Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax )
     Vec_Wec_t * vTfos = Vec_WecStart( Gia_ManObjNum(p) ); // TFO nodes with roots marked
     Vec_Wec_t * vTemp = Vec_WecStart( Gia_ManObjNum(p) ); // storage
     Vec_Int_t * vNodes, * vNodes0, * vNodes1;
+    Vec_Bit_t * vPoDrivers = Vec_BitStart( Gia_ManObjNum(p) );
     int i, k, k2, Id, Fan;
     Gia_ManLevelNum( p );
     Gia_ManCreateRefs( p );
@@ -112,13 +114,15 @@ Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax )
         Vec_IntGrow( vNodes, 1 );
         Vec_IntPush( vNodes, Id );
     }
+    Gia_ManForEachCoDriverId( p, Id, i )
+        Vec_BitWriteEntry( vPoDrivers, Id, 1 );
     Gia_ManForEachAndId( p, Id )
     {
-        int fAlwaysRoot = Gia_ObjRefNumId(p, Id) >= nTfoFanMax;
+        int fAlwaysRoot = Vec_BitEntry(vPoDrivers, Id) || (Gia_ObjRefNumId(p, Id) >= nTfoFanMax);
         vNodes0 = Vec_WecEntry( vTemp, Gia_ObjFaninId0(Gia_ManObj(p, Id), Id) );
         vNodes1 = Vec_WecEntry( vTemp, Gia_ObjFaninId1(Gia_ManObj(p, Id), Id) );
         vNodes = Vec_WecEntry( vTemp, Id );
-        Vec_IntTwoMerge2( vNodes, vNodes0, vNodes1 );
+        Vec_IntTwoMerge2( vNodes0, vNodes1, vNodes );
         k2 = 0;
         Vec_IntForEachEntry( vNodes, Fan, k )
         {
@@ -127,10 +131,16 @@ Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax )
             if ( !fRoot ) Vec_IntWriteEntry( vNodes, k2++, Fan );
         }
         Vec_IntShrink( vNodes, k2 );
-        Vec_IntPush( vNodes, Id );
+        if ( fAlwaysRoot )
+            Vec_WecPush( vTfos, Id, Abc_Var2Lit(Id, 1) );
+        else
+            Vec_IntPush( vNodes, Id );
     }
     Vec_WecFree( vTemp );
+    Vec_BitFree( vPoDrivers );
+
     // print the results
+    if ( 1 )
     Vec_WecForEachLevel( vTfos, vNodes, i )
     {
         if ( !Gia_ObjIsAnd(Gia_ManObj(p, i)) )
@@ -139,8 +149,8 @@ Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax )
         Vec_IntForEachEntry( vNodes, Fan, k )
             printf( "%d%s ", Abc_Lit2Var(Fan), Abc_LitIsCompl(Fan)? "*":"" );
         printf( "\n" );
-
     }
+
     return vTfos;
 }
 
@@ -171,6 +181,7 @@ Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars )
     p->vCover     = Vec_IntStart( 100 );
     p->vLeaves    = Vec_IntAlloc( Gia_ManCiNum(pGia) );
     p->vTfi       = Vec_IntAlloc( Gia_ManAndNum(pGia) );
+    p->vDivs      = Vec_IntAlloc( Gia_ManObjNum(pGia) );
     p->vCounts[0] = Vec_IntAlloc( 100 );
     p->vCounts[1] = Vec_IntAlloc( 100 );
     // start input cuts
@@ -199,8 +210,10 @@ void Sbd_ManStop( Sbd_Man_t * p )
     Vec_IntFree( p->vCover  );
     Vec_IntFree( p->vLeaves );
     Vec_IntFree( p->vTfi );
+    Vec_IntFree( p->vDivs );
     Vec_IntFree( p->vCounts[0] );
     Vec_IntFree( p->vCounts[1] );
+    ABC_FREE( p );
 }
 
 
@@ -234,20 +247,38 @@ void Sbd_ManWindowSim_rec( Sbd_Man_t * p, int Node )
     Sbd_ManWindowSim_rec( p, Gia_ObjFaninId1(pObj, Node) );
     Vec_IntPush( p->vTfi, Node );
     // simulate
-    Abc_TtAndCompl( Sbd_ObjSim0(p, Node), 
-        Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj), 
-        Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), 
-        p->pPars->nWords );
-    if ( pObj->fMark0 )
-        Abc_TtAndCompl( Sbd_ObjSim1(p, Node), 
-            Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj), 
-            Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), 
+    if ( Gia_ObjIsXor(pObj) )
+    {
+        Abc_TtXor( Sbd_ObjSim0(p, Node), 
+            Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), 
+            Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), 
+            p->pPars->nWords, 
+            Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
+        if ( pObj->fMark0 )
+            Abc_TtXor( Sbd_ObjSim1(p, Node), 
+                Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), 
+                Gia_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), 
+                p->pPars->nWords, 
+                Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
+    }
+    else
+    {
+        Abc_TtAndCompl( Sbd_ObjSim0(p, Node), 
+            Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj), 
+            Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), 
             p->pPars->nWords );
+        if ( pObj->fMark0 )
+            Abc_TtAndCompl( Sbd_ObjSim1(p, Node), 
+                Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj), 
+                Gia_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), 
+                p->pPars->nWords );
+    }
 }
 void Sbd_ManPropagateControl( Sbd_Man_t * p, int Node )
 {
-    int iObj0 = Gia_ObjFaninId0(Gia_ManObj(p->pGia, Node), Node);
-    int iObj1 = Gia_ObjFaninId1(Gia_ManObj(p->pGia, Node), Node);
+    Gia_Obj_t * pNode = Gia_ManObj(p->pGia, Node);
+    int iObj0 = Gia_ObjFaninId0(pNode, Node);
+    int iObj1 = Gia_ObjFaninId1(pNode, Node);
     word * pCtrl  = Sbd_ObjSim2(p, Node);
     word * pCtrl0 = Sbd_ObjSim2(p, iObj0);
     word * pCtrl1 = Sbd_ObjSim2(p, iObj1);
@@ -255,10 +286,13 @@ void Sbd_ManPropagateControl( Sbd_Man_t * p, int Node )
     word * pSims0 = Sbd_ObjSim0(p, iObj0);
     word * pSims1 = Sbd_ObjSim0(p, iObj1);
     int w;
+//    printf( "Node %2d : %d %d\n", Node, (int)(pSims[0] & 1), (int)(pCtrl[0] & 1) );
     for ( w = 0; w < p->pPars->nWords; w++ )
     {
-        pCtrl0[w] = pCtrl[w] & (pSims[w] | pSims1[w]);
-        pCtrl1[w] = pCtrl[w] & (pSims[w] | pSims0[w] | (~pSims0[w] & ~pSims1[w]));
+        word Sim0 = Gia_ObjFaninC0(pNode) ? ~pSims0[w] : pSims0[w];
+        word Sim1 = Gia_ObjFaninC1(pNode) ? ~pSims1[w] : pSims1[w];
+        pCtrl0[w] = pCtrl[w] & (pSims[w] | Sim1 | (~Sim0 & ~Sim1));
+        pCtrl1[w] = pCtrl[w] & (pSims[w] | Sim0);
     }
 }
 void Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
@@ -269,11 +303,14 @@ void Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
     p->vTfo = Vec_WecEntry( p->vTfos, Pivot );
     Vec_IntClear( p->vLeaves );
     Vec_IntClear( p->vTfi );
+    Vec_IntClear( p->vDivs );
     // simulate TFI cone
     Gia_ManIncrementTravId( p->pGia );
     Sbd_ManWindowSim_rec( p, Pivot );
     p->nTfiLeaves = Vec_IntSize( p->vLeaves );
     p->nTfiNodes = Vec_IntSize( p->vTfi );
+    Vec_IntAppend( p->vDivs, p->vLeaves );
+    Vec_IntAppend( p->vDivs, p->vTfi );
     // simulate node
     Gia_ManObj(p->pGia, Pivot)->fMark0 = 1;
     Abc_TtCopy( Sbd_ObjSim1(p, Pivot), Sbd_ObjSim0(p, Pivot), p->pPars->nWords, 1 );
@@ -282,7 +319,7 @@ void Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
     {
         Gia_ManObj(p->pGia, Abc_Lit2Var(Node))->fMark0 = 1;
         if ( Abc_LitIsCompl(Node) ) 
-            Sbd_ManWindowSim_rec( p, Node );
+            Sbd_ManWindowSim_rec( p, Abc_Lit2Var(Node) );
     }
     // remove marks
     Gia_ManObj(p->pGia, Pivot)->fMark0 = 0;
@@ -292,9 +329,9 @@ void Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
     Abc_TtClear( Sbd_ObjSim2(p, Pivot), p->pPars->nWords );
     Vec_IntForEachEntry( p->vTfo, Node, i )
         if ( Abc_LitIsCompl(Node) ) // root
-            Abc_TtOrXor( Sbd_ObjSim2(p, Pivot), Sbd_ObjSim0(p, Node), Sbd_ObjSim1(p, Node), p->pPars->nWords );
-    // propagate controlability to TFI
-    for ( i = p->nTfiNodes; i >= 0 && (Node = Vec_IntEntry(p->vTfi, i)); i-- )
+            Abc_TtOrXor( Sbd_ObjSim2(p, Pivot), Sbd_ObjSim0(p, Abc_Lit2Var(Node)), Sbd_ObjSim1(p, Abc_Lit2Var(Node)), p->pPars->nWords );
+    // propagate controlability to fanins for the TFI nodes starting from the pivot
+    for ( i = p->nTfiLeaves + p->nTfiNodes - 1; i >= p->nTfiLeaves && ((Node = Vec_IntEntry(p->vDivs, i)), 1); i-- )
         Sbd_ManPropagateControl( p, Node );
 }
 
@@ -319,11 +356,11 @@ void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot )
     for ( k = 0; k < p->pPars->nWords * 64; k++ )
     {
         printf( "%3d : ", k );
-        Vec_IntForEachEntry( p->vTfi, Id, i )
+        Vec_IntForEachEntry( p->vDivs, Id, i )
         {
             word * pSims = Sbd_ObjSim0( p, Id );
             word * pCtrl = Sbd_ObjSim2( p, Id );
-            if ( i == Vec_IntSize(p->vTfi)-1 )
+            if ( i == Vec_IntSize(p->vDivs)-1 )
             {
                 if ( Abc_TtGetBit(pCtrl, k) )
                     Vec_IntPush( p->vCounts[Abc_TtGetBit(pSims, k)], k );
@@ -335,15 +372,15 @@ void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot )
     }
     // covering table
     printf( "Exploring %d x %d covering table.\n", Vec_IntSize(p->vCounts[0]), Vec_IntSize(p->vCounts[1]) );
-    Vec_IntForEachEntry( p->vCounts[0], Bit0, k0 )
-    Vec_IntForEachEntry( p->vCounts[1], Bit1, k1 )
+    Vec_IntForEachEntryStop( p->vCounts[0], Bit0, k0, 5 )
+    Vec_IntForEachEntryStop( p->vCounts[1], Bit1, k1, 5 )
     {
         printf( "%3d %3d : ", Bit0, Bit1 );
-        Vec_IntForEachEntry( p->vTfi, Id, i )
+        Vec_IntForEachEntry( p->vDivs, Id, i )
         {
             word * pSims = Sbd_ObjSim0( p, Id );
             word * pCtrl = Sbd_ObjSim2( p, Id );
-            if ( i == Vec_IntSize(p->vTfi)-1 )
+            if ( i == Vec_IntSize(p->vDivs)-1 )
                 printf( " " );
             printf( "%c", (Abc_TtGetBit(pCtrl, Bit0) && Abc_TtGetBit(pCtrl, Bit1) && Abc_TtGetBit(pSims, Bit0) != Abc_TtGetBit(pSims, Bit1)) ? '1' : '.' );
         }
@@ -512,9 +549,11 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
     {
         if ( Sbd_ManComputeCut( p, Pivot ) )
             continue;
+        printf( "Looking at node %d\n", Pivot );
         Sbd_ManWindow( p, Pivot );
         if ( Sbd_ManExplore( p, Pivot, pCut, &Truth ) )
             Sbd_ManImplement( p, Pivot, pCut, Truth );
+        break;
     }
     pNew = Sbd_ManDerive( pGia, p->vMirrors );
     Sbd_ManStop( p );
diff --git a/src/opt/sbd/sbdSim.c b/src/opt/sbd/sbdSim.c
new file mode 100644
index 00000000..3bb44159
--- /dev/null
+++ b/src/opt/sbd/sbdSim.c
@@ -0,0 +1,310 @@
+/**CFile****************************************************************
+
+  FileName    [sbdSim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    [Simulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sbdSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline word * Sbd_ObjSims( Gia_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims,   p->iPatsPi * i );  }
+static inline word * Sbd_ObjCtrl( Gia_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSimsPi, p->iPatsPi * i );  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [This does not work.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sbd_GiaSimRoundBack2( Gia_Man_t * p )
+{
+    int nWords = p->iPatsPi;
+    Gia_Obj_t * pObj;
+    int w, i, Id;
+    // init primary outputs
+    Gia_ManForEachCoId( p, Id, i )
+        for ( w = 0; w < nWords; w++ )
+            Sbd_ObjSims(p, Id)[w] = Gia_ManRandomW(0);
+    // transfer to nodes
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj));
+        Abc_TtCopy( Sbd_ObjSims(p, Gia_ObjFaninId0p(p, pObj)), pSims, nWords, Gia_ObjFaninC0(pObj) );
+    }
+    // simulate nodes
+    Gia_ManForEachAndReverse( p, pObj, i )
+    {
+        word * pSims  = Sbd_ObjSims(p, i);
+        word * pSims0 = Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i));
+        word * pSims1 = Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i));
+        word Rand = Gia_ManRandomW(0);
+        for ( w = 0; w < nWords; w++ )
+        {
+            pSims0[w] = pSims[w] | Rand;
+            pSims1[w] = pSims[w] | ~Rand;
+        }
+        if ( Gia_ObjFaninC0(pObj) ) Abc_TtNot( pSims0, nWords );
+        if ( Gia_ObjFaninC1(pObj) ) Abc_TtNot( pSims1, nWords );
+    }
+    // primary inputs are initialized
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Tries to falsify a sequence of two-literal SAT problems.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sbd_GiaSatOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int Value, int fFirst, int iPat )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return (int)pObj->fMark0 == Value;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    pObj->fMark0 = Value;
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj));
+        if ( Abc_TtGetBit( pSims, iPat ) != Value )
+            Abc_TtXorBit( pSims, iPat );
+        return 1;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    assert( !Gia_ObjIsXor(pObj) );
+    if ( Value )
+        return Sbd_GiaSatOne_rec( p, Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), fFirst, iPat ) &&
+               Sbd_GiaSatOne_rec( p, Gia_ObjFanin1(pObj), !Gia_ObjFaninC1(pObj), fFirst, iPat );
+    if ( fFirst )
+        return Sbd_GiaSatOne_rec( p, Gia_ObjFanin0(pObj), Gia_ObjFaninC0(pObj), fFirst, iPat );
+    else
+        return Sbd_GiaSatOne_rec( p, Gia_ObjFanin1(pObj), Gia_ObjFaninC1(pObj), fFirst, iPat );
+}
+int Sbd_GiaSatOne( Gia_Man_t * p, Vec_Int_t * vPairs )
+{
+    int k, n, Var1, Var2, iPat = 0;
+    //Gia_ManSetPhase( p );
+    Vec_IntForEachEntryDouble( vPairs, Var1, Var2, k )
+    {
+        Gia_Obj_t * pObj1 = Gia_ManObj( p, Var1 );
+        Gia_Obj_t * pObj2 = Gia_ManObj( p, Var2 );
+        assert( Var2 > 0 );
+        if ( Var1 == 0 )
+        {
+            for ( n = 0; n < 2; n++ )
+            {
+                Gia_ManIncrementTravId( p );
+                if ( Sbd_GiaSatOne_rec(p, pObj2, !pObj2->fPhase, n, iPat) )
+                {
+                    iPat++;
+                    break;
+                }
+            }
+            printf( "%c", n == 2 ? '.' : 'c' );
+        }
+        else
+        {
+            for ( n = 0; n < 2; n++ )
+            {
+                Gia_ManIncrementTravId( p );
+                if ( Sbd_GiaSatOne_rec(p, pObj1, !pObj1->fPhase, n, iPat) && Sbd_GiaSatOne_rec(p, pObj2, pObj2->fPhase, n, iPat) )
+                {
+                    iPat++;
+                    break;
+                }
+                Gia_ManIncrementTravId( p );
+                if ( Sbd_GiaSatOne_rec(p, pObj1, pObj1->fPhase, n, iPat) && Sbd_GiaSatOne_rec(p, pObj2, !pObj2->fPhase, n, iPat) )
+                {
+                    iPat++;
+                    break;
+                }
+            }
+            printf( "%c", n == 2 ? '.' : 'e' );
+        }
+        if ( iPat == 64 * p->iPatsPi - 1 )
+            break;
+    }
+    printf( "\n" );
+    return iPat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sbd_GiaSimRoundBack( Gia_Man_t * p )
+{
+    extern void Sbd_GiaSimRound( Gia_Man_t * p, int fTry, Vec_Int_t ** pvMap );
+    Vec_Int_t * vReprs = Vec_IntStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vPairs = Vec_IntAlloc( 1000 );
+    Vec_Int_t * vMap; // maps each node into its class
+    int i, nConsts = 0, nClasses = 0, nPats;
+    Sbd_GiaSimRound( p, 0, &vMap );
+    Gia_ManForEachAndId( p, i )
+    {
+        if ( Vec_IntEntry(vMap, i) == 0 )
+            Vec_IntPushTwo( vPairs, 0, i ), nConsts++;
+        else if ( Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)) == 0 )
+            Vec_IntWriteEntry( vReprs, Vec_IntEntry(vMap, i), i );
+        else if ( Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)) != -1 )
+        {
+            Vec_IntPushTwo( vPairs, Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)), i );
+            Vec_IntWriteEntry( vReprs, Vec_IntEntry(vMap, i), -1 );
+            nClasses++;
+        }
+    }
+    Vec_IntFree( vMap );
+    Vec_IntFree( vReprs );
+    printf( "Constants = %d.   Classes = %d.\n", nConsts, nClasses );
+
+    nPats = Sbd_GiaSatOne( p, vPairs );
+    Vec_IntFree( vPairs );
+
+    printf( "Generated %d patterns.\n", nPats );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sbd_GiaSimRound( Gia_Man_t * p, int fTry, Vec_Int_t ** pvMap )
+{
+    int nWords = p->iPatsPi;
+    Vec_Mem_t * vStore;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vMap = Vec_IntStart( Gia_ManObjNum(p) );
+    int w, i, Id, fCompl, RetValue;
+    // init primary inputs
+    if ( fTry )
+    {
+        Sbd_GiaSimRoundBack( p );
+        Gia_ManForEachCiId( p, Id, i )
+            Sbd_ObjSims(p, Id)[0] <<= 1;
+    }
+    else
+    {
+        Gia_ManForEachCiId( p, Id, i )
+            for ( w = 0; w < nWords; w++ )
+                Sbd_ObjSims(p, Id)[w] = Gia_ManRandomW(0) << !w;
+    }
+    // simulate internal nodes
+    vStore = Vec_MemAlloc( nWords, 16 ); // 2^12 N-word entries per page
+    Vec_MemHashAlloc( vStore, 1 << 16 );
+    RetValue = Vec_MemHashInsert( vStore, Sbd_ObjSims(p, 0) ); // const zero
+    assert( RetValue == 0 );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        word * pSims = Sbd_ObjSims(p, i);
+        if ( Gia_ObjIsXor(pObj) )
+            Abc_TtXor( pSims, 
+                Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i)), 
+                Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i)), 
+                nWords, 
+                Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
+        else
+            Abc_TtAndCompl( pSims, 
+                Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i)), Gia_ObjFaninC0(pObj), 
+                Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i)), Gia_ObjFaninC1(pObj), 
+                nWords );
+        // hash sim info
+        fCompl = (int)(pSims[0] & 1);
+        if ( fCompl ) Abc_TtNot( pSims, nWords );
+        Vec_IntWriteEntry( vMap, i, Vec_MemHashInsert(vStore, pSims) );
+        if ( fCompl ) Abc_TtNot( pSims, nWords );
+    }
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj));
+        Abc_TtCopy( pSims, Sbd_ObjSims(p, Gia_ObjFaninId0p(p, pObj)), nWords, Gia_ObjFaninC0(pObj) );
+//        printf( "%d ", Abc_TtCountOnesVec(pSims, nWords) );
+        assert( Gia_ObjPhase(pObj) == (int)(pSims[0] & 1) );
+    }
+//    printf( "\n" );
+    Vec_MemHashFree( vStore );
+    Vec_MemFree( vStore );
+    printf( "Objects = %6d.  Unique = %6d.\n", Gia_ManAndNum(p), Vec_IntCountUnique(vMap) );
+    if ( pvMap )
+        *pvMap = vMap;
+    else
+        Vec_IntFree( vMap );
+}
+void Sbd_GiaSimTest( Gia_Man_t * pGia )
+{
+    Gia_ManSetPhase( pGia );
+
+    // allocate simulation info
+    pGia->iPatsPi = 32;
+    pGia->vSims   = Vec_WrdStart( Gia_ManObjNum(pGia) * pGia->iPatsPi );
+    pGia->vSimsPi = Vec_WrdStart( Gia_ManObjNum(pGia) * pGia->iPatsPi );
+
+    Gia_ManRandom( 1 );
+
+    Sbd_GiaSimRound( pGia, 0, NULL );
+    Sbd_GiaSimRound( pGia, 0, NULL );
+    Sbd_GiaSimRound( pGia, 0, NULL );
+
+    printf( "\n" );
+    Sbd_GiaSimRound( pGia, 1, NULL );
+    printf( "\n" );
+    Sbd_GiaSimRound( pGia, 1, NULL );
+    printf( "\n" );
+    Sbd_GiaSimRound( pGia, 1, NULL );
+
+    Vec_WrdFreeP( &pGia->vSims );
+    Vec_WrdFreeP( &pGia->vSimsPi );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+