Version abc70206

2 files changed, 170 insertions, 0 deletions

diff --git a/src/opt/kit/kit.h b/src/opt/kit/kit.h
index 58c55cd2..ed2745e3 100644
--- a/src/opt/kit/kit.h
+++ b/src/opt/kit/kit.h
@@ -207,6 +207,22 @@ static inline int Kit_TruthIsImply( unsigned * pIn1, unsigned * pIn2, int nVars
             return 0;
     return 1;
 }
+static inline int Kit_TruthIsDisjoint( unsigned * pIn1, unsigned * pIn2, int nVars )
+{
+    int w;
+    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+        if ( pIn1[w] & pIn2[w] )
+            return 0;
+    return 1;
+}
+static inline int Kit_TruthIsDisjoint3( unsigned * pIn1, unsigned * pIn2, unsigned * pIn3, int nVars )
+{
+    int w;
+    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+        if ( pIn1[w] & pIn2[w] & pIn3[w] )
+            return 0;
+    return 1;
+}
 static inline void Kit_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
 {
     int w;
@@ -320,7 +336,11 @@ extern int             Kit_TruthSupport( unsigned * pTruth, int nVars );
 extern void            Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar );
 extern void            Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar );
 extern void            Kit_TruthExist( unsigned * pTruth, int nVars, int iVar );
+extern void            Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
+extern void            Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
 extern void            Kit_TruthForall( unsigned * pTruth, int nVars, int iVar );
+extern void            Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
+extern void            Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
 extern void            Kit_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
 extern void            Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
 extern int             Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
diff --git a/src/opt/kit/kitTruth.c b/src/opt/kit/kitTruth.c
index 5df10d63..429875bc 100644
--- a/src/opt/kit/kitTruth.c
+++ b/src/opt/kit/kitTruth.c
@@ -490,6 +490,81 @@ void Kit_TruthExist( unsigned * pTruth, int nVars, int iVar )
   SeeAlso     []
 
 ***********************************************************************/
+void Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar )
+{
+    int nWords = Kit_TruthWordNum( nVars );
+    int i, k, Step;
+
+    assert( iVar < nVars );
+    switch ( iVar )
+    {
+    case 0:
+        for ( i = 0; i < nWords; i++ )
+            pRes[i] =  pTruth[i] | ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
+        return;
+    case 1:
+        for ( i = 0; i < nWords; i++ )
+            pRes[i] =  pTruth[i] | ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
+        return;
+    case 2:
+        for ( i = 0; i < nWords; i++ )
+            pRes[i] =  pTruth[i] | ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
+        return;
+    case 3:
+        for ( i = 0; i < nWords; i++ )
+            pRes[i] =  pTruth[i] | ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
+        return;
+    case 4:
+        for ( i = 0; i < nWords; i++ )
+            pRes[i] =  pTruth[i] | ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
+        return;
+    default:
+        Step = (1 << (iVar - 5));
+        for ( k = 0; k < nWords; k += 2*Step )
+        {
+            for ( i = 0; i < Step; i++ )
+            {
+                pRes[i]      = pTruth[i] | pTruth[Step+i];
+                pRes[Step+i] = pRes[i];
+            }
+            pRes += 2*Step;
+            pTruth += 2*Step;
+        }
+        return;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Existantially quantifies the set of variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask )
+{
+    int v;
+    Kit_TruthCopy( pRes, pTruth, nVars );
+    for ( v = 0; v < nVars; v++ )
+        if ( uMask & (1 << v) )
+            Kit_TruthExist( pRes, nVars, v );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unversally quantifies the variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Kit_TruthForall( unsigned * pTruth, int nVars, int iVar )
 {
     int nWords = Kit_TruthWordNum( nVars );
@@ -533,6 +608,81 @@ void Kit_TruthForall( unsigned * pTruth, int nVars, int iVar )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Universally quantifies the variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar )
+{
+    int nWords = Kit_TruthWordNum( nVars );
+    int i, k, Step;
+
+    assert( iVar < nVars );
+    switch ( iVar )
+    {
+    case 0:
+        for ( i = 0; i < nWords; i++ )
+            pRes[i] =  pTruth[i] & (((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1));
+        return;
+    case 1:
+        for ( i = 0; i < nWords; i++ )
+            pRes[i] =  pTruth[i] & (((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2));
+        return;
+    case 2:
+        for ( i = 0; i < nWords; i++ )
+            pRes[i] =  pTruth[i] & (((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4));
+        return;
+    case 3:
+        for ( i = 0; i < nWords; i++ )
+            pRes[i] =  pTruth[i] & (((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8));
+        return;
+    case 4:
+        for ( i = 0; i < nWords; i++ )
+            pRes[i] =  pTruth[i] & (((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16));
+        return;
+    default:
+        Step = (1 << (iVar - 5));
+        for ( k = 0; k < nWords; k += 2*Step )
+        {
+            for ( i = 0; i < Step; i++ )
+            {
+                pRes[i]      = pTruth[i] & pTruth[Step+i];
+                pRes[Step+i] = pRes[i];
+            }
+            pRes += 2*Step;
+            pTruth += 2*Step;
+        }
+        return;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Universally quantifies the set of variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask )
+{
+    int v;
+    Kit_TruthCopy( pRes, pTruth, nVars );
+    for ( v = 0; v < nVars; v++ )
+        if ( uMask & (1 << v) )
+            Kit_TruthForall( pRes, nVars, v );
+}
+
 
 /**Function*************************************************************