diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-12 16:12:48 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-12 16:12:48 +0700 |
| commit | d52dafa6c2365837543f15be7abd274f8654ba14 (patch) | |
| tree | 6c67ad06aeab3bab1b95448be34a89d4aa0e92ce /src/proof/acec/acecInt.h | |
| parent | 55b6b4bdab816b34bfa81a58eb4e9fefe0c1cba4 (diff) | |
| download | abc-d52dafa6c2365837543f15be7abd274f8654ba14.tar.gz abc-d52dafa6c2365837543f15be7abd274f8654ba14.tar.bz2 abc-d52dafa6c2365837543f15be7abd274f8654ba14.zip | |
Updates to arithmetic verification.
Diffstat (limited to 'src/proof/acec/acecInt.h')
| -rw-r--r-- | src/proof/acec/acecInt.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h index c0d899e1..0dc3f706 100644 --- a/src/proof/acec/acecInt.h +++ b/src/proof/acec/acecInt.h @@ -70,6 +70,8 @@ struct Acec_Box_t_ /*=== acecCo.c ========================================================*/ extern Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vAddCos, Vec_Int_t ** pvIns, Vec_Int_t ** pvOuts ); 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 ); /*=== acecNorm.c ========================================================*/ extern Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll ); /*=== acecTree.c ========================================================*/ |