diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-10 16:58:24 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-10 16:58:24 +0700 |
| commit | 5fbc0cd7f09a382241266404d78c18c5443d2b9d (patch) | |
| tree | cb6bdfcceb7414b8d2637724dfeac0ffc152eeff /src/proof/acec/acecRe.c | |
| parent | fbdf28e4c937067737d84db37ff6e1a65348df5f (diff) | |
| download | abc-5fbc0cd7f09a382241266404d78c18c5443d2b9d.tar.gz abc-5fbc0cd7f09a382241266404d78c18c5443d2b9d.tar.bz2 abc-5fbc0cd7f09a382241266404d78c18c5443d2b9d.zip | |
Updates to arithmetic verification.
Diffstat (limited to 'src/proof/acec/acecRe.c')
| -rw-r--r-- | src/proof/acec/acecRe.c | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/proof/acec/acecRe.c b/src/proof/acec/acecRe.c index 26faad00..60b894c8 100644 --- a/src/proof/acec/acecRe.c +++ b/src/proof/acec/acecRe.c @@ -392,6 +392,8 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData, int fVerbos } Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose ) { + extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds ); + extern void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds ); Gia_Obj_t * pObj; int * pList0, * pList1, i, nCuts = 0; Hash_IntMan_t * pHash = Hash_IntManStart( 1000 ); @@ -430,6 +432,8 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose Vec_IntSize(vAdds)/6, Vec_IntSize(vData)/3, Hash_IntManEntryNum(pHash), 6.0*Hash_IntManEntryNum(pHash)/Vec_IntSize(vAdds) ); Vec_IntFree( vData ); Hash_IntManStop( pHash ); + Ree_ManRemoveTrivial( p, vAdds ); + Ree_ManRemoveContained( p, vAdds ); return vAdds; } |