Updates to arithmetic verification.

8 files changed, 71 insertions, 47 deletions

diff --git a/src/proof/acec/acec.h b/src/proof/acec/acec.h
index 058e0f56..918119f8 100644
--- a/src/proof/acec/acec.h
+++ b/src/proof/acec/acec.h
@@ -76,6 +76,10 @@ extern Vec_Int_t *   Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVery
 extern Vec_Int_t *   Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t * vHadds, int fVerbose, int fVeryVerbose );
 /*=== acecPolyn.c ========================================================*/
 extern void          Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fSigned, int fVerbose, int fVeryVerbose );
+/*=== acecRe.c ========================================================*/
+extern Vec_Int_t *   Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose );
+extern int           Ree_ManCountFadds( Vec_Int_t * vAdds );
+extern void          Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose );
 
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/proof/acec/acecCl.c b/src/proof/acec/acecCl.c
index 63483d57..145f2e0b 100644
--- a/src/proof/acec/acecCl.c
+++ b/src/proof/acec/acecCl.c
@@ -306,18 +306,10 @@ Gia_Man_t * Acec_DetectXorBuildNew( Gia_Man_t * p, Vec_Int_t * vRootXorSet )
 ***********************************************************************/
 Gia_Man_t * Acec_DetectAdditional( Gia_Man_t * p, int fVerbose )
 {
-    extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose );
-    extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds );
-    extern void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds );
-    extern int Ree_ManCountFadds( Vec_Int_t * vAdds );
-    extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose );
-
     abctime clk = Abc_Clock();
     Gia_Man_t * pNew;
     Vec_Int_t * vRootXorSet;
 //    Vec_Int_t * vXors, * vAdds = Ree_ManComputeCuts( p, &vXors, 0 );
-//    Ree_ManRemoveTrivial( p, vAdds );
-//    Ree_ManRemoveContained( p, vAdds );
 
     //Ree_ManPrintAdders( vAdds, 1 );
 //    printf( "Detected %d full-adders and %d half-adders.  Found %d XOR-cuts.  ", Ree_ManCountFadds(vAdds), Vec_IntSize(vAdds)/6-Ree_ManCountFadds(vAdds), Vec_IntSize(vXors)/4 );
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
 
 
diff --git a/src/proof/acec/acecPa.c b/src/proof/acec/acecPa.c
index b59cdbef..6b382d91 100644
--- a/src/proof/acec/acecPa.c
+++ b/src/proof/acec/acecPa.c
@@ -248,11 +248,6 @@ int Pas_ManComputeCuts( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vOrder, Ve
 ***********************************************************************/
 void Pas_ManComputeCutsTest( Gia_Man_t * p )
 {
-    extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose );
-    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 int Ree_ManCountFadds( Vec_Int_t * vAdds );
-    extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose );
     abctime clk = Abc_Clock();
     Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, 1 );
     Vec_Int_t * vIns, * vOuts;
@@ -273,22 +268,6 @@ void Pas_ManComputeCutsTest( Gia_Man_t * p )
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 }
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p )
-{
-    return NULL;
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/acec/acecPool.c b/src/proof/acec/acecPool.c
index 08ee37f2..0868545e 100644
--- a/src/proof/acec/acecPool.c
+++ b/src/proof/acec/acecPool.c
@@ -303,17 +303,9 @@ void Acec_ManPrintRanks( Vec_Int_t * vPairs )
 ***********************************************************************/
 void Acec_ManProfile( Gia_Man_t * p, int fVerbose )
 {
-    extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose );
-    extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds );
-    extern void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds );
-    extern int Ree_ManCountFadds( Vec_Int_t * vAdds );
-    extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose );
-
     abctime clk = Abc_Clock();
     Vec_Wec_t * vBoxes; int i;
     Vec_Int_t * vXors, * vAdds = Ree_ManComputeCuts( p, &vXors, fVerbose );
-    Ree_ManRemoveTrivial( p, vAdds );
-    Ree_ManRemoveContained( p, vAdds );
 
     //Ree_ManPrintAdders( vAdds, 1 );
     printf( "Detected %d full-adders and %d half-adders.  Found %d XOR-cuts.  ", Ree_ManCountFadds(vAdds), Vec_IntSize(vAdds)/6-Ree_ManCountFadds(vAdds), Vec_IntSize(vXors)/4 );
@@ -396,13 +388,6 @@ Vec_Int_t * Acec_ManPoolTopMost( Gia_Man_t * p, Vec_Int_t * vAdds )
 }
 void Acec_ManPool( Gia_Man_t * p )
 {
-    extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose );
-    extern Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vRootBoxes );
-
-    extern int Ree_ManCountFadds( Vec_Int_t * vAdds );
-    extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose );
-    extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds );
-    extern void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds );
     Vec_Int_t * vTops, * vTree;
     Vec_Wec_t * vTrees;
 
@@ -413,8 +398,6 @@ void Acec_ManPool( Gia_Man_t * p )
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 
     clk = Abc_Clock();
-    Ree_ManRemoveTrivial( p, vAdds );
-    Ree_ManRemoveContained( p, vAdds );
     nFadds = Ree_ManCountFadds( vAdds );
     printf( "Detected %d FAs and %d HAs.  ", nFadds, Vec_IntSize(vAdds)/6-nFadds );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
diff --git a/src/proof/acec/acecRe.c b/src/proof/acec/acecRe.c
index 26faad00..60b894c8 100644
--- a/src/proof/acec/acecRe.c
+++ b/src/proof/acec/acecRe.c
@@ -392,6 +392,8 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData, int fVerbos
 }
 Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose )
 {
+    extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds );
+    extern void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds );
     Gia_Obj_t * pObj; 
     int * pList0, * pList1, i, nCuts = 0;
     Hash_IntMan_t * pHash = Hash_IntManStart( 1000 );
@@ -430,6 +432,8 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose
             Vec_IntSize(vAdds)/6, Vec_IntSize(vData)/3, Hash_IntManEntryNum(pHash), 6.0*Hash_IntManEntryNum(pHash)/Vec_IntSize(vAdds) );
     Vec_IntFree( vData );
     Hash_IntManStop( pHash );
+    Ree_ManRemoveTrivial( p, vAdds );
+    Ree_ManRemoveContained( p, vAdds );
     return vAdds;
 }
 
diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c
new file mode 100644
index 00000000..c2d89a1c
--- /dev/null
+++ b/src/proof/acec/acecTree.c
@@ -0,0 +1,56 @@
+/**CFile****************************************************************
+
+  FileName    [acecTree.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [CEC for arithmetic circuits.]
+
+  Synopsis    [Adder tree construction.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: acecTree.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p )
+{
+    return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/module.make b/src/proof/acec/module.make
index 4003695e..4db695c5 100644
--- a/src/proof/acec/module.make
+++ b/src/proof/acec/module.make
@@ -11,4 +11,5 @@ SRC +=    src/proof/acec/acecCl.c \
     src/proof/acec/acecOrder.c \
     src/proof/acec/acecPolyn.c \
     src/proof/acec/acecSt.c \
+    src/proof/acec/acecTree.c \
     src/proof/acec/acecUtil.c