Moved the code to a different file.

1 files changed, 197 insertions, 0 deletions

diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 14b13234..5561a2c6 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -1404,6 +1404,203 @@ static inline word Abc_Tt6Isop( word uOn, word uOnDc, int nVars )
     return uRes2;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Check if the function is decomposable with the given pair.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_TtCheckDsdAnd( 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 Abc_TtCheckDsdMux( 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;
+}
+static inline 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 = Abc_TtCheckDsdAnd( 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" );
+        }
+    }
+}
+static inline 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 = Abc_TtCheckDsdMux( 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" );
+        }
+    }
+}
+
+
 /*=== utilTruth.c ===========================================================*/