summaryrefslogtreecommitdiffstats
path: root/src/map/if/ifDec.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/map/if/ifDec.c')
-rw-r--r--src/map/if/ifDec.c206
1 files changed, 201 insertions, 5 deletions
diff --git a/src/map/if/ifDec.c b/src/map/if/ifDec.c
index 7409c05a..2dd91cd2 100644
--- a/src/map/if/ifDec.c
+++ b/src/map/if/ifDec.c
@@ -390,6 +390,14 @@ static inline int If_Dec6HasVar( word t, int v )
{
return ((t & Truth6[v]) >> (1<<v)) != (t & ~Truth6[v]);
}
+static inline int If_Dec7HasVar( word t[2], int v )
+{
+ assert( v >= 0 && v < 7 );
+ if ( v == 6 )
+ return t[0] != t[1];
+ return ((t[0] & Truth6[v]) >> (1<<v)) != (t[0] & ~Truth6[v])
+ || ((t[1] & Truth6[v]) >> (1<<v)) != (t[1] & ~Truth6[v]);
+}
static inline void If_DecVerifyPerm( int Pla2Var[6], int Var2Pla[6] )
{
@@ -397,7 +405,7 @@ static inline void If_DecVerifyPerm( int Pla2Var[6], int Var2Pla[6] )
for ( i = 0; i < 6; i++ )
assert( Pla2Var[Var2Pla[i]] == i );
}
-static word If_Dec6Perform( word t, int fDerive )
+word If_Dec6Perform( word t, int fDerive )
{
word r = 0;
int i, v, u, x, Count, Pla2Var[6], Var2Pla[6];
@@ -437,7 +445,7 @@ static word If_Dec6Perform( word t, int fDerive )
assert( i == 15 );
return r;
}
-static word If_Dec7Perform( word t0[2], int fDerive )
+word If_Dec7Perform( word t0[2], int fDerive )
{
word t[2] = {t0[0], t0[1]};
int i, v, u, y, Pla2Var[7], Var2Pla[7];
@@ -468,6 +476,190 @@ static word If_Dec7Perform( word t0[2], int fDerive )
}
+// support minimization
+static inline int If_DecSuppIsMinBase( int Supp )
+{
+ return (Supp & (Supp+1)) == 0;
+}
+static inline word If_Dec6TruthShrink( word uTruth, int nVars, int nVarsAll, unsigned Phase )
+{
+ int i, k, Var = 0;
+ assert( nVarsAll <= 6 );
+ for ( i = 0; i < nVarsAll; i++ )
+ if ( Phase & (1 << i) )
+ {
+ for ( k = i-1; k >= Var; k-- )
+ uTruth = If_Dec6SwapAdjacent( uTruth, k );
+ Var++;
+ }
+ assert( Var == nVars );
+ return uTruth;
+}
+word If_Dec6MinimumBase( word uTruth, int * pSupp, int nVarsAll, int * pnVars )
+{
+ int v, iVar = 0, uSupp = 0;
+ assert( nVarsAll <= 6 );
+ for ( v = 0; v < nVarsAll; v++ )
+ if ( If_Dec6HasVar( uTruth, v ) )
+ {
+ uSupp |= (1 << v);
+ if ( pSupp )
+ pSupp[iVar] = pSupp[v];
+ iVar++;
+ }
+ if ( pnVars )
+ *pnVars = iVar;
+ if ( If_DecSuppIsMinBase( uSupp ) )
+ return uTruth;
+ return If_Dec6TruthShrink( uTruth, iVar, nVarsAll, uSupp );
+}
+
+static inline void If_Dec7TruthShrink( word uTruth[2], int nVars, int nVarsAll, unsigned Phase )
+{
+ int i, k, Var = 0;
+ assert( nVarsAll <= 7 );
+ for ( i = 0; i < nVarsAll; i++ )
+ if ( Phase & (1 << i) )
+ {
+ for ( k = i-1; k >= Var; k-- )
+ If_Dec7SwapAdjacent( uTruth, k );
+ Var++;
+ }
+ assert( Var == nVars );
+}
+void If_Dec7MinimumBase( word uTruth[2], int * pSupp, int nVarsAll, int * pnVars )
+{
+ int v, iVar = 0, uSupp = 0;
+ assert( nVarsAll <= 7 );
+ for ( v = 0; v < nVarsAll; v++ )
+ if ( If_Dec7HasVar( uTruth, v ) )
+ {
+ uSupp |= (1 << v);
+ if ( pSupp )
+ pSupp[iVar] = pSupp[v];
+ iVar++;
+ }
+ if ( pnVars )
+ *pnVars = iVar;
+ if ( If_DecSuppIsMinBase( uSupp ) )
+ return;
+ If_Dec7TruthShrink( uTruth, iVar, nVarsAll, uSupp );
+}
+
+
+
+// check for MUX decomposition
+static inline int If_Dec6SuppSize( word t )
+{
+ int v, Count = 0;
+ for ( v = 0; v < 6; v++ )
+ if ( If_Dec6Cofactor(t, v, 0) != If_Dec6Cofactor(t, v, 1) )
+ Count++;
+ return Count;
+}
+static inline int If_Dec6CheckMux( word t )
+{
+ int v;
+ for ( v = 0; v < 6; v++ )
+ if ( If_Dec6SuppSize(If_Dec6Cofactor(t, v, 0)) < 5 &&
+ If_Dec6SuppSize(If_Dec6Cofactor(t, v, 1)) < 5 )
+ return v;
+ return -1;
+}
+
+// check for MUX decomposition
+static inline void If_Dec7Cofactor( word t[2], int iVar, int fCof1, word r[2] )
+{
+ assert( iVar >= 0 && iVar < 7 );
+ if ( iVar == 6 )
+ {
+ if ( fCof1 )
+ r[0] = r[1] = t[1];
+ else
+ r[0] = r[1] = t[0];
+ }
+ else
+ {
+ if ( fCof1 )
+ {
+ r[0] = (t[0] & Truth6[iVar]) | ((t[0] & Truth6[iVar]) >> (1<<iVar));
+ r[1] = (t[1] & Truth6[iVar]) | ((t[1] & Truth6[iVar]) >> (1<<iVar));
+ }
+ else
+ {
+ r[0] = (t[0] &~Truth6[iVar]) | ((t[0] &~Truth6[iVar]) << (1<<iVar));
+ r[1] = (t[1] &~Truth6[iVar]) | ((t[1] &~Truth6[iVar]) << (1<<iVar));
+ }
+ }
+}
+static inline int If_Dec7SuppSize( word t[2] )
+{
+ word c0[2], c1[2];
+ int v, Count = 0;
+ for ( v = 0; v < 7; v++ )
+ {
+ If_Dec7Cofactor( t, v, 0, c0 );
+ If_Dec7Cofactor( t, v, 1, c1 );
+ if ( c0[0] != c1[0] || c0[1] != c1[1] )
+ Count++;
+ }
+ return Count;
+}
+static inline int If_Dec7CheckMux( word t[2] )
+{
+ word c0[2], c1[2];
+ int v;
+ for ( v = 0; v < 7; v++ )
+ {
+ If_Dec7Cofactor( t, v, 0, c0 );
+ If_Dec7Cofactor( t, v, 1, c1 );
+ if ( If_Dec7SuppSize(c0) < 5 && If_Dec7SuppSize(c1) < 5 )
+ return v;
+ }
+ return -1;
+}
+
+// find the best MUX decomposition
+int If_Dec6PickBestMux( word t, word Cofs[2] )
+{
+ int v, vBest = -1, Count0, Count1, CountBest = 1000;
+ for ( v = 0; v < 6; v++ )
+ {
+ Count0 = If_Dec6SuppSize( If_Dec6Cofactor(t, v, 0) );
+ Count1 = If_Dec6SuppSize( If_Dec6Cofactor(t, v, 1) );
+ if ( Count0 < 5 && Count1 < 5 && CountBest > Count0 + Count1 )
+ {
+ CountBest = Count0 + Count1;
+ vBest = v;
+ Cofs[0] = If_Dec6Cofactor(t, v, 0);
+ Cofs[1] = If_Dec6Cofactor(t, v, 1);
+ }
+ }
+ return vBest;
+}
+int If_Dec7PickBestMux( word t[2], word c0r[2], word c1r[2] )
+{
+ word c0[2], c1[2];
+ int v, vBest = -1, Count0, Count1, CountBest = 1000;
+ for ( v = 0; v < 6; v++ )
+ {
+ If_Dec7Cofactor( t, v, 0, c0 );
+ If_Dec7Cofactor( t, v, 1, c1 );
+ Count0 = If_Dec7SuppSize(c0);
+ Count1 = If_Dec7SuppSize(c1);
+ if ( Count0 < 5 && Count1 < 5 && CountBest > Count0 + Count1 )
+ {
+ CountBest = Count0 + Count1;
+ vBest = v;
+ c0r[0] = c0[0]; c0r[1] = c0[1];
+ c1r[0] = c1[0]; c1r[1] = c1[1];
+ }
+ }
+ return vBest;
+}
+
+
+
/**Function*************************************************************
Synopsis [Performs additional check.]
@@ -486,17 +678,21 @@ int If_CutPerformCheckInt( unsigned * pTruth, int nVars, int nLeaves )
return 1;
if ( nLeaves == 6 )
{
- word t = ((word *)pTruth)[0];
- word z = If_Dec6Perform( t, fDerive );
+ word z, t = ((word *)pTruth)[0];
+ if ( If_Dec6CheckMux(t) >= 0 )
+ return 1;
+ z = If_Dec6Perform( t, fDerive );
if ( fDerive && z )
If_Dec6Verify( t, z );
return z != 0;
}
if ( nLeaves == 7 )
{
- word t[2], z;
+ word z, t[2];
t[0] = ((word *)pTruth)[0];
t[1] = ((word *)pTruth)[1];
+ if ( If_Dec7CheckMux(t) >= 0 )
+ return 1;
z = If_Dec7Perform( t, fDerive );
if ( fDerive && z )
If_Dec7Verify( t, z );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 21:52:12 +0000