summaryrefslogtreecommitdiffstats
path: root/src/misc/util/utilTruth.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/misc/util/utilTruth.h')
-rw-r--r--src/misc/util/utilTruth.h53
1 files changed, 52 insertions, 1 deletions
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index e04ffbc9..4736a291 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -1378,6 +1378,13 @@ static inline void Abc_TtMoveVar( word * pF, int nVars, int * V2P, int * P2V, in
P2V[jVar] ^= P2V[iVar];
P2V[iVar] ^= P2V[jVar];
}
+static inline word Abc_Tt6RemoveVar( word t, int iVar )
+{
+ assert( !Abc_Tt6HasVar(t, iVar) );
+ while ( iVar < 5 )
+ t = Abc_Tt6SwapAdjacent( t, iVar++ );
+ return t;
+}
/**Function*************************************************************
@@ -2209,7 +2216,51 @@ static inline int Abc_Tt6EsopVerify( word t, int nVars )
/**Function*************************************************************
- Synopsis [Check if the function is decomposable with the given pair.]
+ Synopsis [Check if the function is output-decomposable with the given var.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Abc_TtCheckOutAnd( word t, int i, word * pOut )
+{
+ word c0 = Abc_Tt6Cofactor0( t, i );
+ word c1 = Abc_Tt6Cofactor1( t, i );
+ assert( c0 != c1 );
+ if ( c0 == 0 ) // F = i * G
+ {
+ if ( pOut ) *pOut = c1;
+ return 0;
+ }
+ if ( c1 == 0 ) // F = ~i * G
+ {
+ if ( pOut ) *pOut = c0;
+ return 1;
+ }
+ if ( ~c0 == 0 ) // F = ~i + G
+ {
+ if ( pOut ) *pOut = c1;
+ return 2;
+ }
+ if ( ~c1 == 0 ) // F = i + G
+ {
+ if ( pOut ) *pOut = c0;
+ return 3;
+ }
+ if ( c0 == ~c1 ) // F = i # G
+ {
+ if ( pOut ) *pOut = c0;
+ return 4;
+ }
+ return -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Check if the function is input-decomposable with the given pair.]
Description []