Version abc80705

3 files changed, 244 insertions, 18 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ae1c110f..2c34ed67 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -105,6 +105,7 @@ static int Abc_CommandReach          ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandCone           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandNode           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTopmost        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTopAnd         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTrim           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandShortNames     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExdcFree       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -361,6 +362,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "cone",          Abc_CommandCone,             1 );
     Cmd_CommandAdd( pAbc, "Various",      "node",          Abc_CommandNode,             1 );
     Cmd_CommandAdd( pAbc, "Various",      "topmost",       Abc_CommandTopmost,          1 );
+    Cmd_CommandAdd( pAbc, "Various",      "topand",        Abc_CommandTopAnd,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "trim",          Abc_CommandTrim,             1 );
     Cmd_CommandAdd( pAbc, "Various",      "short_names",   Abc_CommandShortNames,       0 );
     Cmd_CommandAdd( pAbc, "Various",      "exdc_free",     Abc_CommandExdcFree,         1 );
@@ -6277,6 +6279,91 @@ usage:
   Description []
                
   SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandTopAnd( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    extern Abc_Ntk_t * Abc_NtkTopAnd( Abc_Ntk_t * pNtk );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
+        return 0;
+    }
+
+    if ( Abc_NtkLatchNum(pNtk) > 0 )
+    {
+        fprintf( stdout, "Currently can only works for combinational circuits.\n" );
+        return 0;
+    } 
+    if ( Abc_NtkPoNum(pNtk) != 1 )
+    {
+        fprintf( stdout, "Currently expects a single-output miter.\n" );
+        return 0;
+    } 
+    if ( Abc_ObjFaninC0(Abc_NtkPo(pNtk, 0)) )
+    {
+        fprintf( stdout, "The PO driver is complemented. AND-decomposition is impossible.\n" );
+        return 0;
+    } 
+    if ( !Abc_ObjIsNode(Abc_ObjChild0(Abc_NtkPo(pNtk, 0))) )
+    {
+        fprintf( stdout, "The PO driver is not a node. AND-decomposition is impossible.\n" );
+        return 0;
+    } 
+    pNtkRes = Abc_NtkTopAnd( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "The command has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: topand [-h]\n" );
+    fprintf( pErr, "\t         AND-decomposition of single-output combinational miter\n" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\tname   : the node name\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
  
   SeeAlso     []
 
@@ -13997,7 +14084,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fPartition;
     int fMiter;
 
-    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose );
+    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
     extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -14097,7 +14184,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // perform equivalence checking
     if ( fSat && fMiter )
-        Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, fVerbose );
+        Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, fVerbose );
     else
         Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose );
 
@@ -14651,12 +14738,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
     int RetValue;
+    int fFlipBits;
+    int fAndOuts;
     int fVerbose;
     int nConfLimit;
     int nInsLimit;
     int clk;
 
-    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose );
+    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
 
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -14664,11 +14753,13 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fFlipBits  = 0;
+    fAndOuts   = 0;
     fVerbose   = 0;
     nConfLimit = 100000;   
     nInsLimit  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CIvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CIfavh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -14694,6 +14785,12 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nInsLimit < 0 ) 
                 goto usage;
             break;
+        case 'f':
+            fFlipBits ^= 1;
+            break;
+        case 'a':
+            fAndOuts ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -14714,12 +14811,13 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
         return 0;
     } 
+/*
     if ( Abc_NtkPoNum(pNtk) != 1 )
     {
         fprintf( stdout, "Currently expects a single-output miter.\n" );
         return 0;
     } 
- 
+*/
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
@@ -14727,7 +14825,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     clk = clock();
-    RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fVerbose );
+    RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fFlipBits, fAndOuts, fVerbose );
     // verify that the pattern is correct
     if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
     {
@@ -14760,11 +14858,13 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dsat [-C num] [-I num] [-vh]\n" );
+    fprintf( pErr, "usage: dsat [-C num] [-I num] [-favh]\n" );
     fprintf( pErr, "\t         solves the combinational miter using SAT solver MiniSat-1.14\n" );
     fprintf( pErr, "\t         derives CNF from the current network and leave it unchanged\n" );
     fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
     fprintf( pErr, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
+    fprintf( pErr, "\t-f     : flip polarity of SAT variables [default = %s]\n", fFlipBits? "yes": "no" );  
+    fprintf( pErr, "\t-a     : constrain each output of multi-output miter [default = %s]\n", fAndOuts? "yes": "no" );  
     fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index d89ee618..2a234b68 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -932,9 +932,9 @@ Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
 {
-    Vec_Ptr_t * vMapped;
+    Vec_Ptr_t * vMapped = NULL;
     Aig_Man_t * pMan;
-    Cnf_Man_t * pManCnf;
+    Cnf_Man_t * pManCnf = NULL;
     Cnf_Dat_t * pCnf;
     Abc_Ntk_t * pNtkNew = NULL;
     assert( Abc_NtkIsStrash(pNtk) );
@@ -954,13 +954,14 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
 
     // derive CNF
     pCnf = Cnf_Derive( pMan, 0 );
-    pManCnf = Cnf_ManRead();
-
+    Cnf_DataTranformPolarity( pCnf );
+/*
     // write the network for verification
+    pManCnf = Cnf_ManRead();
     vMapped = Cnf_ManScanMapping( pManCnf, 1, 0 );
     pNtkNew = Abc_NtkConstructFromCnf( pNtk, pManCnf, vMapped );
     Vec_PtrFree( vMapped );
-
+*/
     // write CNF into a file
     Cnf_DataWriteIntoFile( pCnf, pFileName, 0 );
     Cnf_DataFree( pCnf );
@@ -982,7 +983,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose )
+int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose )
 {
     Aig_Man_t * pMan;
     int RetValue;//, clk = clock();
@@ -990,7 +991,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
     assert( Abc_NtkLatchNum(pNtk) == 0 );
     assert( Abc_NtkPoNum(pNtk) == 1 );
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
-    RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fVerbose ); 
+    RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fFlipBits, fAndOuts, fVerbose ); 
     pNtk->pModel = pMan->pData, pMan->pData = NULL;
     Aig_ManStop( pMan );
     return RetValue;
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 084f6a6c..ad09f084 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -443,7 +443,7 @@ Abc_Obj_t * Abc_NtkTopmost_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int Leve
 Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels )
 {
     Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObjNew, * pPoNew;
+    Abc_Obj_t * pObjNew, * pObjPo;
     int LevelCut;
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkCoNum(pNtk) == 1 );
@@ -458,10 +458,10 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels )
     pObjNew = Abc_NtkTopmost_rec( pNtkNew, Abc_ObjFanin0(Abc_NtkPo(pNtk, 0)), LevelCut );
     pObjNew = Abc_ObjNotCond( pObjNew, Abc_ObjFaninC0(Abc_NtkPo(pNtk, 0)) );
     // add the PO node and name
-    pPoNew = Abc_NtkCreatePo(pNtkNew);
-    Abc_ObjAddFanin( pPoNew, pObjNew );
+    pObjPo = Abc_NtkCreatePo(pNtkNew);
+    Abc_ObjAddFanin( pObjPo, pObjNew );
     Abc_NtkAddDummyPiNames( pNtkNew );
-    Abc_ObjAssignName( pPoNew, Abc_ObjName(Abc_NtkPo(pNtk, 0)), NULL );
+    Abc_ObjAssignName( pObjPo, Abc_ObjName(Abc_NtkPo(pNtk, 0)), NULL );
     // make sure everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
@@ -473,6 +473,131 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels )
 }
 
 
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two integers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Vec_CompareNodeIds( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
+{
+    if ( Abc_ObjRegular(*pp1)->Id < Abc_ObjRegular(*pp2)->Id )
+        return -1;
+    if ( Abc_ObjRegular(*pp1)->Id > Abc_ObjRegular(*pp2)->Id ) //
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the large supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NodeGetSuper( Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t * vSuper, * vFront;
+    Abc_Obj_t * pAnd, * pFanin;
+    int i;
+    assert( Abc_ObjIsNode(pNode) && !Abc_ObjIsComplement(pNode) );
+    vSuper = Vec_PtrAlloc( 100 ); 
+    // explore the frontier
+    vFront = Vec_PtrAlloc( 100 );
+    Vec_PtrPush( vFront, pNode );
+    Vec_PtrForEachEntry( vFront, pAnd, i )
+    {
+        pFanin = Abc_ObjChild0(pAnd);
+        if ( Abc_ObjIsNode(pFanin) && !Abc_ObjIsComplement(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+            Vec_PtrPush( vFront, pFanin );
+        else
+            Vec_PtrPush( vSuper, pFanin );
+
+        pFanin = Abc_ObjChild1(pAnd);
+        if ( Abc_ObjIsNode(pFanin) && !Abc_ObjIsComplement(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+            Vec_PtrPush( vFront, pFanin );
+        else
+            Vec_PtrPush( vSuper, pFanin );
+    }
+    Vec_PtrFree( vFront );
+    // reverse the array of pointers to start with lower IDs
+    vFront = Vec_PtrAlloc( Vec_PtrSize(vSuper) );
+    Vec_PtrForEachEntryReverse( vSuper, pNode, i )
+        Vec_PtrPush( vFront, pNode );
+    Vec_PtrFree( vSuper );
+    vSuper = vFront;
+    // uniquify and return the frontier
+    Vec_PtrUniqify( vSuper, Vec_CompareNodeIds );
+    return vSuper;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Copies the topmost levels of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkTopAnd( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes, * vOrder;
+    Abc_Ntk_t * pNtkAig;
+    Abc_Obj_t * pObj, * pDriver, * pObjPo;
+    int i, nNodes;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // get the first PO
+    pObjPo = Abc_NtkPo(pNtk, 0);
+    vNodes = Abc_NodeGetSuper( Abc_ObjChild0(pObjPo) );
+    assert( Vec_PtrSize(vNodes) >= 2 );
+    // start the new network (constants and CIs of the old network will point to the their counterparts in the new network)
+    Abc_NtkCleanCopy( pNtk );
+    pNtkAig = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+    pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
+    pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+    Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkAig);
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkDupObj( pNtkAig, pObj, 1 );
+    // restrash the nodes reachable from the roots
+    vOrder = Abc_NtkDfsIterNodes( pNtk, vNodes );
+    Vec_PtrForEachEntry( vOrder, pObj, i )
+        pObj->pCopy = Abc_AigAnd( pNtkAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+    Vec_PtrFree( vOrder );
+    // finalize the network
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        pObjPo = Abc_NtkCreatePo(pNtkAig);
+        pDriver = Abc_ObjNotCond(Abc_ObjRegular(pObj)->pCopy, Abc_ObjIsComplement(pObj));
+        Abc_ObjAddFanin( pObjPo, pDriver );
+        Abc_ObjAssignName( pObjPo, Abc_ObjName(pObjPo), NULL );
+    }
+    Vec_PtrFree( vNodes );
+    // perform cleanup if requested
+    if ( (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) ) 
+        printf( "Abc_NtkTopAnd(): AIG cleanup removed %d nodes (this is a bug).\n", nNodes );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkAig ) )
+    {
+        printf( "Abc_NtkStrash: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkAig );
+        return NULL;
+    }
+    return pNtkAig;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////