Commit 3418a882 by Alan Mishchenko

Fixed a bug in matching code.

parent cd4752b5
...@@ -253,7 +253,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi ...@@ -253,7 +253,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
} }
// free the sat_solver // free the sat_solver
// if ( fVerbose ) if ( fVerbose )
Sat_SolverPrintStats( stdout, pSat ); Sat_SolverPrintStats( stdout, pSat );
//sat_solver_store_write( pSat, "trace.cnf" ); //sat_solver_store_write( pSat, "trace.cnf" );
//sat_solver_store_free( pSat ); //sat_solver_store_free( pSat );
......
...@@ -964,6 +964,9 @@ void Io_NtkWriteNodeIntStruct( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vCov ...@@ -964,6 +964,9 @@ void Io_NtkWriteNodeIntStruct( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vCov
// write leaf node // write leaf node
fprintf( pFile, ".names" ); fprintf( pFile, ".names" );
for ( i = 0; i < pLut2[0]; i++ ) for ( i = 0; i < pLut2[0]; i++ )
if ( pLut2[2+i] == nLeaves )
fprintf( pFile, " %s_lut1", Abc_ObjName(Abc_ObjFanout0(pNode)) );
else
fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanin(pNode,pLut2[2+i])) ); fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanin(pNode,pLut2[2+i])) );
fprintf( pFile, " %s_lut2\n", Abc_ObjName(Abc_ObjFanout0(pNode)) ); fprintf( pFile, " %s_lut2\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
// write SOP // write SOP
......
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