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/acecInt.h | |
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/acecInt.h')
-rw-r--r-- | src/proof/acec/acecInt.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h index 125d923f..cc5786bb 100644 --- a/src/proof/acec/acecInt.h +++ b/src/proof/acec/acecInt.h @@ -69,10 +69,11 @@ extern Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Ve extern Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vRootBoxes ); /*=== acecMult.c ========================================================*/ extern Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits ); +extern Vec_Bit_t * Acec_BoothFindPPG( Gia_Man_t * p ); /*=== acecNorm.c ========================================================*/ extern Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll ); /*=== acecTree.c ========================================================*/ -extern Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, int fVerbose ); +extern Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fVerbose ); extern void Acec_BoxFreeP( Acec_Box_t ** ppBox ); /*=== acecUtil.c ========================================================*/ extern void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose ); |