Supporting complemented reduction operators.

5 files changed, 40 insertions, 11 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 399aa076..f800feb5 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -78,6 +78,9 @@ typedef enum {
     WLC_OBJ_REDUCT_AND,    // 34: reduction AND
     WLC_OBJ_REDUCT_OR,     // 35: reduction OR
     WLC_OBJ_REDUCT_XOR,    // 36: reduction XOR
+    WLC_OBJ_REDUCT_NAND,   // 34: reduction NAND
+    WLC_OBJ_REDUCT_NOR,    // 35: reduction NOR
+    WLC_OBJ_REDUCT_NXOR,   // 36: reduction NXOR
     WLC_OBJ_ARI_ADD,       // 37: arithmetic addition
     WLC_OBJ_ARI_SUB,       // 38: arithmetic subtraction
     WLC_OBJ_ARI_MULTI,     // 39: arithmetic multiplier
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index a8f8585b..85301a16 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -170,26 +170,26 @@ void Wlc_BlastRotateLeft( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift,
 }
 int Wlc_BlastReduction( Gia_Man_t * pNew, int * pFans, int nFans, int Type )
 {
-    if ( Type == WLC_OBJ_REDUCT_AND )
+    if ( Type == WLC_OBJ_REDUCT_AND || Type == WLC_OBJ_REDUCT_NAND )
     {
         int k, iLit = 1;
         for ( k = 0; k < nFans; k++ )
             iLit = Gia_ManHashAnd( pNew, iLit, pFans[k] );
-        return iLit;
+        return Abc_LitNotCond( iLit, Type == WLC_OBJ_REDUCT_NAND );
     }
-    if ( Type == WLC_OBJ_REDUCT_OR )
+    if ( Type == WLC_OBJ_REDUCT_OR || Type == WLC_OBJ_REDUCT_NOR )
     {
         int k, iLit = 0;
         for ( k = 0; k < nFans; k++ )
             iLit = Gia_ManHashOr( pNew, iLit, pFans[k] );
-        return iLit;
+        return Abc_LitNotCond( iLit, Type == WLC_OBJ_REDUCT_NOR );
     }
-    if ( Type == WLC_OBJ_REDUCT_XOR )
+    if ( Type == WLC_OBJ_REDUCT_XOR || Type == WLC_OBJ_REDUCT_NXOR )
     {
         int k, iLit = 0;
         for ( k = 0; k < nFans; k++ )
             iLit = Gia_ManHashXor( pNew, iLit, pFans[k] );
-        return iLit;
+        return Abc_LitNotCond( iLit, Type == WLC_OBJ_REDUCT_NXOR );
     }
     assert( 0 );
     return -1;
@@ -1032,7 +1032,8 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
             for ( k = 1; k < nRange; k++ )
                 Vec_IntPush( vRes, 0 );
         }
-        else if ( pObj->Type == WLC_OBJ_REDUCT_AND || pObj->Type == WLC_OBJ_REDUCT_OR || pObj->Type == WLC_OBJ_REDUCT_XOR )
+        else if ( pObj->Type == WLC_OBJ_REDUCT_AND  || pObj->Type == WLC_OBJ_REDUCT_OR  || pObj->Type == WLC_OBJ_REDUCT_XOR ||
+                  pObj->Type == WLC_OBJ_REDUCT_NAND || pObj->Type == WLC_OBJ_REDUCT_NOR || pObj->Type == WLC_OBJ_REDUCT_NXOR )
         {
             Vec_IntPush( vRes, Wlc_BlastReduction( pNew, pFans0, nRange0, pObj->Type ) );
             for ( k = 1; k < nRange; k++ )
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 6e9be0bc..0e4f24a2 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -67,6 +67,9 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = {
     "&",                   // 34: reduction AND
     "|",                   // 35: reduction OR
     "^",                   // 36: reduction XOR
+    "~&",                  // 34: reduction NAND
+    "~|",                  // 35: reduction NOR
+    "~^",                  // 36: reduction NXOR
     "+",                   // 37: arithmetic addition
     "-",                   // 38: arithmetic subtraction
     "*",                   // 39: arithmetic multiplier
@@ -391,6 +394,12 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
             Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_OR,        Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 );
         else if ( pObj->Type == WLC_OBJ_REDUCT_XOR )   
             Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_XOR,   3 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 3 );
+        else if ( pObj->Type == WLC_OBJ_REDUCT_NAND )   
+            Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NAND,       Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 );
+        else if ( pObj->Type == WLC_OBJ_REDUCT_NOR )    
+            Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NOR,        Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 );
+        else if ( pObj->Type == WLC_OBJ_REDUCT_NXOR )   
+            Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NXOR,   3 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 3 );
         else if ( pObj->Type == WLC_OBJ_ARI_ADD )       
             Vec_IntAddToEntry( vAnds, WLC_OBJ_ARI_ADD,      9 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) );
         else if ( pObj->Type == WLC_OBJ_ARI_SUB )       
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index 65fa7acf..6c035c3d 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -685,16 +685,26 @@ static inline int Wlc_PrsFindDefinition( Wlc_Prs_t * p, char * pStr, Vec_Int_t *
         if ( !(pStr = Wlc_PrsReadName(p, pStr, vFanins)) )
             return Wlc_PrsWriteErrorMessage( p, pStr, "Cannot read name after !." );
     }
-    else if ( pStr[0] == '&' || pStr[0] == '|' || pStr[0] == '^' || pStr[0] == '-' )
+    else if ( pStr[0] == '-' || 
+              pStr[0] == '&' || pStr[0] == '|' || pStr[0] == '^' || 
+              (pStr[0] == '~' && pStr[1] == '&') || 
+              (pStr[0] == '~' && pStr[1] == '|') || 
+              (pStr[0] == '~' && pStr[1] == '^') )
     {
-        if ( pStr[0] == '&' )
+        if ( pStr[0] == '-' )
+            Type = WLC_OBJ_ARI_MINUS;
+        else if ( pStr[0] == '&' )
             Type = WLC_OBJ_REDUCT_AND;
         else if ( pStr[0] == '|' )
             Type = WLC_OBJ_REDUCT_OR;
         else if ( pStr[0] == '^' )
             Type = WLC_OBJ_REDUCT_XOR;
-        else if ( pStr[0] == '-' )
-            Type = WLC_OBJ_ARI_MINUS;
+        else if ( pStr[0] == '~' && pStr[1] == '&' )
+            Type = WLC_OBJ_REDUCT_NAND;
+        else if ( pStr[0] == '~' && pStr[1] == '|' )
+            Type = WLC_OBJ_REDUCT_NOR;
+        else if ( pStr[0] == '~' && pStr[1] == '^' )
+            Type = WLC_OBJ_REDUCT_NXOR;
         else assert( 0 );
         if ( !(pStr = Wlc_PrsReadName(p, pStr+1, vFanins)) )
             return Wlc_PrsWriteErrorMessage( p, pStr, "Cannot read name after a unary operator." );
diff --git a/src/base/wlc/wlcWriteVer.c b/src/base/wlc/wlcWriteVer.c
index bb490a66..a8e225ff 100644
--- a/src/base/wlc/wlcWriteVer.c
+++ b/src/base/wlc/wlcWriteVer.c
@@ -272,6 +272,12 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops )
                 fprintf( pFile, "|%s", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) );
             else if ( pObj->Type == WLC_OBJ_REDUCT_XOR )
                 fprintf( pFile, "^%s", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) );
+            else if ( pObj->Type == WLC_OBJ_REDUCT_NAND )
+                fprintf( pFile, "~&%s", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) );
+            else if ( pObj->Type == WLC_OBJ_REDUCT_NOR )
+                fprintf( pFile, "~|%s", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) );
+            else if ( pObj->Type == WLC_OBJ_REDUCT_NXOR )
+                fprintf( pFile, "~^%s", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) );
             else if ( pObj->Type == WLC_OBJ_BIT_SELECT )
                 fprintf( pFile, "%s [%d:%d]", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)), Wlc_ObjRangeEnd(pObj), Wlc_ObjRangeBeg(pObj) );
             else if ( pObj->Type == WLC_OBJ_BIT_SIGNEXT )