Commit e52d3a0c by Alan Mishchenko

Bug fix in handling constants in the updated 'sop' command.

parent 9b29e1a3
...@@ -216,22 +216,17 @@ char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn, ...@@ -216,22 +216,17 @@ char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn,
assert( bFuncOn == bFuncOnDc || Cudd_bddLeq( dd, bFuncOn, bFuncOnDc ) ); assert( bFuncOn == bFuncOnDc || Cudd_bddLeq( dd, bFuncOn, bFuncOnDc ) );
if ( Cudd_IsConstant(bFuncOn) || Cudd_IsConstant(bFuncOnDc) ) if ( Cudd_IsConstant(bFuncOn) || Cudd_IsConstant(bFuncOnDc) )
{ {
if ( fMode == -1 ) // if the phase is not known, write constant 1
fMode = 1;
Vec_StrFill( vCube, nFanins, '-' );
Vec_StrPush( vCube, '\0' );
if ( pMan ) if ( pMan )
pSop = Mem_FlexEntryFetch( pMan, nFanins + 4 ); pSop = Mem_FlexEntryFetch( pMan, nFanins + 4 );
else else
pSop = ABC_ALLOC( char, nFanins + 4 ); pSop = ABC_ALLOC( char, nFanins + 4 );
if ( bFuncOn == Cudd_ReadOne(dd) ) pSop[0] = ' ';
sprintf( pSop, "%s %d\n", vCube->pArray, fMode ); pSop[1] = '0' + (int)(bFuncOn == Cudd_ReadOne(dd));
else pSop[2] = '\n';
sprintf( pSop, "%s %d\n", vCube->pArray, !fMode ); pSop[3] = '\0';
return pSop; return pSop;
} }
if ( fMode == -1 ) if ( fMode == -1 )
{ // try both phases { // try both phases
assert( fAllPrimes == 0 ); assert( fAllPrimes == 0 );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment