From d080336bb5e4508274ed03940d6c8cb6ec3a1200 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 23 Sep 2011 22:35:03 -0700
Subject: Added new feature to bmc3.

---
 src/map/if/ifDec10f.c | 37 ++++++++++++++++++++++---------------
 1 file changed, 22 insertions(+), 15 deletions(-)

(limited to 'src/map/if')

diff --git a/src/map/if/ifDec10f.c b/src/map/if/ifDec10f.c
index 9f30cf96..9e2126e8 100644
--- a/src/map/if/ifDec10f.c
+++ b/src/map/if/ifDec10f.c
@@ -27,6 +27,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define CLU_MAX 16
+
 // the bit count for the first 256 integer numbers
 static int BitCount8[256] = {
     0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
@@ -55,18 +57,7 @@ static word Truth6[6] = {
     0xFFFF0000FFFF0000,
     0xFFFFFFFF00000000
 };
-static word Truth10[10][16] = {
-    0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,
-    0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,
-    0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,
-    0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,
-    0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,
-    0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,
-    0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,
-    0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,
-    0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,
-    0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF
-};
+static word TruthAll[CLU_MAX][1 << (CLU_MAX-6)];
 
 extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
 extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
@@ -76,10 +67,26 @@ extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
 //  moving up means moving from LSB -> MSB
 //  groups list vars indices from MSB to LSB
 
+//  group representation
+//  nVars | nCofs | v5 | v4 | v3 | v2 | v1 | v0 
+//  if nCofs > 2, v0 is the shared variable
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+void If_CluInitTruthTables()
+{
+    int i, k;
+    assert( CLU_MAX <= 16 );
+    for ( i = 0; i < 6; i++ )
+        for ( k = 0; k < (1 << (CLU_MAX-6)); k++ )
+            TruthAll[i][k] = Truth6[i];
+    for ( i = 6; i < CLU_MAX; i++ )
+        for ( k = 0; k < (1 << (CLU_MAX-6)); k++ )
+            TruthAll[i][k] = ((k >> i) & 1) ? ~0 : 0;
+}
+
 // variable permutation for large functions
 static inline int If_CluWordNum( int nVars )
 {
@@ -131,7 +138,7 @@ static inline void If_CluSwapAdjacent( word * pOut, word * pIn, int iVar, int nV
 // moves one var (v) to the given position (p)
 void If_CluMoveVarOneUp( word * pF, int * Var2Pla, int * Pla2Var, int nVars, int v, int p )
 {
-    word pG[16], * pIn = pF, * pOut = pG, * pTemp;
+    word pG[32], * pIn = pF, * pOut = pG, * pTemp;
     int iPlace0, iPlace1, Count = 0;
     assert( v >= 0 && v < nVars );
     assert( Var2Pla[v] >= p );
@@ -156,7 +163,7 @@ void If_CluMoveVarOneUp( word * pF, int * Var2Pla, int * Pla2Var, int nVars, int
 // moves one var (v) to the given position (p)
 void If_CluMoveVarOneDown( word * pF, int * Var2Pla, int * Pla2Var, int nVars, int v, int p )
 {
-    word pG[16], * pIn = pF, * pOut = pG, * pTemp;
+    word pG[32], * pIn = pF, * pOut = pG, * pTemp;
     int iPlace0, iPlace1, Count = 0;
     assert( v >= 0 && v < nVars );
     assert( Var2Pla[v] <= p );
@@ -194,7 +201,7 @@ int If_CluCountCofs( word * pF, int * V2P, int * P2V, int nVars, int nBSsize )
     word iCofs[16], iCof;
     int i, c, nMints = (1 << nBSsize), nCofs = 1;
     assert( nBSsize >= 3 && nBSsize <= 5 );
-    assert( nVars - nBSsize >= 0 && nVars - nBSsize <= 6 );
+    assert( nVars - nBSsize > 0 && nVars - nBSsize <= 6 );
     if ( nVars - nBSsize == 6 )
         Mask = ~0;
     iCofs[0] = pF[0] & Mask;
-- 
cgit v1.2.3