Moved the code to a different file.

1 files changed, 1 insertions, 197 deletions

diff --git a/src/aig/gia/giaShrink7.c b/src/aig/gia/giaShrink7.c
index ddc7da4a..e5556d27 100644
--- a/src/aig/gia/giaShrink7.c
+++ b/src/aig/gia/giaShrink7.c
@@ -52,202 +52,6 @@ extern word Shr_ManComputeTruth6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * v
 
 /**Function*************************************************************
 
-  Synopsis    [Check if the function is decomposable with the given pair.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Unm_ManCheckAnd( word t, int i, int j, word * pOut )
-{
-    word c0 = Abc_Tt6Cofactor0( t, i );
-    word c1 = Abc_Tt6Cofactor1( t, i );
-    word c00 = Abc_Tt6Cofactor0( c0, j );
-    word c01 = Abc_Tt6Cofactor1( c0, j );
-    word c10 = Abc_Tt6Cofactor0( c1, j );
-    word c11 = Abc_Tt6Cofactor1( c1, j );
-    if ( c00 == c01 && c00 == c10 ) //  i *  j
-    {
-        if ( pOut ) *pOut = (~s_Truths6[i] & c00) | (s_Truths6[i] & c11);
-        return 0;
-    }
-    if ( c11 == c00 && c11 == c10 ) //  i * !j
-    {
-        if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c01);
-        return 1;
-    }
-    if ( c11 == c00 && c11 == c01 ) // !i *  j
-    {
-        if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c10);
-        return 2;
-    }
-    if ( c11 == c01 && c11 == c10 ) // !i * !j
-    {
-        if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c00);
-        return 3;
-    }
-    if ( c00 == c11 && c01 == c10 )
-    {
-        if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c10);
-        return 4;
-    }
-    return -1;
-}
-static inline int Unm_ManCheckMux( word t, int i, word * pOut )
-{
-    word c0 = Abc_Tt6Cofactor0( t, i );
-    word c1 = Abc_Tt6Cofactor1( t, i );
-    word c00, c01, c10, c11;
-    int k, fPres0, fPres1, iVar0 = -1, iVar1 = -1;
-    for ( k = 0; k < 6; k++ )
-    {
-        if ( k == i ) continue;
-        fPres0 = Abc_Tt6HasVar( c0, k );
-        fPres1 = Abc_Tt6HasVar( c1, k );
-        if ( fPres0 && !fPres1 )
-        {
-            if ( iVar0 >= 0 )
-                return -1;
-            iVar0 = k;
-        }
-        if ( !fPres0 && fPres1 )
-        {
-            if ( iVar1 >= 0 )
-                return -1;
-            iVar1 = k;
-        }
-    }
-    if ( iVar0 == -1 || iVar1 == -1 )
-        return -1;
-    c00 = Abc_Tt6Cofactor0( c0, iVar0 );
-    c01 = Abc_Tt6Cofactor1( c0, iVar0 );
-    c10 = Abc_Tt6Cofactor0( c1, iVar1 );
-    c11 = Abc_Tt6Cofactor1( c1, iVar1 );
-    if ( c00 ==  c10 && c01 ==  c11 ) //  ITE(i,  iVar1,  iVar0)
-    {
-        if ( pOut ) *pOut = (~s_Truths6[i] & c10) | (s_Truths6[i] & c11);
-        return (Abc_Var2Lit(iVar1, 0) << 16) | Abc_Var2Lit(iVar0, 0);
-    }
-    if ( c00 == ~c10 && c01 == ~c11 ) //  ITE(i,  iVar1, !iVar0)
-    {
-        if ( pOut ) *pOut = (~s_Truths6[i] & c10) | (s_Truths6[i] & c11);
-        return (Abc_Var2Lit(iVar1, 0) << 16) | Abc_Var2Lit(iVar0, 1);
-    }
-    return -1;
-}
-void Unm_ManCheckTest2()
-{
-    word t, t1, Out, Var0, Var1, Var0_, Var1_;
-    int iVar0, iVar1, i, Res;
-    for ( iVar0 = 0; iVar0 < 6; iVar0++ )
-    for ( iVar1 = 0; iVar1 < 6; iVar1++ )
-    {
-        if ( iVar0 == iVar1 )
-            continue;
-        Var0 = s_Truths6[iVar0];
-        Var1 = s_Truths6[iVar1];
-        for ( i = 0; i < 5; i++ )
-        {
-            Var0_ = ((i >> 0) & 1) ? ~Var0 : Var0;
-            Var1_ = ((i >> 1) & 1) ? ~Var1 : Var1;
-
-            t = Var0_ & Var1_;
-            if ( i == 4 )
-                t = ~(Var0_ ^ Var1_);
-
-//            Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" );
-
-            Res = Unm_ManCheckAnd( t, iVar0, iVar1, &Out );
-            if ( Res == -1 )
-            {
-                printf( "No decomposition\n" );
-                continue;
-            }
-
-            Var0_ = s_Truths6[iVar0];
-            Var0_ = ((Res >> 0) & 1) ? ~Var0_ : Var0_;
-
-            Var1_ = s_Truths6[iVar1];
-            Var1_ = ((Res >> 1) & 1) ? ~Var1_ : Var1_;
-
-            t1 = Var0_ & Var1_;
-            if ( Res == 4 )
-                t1 = Var0_ ^ Var1_;
-
-            t1 = (~t1 & Abc_Tt6Cofactor0(Out, iVar0)) | (t1 & Abc_Tt6Cofactor1(Out, iVar0));
-
-//            Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" );
-
-            if ( t1 != t )
-                printf( "Verification failed.\n" );
-            else
-                printf( "Verification succeeded.\n" );
-        }
-    }
-}
-void Unm_ManCheckTest()
-{
-    word t, t1, Out, Ctrl, Var0, Var1, Ctrl_, Var0_, Var1_;
-    int iVar0, iVar1, iCtrl, i, Res;
-    for ( iCtrl = 0; iCtrl < 6; iCtrl++ )
-    for ( iVar0 = 0; iVar0 < 6; iVar0++ )
-    for ( iVar1 = 0; iVar1 < 6; iVar1++ )
-    {
-        if ( iCtrl == iVar0 || iCtrl == iVar1 || iVar0 == iVar1 )
-            continue;
-        Ctrl = s_Truths6[iCtrl];
-        Var0 = s_Truths6[iVar0];
-        Var1 = s_Truths6[iVar1];
-        for ( i = 0; i < 8; i++ )
-        {
-            Ctrl_ = ((i >> 0) & 1) ? ~Ctrl : Ctrl;
-            Var0_ = ((i >> 1) & 1) ? ~Var0 : Var0;
-            Var1_ = ((i >> 2) & 1) ? ~Var1 : Var1;
-
-            t = (~Ctrl_ & Var0_) | (Ctrl_ & Var1_);
-
-//            Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" );
-
-            Res = Unm_ManCheckMux( t, iCtrl, &Out );
-            if ( Res == -1 )
-            {
-                printf( "No decomposition\n" );
-                continue;
-            }
-
-//            Kit_DsdPrintFromTruth( (unsigned *)&Out, 6 ), printf( "\n" );
-
-            Ctrl_ = s_Truths6[iCtrl];
-            Var0_ = s_Truths6[Abc_Lit2Var(Res & 0xFFFF)];
-            Var0_ = Abc_LitIsCompl(Res & 0xFFFF) ? ~Var0_ : Var0_;
-
-            Res >>= 16;
-            Var1_ = s_Truths6[Abc_Lit2Var(Res & 0xFFFF)];
-            Var1_ = Abc_LitIsCompl(Res & 0xFFFF) ? ~Var1_ : Var1_;
-
-            t1 = (~Ctrl_ & Var0_) | (Ctrl_ & Var1_);
-
-//            Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" );
-//            Kit_DsdPrintFromTruth( (unsigned *)&Out, 6 ), printf( "\n" );
-
-            t1 = (~t1 & Abc_Tt6Cofactor0(Out, iCtrl)) | (t1 & Abc_Tt6Cofactor1(Out, iCtrl));
-
-//            Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" );
-
-            if ( t1 != t )
-                printf( "Verification failed.\n" );
-            else
-                printf( "Verification succeeded.\n" );
-        }
-    }
-}
-
-
-/**Function*************************************************************
-
   Synopsis    []
 
   Description []
@@ -474,7 +278,7 @@ Vec_Int_t * Unm_ManCollectDecomp( Unm_Man_t * p, Vec_Int_t * vPairs, int fVerbos
         assert( FanK < FanJ );
         iUsed = Vec_IntEntry( p->vId2Used, iObj );
         uTruth = Vec_WrdEntry( p->vTruths, iUsed );
-        Res = Unm_ManCheckAnd( uTruth, k, j, NULL );
+        Res = Abc_TtCheckDsdAnd( uTruth, k, j, NULL );
         if ( Res == -1 )
             continue;
         // derive literals