From 329cee498196f8751f5ca111ed786e3fc1211c86 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 30 Nov 2016 11:30:38 -0800
Subject: Small changes in handling arithmetic logic.

---
 src/base/wlc/wlcBlast.c | 11 ++++++++++-
 src/proof/acec/acecCo.c | 10 ++++++++--
 2 files changed, 18 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index c86c7cf0..ec3b040d 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -292,6 +292,10 @@ int Wlc_BlastLessSigned( Gia_Man_t * pNew, int * pArg0, int * pArg1, int nBits )
 void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int * ps )
 {
     int fUseXor = 0;
+    int fCompl = (a == 1 || b == 1 || c == 1);
+    // propagate complement through the FA - helps generate less redundant logic
+    if ( fCompl )
+        a = Abc_LitNot(a), b = Abc_LitNot(b), c = Abc_LitNot(c); 
     if ( fUseXor )
     {
         int Xor  = Gia_ManHashXor(pNew, a, b);
@@ -310,6 +314,8 @@ void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int *
         *ps      = Gia_ManHashAnd(pNew, Abc_LitNot(And2), Abc_LitNot(And2_));
         *pc      = Gia_ManHashOr (pNew, And1, And2);
     }
+    if ( fCompl )
+        *ps = Abc_LitNot(*ps), *pc = Abc_LitNot(*pc); 
 }
 void Wlc_BlastAdder( Gia_Man_t * pNew, int * pAdd0, int * pAdd1, int nBits ) // result is in pAdd0
 {
@@ -412,6 +418,7 @@ void Wlc_BlastMultiplier( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA,
     assert( fSigned == 0 || fSigned == 1 );
     // prepare result
     Vec_IntFill( vRes, nArgA + nArgB, 0 );
+    //Vec_IntFill( vRes, nArgA + nArgB + 1, 0 );
     pRes = Vec_IntArray( vRes );
     // prepare intermediate storage
     Vec_IntFill( vTemp, 2 * nArgA, 0 );
@@ -426,6 +433,7 @@ void Wlc_BlastMultiplier( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA,
     pArgS[nArgA-1] = fSigned;
     for ( a = 0; a < nArgA; a++ )
         Wlc_BlastFullAdderCtrl( pNew, 1, pArgC[a], pArgS[a], Carry, &Carry, &pRes[nArgB+a], 0 );
+    //Vec_IntWriteEntry( vRes, nArgA + nArgB, Carry );
 }
 void Wlc_BlastDivider( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes )
 {
@@ -804,7 +812,7 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int
         Vec_WecPush( vLevels, k, 0 );
     }
     //Vec_WecPrint( vProds, 0 );
-
+    //printf( "Cutoff ID for partial products = %d.\n", Gia_ManObjNum(pNew) );
     Wlc_BlastReduceMatrix( pNew, vProds, vLevels, vRes );
 
     Vec_WecFree( vProds );
@@ -1360,6 +1368,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
     {
         pNew = Gia_ManCleanup( pTemp = pNew );
         Gia_ManDupRemapLiterals( vBits, pTemp );
+        //printf( "Cutoff ID %d became %d.\n", 75, Abc_Lit2Var(Gia_ManObj(pTemp, 73)->Value) );
         Gia_ManStop( pTemp );
     }
     // transform AIG with init state
diff --git a/src/proof/acec/acecCo.c b/src/proof/acec/acecCo.c
index 000f530a..1b73c36f 100644
--- a/src/proof/acec/acecCo.c
+++ b/src/proof/acec/acecCo.c
@@ -44,11 +44,14 @@ ABC_NAMESPACE_IMPL_START
 ***********************************************************************/
 void Gia_PolynCoreNonXors_rec( Gia_Man_t * pGia, Gia_Obj_t * pObj, Vec_Int_t * vXorPairs )
 {
+    extern int Gia_ManSuppSizeOne( Gia_Man_t * p, Gia_Obj_t * pObj );
     Gia_Obj_t * pFan0, * pFan1;
     if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
         return;
     Gia_PolynCoreNonXors_rec( pGia, Gia_Regular(pFan0), vXorPairs );
     Gia_PolynCoreNonXors_rec( pGia, Gia_Regular(pFan1), vXorPairs );
+    //if ( Gia_ManSuppSizeOne(pGia, pObj) > 4 )
+    //if ( Gia_ObjId(pGia, pObj) >= 73 )
     Vec_IntPushTwo( vXorPairs, Gia_ObjId(pGia, Gia_Regular(pFan0)), Gia_ObjId(pGia, Gia_Regular(pFan1)) );
 }
 Vec_Int_t * Gia_PolynAddHaRoots( Gia_Man_t * pGia )
@@ -95,7 +98,7 @@ Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t *
     Vec_Int_t * vLeaves = Vec_IntAlloc( 2 * Gia_ManCiNum(pGia) );
     Vec_Wec_t * vMap    = Vec_WecStart( Gia_ManObjNum(pGia) );
     int i, k, Index, Driver, Entry1, Entry2 = -1;
-    // nodes driven by adders into adder indexes
+    // map nodes driven by adders into adder indexes
     for ( i = 0; 5*i < Vec_IntSize(vAdds); i++ )
     {
         Entry1 = Vec_IntEntry( vAdds, 5*i + 3 );
@@ -318,8 +321,11 @@ Gia_Man_t * Gia_PolynCoreDetectTest_int( Gia_Man_t * pGia, Vec_Int_t * vAddCos,
     Vec_Int_t * vAdds = Ree_ManComputeCuts( pGia, 1 );
     Vec_Int_t * vLeaves, * vRoots, * vOrder = Gia_PolynCoreOrder( pGia, vAdds, vAddCos, &vLeaves, &vRoots );
     Vec_Int_t * vNodes = Gia_PolynCoreCollect( pGia, vAdds, vOrder );
+
+    //Gia_ManShow( pGia, vNodes, 0 );
+    
     printf( "Detected %d FAs/HAs. Roots = %d. Leaves = %d. Nodes = %d. Adds = %d. ", 
-        Vec_IntSize(vAdds), Vec_IntSize(vLeaves), Vec_IntSize(vRoots), Vec_IntSize(vNodes), Vec_IntSize(vOrder) );
+        Vec_IntSize(vAdds)/5, Vec_IntSize(vLeaves), Vec_IntSize(vRoots), Vec_IntSize(vNodes), Vec_IntSize(vOrder) );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 
     Gia_PolynCorePrintCones( pGia, vLeaves, fVerbose );
-- 
cgit v1.2.3