Skip to content

Commit 8475386

Browse files
alanminkoalanminko
committed
Making %ufar preserve AIG name.
1 parent 2726f0e commit 8475386

File tree

5 files changed

+84
-7
lines changed

5 files changed

+84
-7
lines changed

‎src/base/wlc/wlcBlast.c‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1434,6 +1434,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
14341434
// create AIG manager
14351435
pNew = Gia_ManStart( 5 * Wlc_NtkObjNum(p) + 1000 );
14361436
pNew->pName = Abc_UtilStrsav( p->pName );
1437+
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
14371438
pNew->fGiaSimple = pPar->fGiaSimple;
14381439
if ( !pPar->fGiaSimple )
14391440
Gia_ManHashAlloc( pNew );
@@ -2730,7 +2731,6 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
27302731
Abc_FrameSetLibBox( pBoxLib );
27312732
}
27322733

2733-
//pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName );
27342734
// dump the miter parts
27352735
if ( 0 )
27362736
{

‎src/opt/ufar/UfarMgr.cpp‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -981,6 +981,10 @@ void UfarManager::Initialize(Wlc_Ntk_t * pNtk, const set<unsigned>& types) {
981981
profile = Profile();
982982

983983
_pOrigNtk = Wlc_NtkDupDfsSimple(pNtk);
984+
if ( _pOrigNtk->pName == NULL )
985+
_pOrigNtk->pName = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec );
986+
if ( _pOrigNtk->pSpec == NULL )
987+
_pOrigNtk->pSpec = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec );
984988

985989
Wlc_Obj_t * pObj;
986990
int i;
@@ -1083,6 +1087,16 @@ Wlc_Ntk_t * UfarManager::BuildCurrentAbstraction() {
10831087
pNew = RemoveAuxPOs(pTemp = pNew, Wlc_NtkPoNum(_pOrigNtk));
10841088
Wlc_NtkFree(pTemp);
10851089

1090+
// Preserve benchmark identity through abstraction refinements so
1091+
// downstream bit-level engines report a meaningful miter name.
1092+
if ( _pOrigNtk )
1093+
{
1094+
ABC_FREE( pNew->pName );
1095+
ABC_FREE( pNew->pSpec );
1096+
pNew->pName = Abc_UtilStrsav( _pOrigNtk->pName ? _pOrigNtk->pName : _pOrigNtk->pSpec );
1097+
pNew->pSpec = Abc_UtilStrsav( _pOrigNtk->pName ? _pOrigNtk->pName : _pOrigNtk->pSpec );
1098+
}
1099+
10861100
// Wlc_WriteVer(pNew, "Abs.v", 0, 0);
10871101

10881102
return pNew;

‎src/opt/ufar/UfarPth.cpp‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,28 @@ using namespace std;
3333

3434
namespace UFAR {
3535

36+
static inline void Ufar_CopyGiaNameToAig( Gia_Man_t * pGia, Aig_Man_t * pAig )
37+
{
38+
char * pName = pGia->pName ? pGia->pName : pGia->pSpec;
39+
if ( pName == NULL )
40+
return;
41+
if ( pAig->pName == NULL )
42+
pAig->pName = Abc_UtilStrsav( pName );
43+
if ( pAig->pSpec == NULL )
44+
pAig->pSpec = Abc_UtilStrsav( pName );
45+
}
46+
47+
static inline void Ufar_CopyAigNameToNtk( Aig_Man_t * pAig, Abc_Ntk_t * pNtk )
48+
{
49+
char * pName = pAig->pName ? pAig->pName : pAig->pSpec;
50+
if ( pName == NULL )
51+
return;
52+
if ( pNtk->pName == NULL )
53+
pNtk->pName = Abc_UtilStrsav( pName );
54+
if ( pNtk->pSpec == NULL )
55+
pNtk->pSpec = Abc_UtilStrsav( pName );
56+
}
57+
3658
// mutext to control access to shared variables
3759
pthread_mutex_t g_mutex;
3860
// cv to control timer
@@ -63,6 +85,7 @@ class PDR : public Solver {
6385
Pth_Data_t * pData = (Pth_Data_t *)pArg;
6486

6587
_pAig = Gia_ManToAigSimple( pData->pGia );
88+
Ufar_CopyGiaNameToAig( pData->pGia, _pAig );
6689

6790
Pdr_Par_t * pPdrPars = &_PdrPars;
6891
Pdr_ManSetDefaultParams(pPdrPars);
@@ -93,6 +116,7 @@ class PDRA : public Solver {
93116
Pth_Data_t * pData = (Pth_Data_t *)pArg;
94117

95118
_pAig = Gia_ManToAigSimple( pData->pGia );
119+
Ufar_CopyGiaNameToAig( pData->pGia, _pAig );
96120

97121
Pdr_Par_t * pPdrPars = &_PdrPars;
98122
Pdr_ManSetDefaultParams(pPdrPars);
@@ -126,7 +150,9 @@ class BMC3 : public Solver {
126150
BMC3 ( void * pArg ) {
127151
Pth_Data_t * pData = (Pth_Data_t *)pArg;
128152
Aig_Man_t * pAig = Gia_ManToAigSimple( pData->pGia );
153+
Ufar_CopyGiaNameToAig( pData->pGia, pAig );
129154
_pNtk = Abc_NtkFromAigPhase( pAig );
155+
Ufar_CopyAigNameToNtk( pAig, _pNtk );
130156
Aig_ManStop( pAig );
131157

132158
Saig_ParBmc_t * pBmcPars = &_Pars;

‎src/opt/untk/NtkNtk.cpp‎

Lines changed: 16 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -52,11 +52,14 @@ static inline int create_buffer(Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFa
5252
Gia_Man_t * BitBlast(Wlc_Ntk_t * pNtk) {
5353
Wlc_BstPar_t Par, * pPar = &Par;
5454
Wlc_BstParDefault( pPar );
55-
return Wlc_NtkBitBlast(pNtk, pPar);
56-
//Gia_Man_t * pGia = Wlc_NtkBitBlast2(pNtk, NULL);
57-
//printf( "Usingn old bit-blaster: " );
58-
//Gia_ManPrintStats( pGia, NULL );
59-
//return pGia;
55+
Gia_Man_t * pGia = Wlc_NtkBitBlast(pNtk, pPar);
56+
if ( pGia == NULL )
57+
return NULL;
58+
if ( pGia->pName == NULL )
59+
pGia->pName = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec );
60+
if ( pGia->pSpec == NULL )
61+
pGia->pSpec = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec );
62+
return pGia;
6063
}
6164

6265
template<typename Functor>
@@ -1292,7 +1295,15 @@ int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileNam
12921295
}
12931296

12941297
Aig_Man_t * pAig = Gia_ManToAig(pGia, 0);
1298+
if ( pAig->pName == NULL )
1299+
pAig->pName = Abc_UtilStrsav( pGia->pName ? pGia->pName : pGia->pSpec );
1300+
if ( pAig->pSpec == NULL )
1301+
pAig->pSpec = Abc_UtilStrsav( pGia->pName ? pGia->pName : pGia->pSpec );
12951302
Abc_Ntk_t * pAbcNtk = Abc_NtkFromAigPhase(pAig);
1303+
if ( pAbcNtk->pName == NULL )
1304+
pAbcNtk->pName = Abc_UtilStrsav( pAig->pName ? pAig->pName : pAig->pSpec );
1305+
if ( pAbcNtk->pSpec == NULL )
1306+
pAbcNtk->pSpec = Abc_UtilStrsav( pAig->pName ? pAig->pName : pAig->pSpec );
12961307

12971308
if (pFileName && !pFileName->empty())
12981309
Gia_AigerWriteSimple(pGia, &((*pFileName + ".aig")[0u]));

‎src/proof/cec/cecProve.c‎

Lines changed: 27 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -83,6 +83,26 @@ typedef struct Par_ThData_t_
8383
Par_Share_t * pShare;
8484
} Par_ThData_t;
8585
static volatile Par_Share_t * g_pUfarShare = NULL;
86+
static inline void Cec_CopyGiaName( Gia_Man_t * pSrc, Gia_Man_t * pDst )
87+
{
88+
char * pName = pSrc->pName ? pSrc->pName : pSrc->pSpec;
89+
if ( pName == NULL )
90+
return;
91+
if ( pDst->pName == NULL )
92+
pDst->pName = Abc_UtilStrsav( pName );
93+
if ( pDst->pSpec == NULL )
94+
pDst->pSpec = Abc_UtilStrsav( pName );
95+
}
96+
static inline void Cec_CopyGiaNameToAig( Gia_Man_t * pGia, Aig_Man_t * pAig )
97+
{
98+
char * pName = pGia->pName ? pGia->pName : pGia->pSpec;
99+
if ( pName == NULL )
100+
return;
101+
if ( pAig->pName == NULL )
102+
pAig->pName = Abc_UtilStrsav( pName );
103+
if ( pAig->pSpec == NULL )
104+
pAig->pSpec = Abc_UtilStrsav( pName );
105+
}
86106
static int Cec_SProveStopUfar( int RunId )
87107
{
88108
(void)RunId;
@@ -161,6 +181,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
161181
pPars->pProgress = (void *)pThData;
162182
}
163183
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
184+
Cec_CopyGiaNameToAig( p, pAig );
164185
RetValue = Saig_ManBmcScalable( pAig, pPars );
165186
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
166187
Aig_ManStop( pAig );
@@ -177,6 +198,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
177198
pPars->pProgress = (void *)pThData;
178199
}
179200
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
201+
Cec_CopyGiaNameToAig( p, pAig );
180202
RetValue = Pdr_ManSolve( pAig, pPars );
181203
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
182204
Aig_ManStop( pAig );
@@ -194,6 +216,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
194216
pPars->pProgress = (void *)pThData;
195217
}
196218
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
219+
Cec_CopyGiaNameToAig( p, pAig );
197220
RetValue = Saig_ManBmcScalable( pAig, pPars );
198221
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
199222
Aig_ManStop( pAig );
@@ -211,6 +234,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
211234
pPars->pProgress = (void *)pThData;
212235
}
213236
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
237+
Cec_CopyGiaNameToAig( p, pAig );
214238
RetValue = Pdr_ManSolve( pAig, pPars );
215239
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
216240
Aig_ManStop( pAig );
@@ -313,6 +337,7 @@ void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int
313337
for ( i = 0; i < nWorkers; i++ )
314338
{
315339
ThData[i].p = Gia_ManDup(p);
340+
Cec_CopyGiaName( p, ThData[i].p );
316341
ThData[i].iEngine = (fUseUif && i == nWorkers - 1) ? PAR_ENGINE_UFAR : i;
317342
ThData[i].nTimeOut = nTimeOut;
318343
ThData[i].fWorking = 0;
@@ -414,7 +439,8 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
414439
}
415440
if ( !fSilent )
416441
{
417-
printf( "Problem \"%s\" is ", p->pSpec );
442+
char * pProbName = p->pSpec ? p->pSpec : Gia_ManName(p);
443+
printf( "Problem \"%s\" is ", pProbName ? pProbName : "(none)" );
418444
if ( RetValue == 0 )
419445
printf( "SATISFIABLE (solved by %d).", RetEngine );
420446
else if ( RetValue == 1 )

0 commit comments

Comments
 (0)