abc/src/opt/fxu/fxuPair.c
/**Function*************************************************************

  Synopsis    [Computes the hash key of the divisor represented by the pair of cubes.]

  Description [Goes through the variables in both cubes. Skips the identical
  ones (this corresponds to making the cubes cube-free). Computes the hash 
  value of the cubes. Assigns the number of literals in the base and in the 
  cubes without base.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Function
Synopsis    [Computes the hash key of the divisor represented by the pair of cubes.]

Description [Goes through the variables in both cubes. Skips the identical
ones (this corresponds to making the cubes cube-free). Computes the hash
value of the cubes. Assigns the number of literals in the base and in the
cubes without base.]




Function Synopsis [ Computes the hash key of the divisor represented by the pair of cubes . ] Description [ Goes through the variables in both cubes . Skips the identical ones ( this corresponds to making the cubes cube - free ) . Computes the hash value of the cubes . Assigns the number of literals in the base and in the cubes without base . ]
unsigned Fxu_PairHashKey( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2, 
                         int * pnBase, int * pnLits1, int * pnLits2 )
{
    int Offset1 = 100, Offset2 = 200;
    int nBase, nLits1, nLits2;
    Fxu_Lit * pLit1, * pLit2;
    unsigned Key;
    Key    = 0;
    nLits1 = 0;
    nLits2 = 0;
    nBase  = 0;
    pLit1  = pCube1->lLits.pHead;
    pLit2  = pCube2->lLits.pHead;
    while ( 1 )
    {
        if ( pLit1 && pLit2 )
        {
            if ( pLit1->iVar == pLit2->iVar )
            { 
                pLit1 = pLit1->pHNext;
                pLit2 = pLit2->pHNext;
                nBase++;
            }
            else if ( pLit1->iVar < pLit2->iVar )
            {
                Key  ^= s_Primes[Offset1+nLits1] * pLit1->iVar;
                pLit1 = pLit1->pHNext;
                nLits1++;
            }
            else
            {
                Key  ^= s_Primes[Offset2+nLits2] * pLit2->iVar;
                pLit2 = pLit2->pHNext;
                nLits2++;
            }
        }
        else if ( pLit1 && !pLit2 )
        {
            Key  ^= s_Primes[Offset1+nLits1] * pLit1->iVar;
            pLit1 = pLit1->pHNext;
            nLits1++;
        }
        else if ( !pLit1 && pLit2 )
        {
            Key  ^= s_Primes[Offset2+nLits2] * pLit2->iVar;
            pLit2 = pLit2->pHNext;
            nLits2++;
        }
        else
            break;
    }
    *pnBase  = nBase;
    *pnLits1 = nLits1;
    *pnLits2 = nLits2;
    return Key;
}
unsigned Fxu_PairHashKey ( Fxu_Matrix * p , Fxu_Cube * pCube1 , Fxu_Cube * pCube2 , int * pnBase , int * pnLits1 , int * pnLits2 ) { int Offset1 = 100 , Offset2 = 200 ; int nBase , nLits1 , nLits2 ; Fxu_Lit * pLit1 , * pLit2 ; unsigned Key ; Key = 0 ; nLits1 = 0 ; nLits2 = 0 ; nBase = 0 ; pLit1 = pCube1 -> lLits . pHead ; pLit2 = pCube2 -> lLits . pHead ; while ( 1 ) { if ( pLit1 && pLit2 ) { if ( pLit1 -> iVar == pLit2 -> iVar ) { pLit1 = pLit1 -> pHNext ; pLit2 = pLit2 -> pHNext ; nBase ++ ; } else if ( pLit1 -> iVar < pLit2 -> iVar ) { Key ^= s_Primes [ Offset1 + nLits1 ] * pLit1 -> iVar ; pLit1 = pLit1 -> pHNext ; nLits1 ++ ; } else { Key ^= s_Primes [ Offset2 + nLits2 ] * pLit2 -> iVar ; pLit2 = pLit2 -> pHNext ; nLits2 ++ ; } } else if ( pLit1 && ! pLit2 ) { Key ^= s_Primes [ Offset1 + nLits1 ] * pLit1 -> iVar ; pLit1 = pLit1 -> pHNext ; nLits1 ++ ; } else if ( ! pLit1 && pLit2 ) { Key ^= s_Primes [ Offset2 + nLits2 ] * pLit2 -> iVar ; pLit2 = pLit2 -> pHNext ; nLits2 ++ ; } else break ; } * pnBase = nBase ; * pnLits1 = nLits1 ; * pnLits2 = nLits2 ; return Key ; }
Function
Synopsis    [Computes the hash key of the divisor represented by the pair of cubes.]
Function Synopsis [ Computes the hash key of the divisor represented by the pair of cubes . ]
// compute the hash key // ensure cube-free // add this literal to the base