Version abc80307

1 files changed, 125 insertions, 0 deletions

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                                ///