diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-09 09:47:48 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-09 09:47:48 -0800 |
| commit | b65ae7349af7de36390ec916701b997cac2a00ed (patch) | |
| tree | 47ce553bcffa963d3debafc0459701a9f6d5ecaa /src/base/abci/abcDar.c | |
| parent | 79aa1f00d6c00118442a240dab12d100e01fdd03 (diff) | |
| download | abc-b65ae7349af7de36390ec916701b997cac2a00ed.tar.gz abc-b65ae7349af7de36390ec916701b997cac2a00ed.tar.bz2 abc-b65ae7349af7de36390ec916701b997cac2a00ed.zip | |
Enabling multi-output solving in 'pdr'.
Diffstat (limited to 'src/base/abci/abcDar.c')
| -rw-r--r-- | src/base/abci/abcDar.c | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index cc703490..e427524a 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -2717,6 +2717,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) Abc_Print( 1, "Converting network into AIG has failed.\n" ); return -1; } +/* // perform ORing the primary outputs if ( pPars->iOutput == -1 ) { @@ -2728,6 +2729,9 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) } else RetValue = Pdr_ManSolve( pMan, pPars, ppCex ); +*/ + RetValue = Pdr_ManSolve( pMan, pPars, ppCex ); + // output the result if ( !pPars->fSilent ) { @@ -2739,7 +2743,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) Abc_Print( 1, "Property UNDECIDED. " ); else assert( 0 ); - ABC_PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); } if ( *ppCex && !Saig_ManVerifyCex( pMan, *ppCex ) ) |