00001 00019 #include "mvc.h" 00020 00024 00025 static void Mvc_CoverDivisorZeroKernel( Mvc_Cover_t * pCover ); 00026 00030 00043 Mvc_Cover_t * Mvc_CoverDivisor( Mvc_Cover_t * pCover ) 00044 { 00045 Mvc_Cover_t * pKernel; 00046 if ( Mvc_CoverReadCubeNum(pCover) <= 1 ) 00047 return NULL; 00048 // allocate the literal array and count literals 00049 if ( Mvc_CoverAnyLiteral( pCover, NULL ) == -1 ) 00050 return NULL; 00051 // duplicate the cover 00052 pKernel = Mvc_CoverDup(pCover); 00053 // perform the kerneling 00054 Mvc_CoverDivisorZeroKernel( pKernel ); 00055 assert( Mvc_CoverReadCubeNum(pKernel) ); 00056 return pKernel; 00057 } 00058 00070 void Mvc_CoverDivisorZeroKernel( Mvc_Cover_t * pCover ) 00071 { 00072 int iLit; 00073 // find any literal that occurs at least two times 00074 // iLit = Mvc_CoverAnyLiteral( pCover, NULL ); 00075 iLit = Mvc_CoverWorstLiteral( pCover, NULL ); 00076 // iLit = Mvc_CoverBestLiteral( pCover, NULL ); 00077 if ( iLit == -1 ) 00078 return; 00079 // derive the cube-free quotient 00080 Mvc_CoverDivideByLiteralQuo( pCover, iLit ); // the same cover 00081 Mvc_CoverMakeCubeFree( pCover ); // the same cover 00082 // call recursively 00083 Mvc_CoverDivisorZeroKernel( pCover ); // the same cover 00084 } 00085 00089 00090
1.6.1