Fixing continues.

This commit is contained in:
Alan Mishchenko 2025-12-24 22:26:01 -08:00
parent 99ca3e4428
commit 8d42237589
6 changed files with 11 additions and 6 deletions

View File

@ -292,8 +292,8 @@ static inline int Abc_Base2LogW( word n ) { int r; if ( n <
static inline int Abc_Base10LogW( word n ) { int r; if ( n < 2 ) return (int)n; for ( r = 0, n--; n; n /= 10, r++ ) {}; return r; }
static inline int Abc_Base16LogW( word n ) { int r; if ( n < 2 ) return (int)n; for ( r = 0, n--; n; n /= 16, r++ ) {}; return r; }
static inline char * Abc_UtilStrsav( char * s ) { return s ? strcpy(ABC_ALLOC(char, strlen(s)+1), s) : NULL; }
static inline char * Abc_UtilStrsavTwo( char * s, char * a ){ char * r; if (!a) return Abc_UtilStrsav(s); r = ABC_ALLOC(char, strlen(s)+strlen(a)+1); sprintf(r, "%s%s", s, a ); return r; }
static inline char * Abc_UtilStrsavNum( char * s, int n ) { char * r; if (!s) return NULL; r = ABC_ALLOC(char, strlen(s)+12+1); sprintf(r, "%s%d", s, n ); return r; }
static inline char * Abc_UtilStrsavTwo( char * s, char * a ){ char * r; if (!a) return Abc_UtilStrsav(s); r = ABC_ALLOC(char, strlen(s)+strlen(a)+1); snprintf(r, strlen(s)+strlen(a)+1, "%s%s", s, a ); return r; }
static inline char * Abc_UtilStrsavNum( char * s, int n ) { char * r; if (!s) return NULL; r = ABC_ALLOC(char, strlen(s)+12+1); snprintf(r, strlen(s)+12+1, "%s%d", s, n ); return r; }
static inline int Abc_BitByteNum( int nBits ) { return (nBits>>3) + ((nBits&7) > 0); }
static inline int Abc_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); }
static inline int Abc_Bit6WordNum( int nBits ) { return (nBits>>6) + ((nBits&63) > 0); }

View File

@ -183,6 +183,8 @@ static inline void Xdbl_Test()
xdbl ten100_ = ABC_CONST(0x014c924d692ca61b);
assert( ten100 == ten100_ );
(void)ten100;
(void)ten100_;
// float f1 = Xdbl_ToDouble(c1);
// Extra_PrintBinary( stdout, (int *)&c1, 32 ); printf( "\n" );

View File

@ -1595,6 +1595,7 @@ static inline int Abc_TtReadBin( word * pWords, int nWords, char * pString )
{
int i, Len = (int)strlen(pString), nWords2 = (Len+63)/64;
assert( nWords2 <= nWords );
(void)nWords2;
memset( pWords, 0, sizeof(word)*nWords );
for ( i = 0; i < Len; i++ )
if ( pString[i] == '1' )
@ -1608,6 +1609,7 @@ static inline word Abc_TtReadBin64( char * pString )
word Word = 0;
int Len = (int)strlen(pString);
assert( Len <= 64 );
(void)Len;
int Res = Abc_TtReadBin( &Word, 1, pString );
if ( Res == 0 ) {
printf( "Reading binary string \"%s\" has failed.\n", pString );
@ -1842,6 +1844,7 @@ static inline int Abc_TtCheckCondDep( word * pTruth, int nVars, int nSuppLim )
word Cof0[128], Cof1[128]; // pow( 2, nVarsMax-6 )
int v, d, nWords = Abc_TtWordNum(nVars);
assert( nVars <= nVarsMax );
(void)nVarsMax;
if ( nVars <= nSuppLim + 1 )
return 0;
for ( v = 0; v < nVars; v++ )

View File

@ -458,7 +458,7 @@ static inline void Vec_MemDumpTruthTables( Vec_Mem_t * p, char * pName, int nLut
{
FILE * pFile;
char pFileName[1000];
sprintf( pFileName, "tt_%s_%02d.txt", pName ? pName : NULL, nLutSize );
snprintf( pFileName, sizeof(pFileName), "tt_%s_%02d.txt", pName ? pName : "", nLutSize );
pFile = pName ? fopen( pFileName, "wb" ) : stdout;
Vec_MemDump( pFile, p );
if ( pFile != stdout )
@ -475,4 +475,3 @@ ABC_NAMESPACE_HEADER_END
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -525,6 +525,7 @@ Vec_Int_t * SimUifPairFinder::_collect_sim_nodes(Wlc_Ntk_t * pNtk) {
int i;
Wlc_Obj_t * pPo;
int range = Wlc_ObjRange(Wlc_NtkPo(pNtk, 1));
(void)range;
Wlc_NtkForEachPo(pNtk, pPo, i) {
if ((i%3)==0) continue;
assert(range == Wlc_ObjRange(pPo));
@ -1419,7 +1420,7 @@ int UfarManager::PerformUIFProve(const timeval& timer) {
auto print_stat = [&]() {
gettimeofday(&curTime, NULL);
elapsedTime = elapsed_time_usec(timer, curTime)/1000000.0;
sprintf(buffer, "Iteration[%2u][%3u]: %4lu White boxes\t%4lu UIF constraints (time = %.4f)", n_iter_wb, n_iter_uif, count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false), _set_uif_pairs.size(), elapsedTime);
snprintf(buffer, sizeof(buffer), "Iteration[%2u][%3u]: %4lu White boxes\t%4lu UIF constraints (time = %.4f)", n_iter_wb, n_iter_uif, count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false), _set_uif_pairs.size(), elapsedTime);
LOG(1) << buffer << _get_profile_uf_wb();
dump_grey_stat();
if(!params.fileStatesOut.empty()) _dump_states(params.fileStatesOut);

View File

@ -35,7 +35,7 @@ using IntPair = std::pair<int, int>;
struct OperatorID;
struct UifPair;
struct Greyness;
class Greyness;
using UIF_PAIR = UifPair;
class SimUifPairFinder;