Version abc80307

4 files changed, 135 insertions, 5 deletions

diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index c14d0317..012b74cf 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -266,6 +266,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
         Abc_NtkAddDummyBoxNames( pNtkNew );
     else
     {
+/*
         {
             int i, k, iFlop, Counter = 0;
             FILE * pFile;
@@ -285,6 +286,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
             fclose( pFile );
             //printf( "\n" );
         }
+*/
         assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) );
         nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) );
         Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
@@ -1622,11 +1624,14 @@ timeInt = 0;
         }
         else
             pNtkInter1 = Abc_NtkInterOne( pNtkOn1, pNtkOff1, fVerbose );
-        Abc_NtkAppend( pNtkInter, pNtkInter1, 1 );
+        if ( pNtkInter1 )
+        {
+            Abc_NtkAppend( pNtkInter, pNtkInter1, 1 );
+            Abc_NtkDelete( pNtkInter1 );
+        }
 
         Abc_NtkDelete( pNtkOn1 );
         Abc_NtkDelete( pNtkOff1 );
-        Abc_NtkDelete( pNtkInter1 );
     }
 //    PRT( "CNF", timeCnf );
 //    PRT( "SAT", timeSat );
diff --git a/src/base/abci/abcDelay.c b/src/base/abci/abcDelay.c
index bb654b73..67e051f3 100644
--- a/src/base/abci/abcDelay.c
+++ b/src/base/abci/abcDelay.c
@@ -33,11 +33,12 @@ static inline void  Abc_ObjSetArrival( Abc_Obj_t * pNode, float Time )  { pNode-
 static inline void  Abc_ObjSetRequired( Abc_Obj_t * pNode, float Time ) { pNode->pNtk->pLutTimes[3*pNode->Id+1] = Time; }
 static inline void  Abc_ObjSetSlack( Abc_Obj_t * pNode, float Time )    { pNode->pNtk->pLutTimes[3*pNode->Id+2] = Time; }
 
+extern void * Abc_FrameReadLibLut();   
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-
 /**Function*************************************************************
 
   Synopsis    [Sorts the pins in the decreasing order of delays.]
@@ -95,7 +96,6 @@ void Abc_NtkDelayTraceSortPins( Abc_Obj_t * pNode, int * pPinPerm, float * pPinD
 ***********************************************************************/
 float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib )
 {
-    extern void * Abc_FrameReadLibLut();   
     int fUseSorting = 0;
     int pPinPerm[32];
     float pPinDelays[32];
diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c
index 7c18ca2c..e40c21d6 100644
--- a/src/base/abci/abcGen.c
+++ b/src/base/abci/abcGen.c
@@ -131,7 +131,7 @@ void Abc_GenSorter( char * pFileName, int nVars )
             fprintf( pFile, " y%02d=%0*d", k, nDigits, Counter++ );
         fprintf( pFile, "\n" );
         Counter -= nVars;
-        for ( i = 1; i < nVars-2; i++ )
+        for ( i = 1; i < 2*nVars-2; i++ )
         {
             fprintf( pFile, ".subckt Layer%d", (i&1) );
             for ( k = 0; k < nVars; k++ )
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 58614584..afdfbdeb 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -591,6 +591,16 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
         ASat_SolverSetPrefVars( pSat, pPrefVars, nVars );
     }
 */
+/*
+    Abc_NtkForEachObj( pNtk, pNode, i )
+    {
+        if ( !pNode->fMarkA )
+            continue;
+        printf( "%10s : ", Abc_ObjName(pNode) );
+        printf( "%3d\n", (int)pNode->pCopy );
+    }
+    printf( "\n" );
+*/
     RetValue = 1;
 Quits :
     // delete
@@ -876,6 +886,121 @@ finish:
 
 
 
+/**Function*************************************************************
+
+  Synopsis    [Writes CNF for the sorter with N inputs asserting Q ones.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens )
+{
+    extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
+    extern void * Abc_FrameGetGlobalFrame();
+    extern Abc_Ntk_t * Abc_FrameReadNtk( void * p );
+
+    char Command[100];
+    void * pAbc;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pObj, * ppNodes[2], * ppRoots[2];
+    Vec_Ptr_t * vNodes;
+    FILE * pFile;
+    int i, Counter;
+
+    if ( nQueens <= 0 && nQueens >= nVars )
+    {
+        printf( "The number of queens (Q = %d) should belong to the interval: 0 < Q < %d.\n", nQueens, nQueens, nVars );
+        return;
+    }
+    assert( nQueens > 0 && nQueens < nVars );
+    pAbc = Abc_FrameGetGlobalFrame();
+    // generate sorter
+    sprintf( Command, "gen -s -N %d sorter%d.blif", nVars, nVars );
+    if ( Cmd_CommandExecute( pAbc, Command ) )
+    {
+        fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
+        return;
+    }
+    // read the file
+    sprintf( Command, "read sorter%d.blif; strash", nVars );
+    if ( Cmd_CommandExecute( pAbc, Command ) )
+    {
+        fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
+        return;
+    }
+
+    // get the current network
+    pNtk = Abc_FrameReadNtk(pAbc);
+    // collect the nodes for the given two primary outputs
+    ppNodes[0] = Abc_NtkPo( pNtk, nVars - nQueens - 1 );
+    ppNodes[1] = Abc_NtkPo( pNtk, nVars - nQueens );
+    ppRoots[0] = Abc_ObjFanin0( ppNodes[0] );
+    ppRoots[1] = Abc_ObjFanin0( ppNodes[1] );
+    vNodes = Abc_NtkDfsNodes( pNtk, ppRoots, 2 );
+
+    // assign CNF variables
+    Counter = 0;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->pCopy = (void *)~0;
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        pObj->pCopy = (void *)Counter++;
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = (void *)Counter++;
+
+/*
+        OutVar   = pCnf->pVarNums[ pObj->Id ];
+        pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
+        pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
+
+        // positive phase
+        *pClas++ = pLits;
+        *pLits++ = 2 * OutVar; 
+        *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj); 
+        *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj); 
+        // negative phase
+        *pClas++ = pLits;
+        *pLits++ = 2 * OutVar + 1; 
+        *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj); 
+        *pClas++ = pLits;
+        *pLits++ = 2 * OutVar + 1; 
+        *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj); 
+*/
+
+    // add clauses for these nodes
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "c CNF for %d-bit sorter with %d bits set to 1 generated by ABC.\n", nVars, nQueens );
+    fprintf( pFile, "p cnf %d %d\n", Counter, 3 * Vec_PtrSize(vNodes) + 2 );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // positive phase
+        fprintf( pFile, "%d %s%d %s%d 0\n", 1+(int)pObj->pCopy, 
+            Abc_ObjFaninC0(pObj)? "" : "-", 1+(int)Abc_ObjFanin0(pObj)->pCopy,
+            Abc_ObjFaninC1(pObj)? "" : "-", 1+(int)Abc_ObjFanin1(pObj)->pCopy );
+        // negative phase
+        fprintf( pFile, "-%d %s%d 0\n", 1+(int)pObj->pCopy, 
+            Abc_ObjFaninC0(pObj)? "-" : "", 1+(int)Abc_ObjFanin0(pObj)->pCopy );
+        fprintf( pFile, "-%d %s%d 0\n", 1+(int)pObj->pCopy, 
+            Abc_ObjFaninC1(pObj)? "-" : "", 1+(int)Abc_ObjFanin1(pObj)->pCopy );
+    }
+    Vec_PtrFree( vNodes );
+
+/*
+    *pClas++ = pLits;
+    *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
+*/
+    // assert the first literal to zero
+    fprintf( pFile, "%s%d 0\n", 
+        Abc_ObjFaninC0(ppNodes[0])? "" : "-", 1+(int)Abc_ObjFanin0(ppNodes[0])->pCopy );
+    // assert the second literal to one
+    fprintf( pFile, "%s%d 0\n", 
+        Abc_ObjFaninC0(ppNodes[1])? "-" : "", 1+(int)Abc_ObjFanin0(ppNodes[1])->pCopy );
+    fclose( pFile );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///