Improvements to the truth table computations.

4 files changed, 36 insertions, 40 deletions

diff --git a/src/base/abci/abcRec3.c b/src/base/abci/abcRec3.c
index ed6148ab..4a9e12b3 100644
--- a/src/base/abci/abcRec3.c
+++ b/src/base/abci/abcRec3.c
@@ -23,11 +23,13 @@
 #include "bool/kit/kit.h"
 #include "aig/gia/giaAig.h"
 #include "misc/vec/vecMem.h"
-#include "bool/lucky/lucky.h"
+#include "opt/dau/dau.h"
 #include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
+//#define LMS_USE_OLD_FORM
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -488,8 +490,11 @@ p->timeCollect += clock() - clk;
         // semi-canonicize
 clk = clock();
         memcpy( p->pTemp1, pTruth, p->nWords * sizeof(word) );
-    //    uCanonPhase = luckyCanonicizer_final_fast( p->pTemp1, nLeaves, pCanonPerm );
+#ifdef LMS_USE_OLD_FORM
         uCanonPhase = Kit_TruthSemiCanonicize( (unsigned *)p->pTemp1, (unsigned *)p->pTemp2, nLeaves, pCanonPerm );
+#else
+        uCanonPhase = Abc_TtCanonicize( p->pTemp1, nLeaves, pCanonPerm );
+#endif
         Abc_TtStretch5( (unsigned *)p->pTemp1, nLeaves, p->nVars );
 p->timeCanon += clock() - clk;
         // pCanonPerm and uCanonPhase show what was the variable corresponding to each var in the current truth
@@ -599,8 +604,11 @@ p->timeCollect += clock() - clk;
     // semi-canonicize truth table
 clk = clock();
     memcpy( p->pTemp1, If_CutTruthW(pCut), p->nWords * sizeof(word) );
-//    uCanonPhase = luckyCanonicizer_final_fast( p->pTemp1, nLeaves, pCanonPerm );
+#ifdef LMS_USE_OLD_FORM
     uCanonPhase = Kit_TruthSemiCanonicize( (unsigned *)p->pTemp1, (unsigned *)p->pTemp2, nLeaves, pCanonPerm );
+#else
+    uCanonPhase = Abc_TtCanonicize( p->pTemp1, nLeaves, pCanonPerm );
+#endif
     Abc_TtStretch5( (unsigned *)p->pTemp1, nLeaves, p->nVars );
 p->timeCanon += clock() - clk;
     // pCanonPerm and uCanonPhase show what was the variable corresponding to each var in the current truth
@@ -762,8 +770,11 @@ static inline int If_CutFindBestStruct( If_Man_t * pIfMan, If_Cut_t * pCut, char
     // semicanonicize the function
 clk = clock();
     memcpy( p->pTemp1, If_CutTruthW(pCut), p->nWords * sizeof(word) );
-//    uCanonPhase = luckyCanonicizer_final_fast( p->pTemp1, nLeaves, pCanonPerm );
+#ifdef LMS_USE_OLD_FORM
     *puCanonPhase = Kit_TruthSemiCanonicize( (unsigned *)p->pTemp1, (unsigned *)p->pTemp2, nLeaves, pCanonPerm );
+#else
+    *puCanonPhase = Abc_TtCanonicize( p->pTemp1, nLeaves, pCanonPerm );
+#endif
     Abc_TtStretch5( (unsigned *)p->pTemp1, nLeaves, p->nVars );
 p->timeCanon += clock() - clk;
 
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index c742aac9..486cbf48 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -53,14 +53,6 @@ static word s_Truths6Neg[6] = {
     0x00000000FFFFFFFF
 };
 
-static word s_CMasks6[5] = {
-    0x1111111111111111,
-    0x0303030303030303,
-    0x000F000F000F000F,
-    0x000000FF000000FF,
-    0x000000000000FFFF
-};
-
 static word s_PMasks[5][3] = {
     { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 },
     { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 },
@@ -299,12 +291,12 @@ static inline int Abc_Tt6Cof1IsConst0( word t, int iVar ) { return (t & s_Truths
 static inline int Abc_Tt6Cof1IsConst1( word t, int iVar ) { return (t & s_Truths6[iVar]) == s_Truths6[iVar];                               }
 static inline int Abc_Tt6CofsOpposite( word t, int iVar ) { return ((t >> (1 << iVar)) & s_Truths6Neg[iVar]) == (~t & s_Truths6Neg[iVar]); } 
 
-static inline word Abc_Tt6Cof0( word t, int iVar )
+static inline word Abc_Tt6Cofactor0( word t, int iVar )
 {
     assert( iVar >= 0 && iVar < 6 );
     return (t &s_Truths6Neg[iVar]) | ((t &s_Truths6Neg[iVar]) << (1<<iVar));
 }
-static inline word Abc_Tt6Cof1( word t, int iVar )
+static inline word Abc_Tt6Cofactor1( word t, int iVar )
 {
     assert( iVar >= 0 && iVar < 6 );
     return (t & s_Truths6[iVar]) | ((t & s_Truths6[iVar]) >> (1<<iVar));
diff --git a/src/opt/dau/dauCanon.c b/src/opt/dau/dauCanon.c
index 2853f238..34387e4d 100644
--- a/src/opt/dau/dauCanon.c
+++ b/src/opt/dau/dauCanon.c
@@ -27,6 +27,14 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static word s_CMasks6[5] = {
+    0x1111111111111111,
+    0x0303030303030303,
+    0x000F000F000F000F,
+    0x000000FF000000FF,
+    0x000000000000FFFF
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -406,8 +414,8 @@ int Abc_TtCountOnesInCofsFast6_rec( word Truth, int iVar, int nBytes, int * pSto
         pStore[2] += bit_count[ Truth & 0x0F ];
         return bit_count[ Truth & 0xFF ];
     }
-    nMints0 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cof0(Truth, iVar), iVar - 1, nBytes/2, pStore );
-    nMints1 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cof1(Truth, iVar), iVar - 1, nBytes/2, pStore );
+    nMints0 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cofactor0(Truth, iVar), iVar - 1, nBytes/2, pStore );
+    nMints1 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cofactor1(Truth, iVar), iVar - 1, nBytes/2, pStore );
     pStore[iVar] += nMints0;
     return nMints0 + nMints1;
 }
@@ -899,7 +907,7 @@ unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm )
 #endif
 
     uCanonPhase = Abc_TtSemiCanonicize( pTruth, nVars, pCanonPerm, pStoreIn );
-    for ( k = 0; k < 3; k++ )
+    for ( k = 0; k < 5; k++ )
     {
         int fChanges = 0;
         for ( i = nVars - 2; i >= 0; i-- )
diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c
index d319e62d..c2cfad35 100644
--- a/src/opt/dau/dauDsd.c
+++ b/src/opt/dau/dauDsd.c
@@ -165,21 +165,6 @@ void Dau_DsdTest2()
   SeeAlso     []
 
 ***********************************************************************/
-static inline word Dau_DsdCof0( word t, int iVar )
-{
-    assert( iVar >= 0 && iVar < 6 );
-    return (t &~s_Truth6[iVar]) | ((t &~s_Truth6[iVar]) << (1<<iVar));
-}
-static inline word Dau_DsdCof1( word t, int iVar )
-{
-    assert( iVar >= 0 && iVar < 6 );
-    return (t & s_Truth6[iVar]) | ((t & s_Truth6[iVar]) >> (1<<iVar));
-}
-static inline word Dau_DsdVarPres( word t, int iVar )
-{
-    assert( iVar >= 0 && iVar < 6 );
-    return (t & s_Truth6[iVar]) != ((t << (1<<iVar)) & s_Truth6[iVar]);
-}
 static inline int Dau_DsdPerformReplace( char * pBuffer, int PosStart, int Pos, int Symb, char * pNext )
 {
     static char pTemp[DAU_MAX_STR+20];
@@ -206,7 +191,7 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
     // perform support minimization
     nVarsNew = 0;
     for ( v = 0; v < nVars; v++ )
-        if ( Dau_DsdVarPres( t, pVars[v] ) )
+        if ( Abc_Tt6HasVar( t, pVars[v] ) )
             pVarsNew[ nVarsNew++ ] = pVars[v];
     assert( nVarsNew > 0 );
     // special case when function is a var
@@ -229,8 +214,8 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
     // decompose on the output side
     for ( v = 0; v < nVarsNew; v++ )
     {
-        Cof0[v] = Dau_DsdCof0( t, pVarsNew[v] );
-        Cof1[v] = Dau_DsdCof1( t, pVarsNew[v] );
+        Cof0[v] = Abc_Tt6Cofactor0( t, pVarsNew[v] );
+        Cof1[v] = Abc_Tt6Cofactor1( t, pVarsNew[v] );
         assert( Cof0[v] != Cof1[v] );
         if ( Cof0[v] == 0 ) // ax
         {
@@ -281,10 +266,10 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
     for ( v = 0; v < nVarsNew; v++ )
     for ( u = v+1; u < nVarsNew; u++ )
     {
-        Cof[0] = Dau_DsdCof0( Cof0[v], pVarsNew[u] );
-        Cof[1] = Dau_DsdCof1( Cof0[v], pVarsNew[u] );
-        Cof[2] = Dau_DsdCof0( Cof1[v], pVarsNew[u] );
-        Cof[3] = Dau_DsdCof1( Cof1[v], pVarsNew[u] );
+        Cof[0] = Abc_Tt6Cofactor0( Cof0[v], pVarsNew[u] );
+        Cof[1] = Abc_Tt6Cofactor1( Cof0[v], pVarsNew[u] );
+        Cof[2] = Abc_Tt6Cofactor0( Cof1[v], pVarsNew[u] );
+        Cof[3] = Abc_Tt6Cofactor1( Cof1[v], pVarsNew[u] );
         if ( Cof[0] == Cof[1] && Cof[0] == Cof[2] ) // vu
         {
             PosStart = Pos;
@@ -333,7 +318,7 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
     {
         int CountCur = 0;
         for ( u = 0; u < nVarsNew; u++ )
-            if ( u != v && Dau_DsdVarPres(Cof0[v], pVarsNew[u]) && Dau_DsdVarPres(Cof1[v], pVarsNew[u]) )
+            if ( u != v && Abc_Tt6HasVar(Cof0[v], pVarsNew[u]) && Abc_Tt6HasVar(Cof1[v], pVarsNew[u]) )
                 CountCur++;
         if ( CountBest > CountCur )
         {