mvcDivisor.c

Go to the documentation of this file.

 
#include "mvc.h"
 
ABC_NAMESPACE_IMPL_START
 

 
static void  Mvc_CoverDivisorZeroKernel( Mvc_Cover_t * pCover );


Mvc_Cover_t * Mvc_CoverDivisor( Mvc_Cover_t * pCover )
{
    Mvc_Cover_t * pKernel;
    if ( Mvc_CoverReadCubeNum(pCover) <= 1 )
        return NULL;
    // allocate the literal array and count literals
    if ( Mvc_CoverAnyLiteral( pCover, NULL ) == -1 )
        return NULL;
    // duplicate the cover
    pKernel = Mvc_CoverDup(pCover);
    // perform the kerneling
    Mvc_CoverDivisorZeroKernel( pKernel );
    assert( Mvc_CoverReadCubeNum(pKernel) );
    return pKernel;
}

void Mvc_CoverDivisorZeroKernel( Mvc_Cover_t * pCover )
{
    int iLit;
    // find any literal that occurs at least two times
//    iLit = Mvc_CoverAnyLiteral( pCover, NULL );
    iLit = Mvc_CoverWorstLiteral( pCover, NULL );
//    iLit = Mvc_CoverBestLiteral( pCover, NULL );
    if ( iLit == -1 )
        return;
    // derive the cube-free quotient
    Mvc_CoverDivideByLiteralQuo( pCover, iLit ); // the same cover
    Mvc_CoverMakeCubeFree( pCover );             // the same cover
    // call recursively
    Mvc_CoverDivisorZeroKernel( pCover );              // the same cover
}

 
 
ABC_NAMESPACE_IMPL_END