diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-09 19:50:05 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-09 19:50:05 +0700 |
| commit | fbdf28e4c937067737d84db37ff6e1a65348df5f (patch) | |
| tree | 562036110ed054b87a7dd1729a0b5b6dc7ff182f /src/proof/acec/acecInt.h | |
| parent | ab6a87a4db2b2d9b188c09d9142b96503261e9ce (diff) | |
| download | abc-fbdf28e4c937067737d84db37ff6e1a65348df5f.tar.gz abc-fbdf28e4c937067737d84db37ff6e1a65348df5f.tar.bz2 abc-fbdf28e4c937067737d84db37ff6e1a65348df5f.zip | |
Updated to arithmetic verification.
Diffstat (limited to 'src/proof/acec/acecInt.h')
| -rw-r--r-- | src/proof/acec/acecInt.h | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h index e761e56e..d53b61c7 100644 --- a/src/proof/acec/acecInt.h +++ b/src/proof/acec/acecInt.h @@ -27,7 +27,6 @@ //////////////////////////////////////////////////////////////////////// #include "aig/gia/gia.h" -#include "proof/cec/cec.h" #include "acec.h" //////////////////////////////////////////////////////////////////////// @@ -38,6 +37,16 @@ ABC_NAMESPACE_HEADER_START +typedef struct Acec_Box_t_ Acec_Box_t; +struct Acec_Box_t_ +{ + Gia_Man_t * pGia; // AIG manager + Vec_Wec_t * vLeafLits; // leaf literals by rank + Vec_Wec_t * vRootLits; // root literals by rank + Vec_Wec_t * vShared; // shared leaves + Vec_Wec_t * vUnique; // unique leaves +}; + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// @@ -54,6 +63,8 @@ ABC_NAMESPACE_HEADER_START /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== acecPa.c ========================================================*/ +extern Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p ); /*=== acecUtil.c ========================================================*/ extern void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose ); extern Vec_Int_t * Gia_PolynCollectLastXor( Gia_Man_t * pGia, int fVerbose ); |