diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-14 20:28:26 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-14 20:28:26 +0700 |
| commit | 1b86911c4fe0b193c3a281e823de7934664da798 (patch) | |
| tree | 44e3f3fe59361848443f9952b3247db0b94d80a6 /src/proof/acec/acecMult.c | |
| parent | 79701f8b4603596095d3d04a13018c8e9598f7a0 (diff) | |
| download | abc-1b86911c4fe0b193c3a281e823de7934664da798.tar.gz abc-1b86911c4fe0b193c3a281e823de7934664da798.tar.bz2 abc-1b86911c4fe0b193c3a281e823de7934664da798.zip | |
Updates to arithmetic verification.
Diffstat (limited to 'src/proof/acec/acecMult.c')
| -rw-r--r-- | src/proof/acec/acecMult.c | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/src/proof/acec/acecMult.c b/src/proof/acec/acecMult.c index 0733c00b..d868c399 100644 --- a/src/proof/acec/acecMult.c +++ b/src/proof/acec/acecMult.c @@ -504,14 +504,18 @@ Vec_Int_t * Acec_MultFindPPs( Gia_Man_t * p ) break; } } -/* - Extra_PrintHex( stdout, (unsigned*)&Truth, Vec_IntSize(vSupp) ); - if ( Vec_IntSize(vSupp) == 4 ) printf( " " ); - if ( Vec_IntSize(vSupp) == 3 ) printf( " " ); - if ( Vec_IntSize(vSupp) <= 2 ) printf( " " ); - printf( " " ); - Vec_IntPrint( vSupp ); -*/ + /* + if ( Saved[i] ) + { + printf( "Obj = %4d ", iObj ); + Extra_PrintHex( stdout, (unsigned*)&Truth, Vec_IntSize(vSupp) ); + if ( Vec_IntSize(vSupp) == 4 ) printf( " " ); + if ( Vec_IntSize(vSupp) == 3 ) printf( " " ); + if ( Vec_IntSize(vSupp) <= 2 ) printf( " " ); + printf( " " ); + Vec_IntPrint( vSupp ); + } + */ } Gia_ManCleanMark0(p); printf( "Collected %d pps and %d nodes.\n", nProds, Vec_IntSize(vBold) ); |