Version abc80314

7 files changed, 237 insertions, 44 deletions

diff --git a/src/aig/bdc/bdcCore.c b/src/aig/bdc/bdcCore.c
index f0b0f3bc..13275377 100644
--- a/src/aig/bdc/bdcCore.c
+++ b/src/aig/bdc/bdcCore.c
@@ -48,11 +48,11 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
     p->pPars = pPars;
     p->nWords = Kit_TruthWordNum( pPars->nVarsMax );
     p->nDivsLimit = 200;
-    // memory
-    p->vMemory = Vec_IntStart( 1 << 16 );
     // internal nodes
     p->nNodesAlloc = 512;
     p->pNodes = ALLOC( Bdc_Fun_t, p->nNodesAlloc );
+    // memory
+    p->vMemory = Vec_IntStart( 4 * p->nWords * p->nNodesAlloc );
     // set up hash table
     p->nTableSize = (1 << p->pPars->nVarsMax);
     p->pTable = ALLOC( Bdc_Fun_t *, p->nTableSize );
@@ -69,7 +69,7 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
     p->pIsfOR = &p->IsfOR;  Bdc_IsfStart( p, p->pIsfOR );
     p->pIsfAL = &p->IsfAL;  Bdc_IsfStart( p, p->pIsfAL );
     p->pIsfAR = &p->IsfAR;  Bdc_IsfStart( p, p->pIsfAR );   
-    return p;
+    return p; 
 }
 
 /**Function*************************************************************
@@ -85,6 +85,18 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
 ***********************************************************************/
 void Bdc_ManFree( Bdc_Man_t * p )
 {
+    if ( p->pPars->fVerbose )
+    {
+        printf( "Bi-decomposition stats: Calls = %d.  Nodes = %d. Reuse = %d.\n", 
+            p->numCalls, p->numNodes, p->numReuse );
+        printf( "ANDs = %d.  ORs = %d.  Weak = %d.  Muxes = %d.  Memory = %.2f K\n", 
+            p->numAnds, p->numOrs, p->numWeaks, p->numMuxes, 4.0 * Vec_IntSize(p->vMemory) / (1<<10) );
+        PRT( "Cache", p->timeCache );
+        PRT( "Check", p->timeCheck );
+        PRT( "Muxes", p->timeMuxes );
+        PRT( "Supps", p->timeSupps );
+        PRT( "TOTAL", p->timeTotal );
+    }
     Vec_IntFree( p->vMemory );
     Vec_IntFree( p->vSpots );
     Vec_PtrFree( p->vTruths );
@@ -118,7 +130,8 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
     // add constant 1
     pNode = Bdc_FunNew( p );
     pNode->Type = BDC_TYPE_CONST1;
-    pNode->puFunc = NULL;
+    pNode->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords); 
+    Kit_TruthFill( pNode->puFunc, p->nVars );
     pNode->uSupp = 0;
     Bdc_TableAdd( p, pNode );
     // add variables
@@ -192,6 +205,7 @@ void Bdc_ManDecPrint( Bdc_Man_t * p )
 int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax )
 {
     Bdc_Isf_t Isf, * pIsf = &Isf;
+    int clk = clock();
     assert( nVars <= p->pPars->nVarsMax );
     // set current manager parameters
     p->nVars = nVars;
@@ -213,8 +227,14 @@ int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int n
     Bdc_SuppMinimize( p, pIsf );
     // call decomposition
     p->pRoot = Bdc_ManDecompose_rec( p, pIsf );
+    p->timeTotal += clock() - clk;
+    p->numCalls++;
+    p->numNodes += p->nNodesNew;
     if ( p->pRoot == NULL )
         return -1;
+    if ( !Bdc_ManNodeVerify( p, pIsf, p->pRoot ) )
+        printf( "Bdc_ManDecompose(): Internal verification failed.\n" );
+//    assert( Bdc_ManNodeVerify( p, pIsf, p->pRoot ) );
     return p->nNodesNew;
 }
 
diff --git a/src/aig/bdc/bdcDec.c b/src/aig/bdc/bdcDec.c
index 13a33196..55ce97a0 100644
--- a/src/aig/bdc/bdcDec.c
+++ b/src/aig/bdc/bdcDec.c
@@ -30,6 +30,82 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Minimizes the support of the ISF.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_SuppMinimize2( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
+{
+    int v, clk;
+    if ( p->pPars->fVerbose )
+        clk = clock();
+    // compute support
+    pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) | 
+        Kit_TruthSupport( pIsf->puOff, p->nVars );
+    // go through the support variables
+    for ( v = 0; v < p->nVars; v++ )
+    {
+        if ( (pIsf->uSupp & (1 << v)) == 0 )
+            continue;
+        Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v );
+        Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v );
+        if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) )
+            continue;
+//        if ( !Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
+//            continue;
+        // remove the variable
+        Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars );
+        Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars );
+//        Kit_TruthExist( pIsf->puOn, p->nVars, v );
+//        Kit_TruthExist( pIsf->puOff, p->nVars, v );
+        pIsf->uSupp &= ~(1 << v);
+    }
+    if ( p->pPars->fVerbose )
+        p->timeSupps += clock() - clk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Minimizes the support of the ISF.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
+{
+    int v, clk;
+    if ( p->pPars->fVerbose )
+        clk = clock();
+    // go through the support variables
+    pIsf->uSupp = 0;
+    for ( v = 0; v < p->nVars; v++ )
+    {
+        if ( !Kit_TruthVarInSupport( pIsf->puOn, p->nVars, v ) && 
+             !Kit_TruthVarInSupport( pIsf->puOff, p->nVars, v ) )
+              continue;
+        if ( Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
+        {
+            Kit_TruthExist( pIsf->puOn, p->nVars, v );
+            Kit_TruthExist( pIsf->puOff, p->nVars, v );
+            continue;
+        }
+        pIsf->uSupp |= (1 << v);
+    }
+    if ( p->pPars->fVerbose )
+        p->timeSupps += clock() - clk;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Updates the ISF of the right after the left was decompoosed.]
 
   Description []
@@ -418,12 +494,16 @@ Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL
     // check if there is any reuse for the components
     if ( WeightOrL + WeightOrR > WeightAndL + WeightAndR )
     {
+        p->numReuse++;
+        p->numOrs++;
         Bdc_IsfCopy( pIsfL, p->pIsfOL );
         Bdc_IsfCopy( pIsfR, p->pIsfOR );
         return BDC_TYPE_OR;
     }
     if ( WeightOrL + WeightOrR < WeightAndL + WeightAndR )
     {
+        p->numReuse++;
+        p->numAnds++;
         Bdc_IsfCopy( pIsfL, p->pIsfAL );
         Bdc_IsfCopy( pIsfR, p->pIsfAR );
         return BDC_TYPE_AND; 
@@ -432,10 +512,16 @@ Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL
     // compare the two-component costs
     if ( WeightOr > WeightAnd )
     {
+        if ( WeightOr < BDC_SCALE )
+            p->numWeaks++;
+        p->numOrs++;
         Bdc_IsfCopy( pIsfL, p->pIsfOL );
         Bdc_IsfCopy( pIsfR, p->pIsfOR );
         return BDC_TYPE_OR;
     }
+    if ( WeightAnd < BDC_SCALE )
+        p->numWeaks++;
+    p->numAnds++;
     Bdc_IsfCopy( pIsfL, p->pIsfAL );
     Bdc_IsfCopy( pIsfR, p->pIsfAR );
     return BDC_TYPE_AND;
@@ -456,6 +542,9 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd
 {
     int Var, VarMin, nSuppMin, nSuppCur;
     unsigned uSupp0, uSupp1;
+    int clk;
+    if ( p->pPars->fVerbose )
+        clk = clock();
     VarMin = -1;
     nSuppMin = 1000;
     for ( Var = 0; Var < p->nVars; Var++ )
@@ -473,7 +562,7 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd
         {
             nSuppMin = nSuppCur;
             VarMin = Var;
-//            break;
+            break;
         }
     }
     if ( VarMin >= 0 )
@@ -485,6 +574,8 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd
         Bdc_SuppMinimize( p, pIsfL );
         Bdc_SuppMinimize( p, pIsfR );
     }
+    if ( p->pPars->fVerbose )
+        p->timeMuxes += clock() - clk;
     return VarMin;
 }
 
@@ -582,6 +673,7 @@ Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
     Bdc_Fun_t * pFunc, * pFunc0, * pFunc1;
     Bdc_Isf_t IsfL, * pIsfL = &IsfL;
     Bdc_Isf_t IsfB, * pIsfR = &IsfB;
+    int iVar, clk;
 /*
 printf( "Init function (%d):\n", LocalCounter );
 Extra_PrintBinary( stdout, pIsf->puOn, 1<<4 );printf("\n");
@@ -589,13 +681,27 @@ Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n");
 */
     // check computed results
     assert( Kit_TruthIsDisjoint(pIsf->puOn, pIsf->puOff, p->nVars) );
-    if ( pFunc = Bdc_TableLookup( p, pIsf ) )
+    if ( p->pPars->fVerbose )
+        clk = clock();
+    pFunc = Bdc_TableLookup( p, pIsf );
+    if ( p->pPars->fVerbose )
+        p->timeCache += clock() - clk;
+    if ( pFunc )
         return pFunc;
     // decide on the decomposition type
+    if ( p->pPars->fVerbose )
+        clk = clock();
     Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR );
+    if ( p->pPars->fVerbose )
+        p->timeCheck += clock() - clk;
     if ( Type == BDC_TYPE_MUX )
     {
-        int iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR );
+        if ( p->pPars->fVerbose )
+            clk = clock();
+        iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR );
+        if ( p->pPars->fVerbose )
+            p->timeMuxes += clock() - clk;
+        p->numMuxes++;
         pFunc0 = Bdc_ManDecompose_rec( p, pIsfL );
         pFunc1 = Bdc_ManDecompose_rec( p, pIsfR );
         if ( pFunc0 == NULL || pFunc1 == NULL )
@@ -625,9 +731,6 @@ Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n");
         // create new gate
         pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, Type );
     }
-    if ( pFunc == NULL )
-        return NULL;
-    assert( Bdc_ManNodeVerify( p, pIsf, pFunc ) );
     return pFunc;
 }
 
diff --git a/src/aig/bdc/bdcInt.h b/src/aig/bdc/bdcInt.h
index 5fda4301..afba0e67 100644
--- a/src/aig/bdc/bdcInt.h
+++ b/src/aig/bdc/bdcInt.h
@@ -106,6 +106,20 @@ struct Bdc_Man_t_
     Bdc_Isf_t * pIsfAR, IsfAR;
     // internal memory manager
     Vec_Int_t *      vMemory;      // memory for internal truth tables
+    // statistics
+    int              numCalls;
+    int              numNodes;
+    int              numMuxes;
+    int              numAnds;
+    int              numOrs;
+    int              numWeaks;
+    int              numReuse;
+    // runtime
+    int              timeCache;
+    int              timeCheck;
+    int              timeMuxes;
+    int              timeSupps;
+    int              timeTotal;
 };
 
 // working with complemented attributes of objects
@@ -132,11 +146,12 @@ static inline void        Bdc_IsfNot( Bdc_Isf_t * p )                   { unsign
 
 /*=== bdcDec.c ==========================================================*/
 extern Bdc_Fun_t *      Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
+extern void             Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
+extern int              Bdc_ManNodeVerify( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Fun_t * pFunc );
 /*=== bdcTable.c ==========================================================*/
 extern Bdc_Fun_t *      Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
 extern void             Bdc_TableAdd( Bdc_Man_t * p, Bdc_Fun_t * pFunc );
 extern void             Bdc_TableClear( Bdc_Man_t * p );
-extern void             Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
 extern int              Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth );
 
 #ifdef __cplusplus
diff --git a/src/aig/bdc/bdcTable.c b/src/aig/bdc/bdcTable.c
index b7f10344..3a6ed126 100644
--- a/src/aig/bdc/bdcTable.c
+++ b/src/aig/bdc/bdcTable.c
@@ -30,39 +30,6 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Minimizes the support of the ISF.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
-{
-    int v;
-    // compute support
-    pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) | 
-        Kit_TruthSupport( pIsf->puOff, p->nVars );
-    // go through the support variables
-    for ( v = 0; v < p->nVars; v++ )
-    {
-        if ( (pIsf->uSupp & (1 << v)) == 0 )
-            continue;
-        Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v );
-        Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v );
-        if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) )
-            continue;
-        // remove the variable
-        Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars );
-        Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars );
-        pIsf->uSupp &= ~(1 << v);
-    }
-}
-
-/**Function*************************************************************
-
   Synopsis    [Checks containment of the function in the ISF.]
 
   Description []
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index a765ec30..e814840f 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -21,6 +21,9 @@
 #include "darInt.h"
 #include "kit.h"
 
+#include "bdc.h"
+#include "bdcInt.h"
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -44,6 +47,9 @@ struct Ref_Man_t_
     Kit_Graph_t *    pGraphBest;     // the best factored form
     int              GainBest;       // the best gain
     int              LevelBest;      // the level of node with the best gain
+    // bi-decomposition
+    Bdc_Par_t        DecPars;        // decomposition parameters
+    Bdc_Man_t *      pManDec;        // decomposition manager
     // node statistics
     int              nNodesInit;     // the initial number of nodes
     int              nNodesTried;    // the number of nodes tried
@@ -111,6 +117,11 @@ Ref_Man_t * Dar_ManRefStart( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
     p->vMemory      = Vec_IntAlloc( 1 << 16 );
     p->vCutNodes    = Vec_PtrAlloc( 256 );
     p->vLeavesBest  = Vec_PtrAlloc( pPars->nLeafMax );
+    // alloc bi-decomposition manager
+    p->DecPars.nVarsMax = pPars->nLeafMax;
+    p->DecPars.fVerbose = pPars->fVerbose;
+    p->DecPars.fVeryVerbose = 0;
+//    p->pManDec = Bdc_ManAlloc( &p->DecPars );
     return p;
 }
 
@@ -151,6 +162,8 @@ void Dar_ManRefPrintStats( Ref_Man_t * p )
 ***********************************************************************/
 void Dar_ManRefStop( Ref_Man_t * p )
 {
+    if ( p->pManDec )
+        Bdc_ManFree( p->pManDec );
     if ( p->pPars->fVerbose )
         Dar_ManRefPrintStats( p );
     Vec_VecFree( p->vCuts );
@@ -381,6 +394,13 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
         if ( RetValue > -1 )
         {
             pGraphCur = Kit_SopFactor( p->vMemory, 0, Vec_PtrSize(vCut), p->vMemory );
+/*
+{
+    int RetValue;
+    RetValue = Bdc_ManDecompose( p->pManDec, pTruth, NULL, Vec_PtrSize(vCut), NULL, 1000 );
+    printf( "Graph = %d. Bidec = %d.\n", Kit_GraphNodeNum(pGraphCur), RetValue );
+}
+*/
             nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required );
             if ( nNodesAdded > -1 )
             {
@@ -403,9 +423,17 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
         // try negative phase
         Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) );
         RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 );
+//        Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) );
         if ( RetValue > -1 )
         {
             pGraphCur = Kit_SopFactor( p->vMemory, 1, Vec_PtrSize(vCut), p->vMemory );
+/*
+{
+    int RetValue;
+    RetValue = Bdc_ManDecompose( p->pManDec, pTruth, NULL, Vec_PtrSize(vCut), NULL, 1000 );
+    printf( "Graph = %d. Bidec = %d.\n", Kit_GraphNodeNum(pGraphCur), RetValue );
+}
+*/
             nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required );
             if ( nNodesAdded > -1 )
             {
@@ -426,6 +454,7 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
                 Kit_GraphFree( pGraphCur );
         }
     }
+
     return p->GainBest;
 }
 
diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h
index 06a93cf0..23e3ce8d 100644
--- a/src/aig/kit/kit.h
+++ b/src/aig/kit/kit.h
@@ -564,6 +564,7 @@ extern void            Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVa
 extern void            Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar );
 extern void            Kit_TruthCofactor0New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
 extern void            Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
+extern int             Kit_TruthVarIsVacuous( unsigned * pOnset, unsigned * pOffset, 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 );
diff --git a/src/aig/kit/kitTruth.c b/src/aig/kit/kitTruth.c
index dab60132..9ddc7562 100644
--- a/src/aig/kit/kitTruth.c
+++ b/src/aig/kit/kitTruth.c
@@ -520,6 +520,64 @@ void Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes negative cofactor of the function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+int Kit_TruthVarIsVacuous( unsigned * pOnset, unsigned * pOffset, 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++ )
+            if ( ((pOnset[i] & (pOffset[i] >> 1)) | (pOffset[i] & (pOnset[i] >> 1))) & 0x55555555 )
+                 return 0;
+        return 1;
+    case 1:
+        for ( i = 0; i < nWords; i++ )
+            if ( ((pOnset[i] & (pOffset[i] >> 2)) | (pOffset[i] & (pOnset[i] >> 2))) & 0x33333333 )
+                 return 0;
+            return 1;
+    case 2:
+        for ( i = 0; i < nWords; i++ )
+            if ( ((pOnset[i] & (pOffset[i] >> 4)) | (pOffset[i] & (pOnset[i] >> 4))) & 0x0F0F0F0F )
+                 return 0;
+        return 1;
+    case 3:
+        for ( i = 0; i < nWords; i++ )
+            if ( ((pOnset[i] & (pOffset[i] >> 8)) | (pOffset[i] & (pOnset[i] >> 8))) & 0x00FF00FF )
+                 return 0;
+        return 1;
+    case 4:
+        for ( i = 0; i < nWords; i++ )
+            if ( ((pOnset[i] & (pOffset[i] >> 16)) || (pOffset[i] & (pOnset[i] >> 16))) & 0x0000FFFF )
+                 return 0;
+        return 1;
+    default:
+        Step = (1 << (iVar - 5));
+        for ( k = 0; k < nWords; k += 2*Step )
+        {
+            for ( i = 0; i < Step; i++ )
+                if ( (pOnset[i] & pOffset[Step+i]) | (pOffset[i] & pOnset[Step+i]) )
+                     return 0;
+            pOnset += 2*Step;
+            pOffset += 2*Step;
+        }
+        return 1;
+    }
+}
+
 
 /**Function*************************************************************