summaryrefslogtreecommitdiffstats
path: root/src/proof/acec/acecInt.h
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-01-10 16:58:24 +0700
committerAlan Mishchenko <alanmi@berkeley.edu>2017-01-10 16:58:24 +0700
commit5fbc0cd7f09a382241266404d78c18c5443d2b9d (patch)
treecb6bdfcceb7414b8d2637724dfeac0ffc152eeff /src/proof/acec/acecInt.h
parentfbdf28e4c937067737d84db37ff6e1a65348df5f (diff)
downloadabc-5fbc0cd7f09a382241266404d78c18c5443d2b9d.tar.gz
abc-5fbc0cd7f09a382241266404d78c18c5443d2b9d.tar.bz2
abc-5fbc0cd7f09a382241266404d78c18c5443d2b9d.zip
Updates to arithmetic verification.
Diffstat (limited to 'src/proof/acec/acecInt.h')
-rw-r--r--src/proof/acec/acecInt.h7
1 files changed, 6 insertions, 1 deletions
diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h
index d53b61c7..065f6300 100644
--- a/src/proof/acec/acecInt.h
+++ b/src/proof/acec/acecInt.h
@@ -63,12 +63,17 @@ struct Acec_Box_t_
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-/*=== acecPa.c ========================================================*/
+/*=== 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 );
+/*=== acecTree.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 );
+
+
ABC_NAMESPACE_HEADER_END