diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-09 00:19:18 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-09 00:19:18 -0800 |
| commit | 0058cefee35e08eaa5740c0febf3829c89781a3c (patch) | |
| tree | 27ade1097da4221ecd9d6934f298d08199fc3133 /src/base | |
| parent | a68593c4f2b79b4adaf76dfe6b5dfc3bc63bb323 (diff) | |
| download | abc-0058cefee35e08eaa5740c0febf3829c89781a3c.tar.gz abc-0058cefee35e08eaa5740c0febf3829c89781a3c.tar.bz2 abc-0058cefee35e08eaa5740c0febf3829c89781a3c.zip | |
Deriving CEX after phase/tempor/reparam.
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abci/abc.c | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index e0bcb523..22e018ab 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -28953,6 +28953,7 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pAig; Vec_Ptr_t * vPosEquivs; +// Vec_Ptr_t * vPiPerms; int c, fDualOut = 0, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "dvh" ) ) != EOF ) @@ -28982,6 +28983,8 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, NULL, fDualOut, fVerbose ); +// pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, &vPiPerms, fDualOut, fVerbose ); +// Vec_VecFree( (Vec_Vec_t *)vPiPerms ); if ( pAig == NULL ) { Abc_Print( -1, "Abc_CommandAbc9Iso(): Transformation has failed.\n" ); @@ -30344,7 +30347,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern void Gia_IsoTest( Gia_Man_t * p, int fVerbose ); // extern void Ga2_ManComputeTest( Gia_Man_t * p ); // extern void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose ); - + extern void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) @@ -30390,6 +30393,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Gia_IsoTest( pAbc->pGia, fVerbose ); // Ga2_ManComputeTest( pAbc->pGia ); // Bmc_CexTest( pAbc->pGia, pAbc->pCex, fVerbose ); + Gia_IsoTest( pAbc->pGia, pAbc->pCex, 0 ); return 0; usage: Abc_Print( -2, "usage: &test [-svh]\n" ); |