summaryrefslogtreecommitdiffstats
path: root/src/proof/acec
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/acec')
-rw-r--r--src/proof/acec/acec.h27
-rw-r--r--src/proof/acec/acecBo.c216
-rw-r--r--src/proof/acec/acecCl.c204
-rw-r--r--src/proof/acec/acecCo.c2
-rw-r--r--src/proof/acec/acecCore.c505
-rw-r--r--src/proof/acec/acecInt.h27
-rw-r--r--src/proof/acec/acecMult.c550
-rw-r--r--src/proof/acec/acecNorm.c226
-rw-r--r--src/proof/acec/acecPa.c5
-rw-r--r--src/proof/acec/acecPool.c17
-rw-r--r--src/proof/acec/acecRe.c47
-rw-r--r--src/proof/acec/acecSt.c2
-rw-r--r--src/proof/acec/acecTree.c754
-rw-r--r--src/proof/acec/acecUtil.c23
-rw-r--r--src/proof/acec/module.make4
15 files changed, 2555 insertions, 54 deletions
diff --git a/src/proof/acec/acec.h b/src/proof/acec/acec.h
index c61b4485..fcbd32df 100644
--- a/src/proof/acec/acec.h
+++ b/src/proof/acec/acec.h
@@ -38,6 +38,22 @@ ABC_NAMESPACE_HEADER_START
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
+// combinational equivalence checking parameters
+typedef struct Acec_ParCec_t_ Acec_ParCec_t;
+struct Acec_ParCec_t_
+{
+ int nBTLimit; // conflict limit at a node
+ int TimeLimit; // the runtime limit in seconds
+ int fMiter; // input circuit is a miter
+ int fDualOutput; // dual-output miter
+ int fTwoOutput; // two-output miter
+ int fBooth; // expecting Booth multiplier
+ int fSilent; // print no messages
+ int fVeryVerbose; // verbose stats
+ int fVerbose; // verbose stats
+ int iOutFail; // the number of failed output
+};
+
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -50,8 +66,11 @@ ABC_NAMESPACE_HEADER_START
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+/*=== acecCl.c ========================================================*/
+extern Gia_Man_t * Acec_ManDecla( Gia_Man_t * pGia, int fBooth, int fVerbose );
/*=== acecCore.c ========================================================*/
-extern int Gia_PolynCec( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Cec_ParCec_t * pPars );
+extern void Acec_ManCecSetDefaultParams( Acec_ParCec_t * p );
+extern int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars );
/*=== acecFadds.c ========================================================*/
extern Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose, Vec_Int_t ** vCutsXor2 );
extern Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose );
@@ -60,6 +79,12 @@ 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 );
+/*=== acecTree.c ========================================================*/
+extern Gia_Man_t * Acec_Normalize( Gia_Man_t * pGia, int fBooth, int fVerbose );
ABC_NAMESPACE_HEADER_END
diff --git a/src/proof/acec/acecBo.c b/src/proof/acec/acecBo.c
new file mode 100644
index 00000000..9cddcd13
--- /dev/null
+++ b/src/proof/acec/acecBo.c
@@ -0,0 +1,216 @@
+/**CFile****************************************************************
+
+ FileName [acecBo.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: acecBo.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 Acec_DetectBoothXorMux( Gia_Man_t * p, Gia_Obj_t * pMux, Gia_Obj_t * pXor, int pIns[3] )
+{
+ Gia_Obj_t * pFan0, * pFan1;
+ Gia_Obj_t * pDat0, * pDat1, * pCtrl;
+ if ( !Gia_ObjIsMuxType(pMux) || !Gia_ObjIsMuxType(pXor) )
+ return 0;
+ if ( !Gia_ObjRecognizeExor( pXor, &pFan0, &pFan1 ) )
+ return 0;
+ pFan0 = Gia_Regular(pFan0);
+ pFan1 = Gia_Regular(pFan1);
+ if ( Gia_ObjId(p, pFan0) > Gia_ObjId(p, pFan1) )
+ ABC_SWAP( Gia_Obj_t *, pFan0, pFan1 );
+ if ( !(pCtrl = Gia_ObjRecognizeMux( pMux, &pDat0, &pDat1 )) )
+ return 0;
+ pDat0 = Gia_Regular(pDat0);
+ pDat1 = Gia_Regular(pDat1);
+ pCtrl = Gia_Regular(pCtrl);
+ if ( !Gia_ObjIsAnd(pDat0) || !Gia_ObjIsAnd(pDat1) )
+ return 0;
+ if ( Gia_ObjFaninId0p(p, pDat0) != Gia_ObjFaninId0p(p, pDat1) ||
+ Gia_ObjFaninId1p(p, pDat0) != Gia_ObjFaninId1p(p, pDat1) )
+ return 0;
+ if ( Gia_ObjFaninId0p(p, pDat0) != Gia_ObjId(p, pFan0) ||
+ Gia_ObjFaninId1p(p, pDat0) != Gia_ObjId(p, pFan1) )
+ return 0;
+ pIns[0] = Gia_ObjId(p, pFan0);
+ pIns[1] = Gia_ObjId(p, pFan1);
+ pIns[2] = Gia_ObjId(p, pCtrl);
+ return 1;
+}
+int Acec_DetectBoothXorFanin( Gia_Man_t * p, Gia_Obj_t * pObj, int pIns[5] )
+{
+ Gia_Obj_t * pFan0, * pFan1;
+ //int Id = Gia_ObjId(p, pObj);
+ if ( !Gia_ObjIsAnd(pObj) )
+ return 0;
+ if ( !Gia_ObjFaninC0(pObj) || !Gia_ObjFaninC1(pObj) )
+ return 0;
+ pFan0 = Gia_ObjFanin0(pObj);
+ pFan1 = Gia_ObjFanin1(pObj);
+ if ( !Gia_ObjIsAnd(pFan0) || !Gia_ObjIsAnd(pFan1) )
+ return 0;
+ if ( Acec_DetectBoothXorMux(p, Gia_ObjFanin0(pFan0), Gia_ObjFanin0(pFan1), pIns) )
+ {
+ pIns[3] = Gia_ObjId(p, Gia_ObjFanin1(pFan0));
+ pIns[4] = Gia_ObjId(p, Gia_ObjFanin1(pFan1));
+ return 1;
+ }
+ if ( Acec_DetectBoothXorMux(p, Gia_ObjFanin0(pFan0), Gia_ObjFanin1(pFan1), pIns) )
+ {
+ pIns[3] = Gia_ObjId(p, Gia_ObjFanin1(pFan0));
+ pIns[4] = Gia_ObjId(p, Gia_ObjFanin0(pFan1));
+ return 1;
+ }
+ if ( Acec_DetectBoothXorMux(p, Gia_ObjFanin1(pFan0), Gia_ObjFanin0(pFan1), pIns) )
+ {
+ pIns[3] = Gia_ObjId(p, Gia_ObjFanin0(pFan0));
+ pIns[4] = Gia_ObjId(p, Gia_ObjFanin1(pFan1));
+ return 1;
+ }
+ if ( Acec_DetectBoothXorMux(p, Gia_ObjFanin1(pFan0), Gia_ObjFanin1(pFan1), pIns) )
+ {
+ pIns[3] = Gia_ObjId(p, Gia_ObjFanin0(pFan0));
+ pIns[4] = Gia_ObjId(p, Gia_ObjFanin0(pFan1));
+ return 1;
+ }
+ return 0;
+}
+int Acec_DetectBoothOne( Gia_Man_t * p, Gia_Obj_t * pObj, int pIns[5] )
+{
+ Gia_Obj_t * pFan0, * pFan1;
+ if ( !Gia_ObjRecognizeExor( pObj, &pFan0, &pFan1 ) )
+ return 0;
+ pFan0 = Gia_Regular(pFan0);
+ pFan1 = Gia_Regular(pFan1);
+ if ( Acec_DetectBoothXorFanin( p, pFan0, pIns ) && pIns[2] == Gia_ObjId(p, pFan1) )
+ return 1;
+ if ( Acec_DetectBoothXorFanin( p, pFan1, pIns ) && pIns[2] == Gia_ObjId(p, pFan0) )
+ return 1;
+ return 0;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Acec_DetectBoothTwoXor( Gia_Man_t * p, Gia_Obj_t * pObj, int pIns[5] )
+{
+ Gia_Obj_t * pFan0, * pFan1;
+ if ( !Gia_ObjIsAnd(pObj) )
+ return 0;
+ if ( Gia_ObjRecognizeExor( Gia_ObjFanin0(pObj), &pFan0, &pFan1 ) )
+ {
+ pIns[0] = Gia_ObjId(p, Gia_Regular(pFan0));
+ pIns[1] = Gia_ObjId(p, Gia_Regular(pFan1));
+ pIns[2] = -1;
+ pIns[3] = 0;
+ pIns[4] = Gia_ObjId(p, Gia_ObjFanin1(pObj));
+ return 1;
+ }
+ if ( Gia_ObjRecognizeExor( Gia_ObjFanin1(pObj), &pFan0, &pFan1 ) )
+ {
+ pIns[0] = Gia_ObjId(p, Gia_Regular(pFan0));
+ pIns[1] = Gia_ObjId(p, Gia_Regular(pFan1));
+ pIns[2] = -1;
+ pIns[3] = 0;
+ pIns[4] = Gia_ObjId(p, Gia_ObjFanin0(pObj));
+ return 1;
+ }
+ return 0;
+}
+int Acec_DetectBoothTwo( Gia_Man_t * p, Gia_Obj_t * pObj, int pIns[5] )
+{
+ Gia_Obj_t * pFan0, * pFan1;
+ if ( !Gia_ObjRecognizeExor( pObj, &pFan0, &pFan1 ) )
+ return 0;
+ pFan0 = Gia_Regular(pFan0);
+ pFan1 = Gia_Regular(pFan1);
+ if ( Acec_DetectBoothTwoXor( p, pFan0, pIns ) )
+ {
+ pIns[2] = Gia_ObjId(p, pFan1);
+ return 1;
+ }
+ if ( Acec_DetectBoothTwoXor( p, pFan1, pIns ) )
+ {
+ pIns[2] = Gia_ObjId(p, pFan0);
+ return 1;
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Acec_DetectBoothTest( Gia_Man_t * p )
+{
+ Gia_Obj_t * pObj;
+ int i, pIns[5];
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ if ( !Acec_DetectBoothOne(p, pObj, pIns) && !Acec_DetectBoothTwo(p, pObj, pIns) )
+ continue;
+ printf( "obj = %4d : b0 = %4d b1 = %4d b2 = %4d a0 = %4d a1 = %4d\n",
+ i, pIns[0], pIns[1], pIns[2], pIns[3], pIns[4] );
+ }
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecCl.c b/src/proof/acec/acecCl.c
index b60c2bf9..6185677b 100644
--- a/src/proof/acec/acecCl.c
+++ b/src/proof/acec/acecCl.c
@@ -127,7 +127,7 @@ Vec_Int_t * Acec_CollectXorTops( Gia_Man_t * p )
break;
}
Vec_IntPush( vRootXorSet, Gia_ObjId(p, pObj) );
- Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan1)) : Gia_ObjId(p, Gia_Regular(pFan0)) );
+ Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan0)) : Gia_ObjId(p, Gia_Regular(pFan1)) );
Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan10)) : Gia_ObjId(p, Gia_Regular(pFan00)) );
Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan11)) : Gia_ObjId(p, Gia_Regular(pFan01)) );
}
@@ -173,10 +173,101 @@ int Acec_DetectLitPolarity( Gia_Man_t * p, int Node, int Leaf )
if ( Lit0 != -1 && Lit1 != -1 )
{
assert( Lit0 == Lit1 );
+ printf( "Problem for leaf %d\n", Leaf );
return Lit0;
}
return Lit0 != -1 ? Lit0 : Lit1;
}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Acec_DetectComputeSuppOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Int_t * vNods )
+{
+ if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Gia_ObjSetTravIdCurrent(p, pObj);
+ if ( pObj->fMark0 )
+ {
+ Vec_IntPush( vSupp, Gia_ObjId(p, pObj) );
+ return;
+ }
+ assert( Gia_ObjIsAnd(pObj) );
+ Acec_DetectComputeSuppOne_rec( p, Gia_ObjFanin0(pObj), vSupp, vNods );
+ Acec_DetectComputeSuppOne_rec( p, Gia_ObjFanin1(pObj), vSupp, vNods );
+ Vec_IntPush( vNods, Gia_ObjId(p, pObj) );
+}
+void Acec_DetectComputeSupports( Gia_Man_t * p, Vec_Int_t * vRootXorSet )
+{
+ Vec_Int_t * vNods = Vec_IntAlloc( 100 );
+ Vec_Int_t * vPols = Vec_IntAlloc( 100 );
+ Vec_Int_t * vSupp = Vec_IntAlloc( 100 ); int i, k, Node, Pol;
+ for ( i = 0; 4*i < Vec_IntSize(vRootXorSet); i++ )
+ {
+ Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 1;
+ Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+2) )->fMark0 = 1;
+ Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+3) )->fMark0 = 1;
+ }
+ for ( i = 1; 4*i < Vec_IntSize(vRootXorSet); i++ )
+ {
+ Vec_IntClear( vSupp );
+ Gia_ManIncrementTravId( p );
+
+ Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 0;
+ Acec_DetectComputeSuppOne_rec( p, Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) ), vSupp, vNods );
+ Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 1;
+
+ Vec_IntSort( vSupp, 0 );
+
+ printf( "Out %4d : %4d \n", i, Vec_IntEntry(vRootXorSet, 4*i+1) );
+ Vec_IntPrint( vSupp );
+
+ printf( "Cone:\n" );
+ Vec_IntForEachEntry( vNods, Node, k )
+ Gia_ObjPrint( p, Gia_ManObj(p, Node) );
+
+
+ Vec_IntClear( vPols );
+ Vec_IntForEachEntry( vSupp, Node, k )
+ Vec_IntPush( vPols, Acec_DetectLitPolarity(p, Vec_IntEntry(vRootXorSet, 4*i+1), Node) );
+
+ Vec_IntForEachEntryTwo( vSupp, vPols, Node, Pol, k )
+ printf( "%d(%d) ", Node, Abc_LitIsCompl(Pol) );
+
+ printf( "\n" );
+
+ Vec_IntPrint( vSupp );
+ }
+ for ( i = 0; 4*i < Vec_IntSize(vRootXorSet); i++ )
+ {
+ Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 0;
+ Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+2) )->fMark0 = 0;
+ Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+3) )->fMark0 = 0;
+ }
+ Vec_IntFree( vSupp );
+ Vec_IntFree( vPols );
+ Vec_IntFree( vNods );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Gia_Man_t * Acec_DetectXorBuildNew( Gia_Man_t * p, Vec_Int_t * vRootXorSet )
{
Gia_Man_t * pNew;
@@ -215,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 );
@@ -236,6 +319,8 @@ Gia_Man_t * Acec_DetectAdditional( Gia_Man_t * p, int fVerbose )
vRootXorSet = Acec_CollectXorTops( p );
if ( vRootXorSet )
{
+ Acec_DetectComputeSupports( p, vRootXorSet );
+
pNew = Acec_DetectXorBuildNew( p, vRootXorSet );
Vec_IntFree( vRootXorSet );
}
@@ -250,6 +335,107 @@ Gia_Man_t * Acec_DetectAdditional( Gia_Man_t * p, int fVerbose )
return pNew;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Acec_RewriteTop( Gia_Man_t * p, Acec_Box_t * pBox )
+{
+ Vec_Int_t * vRes = Vec_IntAlloc( Gia_ManCoNum(p) + 1 );
+ Vec_Int_t * vLevel;
+ int i, k, iStart, iLit, Driver, Count = 0;
+ // determine how much to shift
+ Driver = Gia_ObjFaninId0p( p, Gia_ManCo(p, 0) );
+ Vec_WecForEachLevel( pBox->vRootLits, vLevel, iStart )
+ if ( Abc_Lit2Var(Vec_IntEntry(vLevel,0)) == Driver )
+ break;
+ assert( iStart < Gia_ManCoNum(p) );
+ //Vec_WecPrintLits( pBox->vRootLits );
+ Vec_WecForEachLevelStart( pBox->vRootLits, vLevel, i, iStart )
+ {
+ int In[3] = {0}, Out[2];
+ assert( Vec_IntSize(vLevel) > 0 );
+ assert( Vec_IntSize(vLevel) <= 3 );
+ if ( Vec_IntSize(vLevel) == 1 )
+ {
+ Vec_IntPush( vRes, Vec_IntEntry(vLevel, 0) );
+ continue;
+ }
+ Vec_IntForEachEntry( vLevel, iLit, k )
+ In[k] = iLit;
+ Acec_InsertFadd( p, In, Out );
+ Vec_IntPush( vRes, Out[0] );
+ if ( i+1 < Vec_WecSize(pBox->vRootLits) )
+ Vec_IntPush( Vec_WecEntry(pBox->vRootLits, i+1), Out[1] );
+ else
+ Vec_IntPush( Vec_WecPushLevel(pBox->vRootLits), Out[1] );
+ Count++;
+ }
+ assert( Vec_IntSize(vRes) >= Gia_ManCoNum(p) );
+ Vec_IntShrink( vRes, Gia_ManCoNum(p) );
+ printf( "Added %d adders for replace CLAs. ", Count );
+ return vRes;
+}
+Gia_Man_t * Acec_RewriteReplace( Gia_Man_t * p, Vec_Int_t * vRes )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj; int i;
+ assert( Gia_ManCoNum(p) == Vec_IntSize(vRes) );
+ // create new manager
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManFillValue( p );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachCi( p, pObj, i )
+ pObj->Value = Gia_ManAppendCi(pNew);
+ Gia_ManForEachAnd( p, pObj, i )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ Gia_ManForEachCo( p, pObj, i )
+ {
+ int iLit = Vec_IntEntry( vRes, i );
+ Gia_Obj_t * pRepr = Gia_ManObj( p, Abc_Lit2Var(iLit) );
+ pObj->Value = Gia_ManAppendCo( pNew, pRepr->Value );
+ }
+ // set correct phase
+ Gia_ManSetPhase( p );
+ Gia_ManSetPhase( pNew );
+ Gia_ManForEachCo( pNew, pObj, i )
+ if ( Gia_ObjPhase(pObj) != Gia_ObjPhase(Gia_ManCo(p, i)) )
+ Gia_ObjFlipFaninC0( pObj );
+ // remove dangling nodes
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
+Gia_Man_t * Acec_ManDecla( Gia_Man_t * pGia, int fBooth, int fVerbose )
+{
+ abctime clk = Abc_Clock();
+ Gia_Man_t * pNew = NULL;
+ Vec_Bit_t * vIgnore = fBooth ? Acec_BoothFindPPG(pGia) : NULL;
+ Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, 0, 0, fVerbose );
+ Vec_Int_t * vResult;
+ Vec_BitFreeP( &vIgnore );
+ if ( pBox == NULL ) // cannot match
+ {
+ printf( "Cannot find arithmetic boxes.\n" );
+ return Gia_ManDup( pGia );
+ }
+ vResult = Acec_RewriteTop( pGia, pBox );
+ Acec_BoxFreeP( &pBox );
+ pNew = Acec_RewriteReplace( pGia, vResult );
+ Vec_IntFree( vResult );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ return pNew;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/acec/acecCo.c b/src/proof/acec/acecCo.c
index 1e8ed7bb..a997eb03 100644
--- a/src/proof/acec/acecCo.c
+++ b/src/proof/acec/acecCo.c
@@ -109,7 +109,7 @@ Vec_Int_t * Gia_PolynCoreOrder_int( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Wec
{
Vec_Int_t * vOrder = Vec_IntAlloc( 1000 );
Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(pGia) );
- int i, k, Index, Driver, Entry1, Entry2 = -1;
+ int i, k, Index = -1, Driver, Entry1, Entry2 = -1;
// mark roots
Vec_IntForEachEntry( vRoots, Driver, i )
Vec_BitWriteEntry( vIsRoot, Driver, 1 );
diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c
index ac7ee67b..a2341704 100644
--- a/src/proof/acec/acecCore.c
+++ b/src/proof/acec/acecCore.c
@@ -19,6 +19,9 @@
***********************************************************************/
#include "acecInt.h"
+#include "proof/cec/cec.h"
+#include "misc/util/utilTruth.h"
+#include "misc/extra/extra.h"
ABC_NAMESPACE_IMPL_START
@@ -27,12 +30,450 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+#define TRUTH_UNUSED 0x1234567812345678
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
+ Synopsis [This procedure sets default parameters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Acec_ManCecSetDefaultParams( Acec_ParCec_t * p )
+{
+ memset( p, 0, sizeof(Acec_ParCec_t) );
+ p->nBTLimit = 1000; // conflict limit at a node
+ p->TimeLimit = 0; // the runtime limit in seconds
+ p->fMiter = 0; // input circuit is a miter
+ p->fDualOutput = 0; // dual-output miter
+ p->fTwoOutput = 0; // two-output miter
+ p->fSilent = 0; // print no messages
+ p->fVeryVerbose = 0; // verbose stats
+ p->fVerbose = 0; // verbose stats
+ p->iOutFail = -1; // the number of failed output
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Acec_VerifyClasses( Gia_Man_t * p, Vec_Wec_t * vLits, Vec_Wec_t * vReprs )
+{
+ Vec_Ptr_t * vFunc = Vec_PtrAlloc( Vec_WecSize(vLits) );
+ Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
+ Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vLevel;
+ int i, j, k, Entry, Entry2, nOvers = 0, nErrors = 0;
+ Vec_WecForEachLevel( vLits, vLevel, i )
+ {
+ Vec_Wrd_t * vTruths = Vec_WrdAlloc( Vec_IntSize(vLevel) );
+ Vec_IntForEachEntry( vLevel, Entry, k )
+ {
+ word Truth = Gia_ObjComputeTruth6Cis( p, Entry, vSupp, vTemp );
+ if ( Vec_IntSize(vSupp) > 6 )
+ {
+ nOvers++;
+ Vec_WrdPush( vTruths, TRUTH_UNUSED );
+ continue;
+ }
+ vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize );
+ if ( Vec_IntSize(vSupp) > 5 )
+ {
+ nOvers++;
+ Vec_WrdPush( vTruths, TRUTH_UNUSED );
+ continue;
+ }
+ Vec_WrdPush( vTruths, Truth );
+ }
+ Vec_PtrPush( vFunc, vTruths );
+ }
+ if ( nOvers )
+ printf( "Detected %d oversize support nodes.\n", nOvers );
+ Vec_IntFree( vSupp );
+ Vec_WrdFree( vTemp );
+ // verify the classes
+ Vec_WecForEachLevel( vReprs, vLevel, i )
+ {
+ Vec_Wrd_t * vTruths = (Vec_Wrd_t *)Vec_PtrEntry( vFunc, i );
+ Vec_IntForEachEntry( vLevel, Entry, k )
+ Vec_IntForEachEntryStart( vLevel, Entry2, j, k+1 )
+ {
+ word Truth = Vec_WrdEntry( vTruths, k );
+ word Truth2 = Vec_WrdEntry( vTruths, j );
+ if ( Entry == Entry2 )
+ {
+ nErrors++;
+ if ( Truth != Truth2 && Truth != TRUTH_UNUSED && Truth2 != TRUTH_UNUSED )
+ printf( "Rank %d: Lit %d and %d do not pass verification.\n", i, k, j );
+ }
+ if ( Entry == Abc_LitNot(Entry2) )
+ {
+ nErrors++;
+ if ( Truth != ~Truth2 && Truth != TRUTH_UNUSED && Truth2 != TRUTH_UNUSED )
+ printf( "Rank %d: Lit %d and %d do not pass verification.\n", i, k, j );
+ }
+ }
+ }
+ if ( nErrors )
+ printf( "Total errors in equivalence classes = %d.\n", nErrors );
+ Vec_VecFree( (Vec_Vec_t *)vFunc );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Acec_CommonStart( Gia_Man_t * pBase, Gia_Man_t * pAdd )
+{
+ Gia_Obj_t * pObj;
+ int i;
+ Gia_ManFillValue( pAdd );
+ Gia_ManConst0(pAdd)->Value = 0;
+ if ( pBase == NULL )
+ {
+ pBase = Gia_ManStart( Gia_ManObjNum(pAdd) );
+ pBase->pName = Abc_UtilStrsav( pAdd->pName );
+ pBase->pSpec = Abc_UtilStrsav( pAdd->pSpec );
+ Gia_ManForEachCi( pAdd, pObj, i )
+ pObj->Value = Gia_ManAppendCi(pBase);
+ Gia_ManHashAlloc( pBase );
+ }
+ else
+ {
+ assert( Gia_ManCiNum(pBase) == Gia_ManCiNum(pAdd) );
+ Gia_ManForEachCi( pAdd, pObj, i )
+ pObj->Value = Gia_Obj2Lit( pBase, Gia_ManCi(pBase, i) );
+ }
+ Gia_ManForEachAnd( pAdd, pObj, i )
+ pObj->Value = Gia_ManHashAnd( pBase, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ return pBase;
+}
+void Acec_CommonFinish( Gia_Man_t * pBase )
+{
+ int Id;
+ Gia_ManCreateRefs( pBase );
+ Gia_ManForEachAndId( pBase, Id )
+ if ( Gia_ObjRefNumId(pBase, Id) == 0 )
+ Gia_ManAppendCo( pBase, Abc_Var2Lit(Id,0) );
+}
+Vec_Int_t * Acec_CountRemap( Gia_Man_t * pAdd, Gia_Man_t * pBase )
+{
+ Gia_Obj_t * pObj; int i;
+ Vec_Int_t * vMapNew = Vec_IntStartFull( Gia_ManObjNum(pAdd) );
+ Gia_ManSetPhase( pAdd );
+ Vec_IntWriteEntry( vMapNew, 0, 0 );
+ Gia_ManForEachCand( pAdd, pObj, i )
+ {
+ int iObjBase = Abc_Lit2Var(pObj->Value);
+ Gia_Obj_t * pObjBase = Gia_ManObj( pBase, iObjBase );
+ int iObjRepr = Abc_Lit2Var(pObjBase->Value);
+ Vec_IntWriteEntry( vMapNew, i, Abc_Var2Lit(iObjRepr, Gia_ObjPhase(pObj)) );
+ }
+ return vMapNew;
+}
+void Acec_ComputeEquivClasses( Gia_Man_t * pOne, Gia_Man_t * pTwo, Vec_Int_t ** pvMap1, Vec_Int_t ** pvMap2 )
+{
+ abctime clk = Abc_Clock();
+ Gia_Man_t * pBase, * pRepr;
+ pBase = Acec_CommonStart( NULL, pOne );
+ pBase = Acec_CommonStart( pBase, pTwo );
+ Acec_CommonFinish( pBase );
+ //Gia_ManShow( pBase, NULL, 0, 0, 0 );
+ pRepr = Gia_ManComputeGiaEquivs( pBase, 100, 0 );
+ *pvMap1 = Acec_CountRemap( pOne, pBase );
+ *pvMap2 = Acec_CountRemap( pTwo, pBase );
+ Gia_ManStop( pBase );
+ Gia_ManStop( pRepr );
+ printf( "Finished computing equivalent nodes. " );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+}
+void Acec_MatchBoxesSort( int * pArray, int nSize, int * pCostLits )
+{
+ int i, j, best_i;
+ for ( i = 0; i < nSize-1; i++ )
+ {
+ best_i = i;
+ for ( j = i+1; j < nSize; j++ )
+ if ( Abc_Lit2LitL(pCostLits, pArray[j]) > Abc_Lit2LitL(pCostLits, pArray[best_i]) )
+ best_i = j;
+ ABC_SWAP( int, pArray[i], pArray[best_i] );
+ }
+}
+void Acec_MatchPrintEquivLits( Gia_Man_t * p, Vec_Wec_t * vLits, int * pCostLits, int fVerbose )
+{
+ Vec_Int_t * vSupp;
+ Vec_Wrd_t * vTemp;
+ Vec_Int_t * vLevel;
+ int i, k, Entry;
+ printf( "Leaf literals and their classes:\n" );
+ Vec_WecForEachLevel( vLits, vLevel, i )
+ {
+ if ( Vec_IntSize(vLevel) == 0 )
+ continue;
+ printf( "Rank %2d : %2d ", i, Vec_IntSize(vLevel) );
+ Vec_IntForEachEntry( vLevel, Entry, k )
+ printf( "%s%d(%d) ", Abc_LitIsCompl(Entry) ? "-":"+", Abc_Lit2Var(Entry), Abc_Lit2LitL(pCostLits, Entry) );
+ printf( "\n" );
+ }
+ if ( !fVerbose )
+ return;
+ vSupp = Vec_IntAlloc( 100 );
+ vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+ Vec_WecForEachLevel( vLits, vLevel, i )
+ {
+ //if ( i != 20 )
+ // continue;
+ if ( Vec_IntSize(vLevel) == 0 )
+ continue;
+ Vec_IntForEachEntry( vLevel, Entry, k )
+ {
+ word Truth = Gia_ObjComputeTruth6Cis( p, Entry, vSupp, vTemp );
+/*
+ {
+ int iObj = Abc_Lit2Var(Entry);
+ Gia_Man_t * pGia0 = Gia_ManDupAndCones( p, &iObj, 1, 1 );
+ Gia_ManShow( pGia0, NULL, 0, 0, 0 );
+ Gia_ManStop( pGia0 );
+ }
+*/
+ printf( "Rank = %4d : ", i );
+ printf( "Obj = %4d ", Abc_Lit2Var(Entry) );
+ if ( Vec_IntSize(vSupp) > 6 )
+ {
+ printf( "Supp = %d.\n", Vec_IntSize(vSupp) );
+ continue;
+ }
+ vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize );
+ if ( Vec_IntSize(vSupp) > 5 )
+ {
+ printf( "Supp = %d.\n", Vec_IntSize(vSupp) );
+ continue;
+ }
+ Extra_PrintHex( stdout, (unsigned*)&Truth, Vec_IntSize(vSupp) );
+ if ( Vec_IntSize(vSupp) == 4 ) printf( " " );
+ if ( Vec_IntSize(vSupp) == 3 ) printf( " " );
+ if ( Vec_IntSize(vSupp) <= 2 ) printf( " " );
+ printf( " " );
+ Vec_IntPrint( vSupp );
+ }
+ printf( "\n" );
+ }
+ Vec_IntFree( vSupp );
+ Vec_WrdFree( vTemp );
+}
+Vec_Wec_t * Acec_MatchCopy( Vec_Wec_t * vLits, Vec_Int_t * vMap )
+{
+ Vec_Wec_t * vRes = Vec_WecStart( Vec_WecSize(vLits) );
+ Vec_Int_t * vLevel; int i, k, iLit;
+ Vec_WecForEachLevel( vLits, vLevel, i )
+ Vec_IntForEachEntry( vLevel, iLit, k )
+ Vec_WecPush( vRes, i, Abc_Lit2LitL(Vec_IntArray(vMap), iLit) );
+ return vRes;
+}
+int Acec_MatchCountCommon( Vec_Wec_t * vLits1, Vec_Wec_t * vLits2, int Shift )
+{
+ Vec_Int_t * vRes = Vec_IntAlloc( 100 );
+ Vec_Int_t * vLevel1, * vLevel2;
+ int i, nCommon = 0;
+ Vec_WecForEachLevel( vLits1, vLevel1, i )
+ {
+ if ( i+Shift < 0 || i+Shift >= Vec_WecSize(vLits2) )
+ continue;
+ vLevel2 = Vec_WecEntry( vLits2, i+Shift );
+ nCommon += Vec_IntTwoFindCommonReverse( vLevel1, vLevel2, vRes );
+ }
+ Vec_IntFree( vRes );
+ return nCommon;
+}
+void Vec_IntInsertOrder( Vec_Int_t * vLits, Vec_Int_t * vClasses, int Lit, int Class )
+{
+ int i;
+ for ( i = Vec_IntSize(vClasses)-1; i >= 0; i-- )
+ if ( Vec_IntEntry(vClasses,i) >= Class )
+ break;
+ Vec_IntInsert( vLits, i+1, Lit );
+ Vec_IntInsert( vClasses, i+1, Class );
+}
+void Acec_MoveDuplicates( Vec_Wec_t * vLits, Vec_Wec_t * vClasses )
+{
+ Vec_Int_t * vLevel1, * vLevel2;
+ int i, k, Prev, This, Entry;
+ Vec_WecForEachLevel( vLits, vLevel1, i )
+ {
+ if ( i == Vec_WecSize(vLits) - 1 )
+ break;
+ vLevel2 = Vec_WecEntry(vClasses, i);
+ assert( Vec_IntSize(vLevel1) == Vec_IntSize(vLevel2) );
+ Prev = -1;
+ Vec_IntForEachEntry( vLevel2, This, k )
+ {
+ if ( Prev != This )
+ {
+ Prev = This;
+ continue;
+ }
+ Prev = -1;
+ Entry = Vec_IntEntry( vLevel1, k );
+
+ Vec_IntDrop( vLevel1, k );
+ Vec_IntDrop( vLevel2, k-- );
+
+ Vec_IntDrop( vLevel1, k );
+ Vec_IntDrop( vLevel2, k-- );
+
+ Vec_IntInsertOrder( Vec_WecEntry(vLits, i+1), Vec_WecEntry(vClasses, i+1), Entry, This );
+
+ assert( Vec_IntSize(vLevel1) == Vec_IntSize(vLevel2) );
+ assert( Vec_IntSize(Vec_WecEntry(vLits, i+1)) == Vec_IntSize(Vec_WecEntry(vClasses, i+1)) );
+ }
+ }
+}
+
+void Acec_MatchCheckShift( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Vec_Wec_t * vLits0, Vec_Wec_t * vLits1, Vec_Int_t * vMap0, Vec_Int_t * vMap1, Vec_Wec_t * vRoots0, Vec_Wec_t * vRoots1 )
+{
+ Vec_Wec_t * vRes0 = Acec_MatchCopy( vLits0, vMap0 );
+ Vec_Wec_t * vRes1 = Acec_MatchCopy( vLits1, vMap1 );
+ int nCommon = Acec_MatchCountCommon( vRes0, vRes1, 0 );
+ int nCommonPlus = Acec_MatchCountCommon( vRes0, vRes1, 1 );
+ int nCommonMinus = Acec_MatchCountCommon( vRes0, vRes1, -1 );
+ if ( nCommonPlus >= nCommonMinus && nCommonPlus > nCommon )
+ {
+ Vec_WecInsertLevel( vLits0, 0 );
+ Vec_WecInsertLevel( vRoots0, 0 );
+ Vec_WecInsertLevel( vRes0, 0 );
+ printf( "Shifted one level up.\n" );
+ }
+ else if ( nCommonMinus > nCommonPlus && nCommonMinus > nCommon )
+ {
+ Vec_WecInsertLevel( vLits1, 0 );
+ Vec_WecInsertLevel( vRoots1, 0 );
+ Vec_WecInsertLevel( vRes1, 0 );
+ printf( "Shifted one level down.\n" );
+ }
+ Acec_MoveDuplicates( vLits0, vRes0 );
+ Acec_MoveDuplicates( vLits1, vRes1 );
+
+ //Vec_WecPrintLits( vLits1 );
+ //printf( "Input literals:\n" );
+ //Vec_WecPrintLits( vLits0 );
+ //printf( "Equiv classes:\n" );
+ //Vec_WecPrintLits( vRes0 );
+ //printf( "Input literals:\n" );
+ //Vec_WecPrintLits( vLits1 );
+ //printf( "Equiv classes:\n" );
+ //Vec_WecPrintLits( vRes1 );
+ //Acec_VerifyClasses( pGia0, vLits0, vRes0 );
+ //Acec_VerifyClasses( pGia1, vLits1, vRes1 );
+ Vec_WecFree( vRes0 );
+ Vec_WecFree( vRes1 );
+}
+int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
+{
+ Vec_Int_t * vMap0, * vMap1, * vLevel;
+ int i, nSize, nTotal;
+ Acec_ComputeEquivClasses( pBox0->pGia, pBox1->pGia, &vMap0, &vMap1 );
+ // sort nodes in the classes by their equivalences
+ Vec_WecForEachLevel( pBox0->vLeafLits, vLevel, i )
+ Acec_MatchBoxesSort( Vec_IntArray(vLevel), Vec_IntSize(vLevel), Vec_IntArray(vMap0) );
+ Vec_WecForEachLevel( pBox1->vLeafLits, vLevel, i )
+ Acec_MatchBoxesSort( Vec_IntArray(vLevel), Vec_IntSize(vLevel), Vec_IntArray(vMap1) );
+ Acec_MatchCheckShift( pBox0->pGia, pBox1->pGia, pBox0->vLeafLits, pBox1->vLeafLits, vMap0, vMap1, pBox0->vRootLits, pBox1->vRootLits );
+
+ //Acec_MatchPrintEquivLits( pBox0->pGia, pBox0->vLeafLits, Vec_IntArray(vMap0), 0 );
+ //Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vLeafLits, Vec_IntArray(vMap1), 0 );
+ //printf( "Outputs:\n" );
+ //Vec_WecPrintLits( pBox0->vRootLits );
+ //printf( "Outputs:\n" );
+ //Vec_WecPrintLits( pBox1->vRootLits );
+
+ // reorder nodes to have the same order
+ assert( pBox0->vShared == NULL );
+ assert( pBox1->vShared == NULL );
+ pBox0->vShared = Vec_WecStart( Vec_WecSize(pBox0->vLeafLits) );
+ pBox1->vShared = Vec_WecStart( Vec_WecSize(pBox1->vLeafLits) );
+ pBox0->vUnique = Vec_WecStart( Vec_WecSize(pBox0->vLeafLits) );
+ pBox1->vUnique = Vec_WecStart( Vec_WecSize(pBox1->vLeafLits) );
+ nSize = Abc_MinInt( Vec_WecSize(pBox0->vLeafLits), Vec_WecSize(pBox1->vLeafLits) );
+ Vec_WecForEachLevelStart( pBox0->vLeafLits, vLevel, i, nSize )
+ Vec_IntAppend( Vec_WecEntry(pBox0->vUnique, i), vLevel );
+ Vec_WecForEachLevelStart( pBox1->vLeafLits, vLevel, i, nSize )
+ Vec_IntAppend( Vec_WecEntry(pBox1->vUnique, i), vLevel );
+ for ( i = 0; i < nSize; i++ )
+ {
+ Vec_Int_t * vShared0 = Vec_WecEntry( pBox0->vShared, i );
+ Vec_Int_t * vShared1 = Vec_WecEntry( pBox1->vShared, i );
+ Vec_Int_t * vUnique0 = Vec_WecEntry( pBox0->vUnique, i );
+ Vec_Int_t * vUnique1 = Vec_WecEntry( pBox1->vUnique, i );
+
+ Vec_Int_t * vLevel0 = Vec_WecEntry( pBox0->vLeafLits, i );
+ Vec_Int_t * vLevel1 = Vec_WecEntry( pBox1->vLeafLits, i );
+ int * pBeg0 = Vec_IntArray(vLevel0);
+ int * pBeg1 = Vec_IntArray(vLevel1);
+ int * pEnd0 = Vec_IntLimit(vLevel0);
+ int * pEnd1 = Vec_IntLimit(vLevel1);
+ while ( pBeg0 < pEnd0 && pBeg1 < pEnd1 )
+ {
+ int Entry0 = Abc_Lit2LitL( Vec_IntArray(vMap0), *pBeg0 );
+ int Entry1 = Abc_Lit2LitL( Vec_IntArray(vMap1), *pBeg1 );
+ assert( *pBeg0 && *pBeg1 );
+ if ( Entry0 == Entry1 )
+ {
+ Vec_IntPush( vShared0, *pBeg0++ );
+ Vec_IntPush( vShared1, *pBeg1++ );
+ }
+ else if ( Entry0 > Entry1 )
+ Vec_IntPush( vUnique0, *pBeg0++ );
+ else
+ Vec_IntPush( vUnique1, *pBeg1++ );
+ }
+ while ( pBeg0 < pEnd0 )
+ Vec_IntPush( vUnique0, *pBeg0++ );
+ while ( pBeg1 < pEnd1 )
+ Vec_IntPush( vUnique1, *pBeg1++ );
+ assert( Vec_IntSize(vShared0) == Vec_IntSize(vShared1) );
+ assert( Vec_IntSize(vShared0) + Vec_IntSize(vUnique0) == Vec_IntSize(vLevel0) );
+ assert( Vec_IntSize(vShared1) + Vec_IntSize(vUnique1) == Vec_IntSize(vLevel1) );
+ }
+ nTotal = Vec_WecSizeSize(pBox0->vShared);
+ printf( "Box0: Matched %d entries out of %d.\n", nTotal, Vec_WecSizeSize(pBox0->vLeafLits) );
+ printf( "Box1: Matched %d entries out of %d.\n", nTotal, Vec_WecSizeSize(pBox1->vLeafLits) );
+
+ //Acec_MatchPrintEquivLits( pBox0->pGia, pBox0->vShared, Vec_IntArray(vMap0), 0 );
+ //Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vShared, Vec_IntArray(vMap1), 0 );
+ //printf( "\n" );
+
+ //Acec_MatchPrintEquivLits( pBox0->pGia, pBox0->vUnique, Vec_IntArray(vMap0), 0 );
+ //Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vUnique, Vec_IntArray(vMap1), 0 );
+
+ Vec_IntFree( vMap0 );
+ Vec_IntFree( vMap1 );
+ return nTotal;
+}
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -42,15 +483,61 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-int Gia_PolynCec( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Cec_ParCec_t * pPars )
-{
- Vec_Int_t * vOrder0 = Gia_PolynReorder( pGia0, pPars->fVerbose, pPars->fVeryVerbose );
- Vec_Int_t * vOrder1 = Gia_PolynReorder( pGia1, pPars->fVerbose, pPars->fVeryVerbose );
- Gia_PolynBuild( pGia0, vOrder0, 0, pPars->fVerbose, pPars->fVeryVerbose );
- Gia_PolynBuild( pGia1, vOrder1, 0, pPars->fVerbose, pPars->fVeryVerbose );
- Vec_IntFree( vOrder0 );
- Vec_IntFree( vOrder1 );
- return 1;
+int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
+{
+ int status = -1;
+ abctime clk = Abc_Clock();
+ Gia_Man_t * pMiter;
+ Gia_Man_t * pGia0n = pGia0, * pGia1n = pGia1;
+ Cec_ParCec_t ParsCec, * pCecPars = &ParsCec;
+ Vec_Bit_t * vIgnore0 = pPars->fBooth ? Acec_BoothFindPPG(pGia0) : NULL;
+ Vec_Bit_t * vIgnore1 = pPars->fBooth ? Acec_BoothFindPPG(pGia1) : NULL;
+ Acec_Box_t * pBox0 = Acec_DeriveBox( pGia0, vIgnore0, 0, 0, pPars->fVerbose );
+ Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, vIgnore1, 0, 0, pPars->fVerbose );
+ Vec_BitFreeP( &vIgnore0 );
+ Vec_BitFreeP( &vIgnore1 );
+ if ( pBox0 == NULL || pBox1 == NULL ) // cannot match
+ printf( "Cannot find arithmetic boxes in both LHS and RHS. Trying regular CEC.\n" );
+ else if ( !Acec_MatchBoxes( pBox0, pBox1 ) ) // cannot find matching
+ printf( "Cannot match arithmetic boxes in LHS and RHS. Trying regular CEC.\n" );
+ else
+ {
+ pGia0n = Acec_InsertBox( pBox0, 0 );
+ pGia1n = Acec_InsertBox( pBox1, 0 );
+ printf( "Matching of adder trees in LHS and RHS succeeded. " );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ // remove the last output
+ Gia_ManPatchCoDriver( pGia0n, Gia_ManCoNum(pGia0n)-1, 0 );
+ Gia_ManPatchCoDriver( pGia1n, Gia_ManCoNum(pGia1n)-1, 0 );
+
+ Gia_ManPatchCoDriver( pGia0n, Gia_ManCoNum(pGia0n)-2, 0 );
+ Gia_ManPatchCoDriver( pGia1n, Gia_ManCoNum(pGia1n)-2, 0 );
+ }
+ // solve regular CEC problem
+ Cec_ManCecSetDefaultParams( pCecPars );
+ pCecPars->nBTLimit = pPars->nBTLimit;
+ pMiter = Gia_ManMiter( pGia0n, pGia1n, 0, 1, 0, 0, pPars->fVerbose );
+ if ( pMiter )
+ {
+ int fDumpMiter = 0;
+ if ( fDumpMiter )
+ {
+ Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "acec_miter.aig" );
+ Gia_AigerWrite( pMiter, "acec_miter.aig", 0, 0 );
+ }
+ status = Cec_ManVerify( pMiter, pCecPars );
+ ABC_SWAP( Abc_Cex_t *, pGia0->pCexComb, pMiter->pCexComb );
+ Gia_ManStop( pMiter );
+ }
+ else
+ printf( "Miter computation has failed.\n" );
+ if ( pGia0n != pGia0 )
+ Gia_ManStop( pGia0n );
+ if ( pGia1n != pGia1 )
+ Gia_ManStop( pGia1n );
+ Acec_BoxFreeP( &pBox0 );
+ Acec_BoxFreeP( &pBox1 );
+ return status;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h
index e761e56e..b8ec2455 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,17 @@
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 * vAdds; // adders by rank
+ 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,10 +64,25 @@ ABC_NAMESPACE_HEADER_START
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+/*=== 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 );
+extern Vec_Bit_t * Acec_BoothFindPPG( Gia_Man_t * p );
+/*=== acecNorm.c ========================================================*/
+extern void Acec_InsertFadd( Gia_Man_t * pNew, int In[3], int Out[2] );
+extern Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll );
+/*=== acecTree.c ========================================================*/
+extern void Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds );
+extern Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fFilterIn, int fFilterOut, int fVerbose );
+extern void Acec_BoxFreeP( Acec_Box_t ** ppBox );
/*=== 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/acecMult.c b/src/proof/acec/acecMult.c
new file mode 100644
index 00000000..d868c399
--- /dev/null
+++ b/src/proof/acec/acecMult.c
@@ -0,0 +1,550 @@
+/**CFile****************************************************************
+
+ FileName [acecMult.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [CEC for arithmetic circuits.]
+
+ Synopsis [Multiplier.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: acecMult.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+#include "misc/extra/extra.h"
+#include "misc/util/utilTruth.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+unsigned s_Classes4a[96] = {
+ 0xD728, 0xB748, 0x9F60, 0xD278, 0xB478, 0x96F0, 0xC66C, 0x96CC, 0x9C6C, 0x96AA, 0xA66A, 0x9A6A,
+ 0x28D7, 0x48B7, 0x609F, 0x2D87, 0x4B87, 0x690F, 0x3993, 0x6933, 0x6393, 0x6955, 0x5995, 0x6595,
+ 0xEB14, 0xED12, 0xF906, 0xE1B4, 0xE1D2, 0xF096, 0xC99C, 0xCC96, 0xC9C6, 0xAA96, 0xA99A, 0xA9A6,
+ 0x14EB, 0x12ED, 0x06F9, 0x1E4B, 0x1E2D, 0x0F69, 0x3663, 0x3369, 0x3639, 0x5569, 0x5665, 0x5659,
+ 0x7D82, 0x7B84, 0x6F90, 0x78D2, 0x78B4, 0x69F0, 0x6CC6, 0x69CC, 0x6C9C, 0x69AA, 0x6AA6, 0x6A9A,
+ 0x827D, 0x847B, 0x906F, 0x872D, 0x874B, 0x960F, 0x9339, 0x9633, 0x9363, 0x9655, 0x9559, 0x9565,
+ 0xBE41, 0xDE21, 0xF609, 0xB4E1, 0xD2E1, 0xF069, 0x9CC9, 0xCC69, 0xC6C9, 0xAA69, 0x9AA9, 0xA6A9,
+ 0x41BE, 0x21DE, 0x09F6, 0x4B1E, 0x2D1E, 0x0F96, 0x6336, 0x3396, 0x3936, 0x5596, 0x6556, 0x5956
+};
+
+unsigned s_Classes4b[384] = {
+ 0x35C0, 0x53A0, 0x1DC0, 0x4788, 0x2788, 0x1BA0, 0x3C50, 0x5A30, 0x1CD0, 0x4878, 0x2878, 0x1AB0,
+ 0x34C4, 0x606C, 0x3C44, 0x660C, 0x268C, 0x286C, 0x606A, 0x52A2, 0x486A, 0x468A, 0x660A, 0x5A22,
+ 0x3AC0, 0x5CA0, 0x2EC0, 0x7488, 0x7288, 0x4EA0, 0x3CA0, 0x5AC0, 0x2CE0, 0x7848, 0x7828, 0x4AE0,
+ 0x38C8, 0x6C60, 0x3C88, 0x66C0, 0x62C8, 0x6C28, 0x6A60, 0x58A8, 0x6A48, 0x64A8, 0x66A0, 0x5A88,
+ 0xC530, 0xA350, 0xD10C, 0x8B44, 0x8D22, 0xB10A, 0xC350, 0xA530, 0xD01C, 0x84B4, 0x82D2, 0xB01A,
+ 0xC434, 0x909C, 0xC344, 0x990C, 0x8C26, 0x82C6, 0x909A, 0xA252, 0x84A6, 0x8A46, 0x990A, 0xA522,
+ 0xCA30, 0xAC50, 0xE20C, 0xB844, 0xD822, 0xE40A, 0xC3A0, 0xA5C0, 0xE02C, 0xB484, 0xD282, 0xE04A,
+ 0xC838, 0x9C90, 0xC388, 0x99C0, 0xC862, 0xC682, 0x9A90, 0xA858, 0xA684, 0xA864, 0x99A0, 0xA588,
+ 0x530C, 0x350A, 0x4730, 0x1D22, 0x1B44, 0x2750, 0x503C, 0x305A, 0x4370, 0x12D2, 0x14B4, 0x2570,
+ 0x434C, 0x06C6, 0x443C, 0x0C66, 0x194C, 0x149C, 0x06A6, 0x252A, 0x129A, 0x192A, 0x0A66, 0x225A,
+ 0xA30C, 0xC50A, 0x8B30, 0xD122, 0xB144, 0x8D50, 0xA03C, 0xC05A, 0x83B0, 0xD212, 0xB414, 0x85D0,
+ 0x838C, 0xC606, 0x883C, 0xC066, 0x91C4, 0x9C14, 0xA606, 0x858A, 0x9A12, 0x91A2, 0xA066, 0x885A,
+ 0x5C03, 0x3A05, 0x7403, 0x2E11, 0x4E11, 0x7205, 0x50C3, 0x30A5, 0x7043, 0x21E1, 0x41E1, 0x7025,
+ 0x4C43, 0x09C9, 0x44C3, 0x0C99, 0x4C19, 0x41C9, 0x09A9, 0x2A25, 0x21A9, 0x2A19, 0x0A99, 0x22A5,
+ 0xAC03, 0xCA05, 0xB803, 0xE211, 0xE411, 0xD805, 0xA0C3, 0xC0A5, 0xB083, 0xE121, 0xE141, 0xD085,
+ 0x8C83, 0xC909, 0x88C3, 0xC099, 0xC491, 0xC941, 0xA909, 0x8A85, 0xA921, 0xA291, 0xA099, 0x88A5,
+ 0xC035, 0xA053, 0xC01D, 0x8847, 0x8827, 0xA01B, 0xC305, 0xA503, 0xC10D, 0x8487, 0x8287, 0xA10B,
+ 0xC131, 0x9093, 0xC311, 0x9903, 0x8923, 0x8293, 0x9095, 0xA151, 0x8495, 0x8945, 0x9905, 0xA511,
+ 0xC03A, 0xA05C, 0xC02E, 0x8874, 0x8872, 0xA04E, 0xC30A, 0xA50C, 0xC20E, 0x8784, 0x8782, 0xA40E,
+ 0xC232, 0x9390, 0xC322, 0x9930, 0x9832, 0x9382, 0x9590, 0xA454, 0x9584, 0x9854, 0x9950, 0xA544,
+ 0x30C5, 0x50A3, 0x0CD1, 0x448B, 0x228D, 0x0AB1, 0x3C05, 0x5A03, 0x0DC1, 0x484B, 0x282D, 0x0BA1,
+ 0x31C1, 0x6063, 0x3C11, 0x6603, 0x2389, 0x2839, 0x6065, 0x51A1, 0x4859, 0x4589, 0x6605, 0x5A11,
+ 0x30CA, 0x50AC, 0x0CE2, 0x44B8, 0x22D8, 0x0AE4, 0x3C0A, 0x5A0C, 0x0EC2, 0x4B48, 0x2D28, 0x0EA4,
+ 0x32C2, 0x6360, 0x3C22, 0x6630, 0x3298, 0x3928, 0x6560, 0x54A4, 0x5948, 0x5498, 0x6650, 0x5A44,
+ 0x0C53, 0x0A35, 0x3047, 0x221D, 0x441B, 0x5027, 0x05C3, 0x03A5, 0x3407, 0x212D, 0x414B, 0x5207,
+ 0x1C13, 0x0939, 0x11C3, 0x0399, 0x4613, 0x4163, 0x0959, 0x1A15, 0x2165, 0x2615, 0x0599, 0x11A5,
+ 0x0CA3, 0x0AC5, 0x308B, 0x22D1, 0x44B1, 0x508D, 0x0AC3, 0x0CA5, 0x380B, 0x2D21, 0x4B41, 0x580D,
+ 0x2C23, 0x3909, 0x22C3, 0x3099, 0x6431, 0x6341, 0x5909, 0x4A45, 0x6521, 0x6251, 0x5099, 0x44A5,
+ 0x035C, 0x053A, 0x0374, 0x112E, 0x114E, 0x0572, 0x053C, 0x035A, 0x0734, 0x121E, 0x141E, 0x0752,
+ 0x131C, 0x0636, 0x113C, 0x0366, 0x1346, 0x1436, 0x0656, 0x151A, 0x1256, 0x1526, 0x0566, 0x115A,
+ 0x03AC, 0x05CA, 0x03B8, 0x11E2, 0x11E4, 0x05D8, 0x0A3C, 0x0C5A, 0x0B38, 0x1E12, 0x1E14, 0x0D58,
+ 0x232C, 0x3606, 0x223C, 0x3066, 0x3164, 0x3614, 0x5606, 0x454A, 0x5612, 0x5162, 0x5066, 0x445A
+};
+
+unsigned s_Classes4c[768] = {
+ 0x35C0, 0x53A0, 0x1DC0, 0x4788, 0x2788, 0x1BA0, 0x3C50, 0x5A30, 0x1CD0, 0x4878, 0x2878, 0x1AB0,
+ 0x34C4, 0x606C, 0x3C44, 0x660C, 0x268C, 0x286C, 0x606A, 0x52A2, 0x486A, 0x468A, 0x660A, 0x5A22,
+ 0xCA3F, 0xAC5F, 0xE23F, 0xB877, 0xD877, 0xE45F, 0xC3AF, 0xA5CF, 0xE32F, 0xB787, 0xD787, 0xE54F,
+ 0xCB3B, 0x9F93, 0xC3BB, 0x99F3, 0xD973, 0xD793, 0x9F95, 0xAD5D, 0xB795, 0xB975, 0x99F5, 0xA5DD,
+ 0x3AC0, 0x5CA0, 0x2EC0, 0x7488, 0x7288, 0x4EA0, 0x3CA0, 0x5AC0, 0x2CE0, 0x7848, 0x7828, 0x4AE0,
+ 0x38C8, 0x6C60, 0x3C88, 0x66C0, 0x62C8, 0x6C28, 0x6A60, 0x58A8, 0x6A48, 0x64A8, 0x66A0, 0x5A88,
+ 0xC53F, 0xA35F, 0xD13F, 0x8B77, 0x8D77, 0xB15F, 0xC35F, 0xA53F, 0xD31F, 0x87B7, 0x87D7, 0xB51F,
+ 0xC737, 0x939F, 0xC377, 0x993F, 0x9D37, 0x93D7, 0x959F, 0xA757, 0x95B7, 0x9B57, 0x995F, 0xA577,
+ 0xC530, 0xA350, 0xD10C, 0x8B44, 0x8D22, 0xB10A, 0xC350, 0xA530, 0xD01C, 0x84B4, 0x82D2, 0xB01A,
+ 0xC434, 0x909C, 0xC344, 0x990C, 0x8C26, 0x82C6, 0x909A, 0xA252, 0x84A6, 0x8A46, 0x990A, 0xA522,
+ 0x3ACF, 0x5CAF, 0x2EF3, 0x74BB, 0x72DD, 0x4EF5, 0x3CAF, 0x5ACF, 0x2FE3, 0x7B4B, 0x7D2D, 0x4FE5,
+ 0x3BCB, 0x6F63, 0x3CBB, 0x66F3, 0x73D9, 0x7D39, 0x6F65, 0x5DAD, 0x7B59, 0x75B9, 0x66F5, 0x5ADD,
+ 0xCA30, 0xAC50, 0xE20C, 0xB844, 0xD822, 0xE40A, 0xC3A0, 0xA5C0, 0xE02C, 0xB484, 0xD282, 0xE04A,
+ 0xC838, 0x9C90, 0xC388, 0x99C0, 0xC862, 0xC682, 0x9A90, 0xA858, 0xA684, 0xA864, 0x99A0, 0xA588,
+ 0x35CF, 0x53AF, 0x1DF3, 0x47BB, 0x27DD, 0x1BF5, 0x3C5F, 0x5A3F, 0x1FD3, 0x4B7B, 0x2D7D, 0x1FB5,
+ 0x37C7, 0x636F, 0x3C77, 0x663F, 0x379D, 0x397D, 0x656F, 0x57A7, 0x597B, 0x579B, 0x665F, 0x5A77,
+ 0x530C, 0x350A, 0x4730, 0x1D22, 0x1B44, 0x2750, 0x503C, 0x305A, 0x4370, 0x12D2, 0x14B4, 0x2570,
+ 0x434C, 0x06C6, 0x443C, 0x0C66, 0x194C, 0x149C, 0x06A6, 0x252A, 0x129A, 0x192A, 0x0A66, 0x225A,
+ 0xACF3, 0xCAF5, 0xB8CF, 0xE2DD, 0xE4BB, 0xD8AF, 0xAFC3, 0xCFA5, 0xBC8F, 0xED2D, 0xEB4B, 0xDA8F,
+ 0xBCB3, 0xF939, 0xBBC3, 0xF399, 0xE6B3, 0xEB63, 0xF959, 0xDAD5, 0xED65, 0xE6D5, 0xF599, 0xDDA5,
+ 0xA30C, 0xC50A, 0x8B30, 0xD122, 0xB144, 0x8D50, 0xA03C, 0xC05A, 0x83B0, 0xD212, 0xB414, 0x85D0,
+ 0x838C, 0xC606, 0x883C, 0xC066, 0x91C4, 0x9C14, 0xA606, 0x858A, 0x9A12, 0x91A2, 0xA066, 0x885A,
+ 0x5CF3, 0x3AF5, 0x74CF, 0x2EDD, 0x4EBB, 0x72AF, 0x5FC3, 0x3FA5, 0x7C4F, 0x2DED, 0x4BEB, 0x7A2F,
+ 0x7C73, 0x39F9, 0x77C3, 0x3F99, 0x6E3B, 0x63EB, 0x59F9, 0x7A75, 0x65ED, 0x6E5D, 0x5F99, 0x77A5,
+ 0x5C03, 0x3A05, 0x7403, 0x2E11, 0x4E11, 0x7205, 0x50C3, 0x30A5, 0x7043, 0x21E1, 0x41E1, 0x7025,
+ 0x4C43, 0x09C9, 0x44C3, 0x0C99, 0x4C19, 0x41C9, 0x09A9, 0x2A25, 0x21A9, 0x2A19, 0x0A99, 0x22A5,
+ 0xA3FC, 0xC5FA, 0x8BFC, 0xD1EE, 0xB1EE, 0x8DFA, 0xAF3C, 0xCF5A, 0x8FBC, 0xDE1E, 0xBE1E, 0x8FDA,
+ 0xB3BC, 0xF636, 0xBB3C, 0xF366, 0xB3E6, 0xBE36, 0xF656, 0xD5DA, 0xDE56, 0xD5E6, 0xF566, 0xDD5A,
+ 0xAC03, 0xCA05, 0xB803, 0xE211, 0xE411, 0xD805, 0xA0C3, 0xC0A5, 0xB083, 0xE121, 0xE141, 0xD085,
+ 0x8C83, 0xC909, 0x88C3, 0xC099, 0xC491, 0xC941, 0xA909, 0x8A85, 0xA921, 0xA291, 0xA099, 0x88A5,
+ 0x53FC, 0x35FA, 0x47FC, 0x1DEE, 0x1BEE, 0x27FA, 0x5F3C, 0x3F5A, 0x4F7C, 0x1EDE, 0x1EBE, 0x2F7A,
+ 0x737C, 0x36F6, 0x773C, 0x3F66, 0x3B6E, 0x36BE, 0x56F6, 0x757A, 0x56DE, 0x5D6E, 0x5F66, 0x775A,
+ 0xC035, 0xA053, 0xC01D, 0x8847, 0x8827, 0xA01B, 0xC305, 0xA503, 0xC10D, 0x8487, 0x8287, 0xA10B,
+ 0xC131, 0x9093, 0xC311, 0x9903, 0x8923, 0x8293, 0x9095, 0xA151, 0x8495, 0x8945, 0x9905, 0xA511,
+ 0x3FCA, 0x5FAC, 0x3FE2, 0x77B8, 0x77D8, 0x5FE4, 0x3CFA, 0x5AFC, 0x3EF2, 0x7B78, 0x7D78, 0x5EF4,
+ 0x3ECE, 0x6F6C, 0x3CEE, 0x66FC, 0x76DC, 0x7D6C, 0x6F6A, 0x5EAE, 0x7B6A, 0x76BA, 0x66FA, 0x5AEE,
+ 0xC03A, 0xA05C, 0xC02E, 0x8874, 0x8872, 0xA04E, 0xC30A, 0xA50C, 0xC20E, 0x8784, 0x8782, 0xA40E,
+ 0xC232, 0x9390, 0xC322, 0x9930, 0x9832, 0x9382, 0x9590, 0xA454, 0x9584, 0x9854, 0x9950, 0xA544,
+ 0x3FC5, 0x5FA3, 0x3FD1, 0x778B, 0x778D, 0x5FB1, 0x3CF5, 0x5AF3, 0x3DF1, 0x787B, 0x787D, 0x5BF1,
+ 0x3DCD, 0x6C6F, 0x3CDD, 0x66CF, 0x67CD, 0x6C7D, 0x6A6F, 0x5BAB, 0x6A7B, 0x67AB, 0x66AF, 0x5ABB,
+ 0x30C5, 0x50A3, 0x0CD1, 0x448B, 0x228D, 0x0AB1, 0x3C05, 0x5A03, 0x0DC1, 0x484B, 0x282D, 0x0BA1,
+ 0x31C1, 0x6063, 0x3C11, 0x6603, 0x2389, 0x2839, 0x6065, 0x51A1, 0x4859, 0x4589, 0x6605, 0x5A11,
+ 0xCF3A, 0xAF5C, 0xF32E, 0xBB74, 0xDD72, 0xF54E, 0xC3FA, 0xA5FC, 0xF23E, 0xB7B4, 0xD7D2, 0xF45E,
+ 0xCE3E, 0x9F9C, 0xC3EE, 0x99FC, 0xDC76, 0xD7C6, 0x9F9A, 0xAE5E, 0xB7A6, 0xBA76, 0x99FA, 0xA5EE,
+ 0x30CA, 0x50AC, 0x0CE2, 0x44B8, 0x22D8, 0x0AE4, 0x3C0A, 0x5A0C, 0x0EC2, 0x4B48, 0x2D28, 0x0EA4,
+ 0x32C2, 0x6360, 0x3C22, 0x6630, 0x3298, 0x3928, 0x6560, 0x54A4, 0x5948, 0x5498, 0x6650, 0x5A44,
+ 0xCF35, 0xAF53, 0xF31D, 0xBB47, 0xDD27, 0xF51B, 0xC3F5, 0xA5F3, 0xF13D, 0xB4B7, 0xD2D7, 0xF15B,
+ 0xCD3D, 0x9C9F, 0xC3DD, 0x99CF, 0xCD67, 0xC6D7, 0x9A9F, 0xAB5B, 0xA6B7, 0xAB67, 0x99AF, 0xA5BB,
+ 0x0C53, 0x0A35, 0x3047, 0x221D, 0x441B, 0x5027, 0x05C3, 0x03A5, 0x3407, 0x212D, 0x414B, 0x5207,
+ 0x1C13, 0x0939, 0x11C3, 0x0399, 0x4613, 0x4163, 0x0959, 0x1A15, 0x2165, 0x2615, 0x0599, 0x11A5,
+ 0xF3AC, 0xF5CA, 0xCFB8, 0xDDE2, 0xBBE4, 0xAFD8, 0xFA3C, 0xFC5A, 0xCBF8, 0xDED2, 0xBEB4, 0xADF8,
+ 0xE3EC, 0xF6C6, 0xEE3C, 0xFC66, 0xB9EC, 0xBE9C, 0xF6A6, 0xE5EA, 0xDE9A, 0xD9EA, 0xFA66, 0xEE5A,
+ 0x0CA3, 0x0AC5, 0x308B, 0x22D1, 0x44B1, 0x508D, 0x0AC3, 0x0CA5, 0x380B, 0x2D21, 0x4B41, 0x580D,
+ 0x2C23, 0x3909, 0x22C3, 0x3099, 0x6431, 0x6341, 0x5909, 0x4A45, 0x6521, 0x6251, 0x5099, 0x44A5,
+ 0xF35C, 0xF53A, 0xCF74, 0xDD2E, 0xBB4E, 0xAF72, 0xF53C, 0xF35A, 0xC7F4, 0xD2DE, 0xB4BE, 0xA7F2,
+ 0xD3DC, 0xC6F6, 0xDD3C, 0xCF66, 0x9BCE, 0x9CBE, 0xA6F6, 0xB5BA, 0x9ADE, 0x9DAE, 0xAF66, 0xBB5A,
+ 0x035C, 0x053A, 0x0374, 0x112E, 0x114E, 0x0572, 0x053C, 0x035A, 0x0734, 0x121E, 0x141E, 0x0752,
+ 0x131C, 0x0636, 0x113C, 0x0366, 0x1346, 0x1436, 0x0656, 0x151A, 0x1256, 0x1526, 0x0566, 0x115A,
+ 0xFCA3, 0xFAC5, 0xFC8B, 0xEED1, 0xEEB1, 0xFA8D, 0xFAC3, 0xFCA5, 0xF8CB, 0xEDE1, 0xEBE1, 0xF8AD,
+ 0xECE3, 0xF9C9, 0xEEC3, 0xFC99, 0xECB9, 0xEBC9, 0xF9A9, 0xEAE5, 0xEDA9, 0xEAD9, 0xFA99, 0xEEA5,
+ 0x03AC, 0x05CA, 0x03B8, 0x11E2, 0x11E4, 0x05D8, 0x0A3C, 0x0C5A, 0x0B38, 0x1E12, 0x1E14, 0x0D58,
+ 0x232C, 0x3606, 0x223C, 0x3066, 0x3164, 0x3614, 0x5606, 0x454A, 0x5612, 0x5162, 0x5066, 0x445A,
+ 0xFC53, 0xFA35, 0xFC47, 0xEE1D, 0xEE1B, 0xFA27, 0xF5C3, 0xF3A5, 0xF4C7, 0xE1ED, 0xE1EB, 0xF2A7,
+ 0xDCD3, 0xC9F9, 0xDDC3, 0xCF99, 0xCE9B, 0xC9EB, 0xA9F9, 0xBAB5, 0xA9ED, 0xAE9D, 0xAF99, 0xBBA5
+};
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+ Synopsis [Computes NPN-canonical form using brute-force methods.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Extra_TruthCanonNPN2( unsigned uTruth, int nVars, Vec_Int_t * vRes )
+{
+ static int nVarsOld, nPerms;
+ static char ** pPerms = NULL;
+
+ unsigned uTruthMin, uTruthC, uPhase, uPerm;
+ int nMints, k, i;
+
+ if ( pPerms == NULL )
+ {
+ nPerms = Extra_Factorial( nVars );
+ pPerms = Extra_Permutations( nVars );
+ nVarsOld = nVars;
+ }
+ else if ( nVarsOld != nVars )
+ {
+ ABC_FREE( pPerms );
+ nPerms = Extra_Factorial( nVars );
+ pPerms = Extra_Permutations( nVars );
+ nVarsOld = nVars;
+ }
+
+ nMints = (1 << nVars);
+ uTruthC = (unsigned)( (~uTruth) & ((~((unsigned)0)) >> (32-nMints)) );
+ uTruthMin = 0xFFFFFFFF;
+ for ( i = 0; i < nMints; i++ )
+ {
+ uPhase = Extra_TruthPolarize( uTruth, i, nVars );
+ for ( k = 0; k < nPerms; k++ )
+ {
+ uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 );
+ Vec_IntPushUnique( vRes, uPerm );
+ if ( uTruthMin > uPerm )
+ uTruthMin = uPerm;
+ }
+ uPhase = Extra_TruthPolarize( uTruthC, i, nVars );
+ for ( k = 0; k < nPerms; k++ )
+ {
+ uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 );
+ Vec_IntPushUnique( vRes, uPerm );
+ if ( uTruthMin > uPerm )
+ uTruthMin = uPerm;
+ }
+ }
+ return uTruthMin;
+}
+
+void Acec_MultFuncTest5()
+{
+ Vec_Int_t * vRes = Vec_IntAlloc( 1000 );
+ int i, Entry;
+
+ unsigned Truth = 0xF335ACC0;
+ unsigned Canon = Extra_TruthCanonNPN2( Truth, 5, vRes );
+
+ Extra_PrintHex( stdout, (unsigned*)&Truth, 5 ); printf( "\n" );
+ Extra_PrintHex( stdout, (unsigned*)&Canon, 5 ); printf( "\n" );
+
+ printf( "Members = %d.\n", Vec_IntSize(vRes) );
+ Vec_IntForEachEntry( vRes, Entry, i )
+ {
+ Extra_PrintHex( stdout, (unsigned*)&Entry, 5 );
+ printf( ", " );
+ if ( i % 8 == 7 )
+ printf( "\n" );
+ }
+
+ Vec_IntFree( vRes );
+}
+
+void Acec_MultFuncTest4()
+{
+ Vec_Int_t * vRes = Vec_IntAlloc( 1000 );
+ int i, Entry;
+
+ unsigned Truth = 0x35C0;
+ //unsigned Truth = 0xD728;
+ unsigned Canon = Extra_TruthCanonNPN2( Truth, 4, vRes );
+
+ Extra_PrintHex( stdout, (unsigned*)&Truth, 4 ); printf( "\n" );
+ Extra_PrintHex( stdout, (unsigned*)&Canon, 4 ); printf( "\n" );
+
+ printf( "Members = %d.\n", Vec_IntSize(vRes) );
+ Vec_IntForEachEntry( vRes, Entry, i )
+ {
+ Extra_PrintHex( stdout, (unsigned*)&Entry, 4 );
+ printf( ", " );
+ if ( i % 12 == 11 )
+ printf( "\n" );
+ }
+
+ Vec_IntFree( vRes );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Acec_MultCollectInputs( Vec_Int_t * vPairs, Vec_Int_t * vRanks, int iObj )
+{
+ Vec_Int_t * vItems = Vec_IntAlloc( 100 );
+ int k, iObj1, iObj2;
+ // collect all those appearing with this one
+ Vec_IntForEachEntryDouble( vPairs, iObj1, iObj2, k )
+ if ( iObj == iObj1 )
+ Vec_IntPushUnique( vItems, iObj2 );
+ else if ( iObj == iObj2 )
+ Vec_IntPushUnique( vItems, iObj1 );
+ // sort items by rank cost
+ Vec_IntSelectSortCost( Vec_IntArray(vItems), Vec_IntSize(vItems), vRanks );
+ return vItems;
+}
+Vec_Int_t * Acec_MultDetectInputs1( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits )
+{
+ Vec_Int_t * vInputs = Vec_IntAlloc( 100 );
+ Vec_Int_t * vCounts = Vec_IntStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vRanks = Vec_IntStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vPairs = Vec_IntAlloc( 100 );
+ Vec_Int_t * vItems = Vec_IntAlloc( 100 );
+ Vec_Int_t * vItems0;
+ Vec_Int_t * vItems1;
+ Vec_Int_t * vLevel;
+ int i, k, iLit, iObj, Count;
+ // count how many times each input appears
+ Vec_WecForEachLevel( vLeafLits, vLevel, i )
+ Vec_IntForEachEntry( vLevel, iLit, k )
+ {
+ iObj = Abc_Lit2Var(iLit);
+ Vec_IntAddToEntry( vCounts, Gia_ObjFaninId0(Gia_ManObj(p, iObj), iObj), 1 );
+ Vec_IntAddToEntry( vCounts, Gia_ObjFaninId1(Gia_ManObj(p, iObj), iObj), 1 );
+/*
+ printf( "Rank %2d : Leaf = %4d : (%2d, %2d)\n", i, iObj,
+ Gia_ObjFaninId0(Gia_ManObj(p, iObj), iObj), Gia_ObjFaninId1(Gia_ManObj(p, iObj), iObj) );
+ if ( k == Vec_IntSize(vLevel) - 1 )
+ printf( "\n" );
+*/
+ }
+ // count ranks for each one
+ Vec_WecForEachLevel( vLeafLits, vLevel, i )
+ Vec_IntForEachEntry( vLevel, iLit, k )
+ {
+ iObj = Abc_Lit2Var(iLit);
+ if ( Vec_IntEntry(vCounts, Gia_ObjFaninId0(Gia_ManObj(p, iObj), iObj)) < 2 )
+ {
+ printf( "Skipping %d.\n", iObj );
+ continue;
+ }
+ if ( Vec_IntEntry(vCounts, Gia_ObjFaninId1(Gia_ManObj(p, iObj), iObj)) < 2 )
+ {
+ printf( "Skipping %d.\n", iObj );
+ continue;
+ }
+ Vec_IntAddToEntry( vRanks, Gia_ObjFaninId0(Gia_ManObj(p, iObj), iObj), i );
+ Vec_IntAddToEntry( vRanks, Gia_ObjFaninId1(Gia_ManObj(p, iObj), iObj), i );
+
+ Vec_IntPushTwo( vPairs, Gia_ObjFaninId0(Gia_ManObj(p, iObj), iObj), Gia_ObjFaninId1(Gia_ManObj(p, iObj), iObj) );
+ }
+
+ // print statistics
+ Vec_IntForEachEntry( vCounts, Count, i )
+ {
+ if ( !Count )
+ continue;
+ if ( !Vec_IntEntry(vRanks, i) )
+ continue;
+ Vec_IntPush( vItems, i );
+ printf( "Obj = %3d Occurs = %3d Ranks = %3d\n", i, Count, Vec_IntEntry(vRanks, i) );
+ }
+ // sort items by rank cost
+ Vec_IntSelectSortCost( Vec_IntArray(vItems), Vec_IntSize(vItems), vRanks );
+ // collect all those appearing with the last one
+ vItems0 = Acec_MultCollectInputs( vPairs, vRanks, Vec_IntEntryLast(vItems) );
+ Vec_IntAppend( vInputs, vItems0 );
+ // collect all those appearing with the last one
+ vItems1 = Acec_MultCollectInputs( vPairs, vRanks, Vec_IntEntryLast(vItems0) );
+ Vec_IntAppend( vInputs, vItems1 );
+
+ Vec_IntPrint( vItems0 );
+ Vec_IntPrint( vItems1 );
+
+ Vec_IntFree( vCounts );
+ Vec_IntFree( vRanks );
+ Vec_IntFree( vPairs );
+ Vec_IntFree( vItems );
+ Vec_IntFree( vItems0 );
+ Vec_IntFree( vItems1 );
+ return vInputs;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits )
+{
+ Vec_Int_t * vInputs = Vec_IntAlloc( 100 );
+ Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
+ Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vRanks = Vec_IntStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vCounts = Vec_IntStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vLevel;
+ int i, k, iLit, iObj, j, Entry;
+
+ ABC_FREE( p->pRefs );
+ Gia_ManCreateRefs( p );
+ Gia_ManForEachCiId( p, iObj, i )
+ printf( "%d=%d ", iObj, Gia_ObjRefNumId(p, iObj) );
+ printf( "\n" );
+ Gia_ManForEachAndId( p, iObj )
+ if ( Gia_ObjRefNumId(p, iObj) >= 4 )
+ printf( "%d=%d ", iObj, Gia_ObjRefNumId(p, iObj) );
+ printf( "\n" );
+
+ Vec_WecForEachLevel( vLeafLits, vLevel, i )
+ Vec_IntForEachEntry( vLevel, iLit, k )
+ {
+ word Truth = Gia_ObjComputeTruth6Cis( p, iLit, vSupp, vTemp );
+ if ( Vec_IntSize(vSupp) >= 0 )
+ {
+ printf( "Leaf = %4d : ", Abc_Lit2Var(iLit) );
+ printf( "Rank = %2d ", i );
+ printf( "Supp = %2d ", Vec_IntSize(vSupp) );
+ Extra_PrintHex( stdout, (unsigned*)&Truth, Vec_IntSize(vSupp) );
+ if ( Vec_IntSize(vSupp) == 4 ) printf( " " );
+ if ( Vec_IntSize(vSupp) == 3 ) printf( " " );
+ if ( Vec_IntSize(vSupp) <= 2 ) printf( " " );
+ printf( " " );
+ Vec_IntPrint( vSupp );
+ /*
+ if ( Truth == 0xF335ACC0F335ACC0 )
+ {
+ int iObj = Abc_Lit2Var(iLit);
+ Gia_Man_t * pGia0 = Gia_ManDupAndCones( p, &iObj, 1, 1 );
+ Gia_ManShow( pGia0, NULL, 0, 0, 0 );
+ Gia_ManStop( pGia0 );
+ }
+ */
+ }
+ // support rank counts
+ Vec_IntForEachEntry( vSupp, Entry, j )
+ {
+ Vec_IntAddToEntry( vRanks, Entry, i );
+ Vec_IntAddToEntry( vCounts, Entry, 1 );
+ }
+ if ( k == Vec_IntSize(vLevel)-1 )
+ printf( "\n" );
+ }
+
+ Vec_IntForEachEntry( vCounts, Entry, j )
+ if ( Entry )
+ printf( "%d=%d(%.2f) ", j, Entry, 1.0*Vec_IntEntry(vRanks, j)/Entry );
+ printf( "\n" );
+
+ Vec_IntFree( vSupp );
+ Vec_WrdFree( vTemp );
+ Vec_IntFree( vRanks );
+ Vec_IntFree( vCounts );
+ return vInputs;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Acec_MultFindPPs_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vBold )
+{
+ Gia_Obj_t * pObj;
+ pObj = Gia_ManObj( p, iObj );
+ if ( pObj->fMark0 )
+ return;
+ pObj->fMark0 = 1;
+ if ( !Gia_ObjIsAnd(pObj) )
+ return;
+ Acec_MultFindPPs_rec( p, Gia_ObjFaninId0(pObj, iObj), vBold );
+ Acec_MultFindPPs_rec( p, Gia_ObjFaninId1(pObj, iObj), vBold );
+ Vec_IntPush( vBold, iObj );
+}
+Vec_Int_t * Acec_MultFindPPs( Gia_Man_t * p )
+{
+ word Saved[32] = {
+ ABC_CONST(0xF335ACC0F335ACC0),
+ ABC_CONST(0x35C035C035C035C0),
+ ABC_CONST(0xD728D728D728D728),
+ ABC_CONST(0xFD80FD80FD80FD80),
+ ABC_CONST(0xACC0ACC0ACC0ACC0),
+ ABC_CONST(0x7878787878787878),
+ ABC_CONST(0x2828282828282828),
+ ABC_CONST(0xD0D0D0D0D0D0D0D0),
+ ABC_CONST(0x8080808080808080),
+ ABC_CONST(0x8888888888888888),
+ ABC_CONST(0xAAAAAAAAAAAAAAAA),
+ ABC_CONST(0x5555555555555555),
+
+ ABC_CONST(0xD5A8D5A8D5A8D5A8),
+ ABC_CONST(0x2A572A572A572A57),
+ ABC_CONST(0xF3C0F3C0F3C0F3C0),
+ ABC_CONST(0x5858585858585858),
+ ABC_CONST(0xA7A7A7A7A7A7A7A7),
+ ABC_CONST(0x2727272727272727),
+ ABC_CONST(0xD8D8D8D8D8D8D8D8)
+ };
+
+ Vec_Int_t * vBold = Vec_IntAlloc( 100 );
+ Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
+ Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+ int i, iObj, nProds = 0;
+ Gia_ManCleanMark0(p);
+ Gia_ManForEachAndId( p, iObj )
+ {
+ word Truth = Gia_ObjComputeTruth6Cis( p, Abc_Var2Lit(iObj, 0), vSupp, vTemp );
+ if ( Vec_IntSize(vSupp) > 6 )
+ continue;
+ vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize );
+ if ( Vec_IntSize(vSupp) > 5 )
+ continue;
+ for ( i = 0; i < 32 && Saved[i]; i++ )
+ {
+ if ( Truth == Saved[i] || Truth == ~Saved[i] )
+ {
+ Acec_MultFindPPs_rec( p, iObj, vBold );
+ nProds++;
+ break;
+ }
+ }
+ /*
+ if ( Saved[i] )
+ {
+ printf( "Obj = %4d ", iObj );
+ Extra_PrintHex( stdout, (unsigned*)&Truth, Vec_IntSize(vSupp) );
+ if ( Vec_IntSize(vSupp) == 4 ) printf( " " );
+ if ( Vec_IntSize(vSupp) == 3 ) printf( " " );
+ if ( Vec_IntSize(vSupp) <= 2 ) printf( " " );
+ printf( " " );
+ Vec_IntPrint( vSupp );
+ }
+ */
+ }
+ Gia_ManCleanMark0(p);
+ printf( "Collected %d pps and %d nodes.\n", nProds, Vec_IntSize(vBold) );
+
+ Vec_IntFree( vSupp );
+ Vec_WrdFree( vTemp );
+ return vBold;
+}
+Vec_Bit_t * Acec_BoothFindPPG( Gia_Man_t * p )
+{
+ Vec_Bit_t * vIgnore = Vec_BitStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vMap = Acec_MultFindPPs( p );
+ int i, Entry;
+ Vec_IntForEachEntry( vMap, Entry, i )
+ Vec_BitWriteEntry( vIgnore, Entry, 1 );
+ Vec_IntFree( vMap );
+ return vIgnore;
+}
+void Acec_MultFindPPsTest( Gia_Man_t * p )
+{
+ Vec_Int_t * vBold = Acec_MultFindPPs( p );
+ Gia_ManShow( p, vBold, 1, 0, 0 );
+ Vec_IntFree( vBold );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecNorm.c b/src/proof/acec/acecNorm.c
new file mode 100644
index 00000000..f2acb37b
--- /dev/null
+++ b/src/proof/acec/acecNorm.c
@@ -0,0 +1,226 @@
+/**CFile****************************************************************
+
+ FileName [acecNorm.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [CEC for arithmetic circuits.]
+
+ Synopsis [Adder tree normalization.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: acecNorm.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 []
+
+***********************************************************************/
+void Acec_InsertHadd( Gia_Man_t * pNew, int In[2], int Out[2] )
+{
+ int And, Or;
+ Out[1] = Gia_ManAppendAnd2( pNew, In[0], In[1] );
+ And = Gia_ManAppendAnd2( pNew, Abc_LitNot(In[0]), Abc_LitNot(In[1]) );
+ Or = Gia_ManAppendOr2( pNew, Out[1], And );
+ Out[0] = Abc_LitNot( Or );
+}
+void Acec_InsertFadd( Gia_Man_t * pNew, int In[3], int Out[2] )
+{
+ int In2[2], Out1[2], Out2[2];
+ Acec_InsertHadd( pNew, In, Out1 );
+ In2[0] = Out1[0];
+ In2[1] = In[2];
+ Acec_InsertHadd( pNew, In2, Out2 );
+ Out[0] = Out2[0];
+ Out[1] = Gia_ManAppendOr2( pNew, Out1[1], Out2[1] );
+}
+Vec_Int_t * Acec_InsertTree( Gia_Man_t * pNew, Vec_Wec_t * vLeafMap )
+{
+ Vec_Int_t * vRootRanks = Vec_IntAlloc( Vec_WecSize(vLeafMap) + 5 );
+ Vec_Int_t * vLevel;
+ int i, In[3], Out[2];
+ Vec_WecForEachLevel( vLeafMap, vLevel, i )
+ {
+ if ( Vec_IntSize(vLevel) == 0 )
+ {
+ Vec_IntPush( vRootRanks, 0 );
+ continue;
+ }
+ while ( Vec_IntSize(vLevel) > 1 )
+ {
+ if ( Vec_IntSize(vLevel) == 2 )
+ Vec_IntPush( vLevel, 0 );
+ //In[2] = Vec_IntPop( vLevel );
+ //In[1] = Vec_IntPop( vLevel );
+ //In[0] = Vec_IntPop( vLevel );
+
+ In[0] = Vec_IntEntry( vLevel, 0 );
+ Vec_IntDrop( vLevel, 0 );
+
+ In[1] = Vec_IntEntry( vLevel, 0 );
+ Vec_IntDrop( vLevel, 0 );
+
+ In[2] = Vec_IntEntry( vLevel, 0 );
+ Vec_IntDrop( vLevel, 0 );
+
+ Acec_InsertFadd( pNew, In, Out );
+ Vec_IntPush( vLevel, Out[0] );
+ if ( i+1 < Vec_WecSize(vLeafMap) )
+ vLevel = Vec_WecEntry(vLeafMap, i+1);
+ else
+ vLevel = Vec_WecPushLevel(vLeafMap);
+ Vec_IntPush( vLevel, Out[1] );
+ vLevel = Vec_WecEntry(vLeafMap, i);
+ }
+ assert( Vec_IntSize(vLevel) == 1 );
+ Vec_IntPush( vRootRanks, Vec_IntEntry(vLevel, 0) );
+ }
+ return vRootRanks;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Acec_InsertBox_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ if ( ~pObj->Value )
+ return pObj->Value;
+ assert( Gia_ObjIsAnd(pObj) );
+ Acec_InsertBox_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Acec_InsertBox_rec( pNew, p, Gia_ObjFanin1(pObj) );
+ return (pObj->Value = Gia_ManAppendAnd2( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ));
+}
+Vec_Int_t * Acec_BuildTree( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Int_t * vRootLits )
+{
+ Vec_Wec_t * vLeafMap = Vec_WecStart( Vec_WecSize(vLeafLits) );
+ Vec_Int_t * vLevel, * vRootRanks;
+ int i, k, iLit, iLitNew;
+ // add roo literals
+ if ( vRootLits )
+ Vec_IntForEachEntry( vRootLits, iLit, i )
+ {
+ if ( i < Vec_WecSize(vLeafMap) )
+ vLevel = Vec_WecEntry(vLeafMap, i);
+ else
+ vLevel = Vec_WecPushLevel(vLeafMap);
+ Vec_IntPush( vLevel, iLit );
+ }
+ // add other literals
+ Vec_WecForEachLevel( vLeafLits, vLevel, i )
+ Vec_IntForEachEntry( vLevel, iLit, k )
+ {
+ Gia_Obj_t * pObj = Gia_ManObj( p, Abc_Lit2Var(iLit) );
+ iLitNew = Acec_InsertBox_rec( pNew, p, pObj );
+ iLitNew = Abc_LitNotCond( iLitNew, Abc_LitIsCompl(iLit) );
+ Vec_WecPush( vLeafMap, i, iLitNew );
+ }
+ // construct map of root literals
+ vRootRanks = Acec_InsertTree( pNew, vLeafMap );
+ Vec_WecFree( vLeafMap );
+ return vRootRanks;
+}
+Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll )
+{
+ Gia_Man_t * p = pBox->pGia;
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj;
+ Vec_Int_t * vRootRanks, * vLevel, * vTemp;
+ int i, k, iLit, iLitNew;
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManFillValue(p);
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachCi( p, pObj, i )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ // implement tree
+ if ( fAll )
+ vRootRanks = Acec_BuildTree( pNew, p, pBox->vLeafLits, NULL );
+ else
+ {
+ assert( pBox->vShared != NULL );
+ assert( pBox->vUnique != NULL );
+ vRootRanks = Acec_BuildTree( pNew, p, pBox->vShared, NULL );
+ vRootRanks = Acec_BuildTree( pNew, p, pBox->vUnique, vTemp = vRootRanks );
+ Vec_IntFree( vTemp );
+ }
+ // update polarity of literals
+ Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
+ Vec_IntForEachEntry( vLevel, iLit, k )
+ {
+ pObj = Gia_ManObj( p, Abc_Lit2Var(iLit) );
+ iLitNew = k ? 0 : Vec_IntEntry( vRootRanks, i );
+ pObj->Value = Abc_LitNotCond( iLitNew, Abc_LitIsCompl(iLit) );
+ }
+ Vec_IntFree( vRootRanks );
+ // construct the outputs
+ Gia_ManForEachCo( p, pObj, i )
+ Acec_InsertBox_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Gia_ManForEachCo( p, pObj, i )
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Acec_Normalize( Gia_Man_t * pGia, int fBooth, int fVerbose )
+{
+ Vec_Bit_t * vIgnore = fBooth ? Acec_BoothFindPPG( pGia ) : NULL;
+ Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, 0, 0, fVerbose );
+ Gia_Man_t * pNew = Acec_InsertBox( pBox, 1 );
+ Acec_BoxFreeP( &pBox );
+ Vec_BitFreeP( &vIgnore );
+ return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecPa.c b/src/proof/acec/acecPa.c
index ecaf2047..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;
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..5e5ca688 100644
--- a/src/proof/acec/acecRe.c
+++ b/src/proof/acec/acecRe.c
@@ -147,6 +147,7 @@ static inline int Ree_ManCutFind( int iObj, int * pCut )
}
static inline int Ree_ManCutNotFind( int iObj1, int iObj2, int * pCut )
{
+ assert( pCut[0] == 3 );
if ( pCut[3] != iObj1 && pCut[3] != iObj2 ) return 0;
if ( pCut[2] != iObj1 && pCut[2] != iObj2 ) return 1;
if ( pCut[1] != iObj1 && pCut[1] != iObj2 ) return 2;
@@ -162,13 +163,19 @@ static inline int Ree_ManCutTruthOne( int * pCut0, int * pCut )
Truth0 = fComp0 ? ~Truth0 : Truth0;
if ( pCut0[0] == 2 )
{
- int Truths[3][8] = {
- { 0x00, 0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77 }, // {0,1,-}
- { 0x00, 0x05, 0x0A, 0x0F, 0x50, 0x55, 0x5A, 0x5F }, // {0,-,1}
- { 0x00, 0x03, 0x0C, 0x0F, 0x30, 0x33, 0x3C, 0x3F } // {-,0,1}
- };
- int Truth = Truths[Ree_ManCutNotFind(pCut0[1], pCut0[2], pCut)][Truth0 & 0x7];
- return 0xFF & (fComp0 ? ~Truth : Truth);
+ if ( pCut[0] == 3 )
+ {
+ int Truths[3][8] = {
+ { 0x00, 0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77 }, // {0,1,-}
+ { 0x00, 0x05, 0x0A, 0x0F, 0x50, 0x55, 0x5A, 0x5F }, // {0,-,1}
+ { 0x00, 0x03, 0x0C, 0x0F, 0x30, 0x33, 0x3C, 0x3F } // {-,0,1}
+ };
+ int Truth = Truths[Ree_ManCutNotFind(pCut0[1], pCut0[2], pCut)][Truth0 & 0x7];
+ return 0xFF & (fComp0 ? ~Truth : Truth);
+ }
+ assert( pCut[0] == 2 );
+ assert( pCut[1] == pCut0[1] && pCut[2] == pCut0[2] );
+ return pCut0[pCut0[0]+1];
}
if ( pCut0[0] == 1 )
{
@@ -236,10 +243,10 @@ int Ree_ObjComputeTruth( Gia_Man_t * p, int iObj, int * pCut )
SeeAlso []
***********************************************************************/
-void Ree_ManCutPrint( int * pCut, int Count, word Truth )
+void Ree_ManCutPrint( int * pCut, int Count, word Truth, int iObj )
{
int c;
- printf( "%d : ", Count );
+ printf( "%d : %d : ", Count, iObj );
for ( c = 1; c <= pCut[0]; c++ )
printf( "%3d ", pCut[c] );
for ( ; c <= 4; c++ )
@@ -290,7 +297,7 @@ void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
Vec_IntPushThree( vData, iObj, Value, TruthC );
}
if ( fVerbose )
- Ree_ManCutPrint( pCut, ++Count, TruthC );
+ Ree_ManCutPrint( pCut, ++Count, TruthC, iObj );
}
if ( !vXors )
return;
@@ -370,7 +377,7 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData, int fVerbos
Vec_IntForEachEntryDouble( vXorOne, iObj, Truth, j )
Vec_IntForEachEntryDouble( vMajOne, iObj2, Truth2, k )
{
- int SignAnd[8] = {0x88, 0x44, 0x22, 0x11, 0xEE, 0xDD, 0xBB, 0x77};
+ int SignAnd[8] = {0x88, 0x44, 0x22, 0x11, 0x77, 0xBB, 0xDD, 0xEE};
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++ )
@@ -390,8 +397,18 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData, int fVerbos
Vec_WecFree( vMajMap );
return vAdds;
}
+int Ree_ManCompare( int * pCut0, int * pCut1 )
+{
+ if ( pCut0[3] < pCut1[3] ) return -1;
+ if ( pCut0[3] > pCut1[3] ) return 1;
+ if ( pCut0[4] < pCut1[4] ) return -1;
+ if ( pCut0[4] > pCut1[4] ) return 1;
+ return 0;
+}
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 );
@@ -425,11 +442,15 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose
Vec_IntFree( vTemp );
Vec_IntFree( vCuts );
vAdds = Ree_ManDeriveAdds( pHash, vData, fVerbose );
+ qsort( Vec_IntArray(vAdds), Vec_IntSize(vAdds)/6, 24, (int (*)(const void *, const void *))Ree_ManCompare );
if ( fVerbose )
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 );
+ Ree_ManRemoveTrivial( p, vAdds );
+ Ree_ManRemoveContained( p, vAdds );
+ //Ree_ManPrintAdders( vAdds, 1 );
return vAdds;
}
@@ -503,6 +524,10 @@ void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds )
{
pObjX = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+3) );
pObjM = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+4) );
+ // rule out if MAJ is a fanout of XOR
+ //if ( pObjX == Gia_ObjFanin0(pObjM) || pObjX == Gia_ObjFanin1(pObjM) )
+ // continue;
+ // rule out if MAJ is a fanin of XOR and has no other fanouts
if ( (pObjM == Gia_ObjFanin0(pObjX) || pObjM == Gia_ObjFanin1(pObjX)) && Gia_ObjRefNum(p, pObjM) == 1 )
continue;
}
diff --git a/src/proof/acec/acecSt.c b/src/proof/acec/acecSt.c
index 63aa8131..d97dadc9 100644
--- a/src/proof/acec/acecSt.c
+++ b/src/proof/acec/acecSt.c
@@ -21,6 +21,8 @@
#include "acecInt.h"
#include "misc/vec/vecWec.h"
#include "misc/extra/extra.h"
+#include "aig/aig/aig.h"
+#include "opt/dar/dar.h"
ABC_NAMESPACE_IMPL_START
diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c
new file mode 100644
index 00000000..2461c89b
--- /dev/null
+++ b/src/proof/acec/acecTree.c
@@ -0,0 +1,754 @@
+/**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 ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int Acec_SignBit( Vec_Int_t * vAdds, int iBox, int b ) { return (Vec_IntEntry(vAdds, 6*iBox+5) >> b) & 1; }
+static inline int Acec_SignBit2( Vec_Int_t * vAdds, int iBox, int b ) { return (Vec_IntEntry(vAdds, 6*iBox+5) >> (16+b)) & 1; }
+
+static inline void Acec_SignSetBit( Vec_Int_t * vAdds, int iBox, int b, int v ) { if ( v ) *Vec_IntEntryP(vAdds, 6*iBox+5) |= (1 << b); }
+static inline void Acec_SignSetBit2( Vec_Int_t * vAdds, int iBox, int b, int v ) { if ( v ) *Vec_IntEntryP(vAdds, 6*iBox+5) |= (1 << (16+b)); }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Acec_BoxFree( Acec_Box_t * pBox )
+{
+ Vec_WecFreeP( &pBox->vAdds );
+ Vec_WecFreeP( &pBox->vLeafLits );
+ Vec_WecFreeP( &pBox->vRootLits );
+ Vec_WecFreeP( &pBox->vUnique );
+ Vec_WecFreeP( &pBox->vShared );
+ ABC_FREE( pBox );
+}
+void Acec_BoxFreeP( Acec_Box_t ** ppBox )
+{
+ if ( *ppBox )
+ Acec_BoxFree( *ppBox );
+ *ppBox = NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Acec_VerifyBoxLeaves( Acec_Box_t * pBox, Vec_Bit_t * vIgnore )
+{
+ Vec_Int_t * vLevel;
+ int i, k, iLit, Count = 0;
+ if ( vIgnore == NULL )
+ return;
+ Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i )
+ Vec_IntForEachEntry( vLevel, iLit, k )
+ if ( Gia_ObjIsAnd(Gia_ManObj(pBox->pGia, Abc_Lit2Var(iLit))) && !Vec_BitEntry(vIgnore, Abc_Lit2Var(iLit)) )
+ printf( "Internal node %d of rank %d is not part of PPG.\n", Abc_Lit2Var(iLit), i ), Count++;
+ printf( "Detected %d suspicious leaves.\n", Count );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Filters trees by removing TFO of roots.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Acec_TreeFilterOne( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree )
+{
+ Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(p) );
+ Vec_Bit_t * vMarked = Vec_BitStart( Gia_ManObjNum(p) ) ;
+ Gia_Obj_t * pObj;
+ int i, k = 0, Box, Rank;
+ // mark roots
+ Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+ {
+ Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+3), 1 );
+ Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+4), 1 );
+ }
+ Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+ {
+ Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+0), 0 );
+ Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+1), 0 );
+ Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+2), 0 );
+ }
+ // iterate through nodes to detect TFO of roots
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ if ( Vec_BitEntry(vIsRoot, Gia_ObjFaninId0(pObj,i)) || Vec_BitEntry(vIsRoot, Gia_ObjFaninId1(pObj,i)) ||
+ Vec_BitEntry(vMarked, Gia_ObjFaninId0(pObj,i)) || Vec_BitEntry(vMarked, Gia_ObjFaninId1(pObj,i)) )
+ Vec_BitWriteEntry( vMarked, i, 1 );
+ }
+ // remove those that overlap with roots
+ Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+ {
+ // special case of the first bit
+// if ( i == 0 )
+// continue;
+
+/*
+ if ( Vec_IntEntry(vAdds, 6*Box+3) == 24 && Vec_IntEntry(vAdds, 6*Box+4) == 22 )
+ {
+ printf( "**** removing special one \n" );
+ continue;
+ }
+ if ( Vec_IntEntry(vAdds, 6*Box+3) == 48 && Vec_IntEntry(vAdds, 6*Box+4) == 49 )
+ {
+ printf( "**** removing special one \n" );
+ continue;
+ }
+*/
+ if ( Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+3)) || Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+4)) )
+ {
+ printf( "Removing box %d=(%d,%d) of rank %d.\n", Box, Vec_IntEntry(vAdds, 6*Box+3), Vec_IntEntry(vAdds, 6*Box+4), Rank );
+ continue;
+ }
+ Vec_IntWriteEntry( vTree, k++, Box );
+ Vec_IntWriteEntry( vTree, k++, Rank );
+ }
+ Vec_IntShrink( vTree, k );
+ Vec_BitFree( vIsRoot );
+ Vec_BitFree( vMarked );
+}
+void Acec_TreeFilterTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vTrees )
+{
+ Vec_Int_t * vLevel;
+ int i;
+ Vec_WecForEachLevel( vTrees, vLevel, i )
+ Acec_TreeFilterOne( p, vAdds, vLevel );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Filters trees by removing TFO of roots.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Acec_TreeMarkTFI_rec( Gia_Man_t * p, int Id, Vec_Bit_t * vMarked )
+{
+ Gia_Obj_t * pObj = Gia_ManObj(p, Id);
+ if ( Vec_BitEntry(vMarked, Id) )
+ return;
+ Vec_BitWriteEntry( vMarked, Id, 1 );
+ if ( !Gia_ObjIsAnd(pObj) )
+ return;
+ Acec_TreeMarkTFI_rec( p, Gia_ObjFaninId0(pObj, Id), vMarked );
+ Acec_TreeMarkTFI_rec( p, Gia_ObjFaninId1(pObj, Id), vMarked );
+}
+void Acec_TreeFilterOne2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree )
+{
+ Vec_Bit_t * vIsLeaf = Vec_BitStart( Gia_ManObjNum(p) );
+ Vec_Bit_t * vMarked = Vec_BitStart( Gia_ManObjNum(p) ) ;
+ Gia_Obj_t * pObj;
+ int i, k = 0, Box, Rank;
+ // mark leaves
+ Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+ {
+ Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+0), 1 );
+ Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+1), 1 );
+ Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+2), 1 );
+ }
+ Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+ {
+ Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+3), 0 );
+ Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+4), 0 );
+ }
+ // mark TFI of leaves
+ Gia_ManForEachAnd( p, pObj, i )
+ if ( Vec_BitEntry(vIsLeaf, i) )
+ Acec_TreeMarkTFI_rec( p, i, vMarked );
+ // additional one
+//if ( 10942 < Gia_ManObjNum(p) )
+// Acec_TreeMarkTFI_rec( p, 10942, vMarked );
+ // remove those that overlap with the marked TFI
+ Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+ {
+ if ( Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+3)) || Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+4)) )
+ {
+ printf( "Removing box %d=(%d,%d) of rank %d.\n", Box, Vec_IntEntry(vAdds, 6*Box+3), Vec_IntEntry(vAdds, 6*Box+4), Rank );
+ continue;
+ }
+ Vec_IntWriteEntry( vTree, k++, Box );
+ Vec_IntWriteEntry( vTree, k++, Rank );
+ }
+ Vec_IntShrink( vTree, k );
+ Vec_BitFree( vIsLeaf );
+ Vec_BitFree( vMarked );
+}
+void Acec_TreeFilterTrees2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vTrees )
+{
+ Vec_Int_t * vLevel;
+ int i;
+ Vec_WecForEachLevel( vTrees, vLevel, i )
+ Acec_TreeFilterOne2( p, vAdds, vLevel );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Acec_TreeVerifyPhaseOne_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 = Acec_TreeVerifyPhaseOne_rec( p, Gia_ObjFanin0(pObj) );
+ Truth1 = Acec_TreeVerifyPhaseOne_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 Acec_TreeVerifyPhaseOne( Gia_Man_t * p, Vec_Int_t * vAdds, int iBox )
+{
+ Gia_Obj_t * pObj;
+ unsigned TruthXor, TruthMaj, Truths[3] = { 0xAA, 0xCC, 0xF0 };
+ int k, iObj, fFadd = Vec_IntEntry(vAdds, 6*iBox+2) > 0;
+ int fFlip = !fFadd && Acec_SignBit2(vAdds, iBox, 2);
+
+ 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 = (Acec_SignBit2(vAdds, iBox, k) ^ fFlip) ? 0xFF & ~Truths[k] : Truths[k];
+ Gia_ObjSetTravIdCurrent( p, pObj );
+ }
+
+ iObj = Vec_IntEntry( vAdds, 6*iBox+3 );
+ TruthXor = Acec_TreeVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
+ TruthXor = (Acec_SignBit2(vAdds, iBox, 3) ^ fFlip) ? 0xFF & ~TruthXor : TruthXor;
+
+ iObj = Vec_IntEntry( vAdds, 6*iBox+4 );
+ TruthMaj = Acec_TreeVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
+ TruthMaj = (Acec_SignBit2(vAdds, iBox, 4) ^ fFlip) ? 0xFF & ~TruthMaj : TruthMaj;
+
+ if ( fFadd ) // FADD
+ {
+ if ( TruthXor != 0x96 )
+ printf( "Fadd %d sum %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+3 ) );
+ if ( TruthMaj != 0xE8 )
+ printf( "Fadd %d carry %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+4 ) );
+ }
+ else
+ {
+ //printf( "Sign1 = %d%d%d %d\n", Acec_SignBit(vAdds, iBox, 0), Acec_SignBit(vAdds, iBox, 1), Acec_SignBit(vAdds, iBox, 2), Acec_SignBit(vAdds, iBox, 3) );
+ //printf( "Sign2 = %d%d%d %d%d\n", Acec_SignBit2(vAdds, iBox, 0), Acec_SignBit2(vAdds, iBox, 1), Acec_SignBit2(vAdds, iBox, 2), Acec_SignBit2(vAdds, iBox, 3), Acec_SignBit2(vAdds, iBox, 4) );
+ if ( TruthXor != 0x66 )
+ printf( "Hadd %d sum %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+3 ) );
+ if ( TruthMaj != 0x88 )
+ printf( "Hadd %d carry %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+4 ) );
+ }
+}
+void Acec_TreeVerifyPhases( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes )
+{
+ Vec_Int_t * vLevel;
+ int i, k, Box;
+ Vec_WecForEachLevel( vBoxes, vLevel, i )
+ Vec_IntForEachEntry( vLevel, Box, k )
+ Acec_TreeVerifyPhaseOne( p, vAdds, Box );
+}
+void Acec_TreeVerifyPhases2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes )
+{
+ Vec_Bit_t * vPhase = Vec_BitStart( Gia_ManObjNum(p) );
+ Vec_Bit_t * vRoots = Vec_BitStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vLevel;
+ int i, k, n, Box;
+ // mark all output points and their values
+ Vec_WecForEachLevel( vBoxes, vLevel, i )
+ Vec_IntForEachEntry( vLevel, Box, k )
+ {
+ Vec_BitWriteEntry( vRoots, Vec_IntEntry( vAdds, 6*Box+3 ), 1 );
+ Vec_BitWriteEntry( vRoots, Vec_IntEntry( vAdds, 6*Box+4 ), 1 );
+ Vec_BitWriteEntry( vPhase, Vec_IntEntry( vAdds, 6*Box+3 ), Acec_SignBit2(vAdds, Box, 3) );
+ Vec_BitWriteEntry( vPhase, Vec_IntEntry( vAdds, 6*Box+4 ), Acec_SignBit2(vAdds, Box, 4) );
+ }
+ // compare with input points
+ Vec_WecForEachLevel( vBoxes, vLevel, i )
+ Vec_IntForEachEntry( vLevel, Box, k )
+ for ( n = 0; n < 3; n++ )
+ {
+ if ( !Vec_BitEntry(vRoots, Vec_IntEntry(vAdds, 6*Box+n)) )
+ continue;
+ if ( Vec_BitEntry(vPhase, Vec_IntEntry(vAdds, 6*Box+n)) == Acec_SignBit2(vAdds, Box, n) )
+ continue;
+ printf( "Phase of input %d=%d is mismatched in box %d=(%d,%d).\n",
+ n, Vec_IntEntry(vAdds, 6*Box+n), Box, Vec_IntEntry(vAdds, 6*Box+3), Vec_IntEntry(vAdds, 6*Box+4) );
+ }
+ Vec_BitFree( vPhase );
+ Vec_BitFree( vRoots );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates polarity.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Acec_TreeCarryMap( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes )
+{
+ Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
+ Vec_Int_t * vLevel;
+ int i, k, Box;
+ Vec_WecForEachLevel( vBoxes, vLevel, i )
+ Vec_IntForEachEntry( vLevel, Box, k )
+ Vec_IntWriteEntry( vMap, Vec_IntEntry(vAdds, 6*Box+4), Box );
+ return vMap;
+}
+void Acec_TreePhases_rec( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, int Node, int fPhase, Vec_Bit_t * vVisit )
+{
+ int k, iBox, iXor, fXorPhase, fPhaseThis;
+ assert( Node != 0 );
+ iBox = Vec_IntEntry( vMap, Node );
+ if ( iBox == -1 )
+ return;
+ assert( Node == Vec_IntEntry( vAdds, 6*iBox+4 ) );
+ if ( Vec_BitEntry(vVisit, iBox) )
+ return;
+ Vec_BitWriteEntry( vVisit, iBox, 1 );
+ iXor = Vec_IntEntry( vAdds, 6*iBox+3 );
+ fXorPhase = Acec_SignBit(vAdds, iBox, 3);
+ if ( Vec_IntEntry(vAdds, 6*iBox+2) == 0 )
+ {
+ //fPhaseThis = Acec_SignBit( vAdds, iBox, 2 ) ^ fPhase;
+ //fXorPhase ^= fPhaseThis;
+ //Acec_SignSetBit2( vAdds, iBox, 2, fPhaseThis ); // complemented HADD -- create const1 input
+ fPhase ^= Acec_SignBit( vAdds, iBox, 2 );
+ fXorPhase ^= fPhase;
+ Acec_SignSetBit2( vAdds, iBox, 2, fPhase ); // complemented HADD -- create const1 input
+ }
+ for ( k = 0; k < 3; k++ )
+ {
+ int iObj = Vec_IntEntry( vAdds, 6*iBox+k );
+ if ( iObj == 0 )
+ continue;
+ fPhaseThis = Acec_SignBit(vAdds, iBox, k) ^ fPhase;
+ fXorPhase ^= fPhaseThis;
+ Acec_TreePhases_rec( p, vAdds, vMap, iObj, fPhaseThis, vVisit );
+ Acec_SignSetBit2( vAdds, iBox, k, fPhaseThis );
+ }
+ Acec_SignSetBit2( vAdds, iBox, 3, fXorPhase );
+ Acec_SignSetBit2( vAdds, iBox, 4, fPhase );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Find internal cut points with exactly one adder fanin/fanout.]
+
+ Description [Returns a map of point into its input/output adder.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Acec_TreeAddInOutPoint( Vec_Int_t * vMap, int iObj, int iAdd, int fOut )
+{
+ int * pPlace = Vec_IntEntryP( vMap, Abc_Var2Lit(iObj, fOut) );
+ if ( *pPlace == -1 )
+ *pPlace = iAdd;
+ else if ( *pPlace >= 0 )
+ *pPlace = -2;
+}
+Vec_Int_t * Acec_TreeFindPoints( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vIgnore )
+{
+ Vec_Int_t * vMap = Vec_IntStartFull( 2*Gia_ManObjNum(p) );
+ int i;
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+ {
+ if ( vIgnore && (Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+3)) || Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+4))) )
+ continue;
+ Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+0), i, 0 );
+ Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+1), i, 0 );
+ Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+2), i, 0 );
+ Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+3), i, 1 );
+ Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+4), i, 1 );
+ }
+ return vMap;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Find adder trees as groups of adders connected vis cut-points.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Acec_TreeWhichPoint( Vec_Int_t * vAdds, int iAdd, int iObj )
+{
+ int k;
+ for ( k = 0; k < 5; k++ )
+ if ( Vec_IntEntry(vAdds, 6*iAdd+k) == iObj )
+ return k;
+ assert( 0 );
+ return -1;
+}
+void Acec_TreeFindTrees2_rec( Vec_Int_t * vAdds, Vec_Int_t * vMap, int iAdd, int Rank, Vec_Int_t * vTree, Vec_Bit_t * vFound )
+{
+ extern void Acec_TreeFindTrees_rec( Vec_Int_t * vAdds, Vec_Int_t * vMap, int iObj, int Rank, Vec_Int_t * vTree, Vec_Bit_t * vFound );
+ int k;
+ if ( Vec_BitEntry(vFound, iAdd) )
+ return;
+ Vec_BitWriteEntry( vFound, iAdd, 1 );
+ Vec_IntPush( vTree, iAdd );
+ Vec_IntPush( vTree, Rank );
+ //printf( "Assigning rank %d to (%d:%d).\n", Rank, Vec_IntEntry(vAdds, 6*iAdd+3), Vec_IntEntry(vAdds, 6*iAdd+4) );
+ for ( k = 0; k < 5; k++ )
+ Acec_TreeFindTrees_rec( vAdds, vMap, Vec_IntEntry(vAdds, 6*iAdd+k), k == 4 ? Rank + 1 : Rank, vTree, vFound );
+}
+void Acec_TreeFindTrees_rec( Vec_Int_t * vAdds, Vec_Int_t * vMap, int iObj, int Rank, Vec_Int_t * vTree, Vec_Bit_t * vFound )
+{
+ int In = Vec_IntEntry( vMap, Abc_Var2Lit(iObj, 1) );
+ int Out = Vec_IntEntry( vMap, Abc_Var2Lit(iObj, 0) );
+ if ( In < 0 || Out < 0 )
+ return;
+ Acec_TreeFindTrees2_rec( vAdds, vMap, In, Acec_TreeWhichPoint(vAdds, In, iObj) == 4 ? Rank-1 : Rank, vTree, vFound );
+ Acec_TreeFindTrees2_rec( vAdds, vMap, Out, Rank, vTree, vFound );
+}
+Vec_Wec_t * Acec_TreeFindTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vIgnore, int fFilterIn, int fFilterOut )
+{
+ Vec_Wec_t * vTrees = Vec_WecAlloc( 10 );
+ Vec_Int_t * vMap = Acec_TreeFindPoints( p, vAdds, vIgnore );
+ Vec_Bit_t * vFound = Vec_BitStart( Vec_IntSize(vAdds)/6 );
+ Vec_Int_t * vTree;
+ int i, k, In, Out, Box, Rank, MinRank;
+ // go through the cut-points
+ Vec_IntForEachEntryDouble( vMap, In, Out, i )
+ {
+ if ( In < 0 || Out < 0 )
+ continue;
+ assert( Vec_BitEntry(vFound, In) == Vec_BitEntry(vFound, Out) );
+ if ( Vec_BitEntry(vFound, In) )
+ continue;
+ vTree = Vec_WecPushLevel( vTrees );
+ Acec_TreeFindTrees_rec( vAdds, vMap, i/2, 0, vTree, vFound );
+ // normalize rank
+ MinRank = ABC_INFINITY;
+ Vec_IntForEachEntryDouble( vTree, Box, Rank, k )
+ MinRank = Abc_MinInt( MinRank, Rank );
+ Vec_IntForEachEntryDouble( vTree, Box, Rank, k )
+ Vec_IntWriteEntry( vTree, k+1, Rank - MinRank );
+ }
+ Vec_BitFree( vFound );
+ Vec_IntFree( vMap );
+ // filter trees
+ if ( fFilterIn )
+ Acec_TreeFilterTrees2( p, vAdds, vTrees );
+ else if ( fFilterOut )
+ Acec_TreeFilterTrees( p, vAdds, vTrees );
+ // sort by size
+ Vec_WecSort( vTrees, 1 );
+ return vTrees;
+}
+void Acec_TreeFindTreesTest( Gia_Man_t * p )
+{
+ Vec_Wec_t * vTrees;
+
+ abctime clk = Abc_Clock();
+ Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, 1 );
+ int nFadds = Ree_ManCountFadds( vAdds );
+ printf( "Detected %d adders (%d FAs and %d HAs). ", Vec_IntSize(vAdds)/6, nFadds, Vec_IntSize(vAdds)/6-nFadds );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+
+ clk = Abc_Clock();
+ vTrees = Acec_TreeFindTrees( p, vAdds, NULL, 0, 0 );
+ printf( "Collected %d trees with %d adders in them. ", Vec_WecSize(vTrees), Vec_WecSizeSize(vTrees)/2 );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ Vec_WecPrint( vTrees, 0 );
+
+ Vec_WecFree( vTrees );
+ Vec_IntFree( vAdds );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Derives one adder tree.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds )
+{
+ Vec_Int_t * vLevel;
+ int i, k, iBox;
+ Vec_WecForEachLevel( vBoxes, vLevel, i )
+ {
+ printf( " %4d : %2d {", i, Vec_IntSize(vLevel) );
+ Vec_IntForEachEntry( vLevel, iBox, k )
+ {
+ printf( " %s%d=(%d,%d)", Vec_IntEntry(vAdds, 6*iBox+2) == 0 ? "*":"", iBox,
+ Vec_IntEntry(vAdds, 6*iBox+3), Vec_IntEntry(vAdds, 6*iBox+4) );
+ //printf( "(%d,%d,%d)", Vec_IntEntry(vAdds, 6*iBox+0), Vec_IntEntry(vAdds, 6*iBox+1), Vec_IntEntry(vAdds, 6*iBox+2) );
+ }
+ printf( " }\n" );
+ }
+}
+void Acec_PrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds )
+{
+ printf( "Adders:\n" );
+ Acec_PrintAdders( pBox->vAdds, vAdds );
+ printf( "Inputs:\n" );
+ Vec_WecPrintLits( pBox->vLeafLits );
+ printf( "Outputs:\n" );
+ Vec_WecPrintLits( pBox->vRootLits );
+}
+
+int Acec_CreateBoxMaxRank( Vec_Int_t * vTree )
+{
+ int k, Box, Rank, MaxRank = 0;
+ Vec_IntForEachEntryDouble( vTree, Box, Rank, k )
+ MaxRank = Abc_MaxInt( MaxRank, Rank );
+ return MaxRank;
+}
+Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree )
+{
+ int MaxRank = Acec_CreateBoxMaxRank(vTree);
+ Vec_Bit_t * vVisit = Vec_BitStart( Vec_IntSize(vAdds)/6 );
+ Vec_Bit_t * vIsLeaf = Vec_BitStart( Gia_ManObjNum(p) );
+ Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vLevel, * vMap;
+ int i, j, k, Box, Rank;//, Count = 0;
+
+ Acec_Box_t * pBox = ABC_CALLOC( Acec_Box_t, 1 );
+ pBox->pGia = p;
+ pBox->vAdds = Vec_WecStart( MaxRank + 1 );
+ pBox->vLeafLits = Vec_WecStart( MaxRank + 1 );
+ pBox->vRootLits = Vec_WecStart( MaxRank + 2 );
+
+ // collect boxes; mark inputs/outputs
+ Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+ {
+// if ( 37 == Box && 6 == Rank )
+// {
+// printf( "Skipping one adder...\n" );
+// continue;
+// }
+ Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+0), 1 );
+ Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+1), 1 );
+ Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+2), 1 );
+ Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+3), 1 );
+ Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+4), 1 );
+ Vec_WecPush( pBox->vAdds, Rank, Box );
+ }
+ // sort each level
+ Vec_WecForEachLevel( pBox->vAdds, vLevel, i )
+ Vec_IntSort( vLevel, 0 );
+
+ // set phases starting from roots
+ vMap = Acec_TreeCarryMap( p, vAdds, pBox->vAdds );
+ Vec_WecForEachLevelReverse( pBox->vAdds, vLevel, i )
+ Vec_IntForEachEntry( vLevel, Box, k )
+ if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+4) ) )
+ {
+ //printf( "Pushing phase of output %d of box %d\n", Vec_IntEntry(vAdds, 6*Box+4), Box );
+ Acec_TreePhases_rec( p, vAdds, vMap, Vec_IntEntry(vAdds, 6*Box+4), Vec_IntEntry(vAdds, 6*Box+2) != 0, vVisit );
+ }
+ Acec_TreeVerifyPhases( p, vAdds, pBox->vAdds );
+ Acec_TreeVerifyPhases2( p, vAdds, pBox->vAdds );
+ Vec_BitFree( vVisit );
+ Vec_IntFree( vMap );
+
+ // collect inputs/outputs
+ Vec_BitWriteEntry( vIsRoot, 0, 1 );
+ Vec_WecForEachLevel( pBox->vAdds, vLevel, i )
+ Vec_IntForEachEntry( vLevel, Box, j )
+ {
+ for ( k = 0; k < 3; k++ )
+ if ( !Vec_BitEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+k) ) )
+ Vec_WecPush( pBox->vLeafLits, i, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), Acec_SignBit2(vAdds, Box, k)) );
+ for ( k = 3; k < 5; k++ )
+ if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+k) ) )
+ {
+ //if ( Vec_IntEntry(vAdds, 6*Box+k) == 10942 )
+ //{
+ // printf( "++++++++++++ Skipping special\n" );
+ // continue;
+ //}
+ Vec_WecPush( pBox->vRootLits, k == 4 ? i + 1 : i, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), Acec_SignBit2(vAdds, Box, k)) );
+ }
+ if ( Vec_IntEntry(vAdds, 6*Box+2) == 0 && Acec_SignBit2(vAdds, Box, 2) )
+ Vec_WecPush( pBox->vLeafLits, i, 1 );
+ }
+ Vec_BitFree( vIsLeaf );
+ Vec_BitFree( vIsRoot );
+ // sort each level
+ Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i )
+ Vec_IntSort( vLevel, 0 );
+ Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
+ Vec_IntSort( vLevel, 1 );
+ //return pBox;
+/*
+ // push literals forward
+ //Vec_WecPrint( pBox->vLeafLits, 0 );
+ Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i )
+ {
+ int This, Prev = Vec_IntEntry(vLevel, 0);
+ Vec_IntForEachEntryStart( vLevel, This, j, 1 )
+ {
+ if ( Prev != This )
+ {
+ Prev = This;
+ continue;
+ }
+ if ( i+1 >= Vec_WecSize(pBox->vLeafLits) )
+ continue;
+ Vec_IntPushOrder( Vec_WecEntry(pBox->vLeafLits, i+1), This );
+ Vec_IntDrop( vLevel, j-- );
+ Vec_IntDrop( vLevel, j-- );
+ Prev = -1;
+ Count++;
+ }
+ }
+ printf( "Pushed forward %d input literals.\n", Count );
+*/
+ //Vec_WecPrint( pBox->vLeafLits, 0 );
+ return pBox;
+}
+void Acec_CreateBoxTest( Gia_Man_t * p )
+{
+ Acec_Box_t * pBox;
+ Vec_Wec_t * vTrees;
+ Vec_Int_t * vTree;
+
+ abctime clk = Abc_Clock();
+ Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, 1 );
+ int i, nFadds = Ree_ManCountFadds( vAdds );
+ printf( "Detected %d adders (%d FAs and %d HAs). ", Vec_IntSize(vAdds)/6, nFadds, Vec_IntSize(vAdds)/6-nFadds );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+
+ clk = Abc_Clock();
+ vTrees = Acec_TreeFindTrees( p, vAdds, NULL, 0, 0 );
+ printf( "Collected %d trees with %d adders in them. ", Vec_WecSize(vTrees), Vec_WecSizeSize(vTrees)/2 );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ //Vec_WecPrint( vTrees, 0 );
+
+ Vec_WecForEachLevel( vTrees, vTree, i )
+ {
+ pBox = Acec_CreateBox( p, vAdds, Vec_WecEntry(vTrees, i) );
+ printf( "Processing tree %d: Ranks = %d. Adders = %d. Leaves = %d. Roots = %d.\n",
+ i, Vec_WecSize(pBox->vAdds), Vec_WecSizeSize(pBox->vAdds),
+ Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits) );
+ Acec_PrintBox( pBox, vAdds );
+ Acec_BoxFreeP( &pBox );
+ }
+
+ Vec_WecFree( vTrees );
+ Vec_IntFree( vAdds );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fFilterIn, int fFilterOut, int fVerbose )
+{
+ Acec_Box_t * pBox = NULL;
+ Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, fVerbose );
+ Vec_Wec_t * vTrees = Acec_TreeFindTrees( p, vAdds, vIgnore, fFilterIn, fFilterOut );
+ if ( vTrees && Vec_WecSize(vTrees) > 0 )
+ {
+ pBox = Acec_CreateBox( p, vAdds, Vec_WecEntry(vTrees, 0) );
+ Acec_VerifyBoxLeaves( pBox, vIgnore );
+ }
+ if ( pBox )//&& fVerbose )
+ printf( "Processing tree %d: Ranks = %d. Adders = %d. Leaves = %d. Roots = %d.\n",
+ 0, Vec_WecSize(pBox->vAdds), Vec_WecSizeSize(pBox->vAdds),
+ Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits) );
+ if ( pBox && fVerbose )
+ Acec_PrintBox( pBox, vAdds );
+ //Acec_PrintAdders( pBox0->vAdds, vAdds );
+ //Acec_MultDetectInputs( p, pBox->vLeafLits, pBox->vRootLits );
+ Vec_WecFreeP( &vTrees );
+ Vec_IntFree( vAdds );
+ return pBox;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecUtil.c b/src/proof/acec/acecUtil.c
index 191856cf..be12afef 100644
--- a/src/proof/acec/acecUtil.c
+++ b/src/proof/acec/acecUtil.c
@@ -90,6 +90,29 @@ void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose )
Vec_IntFree( vXors );
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupTopMostRange( Gia_Man_t * p )
+{
+ Gia_Man_t * pNew;
+ Vec_Int_t * vTops = Vec_IntAlloc( 10 );
+ int i;
+ for ( i = 45; i < 52; i++ )
+ Vec_IntPush( vTops, Gia_ObjId( p, Gia_ObjFanin0(Gia_ManCo(p, i)) ) );
+ pNew = Gia_ManDupAndConesLimit( p, Vec_IntArray(vTops), Vec_IntSize(vTops), 100 );
+ Vec_IntFree( vTops );
+ return pNew;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/acec/module.make b/src/proof/acec/module.make
index df6db695..dbf86ac2 100644
--- a/src/proof/acec/module.make
+++ b/src/proof/acec/module.make
@@ -1,13 +1,17 @@
SRC += src/proof/acec/acecCl.c \
src/proof/acec/acecCore.c \
src/proof/acec/acecCo.c \
+ src/proof/acec/acecBo.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/acecMult.c \
+ src/proof/acec/acecNorm.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
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-30 17:14:53 +0000