diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-19 13:24:47 +0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-19 13:24:47 +0800 |
| commit | b193ef056d2fb11d5e24b7e4f250e07d069c2ae2 (patch) | |
| tree | fb201b5a4f64e1f9400a2f50f8d3650dfe1062a6 /src/proof/acec/acecTree.c | |
| parent | 7457b8a64ae92880b8c04f1128298ee51becb76f (diff) | |
| download | abc-b193ef056d2fb11d5e24b7e4f250e07d069c2ae2.tar.gz abc-b193ef056d2fb11d5e24b7e4f250e07d069c2ae2.tar.bz2 abc-b193ef056d2fb11d5e24b7e4f250e07d069c2ae2.zip | |
Updates to arithmetic verification.
Diffstat (limited to 'src/proof/acec/acecTree.c')
| -rw-r--r-- | src/proof/acec/acecTree.c | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c index fe5ca01b..2461c89b 100644 --- a/src/proof/acec/acecTree.c +++ b/src/proof/acec/acecTree.c @@ -207,6 +207,9 @@ void Acec_TreeFilterOne2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree ) Gia_ManForEachAnd( p, pObj, i ) if ( Vec_BitEntry(vIsLeaf, i) ) Acec_TreeMarkTFI_rec( p, i, vMarked ); + // additional one +//if ( 10942 < Gia_ManObjNum(p) ) +// Acec_TreeMarkTFI_rec( p, 10942, vMarked ); // remove those that overlap with the marked TFI Vec_IntForEachEntryDouble( vTree, Box, Rank, i ) { @@ -419,7 +422,7 @@ Vec_Int_t * Acec_TreeFindPoints( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * v int i; for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ ) { - if ( vIgnore && (Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+3)) && Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+4))) ) + if ( vIgnore && (Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+3)) || Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+4))) ) continue; Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+0), i, 0 ); Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+1), i, 0 ); |