Fixing compiler problem.

This commit is contained in:
Alan Mishchenko 2026-02-13 07:12:50 -08:00
parent 3285adaf32
commit 2726f0e470
2 changed files with 9 additions and 9 deletions

View File

@ -680,6 +680,11 @@ extern Vec_Ptr_t * Abc_NtkCollectCoNames( Abc_Ntk_t * pNtk );
extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut );
typedef struct Wlc_Ntk_t_ Wlc_Ntk_t;
typedef struct Wlc_BstPar_t_ Wlc_BstPar_t;
extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pPars );
extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -51320,10 +51325,6 @@ usage:
***********************************************************************/
int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
typedef struct Wlc_Ntk_t_ Wlc_Ntk_t;
typedef struct Wlc_BstPar_t_ Wlc_BstPar_t;
extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pPars );
extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent );
Gia_Man_t * pGiaUse = pAbc->pGia, * pGiaTemp = NULL;
Wlc_Ntk_t * pWlc = (Wlc_Ntk_t *)pAbc->pAbcWlc;
int c, nProcs = 5, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0;

View File

@ -1722,7 +1722,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
Wlc_ObjForEachFanin( pObj, iFanin, k )
if ( k > 0 )
fSigned &= Wlc_NtkObj(p, iFanin)->Signed;
if ( pParIn->fBlastNew && nRange0 <= 16 )
if ( pPar->fBlastNew && nRange0 <= 16 )
{
char * pNums = Wlc_NtkMuxTreeString( nRange0 );
Vec_Int_t ** pvDecs = Wlc_NtkMuxTree3DecsDerive( pNew, pFans0, nRange0, pNums );
@ -1989,9 +1989,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
int fCompl = (pObj->Type == WLC_OBJ_COMP_MOREEQU || pObj->Type == WLC_OBJ_COMP_LESSEQU);
if ( fSwap ) ABC_SWAP( int *, pArg0, pArg1 );
if ( fSigned )
iLit = pParIn->fBlastNew ? Wlc_BlastLessSigned3( pNew, pArg0, pArg1, nRangeMax ) : Wlc_BlastLessSigned( pNew, pArg0, pArg1, nRangeMax );
iLit = pPar->fBlastNew ? Wlc_BlastLessSigned3( pNew, pArg0, pArg1, nRangeMax ) : Wlc_BlastLessSigned( pNew, pArg0, pArg1, nRangeMax );
else
iLit = pParIn->fBlastNew ? Wlc_BlastLess3( pNew, pArg0, pArg1, nRangeMax ) : Wlc_BlastLess( pNew, pArg0, pArg1, nRangeMax );
iLit = pPar->fBlastNew ? Wlc_BlastLess3( pNew, pArg0, pArg1, nRangeMax ) : Wlc_BlastLess( pNew, pArg0, pArg1, nRangeMax );
iLit = Abc_LitNotCond( iLit, fCompl );
Vec_IntFill( vRes, 1, iLit );
for ( k = 1; k < nRange; k++ )
@ -2124,7 +2124,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
else if ( pObj->Type == WLC_OBJ_DEC )
{
int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRange0, 0 );
if ( pParIn->fBlastNew )
if ( pPar->fBlastNew )
Wlc_BlastDecoder2( pNew, pArg0, nRange0, vTemp2, vRes );
else
Wlc_BlastDecoder( pNew, pArg0, nRange0, vTemp2, vRes );
@ -3015,4 +3015,3 @@ void Wlc_MultBlastTest()
ABC_NAMESPACE_IMPL_END