summaryrefslogtreecommitdiffstats
path: root/src/base/io
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/io')
-rw-r--r--src/base/io/ioRead.c3
-rw-r--r--src/base/io/ioReadBench.c2
-rw-r--r--src/base/io/ioWriteCnf.c40
-rw-r--r--src/base/io/ioWriteDot.c8
-rw-r--r--src/base/io/ioWriteList.c30
5 files changed, 64 insertions, 19 deletions
diff --git a/src/base/io/ioRead.c b/src/base/io/ioRead.c
index 6422461c..70e648a7 100644
--- a/src/base/io/ioRead.c
+++ b/src/base/io/ioRead.c
@@ -42,6 +42,9 @@
Abc_Ntk_t * Io_Read( char * pFileName, int fCheck )
{
Abc_Ntk_t * pNtk, * pTemp;
+// extern int s_TotalNodes;
+// extern int s_TotalChanges;
+// s_TotalNodes = s_TotalChanges = 0;
// set the new network
if ( Extra_FileNameCheckExtension( pFileName, "blif" ) )
pNtk = Io_ReadBlif( pFileName, fCheck );
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index 1cb0ae5d..aa7f82e3 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -136,7 +136,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
Abc_ObjSetData( pNode, Abc_SopCreateNor(pNtk->pManFunc, nNames) );
else if ( strcmp(pType, "XOR") == 0 )
Abc_ObjSetData( pNode, Abc_SopCreateXor(pNtk->pManFunc, nNames) );
- else if ( strcmp(pType, "NXOR") == 0 )
+ else if ( strcmp(pType, "NXOR") == 0 || strcmp(pType, "XNOR") == 0 )
Abc_ObjSetData( pNode, Abc_SopCreateNxor(pNtk->pManFunc, nNames) );
else if ( strncmp(pType, "BUF", 3) == 0 )
Abc_ObjSetData( pNode, Abc_SopCreateBuf(pNtk->pManFunc) );
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
index 9e5ceb9f..24612566 100644
--- a/src/base/io/ioWriteCnf.c
+++ b/src/base/io/ioWriteCnf.c
@@ -23,6 +23,8 @@
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+
+static Abc_Ntk_t * s_pNtk = NULL;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -57,15 +59,51 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName )
fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter for combinational circuits.\n" );
return 0;
}
+ if ( Abc_NtkNodeNum(pNtk) == 0 )
+ {
+ fprintf( stdout, "The network has no logic nodes. No CNF file is generaled.\n" );
+ return 0;
+ }
// create solver with clauses
- pSat = Abc_NtkMiterSatCreate( pNtk );
+ pSat = Abc_NtkMiterSatCreate( pNtk, 0 );
+ if ( pSat == NULL )
+ {
+ fprintf( stdout, "The problem is trivially UNSAT. No CNF file is generated.\n" );
+ return 1;
+ }
// write the clauses
+ s_pNtk = pNtk;
Asat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 );
+ s_pNtk = NULL;
// free the solver
solver_delete( pSat );
return 1;
}
+/**Function*************************************************************
+
+ Synopsis [Output the mapping of PIs into variable numbers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_WriteCnfOutputPiMapping( FILE * pFile, int incrementVars )
+{
+ extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
+ Abc_Ntk_t * pNtk = s_pNtk;
+ Vec_Int_t * vCiIds;
+ Abc_Obj_t * pObj;
+ int i;
+ vCiIds = Abc_NtkGetCiSatVarNums( pNtk );
+ fprintf( pFile, "c PI variable numbers: <PI_name> <SAT_var_number>\n" );
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ fprintf( pFile, "c %s %d\n", Abc_ObjName(pObj), Vec_IntEntry(vCiIds, i) + (int)(incrementVars > 0) );
+ Vec_IntFree( vCiIds );
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index dbf157bf..ed6acb24 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -412,7 +412,13 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
// transform logic functions from BDD to SOP
if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
- Abc_NtkBddToSop(pNtk, 0);
+ {
+ if ( !Abc_NtkBddToSop(pNtk, 0) )
+ {
+ printf( "Converting to SOPs has failed.\n" );
+ return;
+ }
+ }
// mark the nodes from the set
Vec_PtrForEachEntry( vNodes, pNode, i )
diff --git a/src/base/io/ioWriteList.c b/src/base/io/ioWriteList.c
index ab216eb3..f0981a8e 100644
--- a/src/base/io/ioWriteList.c
+++ b/src/base/io/ioWriteList.c
@@ -120,8 +120,8 @@ void Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int fUseHost )
if ( Abc_ObjFanoutNum( Abc_NtkConst1(pNtk) ) > 0 )
Io_WriteListEdge( pFile, Abc_NtkConst1(pNtk) );
- // write the PO edges
- Abc_NtkForEachCi( pNtk, pObj, i )
+ // write the PI edges
+ Abc_NtkForEachPi( pNtk, pObj, i )
Io_WriteListEdge( pFile, pObj );
// write the internal nodes
@@ -132,7 +132,7 @@ void Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int fUseHost )
if ( fUseHost )
Io_WriteListHost( pFile, pNtk );
else
- Abc_NtkForEachCo( pNtk, pObj, i )
+ Abc_NtkForEachPo( pNtk, pObj, i )
Io_WriteListEdge( pFile, pObj );
fprintf( pFile, "\n" );
@@ -157,12 +157,13 @@ void Io_WriteListEdge( FILE * pFile, Abc_Obj_t * pObj )
fprintf( pFile, "%-10s > ", Abc_ObjName(pObj) );
Abc_ObjForEachFanout( pObj, pFanout, i )
{
- fprintf( pFile, " %s ([%s_to_%s] = %d)", Abc_ObjName(pFanout), Abc_ObjName(pObj), Abc_ObjName(pFanout), Seq_ObjFanoutL(pObj, pFanout) );
- if ( i == Abc_ObjFanoutNum(pObj) - 1 )
- fprintf( pFile, "." );
- else
+ fprintf( pFile, " %s", Abc_ObjName(pFanout) );
+ fprintf( pFile, " ([%s_to_", Abc_ObjName(pObj) );
+ fprintf( pFile, "%s] = %d)", Abc_ObjName(pFanout), Seq_ObjFanoutL(pObj, pFanout) );
+ if ( i != Abc_ObjFanoutNum(pObj) - 1 )
fprintf( pFile, "," );
}
+ fprintf( pFile, "." );
fprintf( pFile, "\n" );
}
@@ -186,22 +187,19 @@ void Io_WriteListHost( FILE * pFile, Abc_Ntk_t * pNtk )
{
fprintf( pFile, "%-10s > ", Abc_ObjName(pObj) );
fprintf( pFile, " %s ([%s_to_%s] = %d)", "HOST", Abc_ObjName(pObj), "HOST", 0 );
- if ( i == Abc_NtkPoNum(pNtk) - 1 )
- fprintf( pFile, "." );
- else
- fprintf( pFile, "," );
+ fprintf( pFile, "." );
+ fprintf( pFile, "\n" );
}
- fprintf( pFile, "\n" );
fprintf( pFile, "%-10s > ", "HOST" );
Abc_NtkForEachPi( pNtk, pObj, i )
{
- fprintf( pFile, " %s ([%s_to_%s] = %d)", Abc_ObjName(pObj), "HOST", Abc_ObjName(pObj), 0 );
- if ( i == Abc_NtkPiNum(pNtk) - 1 )
- fprintf( pFile, "." );
- else
+ fprintf( pFile, " %s", Abc_ObjName(pObj) );
+ fprintf( pFile, " ([%s_to_%s] = %d)", "HOST", Abc_ObjName(pObj), 0 );
+ if ( i != Abc_NtkPiNum(pNtk) - 1 )
fprintf( pFile, "," );
}
+ fprintf( pFile, "." );
fprintf( pFile, "\n" );
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-08 09:07:42 +0000