Version abc50828

9 files changed, 162 insertions, 35 deletions

diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c
index c2b739b5..f8871ba9 100644
--- a/src/base/abc/abc.c
+++ b/src/base/abc/abc.c
@@ -1065,6 +1065,11 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+    if ( Abc_NtkIsAig(pNtk) )
+    {
+        fprintf( pErr, "Cleanup cannot be performed on the AIG.\n" );
+        return 1;
+    }
 
     // modify the current network
     Abc_NtkCleanup( pNtk, 0 );
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 200d2501..2366aa10 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -406,6 +406,7 @@ extern Abc_Ntk_t *        Abc_NtkStartRead( char * pName );
 extern void               Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkDup( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis );
+extern Abc_Ntk_t *        Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues );
 extern void               Abc_NtkDelete( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
@@ -532,10 +533,13 @@ extern void               Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk );
 /*=== abcSop.c ==========================================================*/
 extern char *             Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
 extern char *             Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
+extern char *             Abc_SopCreateConst0( Extra_MmFlex_t * pMan );
+extern char *             Abc_SopCreateConst1( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 );
 extern char *             Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
+extern char *             Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
 extern char *             Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars );
@@ -559,6 +563,7 @@ extern void               Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_In
 extern void               Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp );
 /*=== abcStrash.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes );
+extern Abc_Obj_t *        Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
 extern Abc_Obj_t *        Abc_NodeStrashDec( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t * vForm );
 extern int                Abc_NodeStrashDecCount( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, Vec_Int_t * vLevels, int NodeMax, int LevelMax );
 extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index d42fdac0..2200bea1 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -172,6 +172,10 @@ Abc_Aig_t * Abc_AigDup( Abc_Aig_t * pMan, Abc_Aig_t * pManNew )
         Abc_ObjSetFaninL0( pObj->pCopy, Abc_ObjFaninL0(pObj) );
         Abc_ObjSetFaninL1( pObj->pCopy, Abc_ObjFaninL1(pObj) );
     }
+    // relink the choice nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        if ( pObj->pData )
+            pObj->pCopy->pData = ((Abc_Obj_t *)pObj->pData)->pCopy;
     Vec_PtrFree( vNodes );
     // relink the CO nodes
     Abc_NtkForEachCo( pMan->pNtkAig, pObj, i )
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index ee77cd02..e8b00271 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -361,7 +361,8 @@ bool Abc_NtkCheckPos( Abc_Ntk_t * pNtk )
 bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pFanin, * pFanout;
-    int i, k, Value = 1;
+    int i, Value = 1;
+//    int k;
 
     // check the network
     if ( pObj->pNtk != pNtk )
@@ -395,7 +396,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
             Value = 0;
         }
     }
-
+/*
     // make sure fanins are not duplicated
     for ( i = 0; i < pObj->vFanins.nSize; i++ )
         for ( k = i + 1; k < pObj->vFanins.nSize; k++ )
@@ -417,7 +418,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
                 printf( "Warning: Node %s has", Abc_ObjName(pObj) );
                 printf( " duplicated fanout %s.\n", Abc_ObjName(Abc_ObjFanout(pObj,k)) );
             }
-
+*/
     return Value;
 }
 
diff --git a/src/base/abc/abcCreate.c b/src/base/abc/abcCreate.c
index 9f192979..7de9ea3e 100644
--- a/src/base/abc/abcCreate.c
+++ b/src/base/abc/abcCreate.c
@@ -333,7 +333,64 @@ Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAll
     Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) );
 
     if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkDup(): Network check has failed.\n" );
+        fprintf( stdout, "Abc_NtkSplitOutput(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the network composed of one output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pFinal, * pOther, * pNodePo;
+    int i;
+
+    assert( Abc_NtkIsLogic(pNtk) );
+    
+    // start the network
+    Abc_NtkCleanCopy( pNtk );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_AIG );
+    pNtkNew->pName = util_strsav(pNtk->pName);
+
+    // collect the nodes in the TFI of the output
+    vNodes = Abc_NtkDfsNodes( pNtk, (Abc_Obj_t **)vRoots->pArray, vRoots->nSize );
+    // create the PIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+    {
+        pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
+    }
+    // copy the nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = Abc_NodeStrash( pNtkNew->pManFunc, pObj );
+    Vec_PtrFree( vNodes );
+
+    // add the PO
+    pFinal = Abc_AigConst1( pNtkNew->pManFunc );
+    Vec_PtrForEachEntry( vRoots, pObj, i )
+    {
+        pOther = pObj->pCopy;
+        if ( Vec_IntEntry(vValues, i) == 0 )
+            pOther = Abc_ObjNot(pOther);
+        pFinal = Abc_AigAnd( pNtkNew->pManFunc, pFinal, pOther );
+    }
+
+    // add the PO corresponding to this output
+    pNodePo = Abc_NtkCreatePo( pNtkNew );
+    Abc_ObjAddFanin( pNodePo, pFinal );
+    Abc_NtkLogicStoreName( pNodePo, "miter" );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
     return pNtkNew;
 }
 
diff --git a/src/base/abc/abcFraig.c b/src/base/abc/abcFraig.c
index c0eb1c0a..724c3877 100644
--- a/src/base/abc/abcFraig.c
+++ b/src/base/abc/abcFraig.c
@@ -89,7 +89,7 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
     ProgressBar * pProgress;
     Fraig_Node_t * pNodeFraig;
     Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pNode, * pConst1;
+    Abc_Obj_t * pNode, * pConst1, * pReset;
     int i;
 
     assert( Abc_NtkIsAig(pNtk) );
@@ -102,6 +102,7 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
     Abc_NtkForEachCi( pNtk, pNode, i )
         pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
     pConst1 = Abc_AigConst1( pNtk->pManFunc );
+    pReset  = Abc_AigReset( pNtk->pManFunc );
 
     // perform strashing
     vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
@@ -111,6 +112,8 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
         Extra_ProgressBarUpdate( pProgress, i, NULL );
         if ( pNode == pConst1 )
             pNodeFraig = Fraig_ManReadConst1(pMan);
+        else if ( pNode == pReset )
+            continue;
         else
             pNodeFraig = Fraig_NodeAnd( pMan, 
                 Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index bfa41842..8e10b391 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -254,23 +254,26 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
         if ( !Abc_NodeIsAigChoice(pObj) )
             continue;
         // create an OR gate
-        pNodeNew = Abc_NtkCreateNode(pNtk);
+        pNodeNew = Abc_NtkCreateNode(pNtkNew);
         // add fanins
         Vec_IntClear( pNtk->vIntTemp );
-        for ( k = 0, pFanin = pObj; pFanin; pFanin = pFanin->pData, k++ )
+        for ( pFanin = pObj; pFanin; pFanin = pFanin->pData )
         {
             Vec_IntPush( pNtk->vIntTemp, (int)(pObj->fPhase != pFanin->fPhase) );
             Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
         }
         // create the logic function
-        pNodeNew->pData = Abc_SopCreateOr( pNtk->pManFunc, pNtk->vIntTemp->nSize, pNtk->vIntTemp->pArray );
+        pNodeNew->pData = Abc_SopCreateOrMultiCube( pNtkNew->pManFunc, pNtk->vIntTemp->nSize, pNtk->vIntTemp->pArray );
         // set the new node
-        pObj->pCopy = pNodeNew;
+        pObj->pCopy->pCopy = pNodeNew;
     }
     // connect the internal nodes
     Abc_NtkForEachNode( pNtk, pObj, i )
         Abc_ObjForEachFanin( pObj, pFanin, k )
-            Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+            if ( pFanin->pCopy->pCopy )
+                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy->pCopy );
+            else
+                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
     // connect the COs
     Abc_NtkFinalize( pNtk, pNtkNew );
     // fix the problem with complemented and duplicated CO edges
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index b6972d58..28e92889 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -92,7 +92,39 @@ char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the constant 1 cover with 0 variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopCreateConst1( Extra_MmFlex_t * pMan )
+{
+    return Abc_SopRegister( pMan, " 1\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the constant 1 cover with 0 variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopCreateConst0( Extra_MmFlex_t * pMan )
+{
+    return Abc_SopRegister( pMan, " 0\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the AND2 cover.]
 
   Description []
                
@@ -115,7 +147,7 @@ char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input AND cover.]
 
   Description []
                
@@ -136,7 +168,7 @@ char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input NAND cover.]
 
   Description []
                
@@ -158,7 +190,7 @@ char * Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input OR cover.]
 
   Description []
                
@@ -180,7 +212,32 @@ char * Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input OR cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
+{
+    char * pSop, * pCube;
+    int i;
+    pSop = Abc_SopStart( pMan, nVars, nVars );
+    i = 0;
+    Abc_SopForEachCube( pSop, nVars, pCube )
+    {
+        pCube[i] = '1' - (pfCompl? pfCompl[i] : 0);
+        i++;
+    }
+    return pSop;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the multi-input NOR cover.]
 
   Description []
                
@@ -201,7 +258,7 @@ char * Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input XOR cover.]
 
   Description []
                
@@ -218,7 +275,7 @@ char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input XNOR cover.]
 
   Description []
                
@@ -235,7 +292,7 @@ char * Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the inv cover.]
 
   Description []
                
@@ -251,7 +308,7 @@ char * Abc_SopCreateInv( Extra_MmFlex_t * pMan )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the buf cover.]
 
   Description []
                
@@ -367,18 +424,11 @@ int Abc_SopGetPhase( char * pSop )
 int Abc_SopGetIthCareLit( char * pSop, int i )
 {
     char * pCube;
-    int nVars, c;
+    int nVars;
     nVars = Abc_SopGetVarNum( pSop );
-    for ( c = 0; ; c++ )
-    {
-        // get the cube
-        pCube = pSop + c * (nVars + 3);
-        if ( *pCube == 0 )
-            break;
-        // get the literal
+    Abc_SopForEachCube( pSop, nVars, pCube )
         if ( pCube[i] != '-' )
             return pCube[i] - '0';
-    }
     return -1;
 }
 
@@ -520,6 +570,8 @@ bool Abc_SopIsAndType( char * pSop )
     for ( pCur = pSop; *pCur != ' '; pCur++ )
         if ( *pCur == '-' )
             return 0;
+    if ( pCur[1] != '1' )
+        return 0;
     return 1;
 }
 
@@ -537,14 +589,12 @@ bool Abc_SopIsAndType( char * pSop )
 bool Abc_SopIsOrType( char * pSop )
 {
     char * pCube, * pCur;
-    int nVars, nLits, c;
+    int nVars, nLits;
     nVars = Abc_SopGetVarNum( pSop );
-    for ( c = 0; ; c++ )
+    if ( nVars != Abc_SopGetCubeNum(pSop) )
+        return 0;
+    Abc_SopForEachCube( pSop, nVars, pCube )
     {
-        // get the cube
-        pCube = pSop + c * (nVars + 3);
-        if ( *pCube == 0 )
-            break;
         // count the number of literals in the cube
         nLits = 0;
         for ( pCur = pCube; *pCur != ' '; pCur++ )
diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c
index 961e6c5f..bf97c5bf 100644
--- a/src/base/abc/abcStrash.c
+++ b/src/base/abc/abcStrash.c
@@ -28,7 +28,6 @@
 
 // static functions
 static void        Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fAllNodes );
-static Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
 static Abc_Obj_t * Abc_NodeStrashSop( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop );
 static Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop );