summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/acec/acecCl.c55
-rw-r--r--src/proof/acec/acecCo.c158
-rw-r--r--src/proof/acec/acecPa.c282
-rw-r--r--src/proof/acec/acecPolyn.c2
-rw-r--r--src/proof/acec/acecPool.c445
-rw-r--r--src/proof/acec/acecRe.c205
-rw-r--r--src/proof/acec/module.make5
7 files changed, 1078 insertions, 74 deletions
diff --git a/src/proof/acec/acecCl.c b/src/proof/acec/acecCl.c
new file mode 100644
index 00000000..32be3b30
--- /dev/null
+++ b/src/proof/acec/acecCl.c
@@ -0,0 +1,55 @@
+/**CFile****************************************************************
+
+ FileName [acecCl.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [CEC for arithmetic circuits.]
+
+ Synopsis [Core procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: acecCl.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+#include "misc/vec/vecWec.h"
+#include "misc/extra/extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecCo.c b/src/proof/acec/acecCo.c
index 000f530a..1e8ed7bb 100644
--- a/src/proof/acec/acecCo.c
+++ b/src/proof/acec/acecCo.c
@@ -44,11 +44,14 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
void Gia_PolynCoreNonXors_rec( Gia_Man_t * pGia, Gia_Obj_t * pObj, Vec_Int_t * vXorPairs )
{
+ extern int Gia_ManSuppSizeOne( Gia_Man_t * p, Gia_Obj_t * pObj );
Gia_Obj_t * pFan0, * pFan1;
if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
return;
Gia_PolynCoreNonXors_rec( pGia, Gia_Regular(pFan0), vXorPairs );
Gia_PolynCoreNonXors_rec( pGia, Gia_Regular(pFan1), vXorPairs );
+ //if ( Gia_ManSuppSizeOne(pGia, pObj) > 4 )
+ //if ( Gia_ObjId(pGia, pObj) >= 73 )
Vec_IntPushTwo( vXorPairs, Gia_ObjId(pGia, Gia_Regular(pFan0)), Gia_ObjId(pGia, Gia_Regular(pFan1)) );
}
Vec_Int_t * Gia_PolynAddHaRoots( Gia_Man_t * pGia )
@@ -87,38 +90,30 @@ Vec_Int_t * Gia_PolynAddHaRoots( Gia_Man_t * pGia )
SeeAlso []
***********************************************************************/
-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 )
+Vec_Wec_t * Gia_PolynComputeMap( Vec_Int_t * vAdds, int nObjs )
{
- Vec_Int_t * vOrder = Vec_IntAlloc( 1000 );
- Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(pGia) );
- Vec_Int_t * vRoots = Vec_IntAlloc( 5 * Gia_ManCoNum(pGia) );
- Vec_Int_t * vLeaves = Vec_IntAlloc( 2 * Gia_ManCiNum(pGia) );
- Vec_Wec_t * vMap = Vec_WecStart( Gia_ManObjNum(pGia) );
- int i, k, Index, Driver, Entry1, Entry2 = -1;
- // nodes driven by adders into adder indexes
- for ( i = 0; 5*i < Vec_IntSize(vAdds); i++ )
+ // map nodes driven by adders into adder indexes
+ Vec_Wec_t * vMap = Vec_WecStart( nObjs ); int i;
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
{
- Entry1 = Vec_IntEntry( vAdds, 5*i + 3 );
- Entry2 = Vec_IntEntry( vAdds, 5*i + 4 );
+ int Entry1 = Vec_IntEntry( vAdds, 6*i + 3 );
+ int Entry2 = Vec_IntEntry( vAdds, 6*i + 4 );
Vec_WecPush( vMap, Entry1, i );
Vec_WecPush( vMap, Entry1, Entry2 );
Vec_WecPush( vMap, Entry2, i );
Vec_WecPush( vMap, Entry2, Entry1 );
}
- // collect roots
- Gia_ManForEachCoDriverId( pGia, Driver, i )
- {
- Vec_IntPush( vRoots, Driver );
- Vec_BitWriteEntry( vIsRoot, Driver, 1 );
- }
- // collect additional outputs
- Vec_IntForEachEntry( vAddCos, Driver, i )
- {
- Vec_IntPush( vRoots, Driver );
+ return vMap;
+}
+Vec_Int_t * Gia_PolynCoreOrder_int( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Wec_t * vMap, Vec_Int_t * vRoots, Vec_Int_t ** pvIns )
+{
+ Vec_Int_t * vOrder = Vec_IntAlloc( 1000 );
+ Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(pGia) );
+ int i, k, Index, Driver, Entry1, Entry2 = -1;
+ // mark roots
+ Vec_IntForEachEntry( vRoots, Driver, i )
Vec_BitWriteEntry( vIsRoot, Driver, 1 );
- }
- // detect full adder tree
- *pvOuts = Vec_IntDup( vRoots );
+ // collect boxes
while ( 1 )
{
// iterate through boxes driving this one
@@ -140,9 +135,9 @@ Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t *
Vec_IntRemove( vRoots, Entry1 );
Vec_IntRemove( vRoots, Entry2 );
// set new marks
- Entry1 = Vec_IntEntry( vAdds, 5*Index + 0 );
- Entry2 = Vec_IntEntry( vAdds, 5*Index + 1 );
- Driver = Vec_IntEntry( vAdds, 5*Index + 2 );
+ Entry1 = Vec_IntEntry( vAdds, 6*Index + 0 );
+ Entry2 = Vec_IntEntry( vAdds, 6*Index + 1 );
+ Driver = Vec_IntEntry( vAdds, 6*Index + 2 );
Vec_BitWriteEntry( vIsRoot, Entry1, 1 );
Vec_BitWriteEntry( vIsRoot, Entry2, 1 );
Vec_BitWriteEntry( vIsRoot, Driver, 1 );
@@ -155,19 +150,99 @@ Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t *
break;
}
// collect remaining leaves
- Vec_BitForEachEntryStart( vIsRoot, Driver, i, 1 )
- if ( Driver )
- Vec_IntPush( vLeaves, i );
- *pvIns = vLeaves;
- // cleanup
+ if ( pvIns )
+ {
+ *pvIns = Vec_IntAlloc( Vec_BitSize(vIsRoot) );
+ Vec_BitForEachEntryStart( vIsRoot, Driver, i, 1 )
+ if ( Driver )
+ Vec_IntPush( *pvIns, i );
+ }
Vec_BitFree( vIsRoot );
+ return vOrder;
+}
+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 )
+{
+ Vec_Int_t * vOrder;
+ Vec_Wec_t * vMap = Gia_PolynComputeMap( vAdds, Gia_ManObjNum(pGia) );
+ Vec_Int_t * vRoots = Vec_IntAlloc( Gia_ManCoNum(pGia) );
+ int i, Driver;
+ // collect roots
+ Gia_ManForEachCoDriverId( pGia, Driver, i )
+ Vec_IntPush( vRoots, Driver );
+ // collect additional outputs
+ if ( vAddCos )
+ Vec_IntForEachEntry( vAddCos, Driver, i )
+ Vec_IntPush( vRoots, Driver );
+ // remember roots
+ if ( pvOuts )
+ *pvOuts = Vec_IntDup( vRoots );
+ // create order
+ vOrder = Gia_PolynCoreOrder_int( pGia, vAdds, vMap, vRoots, pvIns );
Vec_IntFree( vRoots );
Vec_WecFree( vMap );
+ printf( "Collected %d boxes.\n", Vec_IntSize(vOrder) );
return vOrder;
}
/**Function*************************************************************
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_PolyCollectRoots_rec( Vec_Int_t * vAdds, Vec_Wec_t * vMap, Vec_Bit_t * vMarks, int iBox, Vec_Int_t * vRoots )
+{
+ int k;
+ for ( k = 0; k < 3; k++ )
+ {
+ int i, Index, Sum, Carry = Vec_IntEntry( vAdds, 6*iBox+k );
+ Vec_Int_t * vLevel = Vec_WecEntry( vMap, Carry );
+ if ( Carry == 0 )
+ continue;
+ Vec_IntForEachEntryDouble( vLevel, Index, Sum, i )
+ if ( Vec_IntEntry(vAdds, 6*Index+4) == Carry && !Vec_BitEntry(vMarks, Sum) )
+ {
+ Vec_IntPush( vRoots, Sum );
+ Gia_PolyCollectRoots_rec( vAdds, vMap, vMarks, Index, vRoots );
+ }
+ }
+}
+void Gia_PolyCollectRoots( Vec_Int_t * vAdds, Vec_Wec_t * vMap, Vec_Bit_t * vMarks, int iBox, Vec_Int_t * vRoots )
+{
+ Vec_IntClear( vRoots );
+ Vec_IntPush( vRoots, Vec_IntEntry(vAdds, 6*iBox+3) );
+ Vec_IntPush( vRoots, Vec_IntEntry(vAdds, 6*iBox+4) );
+ Gia_PolyCollectRoots_rec( vAdds, vMap, vMarks, iBox, vRoots );
+}
+Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vRootBoxes )
+{
+ extern Vec_Bit_t * Acec_ManPoolGetPointed( Gia_Man_t * p, Vec_Int_t * vAdds );
+ Vec_Bit_t * vMarks = Acec_ManPoolGetPointed( pGia, vAdds );
+ Vec_Wec_t * vMap = Gia_PolynComputeMap( vAdds, Gia_ManObjNum(pGia) );
+ Vec_Wec_t * vRes = Vec_WecStart( Vec_IntSize(vRootBoxes) );
+ Vec_Int_t * vRoots = Vec_IntAlloc( 64 );
+ Vec_Int_t * vOrder;
+ int i, iBox;
+ Vec_IntForEachEntry( vRootBoxes, iBox, i )
+ {
+ Gia_PolyCollectRoots( vAdds, vMap, vMarks, iBox, vRoots );
+ vOrder = Gia_PolynCoreOrder_int( pGia, vAdds, vMap, vRoots, NULL );
+ Vec_IntAppend( Vec_WecEntry(vRes, i), vOrder );
+ Vec_IntFree( vOrder );
+ }
+ Vec_BitFree( vMarks );
+ Vec_IntFree( vRoots );
+ Vec_WecFree( vMap );
+ return vRes;
+}
+
+/**Function*************************************************************
+
Synopsis [Collect internal node order.]
Description []
@@ -194,15 +269,15 @@ Vec_Int_t * Gia_PolynCoreCollect( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t
Vec_IntForEachEntryReverse( vOrder, Index, i )
{
// mark inputs
- Entry1 = Vec_IntEntry( vAdds, 5*Index + 0 );
- Entry2 = Vec_IntEntry( vAdds, 5*Index + 1 );
- Entry3 = Vec_IntEntry( vAdds, 5*Index + 2 );
+ Entry1 = Vec_IntEntry( vAdds, 6*Index + 0 );
+ Entry2 = Vec_IntEntry( vAdds, 6*Index + 1 );
+ Entry3 = Vec_IntEntry( vAdds, 6*Index + 2 );
Vec_BitWriteEntry( vVisited, Entry1, 1 );
Vec_BitWriteEntry( vVisited, Entry2, 1 );
Vec_BitWriteEntry( vVisited, Entry3, 1 );
// traverse from outputs
- Entry1 = Vec_IntEntry( vAdds, 5*Index + 3 );
- Entry2 = Vec_IntEntry( vAdds, 5*Index + 4 );
+ Entry1 = Vec_IntEntry( vAdds, 6*Index + 3 );
+ Entry2 = Vec_IntEntry( vAdds, 6*Index + 4 );
Gia_PolynCoreCollect_rec( pGia, Entry1, vNodes, vVisited );
Gia_PolynCoreCollect_rec( pGia, Entry2, vNodes, vVisited );
}
@@ -312,14 +387,17 @@ Gia_Man_t * Gia_PolynCoreDupTree( Gia_Man_t * p, Vec_Int_t * vAddCos, Vec_Int_t
***********************************************************************/
Gia_Man_t * Gia_PolynCoreDetectTest_int( Gia_Man_t * pGia, Vec_Int_t * vAddCos, int fAddCones, int fVerbose )
{
- extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose );
+ extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose );
abctime clk = Abc_Clock();
Gia_Man_t * pNew;
- Vec_Int_t * vAdds = Ree_ManComputeCuts( pGia, 1 );
+ Vec_Int_t * vAdds = Ree_ManComputeCuts( pGia, NULL, 1 );
Vec_Int_t * vLeaves, * vRoots, * vOrder = Gia_PolynCoreOrder( pGia, vAdds, vAddCos, &vLeaves, &vRoots );
Vec_Int_t * vNodes = Gia_PolynCoreCollect( pGia, vAdds, vOrder );
+
+ //Gia_ManShow( pGia, vNodes, 0 );
+
printf( "Detected %d FAs/HAs. Roots = %d. Leaves = %d. Nodes = %d. Adds = %d. ",
- Vec_IntSize(vAdds), Vec_IntSize(vLeaves), Vec_IntSize(vRoots), Vec_IntSize(vNodes), Vec_IntSize(vOrder) );
+ Vec_IntSize(vAdds)/6, Vec_IntSize(vLeaves), Vec_IntSize(vRoots), Vec_IntSize(vNodes), Vec_IntSize(vOrder) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Gia_PolynCorePrintCones( pGia, vLeaves, fVerbose );
diff --git a/src/proof/acec/acecPa.c b/src/proof/acec/acecPa.c
new file mode 100644
index 00000000..ecaf2047
--- /dev/null
+++ b/src/proof/acec/acecPa.c
@@ -0,0 +1,282 @@
+/**CFile****************************************************************
+
+ FileName [acecPa.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [CEC for arithmetic circuits.]
+
+ Synopsis [Core procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: acecPa.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+#include "misc/vec/vecWec.h"
+#include "misc/extra/extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pas_ManVerifyPhaseOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ int Truth0, Truth1;
+ if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+ return pObj->Value;
+ Gia_ObjSetTravIdCurrent(p, pObj);
+ assert( Gia_ObjIsAnd(pObj) );
+ assert( !Gia_ObjIsXor(pObj) );
+ Truth0 = Pas_ManVerifyPhaseOne_rec( p, Gia_ObjFanin0(pObj) );
+ Truth1 = Pas_ManVerifyPhaseOne_rec( p, Gia_ObjFanin1(pObj) );
+ Truth0 = Gia_ObjFaninC0(pObj) ? 0xFF & ~Truth0 : Truth0;
+ Truth1 = Gia_ObjFaninC1(pObj) ? 0xFF & ~Truth1 : Truth1;
+ return (pObj->Value = Truth0 & Truth1);
+}
+void Pas_ManVerifyPhaseOne( Gia_Man_t * p, Vec_Int_t * vAdds, int iBox, Vec_Bit_t * vPhase )
+{
+ Gia_Obj_t * pObj;
+ unsigned TruthXor, TruthMaj, Truths[3] = { 0xAA, 0xCC, 0xF0 };
+ int k, iObj, fFadd = Vec_IntEntry(vAdds, 6*iBox+2) > 0;
+
+ if ( !fFadd )
+ return;
+
+ Gia_ManIncrementTravId( p );
+ for ( k = 0; k < 3; k++ )
+ {
+ iObj = Vec_IntEntry( vAdds, 6*iBox+k );
+ if ( iObj == 0 )
+ continue;
+ pObj = Gia_ManObj( p, iObj );
+ pObj->Value = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~Truths[k] : Truths[k];
+ Gia_ObjSetTravIdCurrent( p, pObj );
+ }
+
+ iObj = Vec_IntEntry( vAdds, 6*iBox+3 );
+ TruthXor = Pas_ManVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
+ TruthXor = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~TruthXor : TruthXor;
+
+ iObj = Vec_IntEntry( vAdds, 6*iBox+4 );
+ TruthMaj = Pas_ManVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
+ TruthMaj = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~TruthMaj : TruthMaj;
+
+ if ( fFadd ) // FADD
+ {
+ if ( TruthXor != 0x96 )
+ printf( "Fadd %d sum is wrong.\n", iBox );
+ if ( TruthMaj != 0xE8 )
+ printf( "Fadd %d carry is wrong.\n", iBox );
+ }
+ else
+ {
+ if ( TruthXor != 0x66 )
+ printf( "Hadd %d sum is wrong.\n", iBox );
+ if ( TruthMaj != 0x88 )
+ printf( "Hadd %d carry is wrong.\n", iBox );
+ }
+}
+void Pas_ManVerifyPhase( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vOrder, Vec_Bit_t * vPhase )
+{
+ int k, iBox;
+ Vec_IntForEachEntry( vOrder, iBox, k )
+ Pas_ManVerifyPhaseOne( p, vAdds, iBox, vPhase );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pas_ManPhase_rec( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, Gia_Obj_t * pObj, int fPhase, Vec_Bit_t * vPhase, Vec_Bit_t * vConstPhase )
+{
+ int k, iBox, iXor, Sign, fXorPhase;
+ assert( pObj != Gia_ManConst0(p) );
+ if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Gia_ObjSetTravIdCurrent(p, pObj);
+ if ( fPhase )
+ Vec_BitWriteEntry( vPhase, Gia_ObjId(p, pObj), fPhase );
+ if ( !Gia_ObjIsAnd(pObj) )
+ return;
+ iBox = Vec_IntEntry( vMap, Gia_ObjId(p, pObj) );
+ if ( iBox == -1 )
+ return;
+ iXor = Vec_IntEntry( vAdds, 6*iBox+3 );
+ Sign = Vec_IntEntry( vAdds, 6*iBox+5 );
+ fXorPhase = ((Sign >> 3) & 1);
+ // remember complemented HADD
+ if ( Vec_IntEntry(vAdds, 6*iBox+2) == 0 && fPhase )
+ Vec_BitWriteEntry( vConstPhase, iBox, 1 );
+ for ( k = 0; k < 3; k++ )
+ {
+ int iObj = Vec_IntEntry( vAdds, 6*iBox+k );
+ int fPhaseThis = ((Sign >> k) & 1) ^ fPhase;
+ fXorPhase ^= fPhaseThis;
+ if ( iObj == 0 )
+ continue;
+ Pas_ManPhase_rec( p, vAdds, vMap, Gia_ManObj(p, iObj), fPhaseThis, vPhase, vConstPhase );
+ }
+ Vec_BitWriteEntry( vPhase, iXor, fXorPhase );
+}
+Vec_Bit_t * Pas_ManPhase( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, Vec_Int_t * vRoots, Vec_Bit_t ** pvConstPhase )
+{
+ Vec_Bit_t * vPhase = Vec_BitStart( Vec_IntSize(vMap) );
+ Vec_Bit_t * vConstPhase = Vec_BitStart( Vec_IntSize(vAdds)/6 );
+ int i, iRoot;
+ Gia_ManIncrementTravId( p );
+ Vec_IntForEachEntry( vRoots, iRoot, i )
+ Pas_ManPhase_rec( p, vAdds, vMap, Gia_ManObj(p, iRoot), 1, vPhase, vConstPhase );
+ *pvConstPhase = vConstPhase;
+ return vPhase;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pas_ManComputeCuts( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vOrder, Vec_Int_t * vIns, Vec_Int_t * vOuts )
+{
+ Vec_Bit_t * vUnique = Vec_BitStart( Gia_ManObjNum(p) );
+ Vec_Bit_t * vUsed = Vec_BitStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
+ Vec_Int_t * vRoots = Vec_IntAlloc( 100 );
+ Vec_Bit_t * vPhase, * vConstPhase;
+ int i, k, Entry, nTrees;
+
+ // map carries into adder indexes and mark driven nodes
+ Vec_IntForEachEntry( vOrder, i, k )
+ {
+ int Carry = Vec_IntEntry(vAdds, 6*i+4);
+ if ( Vec_BitEntry(vUnique, Carry) )
+ printf( "Carry %d participates more than once.\n", Carry );
+ Vec_BitWriteEntry( vUnique, Carry, 1 );
+ Vec_IntWriteEntry( vMap, Carry, i );
+ // mark driven
+ Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+0), 1 );
+ Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+1), 1 );
+ Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+2), 1 );
+ }
+ // collect carries that do not drive other adders
+ for ( i = 0; i < Gia_ManObjNum(p); i++ )
+ if ( Vec_BitEntry(vUnique, i) && !Vec_BitEntry(vUsed, i) )
+ Vec_IntPush( vRoots, i );
+ nTrees = Vec_IntSize( vRoots );
+
+ Vec_IntPrint( vRoots );
+
+ // compute phases
+ if ( Vec_IntSize(vRoots) > 0 )
+ {
+ int nCompls = 0;
+
+ vPhase = Pas_ManPhase( p, vAdds, vMap, vRoots, &vConstPhase );
+ Pas_ManVerifyPhase( p, vAdds, vOrder, vPhase );
+
+ printf( "Outputs: " );
+ Vec_IntForEachEntry( vOuts, Entry, i )
+ printf( "%d(%d) ", Entry, Vec_BitEntry(vPhase, Entry) );
+ printf( "\n" );
+
+ printf( "Inputs: " );
+ Vec_IntForEachEntry( vIns, Entry, i )
+ {
+ printf( "%d(%d) ", Entry, Vec_BitEntry(vPhase, Entry) );
+ nCompls += Vec_BitEntry(vPhase, Entry);
+ }
+ printf( " Compl = %d\n", nCompls );
+
+ Vec_BitFreeP( &vPhase );
+ Vec_BitFreeP( &vConstPhase );
+ }
+
+ Vec_IntFree( vRoots );
+ Vec_IntFree( vMap );
+ Vec_BitFree( vUnique );
+ Vec_BitFree( vUsed );
+ return nTrees;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+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;
+ Vec_Int_t * vOrder = Gia_PolynCoreOrder( p, vAdds, NULL, &vIns, &vOuts );
+ int nTrees, nFadds = Ree_ManCountFadds( vAdds );
+ //Ree_ManPrintAdders( vAdds, 1 );
+ printf( "Detected %d FAs and %d HAs. Collected %d adders. ", nFadds, Vec_IntSize(vAdds)/6-nFadds, Vec_IntSize(vOrder) );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ // detect trees
+ clk = Abc_Clock();
+ nTrees = Pas_ManComputeCuts( p, vAdds, vOrder, vIns, vOuts );
+ Vec_IntFree( vAdds );
+ Vec_IntFree( vOrder );
+ Vec_IntFree( vIns );
+ Vec_IntFree( vOuts );
+
+ printf( "Detected %d adder trees. ", nTrees );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecPolyn.c b/src/proof/acec/acecPolyn.c
index 042e0c59..53ddf710 100644
--- a/src/proof/acec/acecPolyn.c
+++ b/src/proof/acec/acecPolyn.c
@@ -429,7 +429,7 @@ void Gia_PolynBuild2( Gia_Man_t * pGia, int fSigned, int fVerbose, int fVeryVerb
{
Hsh_VecMan_t * pHashC = Hsh_VecManStart( 1000 ); // hash table for constants
Hsh_VecMan_t * pHashM = Hsh_VecManStart( 1000 ); // hash table for monomials
- Vec_Wec_t * vLit2Mono = Vec_WecStart( Gia_ManObjNum(pGia) * 2 );
+ //Vec_Wec_t * vLit2Mono = Vec_WecStart( Gia_ManObjNum(pGia) * 2 );
Hsh_VecManStop( pHashC );
Hsh_VecManStop( pHashM );
diff --git a/src/proof/acec/acecPool.c b/src/proof/acec/acecPool.c
new file mode 100644
index 00000000..08ee37f2
--- /dev/null
+++ b/src/proof/acec/acecPool.c
@@ -0,0 +1,445 @@
+/**CFile****************************************************************
+
+ FileName [acecPool.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [CEC for arithmetic circuits.]
+
+ Synopsis [Core procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: acecPool.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+#include "misc/vec/vecWec.h"
+#include "misc/extra/extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Acec_ManCreateCarryMap( Gia_Man_t * p, Vec_Int_t * vAdds )
+{
+ // map carries into their boxes
+ Vec_Int_t * vCarryMap = Vec_IntStartFull( Gia_ManObjNum(p) ); int i;
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+ Vec_IntWriteEntry( vCarryMap, Vec_IntEntry(vAdds, 6*i+4), i );
+ return vCarryMap;
+}
+int Acec_ManCheckCarryMap( Gia_Man_t * p, int Carry, Vec_Int_t * vAdds, Vec_Int_t * vCarryMap )
+{
+ int iBox = Vec_IntEntry( vCarryMap, Carry );
+ assert( iBox >= 0 );
+ return Vec_IntEntry( vCarryMap, Vec_IntEntry(vAdds, 6*iBox+0) ) >= 0 ||
+ Vec_IntEntry( vCarryMap, Vec_IntEntry(vAdds, 6*iBox+1) ) >= 0 ||
+ Vec_IntEntry( vCarryMap, Vec_IntEntry(vAdds, 6*iBox+2) ) >= 0;
+}
+Vec_Int_t * Acec_ManCollectCarryRoots( Gia_Man_t * p, Vec_Int_t * vAdds )
+{
+ Vec_Int_t * vCarryRoots = Vec_IntAlloc( 100 );
+ Vec_Bit_t * vIns = Vec_BitStart( Gia_ManObjNum(p) ); int i;
+ // marks box inputs
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+ {
+ Vec_BitWriteEntry( vIns, Vec_IntEntry(vAdds, 6*i+0), 1 );
+ Vec_BitWriteEntry( vIns, Vec_IntEntry(vAdds, 6*i+1), 1 );
+ Vec_BitWriteEntry( vIns, Vec_IntEntry(vAdds, 6*i+2), 1 );
+ }
+ // collect roots
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+ if ( !Vec_BitEntry(vIns, Vec_IntEntry(vAdds, 6*i+4)) )
+ Vec_IntPush( vCarryRoots, Vec_IntEntry(vAdds, 6*i+4) );
+ Vec_BitFree( vIns );
+ return vCarryRoots;
+}
+Vec_Int_t * Acec_ManCollectXorRoots( Gia_Man_t * p, Vec_Int_t * vXors )
+{
+ Vec_Int_t * vXorRoots = Vec_IntAlloc( 100 );
+ Vec_Bit_t * vIns = Vec_BitStart( Gia_ManObjNum(p) ); int i;
+ // marks box inputs
+ for ( i = 0; 4*i < Vec_IntSize(vXors); i++ )
+ {
+ Vec_BitWriteEntry( vIns, Vec_IntEntry(vXors, 4*i+1), 1 );
+ Vec_BitWriteEntry( vIns, Vec_IntEntry(vXors, 4*i+2), 1 );
+ Vec_BitWriteEntry( vIns, Vec_IntEntry(vXors, 4*i+3), 1 );
+ }
+ // collect roots
+ for ( i = 0; 4*i < Vec_IntSize(vXors); i++ )
+ if ( !Vec_BitEntry(vIns, Vec_IntEntry(vXors, 4*i)) )
+ Vec_IntPush( vXorRoots, Vec_IntEntry(vXors, 4*i) );
+ Vec_BitFree( vIns );
+ return vXorRoots;
+}
+void Acec_ManCountXorTreeInputs_rec( Gia_Man_t * p, int Node, Vec_Int_t * vXors, Vec_Int_t * vXorMap, Vec_Bit_t * vIsCarryRoot, Vec_Int_t * vCarryRootSet, Vec_Int_t * vXorSet )
+{
+ int k, iXorBox;
+ if ( Node == 0 || Gia_ObjIsTravIdCurrentId(p, Node) )
+ return;
+ Gia_ObjSetTravIdCurrentId(p, Node);
+ iXorBox = Vec_IntEntry( vXorMap, Node );
+ if ( iXorBox == -1 )
+ {
+ if ( Vec_BitEntry(vIsCarryRoot, Node) )
+ Vec_IntPush( vCarryRootSet, Node );
+ return;
+ }
+ for ( k = 1; k < 4; k++ )
+ Acec_ManCountXorTreeInputs_rec( p, Vec_IntEntry(vXors, 4*iXorBox+k), vXors, vXorMap, vIsCarryRoot, vCarryRootSet, vXorSet );
+ Vec_IntPush( vXorSet, Vec_IntEntry(vXors, 4*iXorBox) );
+}
+Vec_Wec_t * Acec_ManCollectCarryRootSets( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vCarryMap, Vec_Int_t * vXors, Vec_Int_t * vXorRoots, Vec_Int_t * vCarryRoots )
+{
+ Vec_Wec_t * vCarryRootSets = Vec_WecAlloc( 100 ); // XorBoxes, CarryRoots, AdderBoxes, Ins/Ranks, Outs/Ranks
+ Vec_Int_t * vCarryRootSet = Vec_IntAlloc( 100 );
+ Vec_Bit_t * vIsCarryRoot = Vec_BitStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vXorSet = Vec_IntAlloc( 100 ), * vLevel;
+ int i, k, XorRoot, CarryRoot;
+ // map XORs into their cuts
+ Vec_Int_t * vXorMap = Vec_IntStartFull( Gia_ManObjNum(p) );
+ for ( i = 0; 4*i < Vec_IntSize(vXors); i++ )
+ Vec_IntWriteEntry( vXorMap, Vec_IntEntry(vXors, 4*i), i );
+ // create carry root marks
+ Vec_IntForEachEntry( vCarryRoots, CarryRoot, i )
+ Vec_BitWriteEntry( vIsCarryRoot, CarryRoot, 1 );
+ // collect carry roots attached to each XOR root
+ Vec_IntForEachEntry( vXorRoots, XorRoot, i )
+ {
+ Vec_IntClear( vXorSet );
+ Vec_IntClear( vCarryRootSet );
+ Gia_ManIncrementTravId( p );
+ Acec_ManCountXorTreeInputs_rec( p, XorRoot, vXors, vXorMap, vIsCarryRoot, vCarryRootSet, vXorSet );
+ // skip trivial
+ Vec_IntForEachEntry( vCarryRootSet, CarryRoot, k )
+ if ( Acec_ManCheckCarryMap(p, CarryRoot, vAdds, vCarryMap) )
+ break;
+ if ( k == Vec_IntSize(vCarryRootSet) )
+ continue;
+ Vec_IntSort( vCarryRootSet, 0 );
+ vLevel = Vec_WecPushLevel( vCarryRootSets );
+ Vec_IntAppend( vLevel, vXorSet );
+ vLevel = Vec_WecPushLevel( vCarryRootSets );
+ Vec_IntAppend( vLevel, vCarryRootSet );
+ vLevel = Vec_WecPushLevel( vCarryRootSets );
+ vLevel = Vec_WecPushLevel( vCarryRootSets );
+ vLevel = Vec_WecPushLevel( vCarryRootSets );
+ // unmark carry root set
+ Vec_IntForEachEntry( vCarryRootSet, CarryRoot, k )
+ {
+ assert( Vec_BitEntry(vIsCarryRoot, CarryRoot) );
+ Vec_BitWriteEntry( vIsCarryRoot, CarryRoot, 0 );
+ }
+ }
+ Vec_IntFree( vCarryRootSet );
+ Vec_IntFree( vXorSet );
+ Vec_IntFree( vXorMap );
+ // collect unmarked carry roots
+ Vec_IntForEachEntry( vCarryRoots, CarryRoot, k )
+ {
+ if ( !Vec_BitEntry(vIsCarryRoot, CarryRoot) )
+ continue;
+ if ( !Acec_ManCheckCarryMap(p, CarryRoot, vAdds, vCarryMap) )
+ continue;
+ vLevel = Vec_WecPushLevel( vCarryRootSets );
+ vLevel = Vec_WecPushLevel( vCarryRootSets );
+ Vec_IntFill( vLevel, 1, CarryRoot );
+ vLevel = Vec_WecPushLevel( vCarryRootSets );
+ vLevel = Vec_WecPushLevel( vCarryRootSets );
+ vLevel = Vec_WecPushLevel( vCarryRootSets );
+ }
+ Vec_BitFree( vIsCarryRoot );
+ return vCarryRootSets;
+}
+int Acec_ManCompareTwo( int * pPair0, int * pPair1 )
+{
+ if ( pPair0[1] < pPair1[1] ) return -1;
+ if ( pPair0[1] > pPair1[1] ) return 1;
+ return 0;
+}
+void Acec_ManCollectInsOuts( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vBoxes, Vec_Int_t * vBoxRanks, Vec_Bit_t * vBoxIns, Vec_Bit_t * vBoxOuts, Vec_Int_t * vResIns, Vec_Int_t * vResOuts )
+{
+ int i, k, iBox, iObj, Rank, RankMax = 0;
+ // mark box inputs/outputs
+ Vec_IntForEachEntry( vBoxes, iBox, i )
+ {
+ Vec_BitWriteEntry( vBoxIns, Vec_IntEntry(vAdds, 6*iBox+0), 1 );
+ Vec_BitWriteEntry( vBoxIns, Vec_IntEntry(vAdds, 6*iBox+1), 1 );
+ Vec_BitWriteEntry( vBoxIns, Vec_IntEntry(vAdds, 6*iBox+2), 1 );
+ Vec_BitWriteEntry( vBoxOuts, Vec_IntEntry(vAdds, 6*iBox+3), 1 );
+ Vec_BitWriteEntry( vBoxOuts, Vec_IntEntry(vAdds, 6*iBox+4), 1 );
+ }
+ // collect unmarked inputs/output and their ranks
+ Vec_IntForEachEntry( vBoxes, iBox, i )
+ {
+ for ( k = 0; k < 3; k++ )
+ if ( !Vec_BitEntry(vBoxOuts, Vec_IntEntry(vAdds, 6*iBox+k)) )
+ Vec_IntPushTwo( vResIns, Vec_IntEntry(vAdds, 6*iBox+k), Vec_IntEntry(vBoxRanks, iBox) );
+ for ( k = 3; k < 5; k++ )
+ if ( Vec_IntEntry(vAdds, 6*iBox+k) && !Vec_BitEntry(vBoxIns, Vec_IntEntry(vAdds, 6*iBox+k)) )
+ Vec_IntPushTwo( vResOuts, Vec_IntEntry(vAdds, 6*iBox+k), Vec_IntEntry(vBoxRanks, iBox)-(int)(k==4) );
+ }
+ // unmark box inputs/outputs
+ Vec_IntForEachEntry( vBoxes, iBox, i )
+ {
+ Vec_BitWriteEntry( vBoxIns, Vec_IntEntry(vAdds, 6*iBox+0), 0 );
+ Vec_BitWriteEntry( vBoxIns, Vec_IntEntry(vAdds, 6*iBox+1), 0 );
+ Vec_BitWriteEntry( vBoxIns, Vec_IntEntry(vAdds, 6*iBox+2), 0 );
+ Vec_BitWriteEntry( vBoxOuts, Vec_IntEntry(vAdds, 6*iBox+3), 0 );
+ Vec_BitWriteEntry( vBoxOuts, Vec_IntEntry(vAdds, 6*iBox+4), 0 );
+ }
+ // normalize ranks
+ Vec_IntForEachEntryDouble( vResIns, iObj, Rank, k )
+ RankMax = Abc_MaxInt( RankMax, Rank );
+ Vec_IntForEachEntryDouble( vResOuts, iObj, Rank, k )
+ RankMax = Abc_MaxInt( RankMax, Rank );
+ Vec_IntForEachEntryDouble( vResIns, iObj, Rank, k )
+ Vec_IntWriteEntry( vResIns, k+1, 1 + RankMax - Rank );
+ Vec_IntForEachEntryDouble( vResOuts, iObj, Rank, k )
+ Vec_IntWriteEntry( vResOuts, k+1, 1 + RankMax - Rank );
+ // sort by rank
+ qsort( Vec_IntArray(vResIns), Vec_IntSize(vResIns)/2, 8, (int (*)(const void *, const void *))Acec_ManCompareTwo );
+ qsort( Vec_IntArray(vResOuts), Vec_IntSize(vResOuts)/2, 8, (int (*)(const void *, const void *))Acec_ManCompareTwo );
+}
+void Acec_ManCollectBoxSets_rec( Gia_Man_t * p, int Carry, int iRank, Vec_Int_t * vAdds, Vec_Int_t * vCarryMap, Vec_Int_t * vBoxes, Vec_Int_t * vBoxRanks )
+{
+ int iBox = Vec_IntEntry( vCarryMap, Carry );
+ if ( iBox == -1 )
+ return;
+ Acec_ManCollectBoxSets_rec( p, Vec_IntEntry(vAdds, 6*iBox+0), iRank+1, vAdds, vCarryMap, vBoxes, vBoxRanks );
+ Acec_ManCollectBoxSets_rec( p, Vec_IntEntry(vAdds, 6*iBox+1), iRank+1, vAdds, vCarryMap, vBoxes, vBoxRanks );
+ if ( Vec_IntEntry(vAdds, 6*iBox+2) )
+ Acec_ManCollectBoxSets_rec( p, Vec_IntEntry(vAdds, 6*iBox+2), iRank+1, vAdds, vCarryMap, vBoxes, vBoxRanks );
+ Vec_IntPush( vBoxes, iBox );
+ Vec_IntWriteEntry( vBoxRanks, iBox, iRank );
+}
+Vec_Wec_t * Acec_ManCollectBoxSets( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vXors )
+{
+ Vec_Int_t * vCarryMap = Acec_ManCreateCarryMap( p, vAdds );
+ Vec_Int_t * vCarryRoots = Acec_ManCollectCarryRoots( p, vAdds );
+ Vec_Int_t * vXorRoots = Acec_ManCollectXorRoots( p, vXors );
+ Vec_Wec_t * vBoxSets = Acec_ManCollectCarryRootSets( p, vAdds, vCarryMap, vXors, vXorRoots, vCarryRoots );
+ Vec_Int_t * vBoxRanks = Vec_IntStart( Vec_IntSize(vAdds)/6 );
+ Vec_Bit_t * vBoxIns = Vec_BitStart( Gia_ManObjNum(p) );
+ Vec_Bit_t * vBoxOuts = Vec_BitStart( Gia_ManObjNum(p) ); int i, k, Root;
+ Vec_IntFree( vCarryRoots );
+ Vec_IntFree( vXorRoots );
+ // collect boxes for each carry set
+ assert( Vec_WecSize(vBoxSets) % 5 == 0 );
+ for ( i = 0; 5*i < Vec_WecSize(vBoxSets); i++ )
+ {
+ Vec_Int_t * vRoots = Vec_WecEntry( vBoxSets, 5*i+1 );
+ Vec_Int_t * vBoxes = Vec_WecEntry( vBoxSets, 5*i+2 );
+ Vec_Int_t * vIns = Vec_WecEntry( vBoxSets, 5*i+3 );
+ Vec_Int_t * vOuts = Vec_WecEntry( vBoxSets, 5*i+4 );
+ Vec_IntForEachEntry( vRoots, Root, k )
+ Acec_ManCollectBoxSets_rec( p, Root, 1, vAdds, vCarryMap, vBoxes, vBoxRanks );
+ Acec_ManCollectInsOuts( p, vAdds, vBoxes, vBoxRanks, vBoxIns, vBoxOuts, vIns, vOuts );
+ }
+ Vec_IntFree( vBoxRanks );
+ Vec_BitFree( vBoxIns );
+ Vec_BitFree( vBoxOuts );
+ Vec_IntFree( vCarryMap );
+ return vBoxSets;
+}
+void Acec_ManPrintRanks2( Vec_Int_t * vPairs )
+{
+ int k, iObj, Rank;
+ Vec_IntForEachEntryDouble( vPairs, iObj, Rank, k )
+ printf( "%d ", Rank );
+ printf( "\n" );
+}
+void Acec_ManPrintRanks( Vec_Int_t * vPairs )
+{
+ int k, iObj, Count, Rank, RankMax = 0;
+ Vec_Int_t * vCounts = Vec_IntStart( 100 );
+ Vec_IntForEachEntryDouble( vPairs, iObj, Rank, k )
+ {
+ Vec_IntFillExtra( vCounts, Rank+1, 0 );
+ Vec_IntAddToEntry( vCounts, Rank, 1 );
+ RankMax = Abc_MaxInt( RankMax, Rank );
+ }
+ Vec_IntForEachEntryStartStop( vCounts, Count, Rank, 1, RankMax+1 )
+ printf( "%2d=%2d ", Rank, Count );
+ printf( "\n" );
+ Vec_IntFree( vCounts );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+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 );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+
+ clk = Abc_Clock();
+ vBoxes = Acec_ManCollectBoxSets( p, vAdds, vXors );
+ printf( "Detected %d adder-tree%s. ", Vec_WecSize(vBoxes)/5, Vec_WecSize(vBoxes)/5 > 1 ? "s":"" );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+
+ if ( fVerbose )
+ for ( i = 0; 5*i < Vec_WecSize(vBoxes); i++ )
+ {
+ printf( "Tree %3d : ", i );
+ printf( "Xor = %4d ", Vec_IntSize(Vec_WecEntry(vBoxes,5*i+0)) );
+ printf( "Root = %4d ", Vec_IntSize(Vec_WecEntry(vBoxes,5*i+1)) );
+ //printf( "(Top = %5d) ", Vec_IntEntryLast(Vec_WecEntry(vBoxes,5*i+1)) );
+ printf( "Adder = %4d ", Vec_IntSize(Vec_WecEntry(vBoxes,5*i+2)) );
+ printf( "In = %4d ", Vec_IntSize(Vec_WecEntry(vBoxes,5*i+3))/2 );
+ printf( "Out = %4d ", Vec_IntSize(Vec_WecEntry(vBoxes,5*i+4))/2 );
+ printf( "\n" );
+ printf( " Ins: " );
+ Acec_ManPrintRanks( Vec_WecEntry(vBoxes,5*i+3) );
+ printf( " Outs: " );
+ Acec_ManPrintRanks( Vec_WecEntry(vBoxes,5*i+4) );
+ }
+
+ Vec_IntFree( vXors );
+ Vec_IntFree( vAdds );
+ Vec_WecFree( vBoxes );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Bit_t * Acec_ManPoolGetPointed( Gia_Man_t * p, Vec_Int_t * vAdds )
+{
+ Vec_Bit_t * vMarks = Vec_BitStart( Gia_ManObjNum(p) );
+ int i, k;
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+ for ( k = 0; k < 3; k++ )
+ Vec_BitWriteEntry( vMarks, Vec_IntEntry(vAdds, 6*i+k), 1 );
+ return vMarks;
+}
+
+Vec_Int_t * Acec_ManPoolTopMost( Gia_Man_t * p, Vec_Int_t * vAdds )
+{
+ int i, k, iTop, fVerbose = 0;
+ Vec_Int_t * vTops = Vec_IntAlloc( 1000 );
+ Vec_Bit_t * vMarks = Acec_ManPoolGetPointed( p, vAdds );
+
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+ if ( !Vec_BitEntry(vMarks, Vec_IntEntry(vAdds, 6*i+3)) &&
+ !Vec_BitEntry(vMarks, Vec_IntEntry(vAdds, 6*i+4)) )
+ Vec_IntPush( vTops, i );
+
+ if ( fVerbose )
+ Vec_IntForEachEntry( vTops, iTop, i )
+ {
+ printf( "%4d : ", iTop );
+ for ( k = 0; k < 3; k++ )
+ printf( "%4d ", Vec_IntEntry(vAdds, 6*iTop+k) );
+ printf( " -> " );
+ for ( k = 3; k < 5; k++ )
+ printf( "%4d ", Vec_IntEntry(vAdds, 6*iTop+k) );
+ printf( "\n" );
+ }
+
+ Vec_BitFree( vMarks );
+ return vTops;
+}
+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;
+
+ abctime clk = Abc_Clock();
+ Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, 1 );
+ int i, nFadds = Ree_ManCountFadds( vAdds );
+ printf( "Detected %d FAs and %d HAs. ", nFadds, Vec_IntSize(vAdds)/6-nFadds );
+ 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 );
+
+ //Ree_ManPrintAdders( vAdds, 1 );
+
+ // detect topmost nodes
+ vTops = Acec_ManPoolTopMost( p, vAdds );
+ printf( "Detected %d topmost adder%s.\n", Vec_IntSize(vTops), Vec_IntSize(vTops) > 1 ? "s":"" );
+
+ // collect adder trees
+ vTrees = Gia_PolynCoreOrderArray( p, vAdds, vTops );
+ Vec_WecForEachLevel( vTrees, vTree, i )
+ printf( "Adder %5d : Tree with %5d nodes.\n", Vec_IntEntry(vTops, i), Vec_IntSize(vTree) );
+
+ Vec_WecFree( vTrees );
+ Vec_IntFree( vAdds );
+ Vec_IntFree( vTops );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecRe.c b/src/proof/acec/acecRe.c
index 1f10d249..26faad00 100644
--- a/src/proof/acec/acecRe.c
+++ b/src/proof/acec/acecRe.c
@@ -69,6 +69,18 @@ void Ree_TruthPrecompute()
}
printf( "\n" );
}
+void Ree_TruthPrecompute2()
+{
+ int i, b;
+ for ( i = 0; i < 8; i++ )
+ {
+ word Truth = 0xE8;
+ for ( b = 0; b < 3; b++ )
+ if ( (i >> b) & 1 )
+ Truth = Abc_Tt6Flip( Truth, b );
+ printf( "%d = %X\n", i, 0xFF & (int)Truth );
+ }
+}
/**Function*************************************************************
@@ -236,10 +248,11 @@ void Ree_ManCutPrint( int * pCut, int Count, word Truth )
Abc_TtPrintHexRev( stdout, &Truth, 3 );
printf( "\n" );
}
-void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_Int_t * vCuts, Hash_IntMan_t * pHash, Vec_Int_t * vData )
+void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_Int_t * vCuts, Hash_IntMan_t * pHash, Vec_Int_t * vData, Vec_Int_t * vXors )
{
int fVerbose = 0;
- int i, k, c, Value, Truth, TruthC, * pCut0, * pCut1, pCut[5], Count = 0;
+ int i, k, c, Value, Truth, TruthC, * pCut0, * pCut1, pCut[6], Count = 0;
+ int iXor2 = -1, iXor3 = -1;
if ( fVerbose )
printf( "Object %d\n", iObj );
Vec_IntFill( vCuts, 2, 1 );
@@ -254,12 +267,16 @@ void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
continue;
Truth = TruthC = Ree_ManCutTruth(Gia_ManObj(p, iObj), pCut0, pCut1, pCut);
//assert( Truth == Ree_ObjComputeTruth(p, iObj, pCut) );
+ if ( Truth & 0x80 )
+ Truth = 0xFF & ~Truth;
+ if ( Truth == 0x66 && iXor2 == -1 )
+ iXor2 = Vec_IntSize(vCuts);
+ else if ( Truth == 0x69 && iXor3 == -1 )
+ iXor3 = Vec_IntSize(vCuts);
Vec_IntAddToEntry( vCuts, 0, 1 );
for ( c = 0; c <= pCut[0]; c++ )
Vec_IntPush( vCuts, pCut[c] );
- Vec_IntPush( vCuts, Truth );
- if ( Truth & 0x80 )
- Truth = 0xFF & ~Truth;
+ Vec_IntPush( vCuts, TruthC );
if ( (Truth == 0x66 || Truth == 0x11 || Truth == 0x22 || Truth == 0x44 || Truth == 0x77) && pCut[0] == 2 )
{
assert( pCut[0] == 2 );
@@ -275,6 +292,19 @@ void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
if ( fVerbose )
Ree_ManCutPrint( pCut, ++Count, TruthC );
}
+ if ( !vXors )
+ return;
+ if ( iXor2 > 0 )
+ pCut0 = Vec_IntEntryP( vCuts, iXor2 );
+ else if ( iXor3 > 0 )
+ pCut0 = Vec_IntEntryP( vCuts, iXor3 );
+ else
+ return;
+ Vec_IntPush( vXors, iObj );
+ for ( c = 1; c <= pCut0[0]; c++ )
+ Vec_IntPush( vXors, pCut0[c] );
+ if ( pCut0[0] == 2 )
+ Vec_IntPush( vXors, 0 );
}
/**Function*************************************************************
@@ -288,9 +318,9 @@ void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
SeeAlso []
***********************************************************************/
-Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData )
+Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData, int fVerbose )
{
- int i, j, k, iObj, iObj2, Value, Truth, CountX, CountM, Index = 0;
+ int i, j, k, iObj, iObj2, Value, Truth, Truth2, CountX, CountM, Index = 0;
int nEntries = Hash_IntManEntryNum(p);
Vec_Int_t * vAdds = Vec_IntAlloc( 1000 );
Vec_Int_t * vXors = Vec_IntStart( nEntries + 1 );
@@ -315,7 +345,8 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData )
}
Vec_IntFree( vXors );
Vec_IntFree( vMajs );
- printf( "Detected %d shared cuts among %d hashed cuts.\n", Index, nEntries );
+ //if ( fVerbose )
+ // printf( "Detected %d shared cuts among %d hashed cuts.\n", Index, nEntries );
// collect nodes
vXorMap = Vec_WecStart( Index );
vMajMap = Vec_WecStart( Index );
@@ -325,9 +356,9 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData )
if ( Index == -1 )
continue;
if ( Truth == 0x66 || Truth == 0x99 || Truth == 0x69 || Truth == 0x96 )
- Vec_WecPush( vXorMap, Index, iObj );
+ Vec_IntPushTwo( Vec_WecEntry(vXorMap, Index), iObj, Truth );
else
- Vec_WecPush( vMajMap, Index, iObj );
+ Vec_IntPushTwo( Vec_WecEntry(vMajMap, Index), iObj, Truth );
}
Vec_IntFree( vIndex );
// create pairs
@@ -336,11 +367,22 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData )
Vec_Int_t * vXorOne = Vec_WecEntry( vXorMap, i );
Vec_Int_t * vMajOne = Vec_WecEntry( vMajMap, i );
Hash_IntObj_t * pObj = Hash_IntObj( p, Value );
- Vec_IntForEachEntry( vXorOne, iObj, j )
- Vec_IntForEachEntry( vMajOne, iObj2, k )
+ Vec_IntForEachEntryDouble( vXorOne, iObj, Truth, j )
+ Vec_IntForEachEntryDouble( vMajOne, iObj2, Truth2, k )
{
+ int SignAnd[8] = {0x88, 0x44, 0x22, 0x11, 0xEE, 0xDD, 0xBB, 0x77};
+ int SignMaj[8] = {0xE8, 0xD4, 0xB2, 0x71, 0x8E, 0x4D, 0x2B, 0x17};
+ int n, SignXor = (Truth == 0x99 || Truth == 0x69) << 3;
+ for ( n = 0; n < 8; n++ )
+ if ( Truth2 == SignMaj[n] )
+ break;
+ if ( n == 8 )
+ for ( n = 0; n < 8; n++ )
+ if ( Truth2 == SignAnd[n] )
+ break;
+ assert( n < 8 );
Vec_IntPushThree( vAdds, pObj->iData0, pObj->iData1, pObj->iData2 );
- Vec_IntPushTwo( vAdds, iObj, iObj2 );
+ Vec_IntPushThree( vAdds, iObj, iObj2, SignXor | n );
}
}
Vec_IntFree( vIndexRev );
@@ -348,7 +390,7 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData )
Vec_WecFree( vMajMap );
return vAdds;
}
-Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose )
+Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose )
{
Gia_Obj_t * pObj;
int * pList0, * pList1, i, nCuts = 0;
@@ -367,24 +409,25 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose )
Vec_IntPush( vCuts, Gia_ObjId(p, pObj) );
Vec_IntPush( vCuts, 0xAA );
}
+ if ( pvXors ) *pvXors = Vec_IntAlloc( 1000 );
Gia_ManForEachAnd( p, pObj, i )
{
pList0 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId0(pObj, i)) );
pList1 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId1(pObj, i)) );
- Ree_ManCutMerge( p, i, pList0, pList1, vTemp, pHash, vData );
+ Ree_ManCutMerge( p, i, pList0, pList1, vTemp, pHash, vData, pvXors ? *pvXors : NULL );
Vec_IntWriteEntry( vCuts, i, Vec_IntSize(vCuts) );
Vec_IntAppend( vCuts, vTemp );
nCuts += Vec_IntEntry( vTemp, 0 );
}
if ( fVerbose )
- printf( "Nodes = %d. Cuts = %d. Cuts/Node = %.2f. Ints/Node = %.2f.\n",
+ printf( "AIG nodes = %d. Cuts = %d. Cuts/Node = %.2f. Ints/Node = %.2f.\n",
Gia_ManAndNum(p), nCuts, 1.0*nCuts/Gia_ManAndNum(p), 1.0*Vec_IntSize(vCuts)/Gia_ManAndNum(p) );
Vec_IntFree( vTemp );
Vec_IntFree( vCuts );
- vAdds = Ree_ManDeriveAdds( pHash, vData );
+ vAdds = Ree_ManDeriveAdds( pHash, vData, fVerbose );
if ( fVerbose )
- printf( "Adds = %d. Total = %d. Hashed = %d. Hashed/Adds = %.2f.\n",
- Vec_IntSize(vAdds)/5, Vec_IntSize(vData)/3, Hash_IntManEntryNum(pHash), 5.0*Hash_IntManEntryNum(pHash)/Vec_IntSize(vAdds) );
+ printf( "Adders = %d. Total cuts = %d. Hashed cuts = %d. Hashed/Adders = %.2f.\n",
+ 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 );
return vAdds;
@@ -392,6 +435,52 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose )
/**Function*************************************************************
+ Synopsis [Highlight nodes inside FAs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ree_CollectInsiders_rec( Gia_Man_t * pGia, int iObj, Vec_Bit_t * vVisited, Vec_Bit_t * vInsiders )
+{
+ if ( Vec_BitEntry(vVisited, iObj) )
+ return;
+ Vec_BitSetEntry( vVisited, iObj, 1 );
+ Ree_CollectInsiders_rec( pGia, Gia_ObjFaninId0p(pGia, Gia_ManObj(pGia, iObj)), vVisited, vInsiders );
+ Ree_CollectInsiders_rec( pGia, Gia_ObjFaninId1p(pGia, Gia_ManObj(pGia, iObj)), vVisited, vInsiders );
+ Vec_BitSetEntry( vInsiders, iObj, 1 );
+}
+Vec_Bit_t * Ree_CollectInsiders( Gia_Man_t * pGia, Vec_Int_t * vAdds )
+{
+ Vec_Bit_t * vVisited = Vec_BitStart( Gia_ManObjNum(pGia) );
+ Vec_Bit_t * vInsiders = Vec_BitStart( Gia_ManObjNum(pGia) );
+ int i, Entry1, Entry2, Entry3;
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+ {
+ if ( Vec_IntEntry(vAdds, 6*i+2) == 0 ) // HADD
+ continue;
+ // mark inputs
+ Entry1 = Vec_IntEntry( vAdds, 6*i + 0 );
+ Entry2 = Vec_IntEntry( vAdds, 6*i + 1 );
+ Entry3 = Vec_IntEntry( vAdds, 6*i + 2 );
+ Vec_BitWriteEntry( vVisited, Entry1, 1 );
+ Vec_BitWriteEntry( vVisited, Entry2, 1 );
+ Vec_BitWriteEntry( vVisited, Entry3, 1 );
+ // traverse from outputs
+ Entry1 = Vec_IntEntry( vAdds, 6*i + 3 );
+ Entry2 = Vec_IntEntry( vAdds, 6*i + 4 );
+ Ree_CollectInsiders_rec( pGia, Entry1, vVisited, vInsiders );
+ Ree_CollectInsiders_rec( pGia, Entry2, vVisited, vInsiders );
+ }
+ Vec_BitFree( vVisited );
+ return vInsiders;
+}
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -401,28 +490,80 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose )
SeeAlso []
***********************************************************************/
-void Ree_ManComputeCutsTest( Gia_Man_t * p )
+// removes HAs whose AND2 is part of XOR2 without additional fanout
+void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds )
+{
+ Gia_Obj_t * pObjX, * pObjM;
+ int i, k = 0;
+ ABC_FREE( p->pRefs );
+ Gia_ManCreateRefs( p );
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+ {
+ if ( Vec_IntEntry(vAdds, 6*i+2) == 0 ) // HADD
+ {
+ pObjX = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+3) );
+ pObjM = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+4) );
+ if ( (pObjM == Gia_ObjFanin0(pObjX) || pObjM == Gia_ObjFanin1(pObjX)) && Gia_ObjRefNum(p, pObjM) == 1 )
+ continue;
+ }
+ memmove( Vec_IntArray(vAdds) + 6*k++, Vec_IntArray(vAdds) + 6*i, 6*sizeof(int) );
+ }
+ assert( k <= i );
+ Vec_IntShrink( vAdds, 6*k );
+}
+// removes HAs fully contained inside FAs
+void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds )
+{
+ Vec_Bit_t * vInsiders = Ree_CollectInsiders( p, vAdds );
+ int i, k = 0;
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+ {
+ if ( Vec_IntEntry(vAdds, 6*i+2) == 0 ) // HADD
+ if ( Vec_BitEntry(vInsiders, Vec_IntEntry(vAdds, 6*i+3)) && Vec_BitEntry(vInsiders, Vec_IntEntry(vAdds, 6*i+4)) )
+ continue;
+ memmove( Vec_IntArray(vAdds) + 6*k++, Vec_IntArray(vAdds) + 6*i, 6*sizeof(int) );
+ }
+ assert( k <= i );
+ Vec_IntShrink( vAdds, 6*k );
+ Vec_BitFree( vInsiders );
+}
+
+int Ree_ManCountFadds( Vec_Int_t * vAdds )
{
- abctime clk = Abc_Clock();
- Vec_Int_t * vAdds = Ree_ManComputeCuts( p, 1 );
int i, Count = 0;
- for ( i = 0; 5*i < Vec_IntSize(vAdds); i++ )
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+ if ( Vec_IntEntry(vAdds, 6*i+2) != 0 )
+ Count++;
+ return Count;
+}
+void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose )
+{
+ int i;
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
{
- if ( Vec_IntEntry(vAdds, 5*i+2) == 0 )
+ //if ( Vec_IntEntry(vAdds, 6*i+2) == 0 )
+ // continue;
+ if ( !fVerbose )
continue;
- Count++;
- continue;
printf( "%6d : ", i );
- printf( "%6d ", Vec_IntEntry(vAdds, 5*i+0) );
- printf( "%6d ", Vec_IntEntry(vAdds, 5*i+1) );
- printf( "%6d ", Vec_IntEntry(vAdds, 5*i+2) );
+ printf( "%6d ", Vec_IntEntry(vAdds, 6*i+0) );
+ printf( "%6d ", Vec_IntEntry(vAdds, 6*i+1) );
+ printf( "%6d ", Vec_IntEntry(vAdds, 6*i+2) );
printf( " -> " );
- printf( "%6d ", Vec_IntEntry(vAdds, 5*i+3) );
- printf( "%6d ", Vec_IntEntry(vAdds, 5*i+4) );
+ printf( "%6d ", Vec_IntEntry(vAdds, 6*i+3) );
+ printf( "%6d ", Vec_IntEntry(vAdds, 6*i+4) );
+ printf( " (%d)", Vec_IntEntry(vAdds, 6*i+5) );
printf( "\n" );
}
+}
+void Ree_ManComputeCutsTest( Gia_Man_t * p )
+{
+ abctime clk = Abc_Clock();
+ Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, 1 );
+ int nFadds = Ree_ManCountFadds( vAdds );
+ Ree_ManPrintAdders( vAdds, 1 );
+ printf( "Detected %d FAs and %d HAs. ", nFadds, Vec_IntSize(vAdds)/6-nFadds );
Vec_IntFree( vAdds );
- printf( "Detected %d FAs and %d HAs. ", Count, Vec_IntSize(vAdds)/5-Count );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
diff --git a/src/proof/acec/module.make b/src/proof/acec/module.make
index e66bf6e8..df6db695 100644
--- a/src/proof/acec/module.make
+++ b/src/proof/acec/module.make
@@ -1,7 +1,10 @@
-SRC += src/proof/acec/acecCore.c \
+SRC += src/proof/acec/acecCl.c \
+ src/proof/acec/acecCore.c \
src/proof/acec/acecCo.c \
src/proof/acec/acecRe.c \
+ src/proof/acec/acecPa.c \
src/proof/acec/acecPo.c \
+ src/proof/acec/acecPool.c \
src/proof/acec/acecCover.c \
src/proof/acec/acecFadds.c \
src/proof/acec/acecOrder.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-04 05:22:29 +0000