diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-14 16:11:59 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-14 16:11:59 +0700 |
| commit | 79701f8b4603596095d3d04a13018c8e9598f7a0 (patch) | |
| tree | a8bf60919f71452cc9f59106a7d7f5191b49489c /src/proof/acec/acecNorm.c | |
| parent | 6d606b51ab084c96d92848be789397700bb3591f (diff) | |
| download | abc-79701f8b4603596095d3d04a13018c8e9598f7a0.tar.gz abc-79701f8b4603596095d3d04a13018c8e9598f7a0.tar.bz2 abc-79701f8b4603596095d3d04a13018c8e9598f7a0.zip | |
Updates to arithmetic verification.
Diffstat (limited to 'src/proof/acec/acecNorm.c')
| -rw-r--r-- | src/proof/acec/acecNorm.c | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/proof/acec/acecNorm.c b/src/proof/acec/acecNorm.c index 9faf7acf..4ed32e7b 100644 --- a/src/proof/acec/acecNorm.c +++ b/src/proof/acec/acecNorm.c @@ -198,11 +198,13 @@ Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Acec_Normalize( Gia_Man_t * pGia, int fVerbose ) +Gia_Man_t * Acec_Normalize( Gia_Man_t * pGia, int fBooth, int fVerbose ) { - Acec_Box_t * pBox = Acec_DeriveBox( pGia, fVerbose ); + Vec_Bit_t * vIgnore = fBooth ? Acec_BoothFindPPG( pGia ) : NULL; + Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, fVerbose ); Gia_Man_t * pNew = Acec_InsertBox( pBox, 1 ); Acec_BoxFreeP( &pBox ); + Vec_BitFreeP( &vIgnore ); return pNew; } |