summaryrefslogtreecommitdiffstats
path: root/src/aig/ioa
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ioa')
-rw-r--r--src/aig/ioa/ioa.h80
-rw-r--r--src/aig/ioa/ioaReadAig.c312
-rw-r--r--src/aig/ioa/ioaUtil.c117
-rw-r--r--src/aig/ioa/ioaWriteAig.c292
-rw-r--r--src/aig/ioa/module.make3
5 files changed, 0 insertions, 804 deletions
diff --git a/src/aig/ioa/ioa.h b/src/aig/ioa/ioa.h
deleted file mode 100644
index 3458d12e..00000000
--- a/src/aig/ioa/ioa.h
+++ /dev/null
@@ -1,80 +0,0 @@
-/**CFile****************************************************************
-
- FileName [ioa.h]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [AIG package.]
-
- Synopsis [External declarations.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - April 28, 2007.]
-
- Revision [$Id: ioa.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __IOA_H__
-#define __IOA_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// INCLUDES ///
-////////////////////////////////////////////////////////////////////////
-
-#include <stdio.h>
-#include <stdlib.h>
-#include <string.h>
-#include <assert.h>
-#include <time.h>
-
-#include "vec.h"
-#include "bar.h"
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-/// PARAMETERS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// BASIC TYPES ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// ITERATORS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== ioaReadAig.c ========================================================*/
-extern Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck );
-/*=== ioaWriteAig.c =======================================================*/
-extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols );
-/*=== ioaUtil.c =======================================================*/
-extern int Ioa_FileSize( char * pFileName );
-extern char * Ioa_FileNameGeneric( char * FileName );
-extern char * Ioa_TimeStamp();
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/aig/ioa/ioaReadAig.c b/src/aig/ioa/ioaReadAig.c
deleted file mode 100644
index 937e446f..00000000
--- a/src/aig/ioa/ioaReadAig.c
+++ /dev/null
@@ -1,312 +0,0 @@
-/**CFile****************************************************************
-
- FileName [ioaReadAiger.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Command processing package.]
-
- Synopsis [Procedures to read binary AIGER format developed by
- Armin Biere, Johannes Kepler University (http://fmv.jku.at/)]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - December 16, 2006.]
-
- Revision [$Id: ioaReadAiger.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "ioa.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-unsigned Ioa_ReadAigerDecode( char ** ppPos );
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Reads the AIG in the binary AIGER format.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
-{
- Bar_Progress_t * pProgress;
- FILE * pFile;
- Vec_Ptr_t * vNodes, * vDrivers;//, * vTerms;
- Aig_Obj_t * pObj, * pNode0, * pNode1;
- Aig_Man_t * pManNew;
- int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, i;//, iTerm, nDigits;
- char * pContents, * pDrivers, * pSymbols, * pCur, * pName;//, * pType;
- unsigned uLit0, uLit1, uLit;
-
- // read the file into the buffer
- nFileSize = Ioa_FileSize( pFileName );
- pFile = fopen( pFileName, "rb" );
- pContents = ALLOC( char, nFileSize );
- fread( pContents, nFileSize, 1, pFile );
- fclose( pFile );
-
- // check if the input file format is correct
- if ( strncmp(pContents, "aig", 3) != 0 )
- {
- fprintf( stdout, "Wrong input file format.\n" );
- return NULL;
- }
-
- // read the file type
- pCur = pContents; while ( *pCur++ != ' ' );
- // read the number of objects
- nTotal = atoi( pCur ); while ( *pCur++ != ' ' );
- // read the number of inputs
- nInputs = atoi( pCur ); while ( *pCur++ != ' ' );
- // read the number of latches
- nLatches = atoi( pCur ); while ( *pCur++ != ' ' );
- // read the number of outputs
- nOutputs = atoi( pCur ); while ( *pCur++ != ' ' );
- // read the number of nodes
- nAnds = atoi( pCur ); while ( *pCur++ != '\n' );
- // check the parameters
- if ( nTotal != nInputs + nLatches + nAnds )
- {
- fprintf( stdout, "The paramters are wrong.\n" );
- return NULL;
- }
-
- // allocate the empty AIG
- pManNew = Aig_ManStart( nAnds );
- pName = Ioa_FileNameGeneric( pFileName );
- pManNew->pName = Aig_UtilStrsav( pName );
-// pManNew->pSpec = Ioa_UtilStrsav( pFileName );
- free( pName );
-
- // prepare the array of nodes
- vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
- Vec_PtrPush( vNodes, Aig_ManConst0(pManNew) );
-
- // create the PIs
- for ( i = 0; i < nInputs + nLatches; i++ )
- {
- pObj = Aig_ObjCreatePi(pManNew);
- Vec_PtrPush( vNodes, pObj );
- }
-/*
- // create the POs
- for ( i = 0; i < nOutputs + nLatches; i++ )
- {
- pObj = Aig_ObjCreatePo(pManNew);
- }
-*/
- // create the latches
- pManNew->nRegs = nLatches;
-/*
- nDigits = Ioa_Base10Log( nLatches );
- for ( i = 0; i < nLatches; i++ )
- {
- pObj = Aig_ObjCreateLatch(pManNew);
- Aig_LatchSetInit0( pObj );
- pNode0 = Aig_ObjCreateBi(pManNew);
- pNode1 = Aig_ObjCreateBo(pManNew);
- Aig_ObjAddFanin( pObj, pNode0 );
- Aig_ObjAddFanin( pNode1, pObj );
- Vec_PtrPush( vNodes, pNode1 );
- // assign names to latch and its input
-// Aig_ObjAssignName( pObj, Aig_ObjNameDummy("_L", i, nDigits), NULL );
-// printf( "Creating latch %s with input %d and output %d.\n", Aig_ObjName(pObj), pNode0->Id, pNode1->Id );
- }
-*/
-
- // remember the beginning of latch/PO literals
- pDrivers = pCur;
-
- // scroll to the beginning of the binary data
- for ( i = 0; i < nLatches + nOutputs; )
- if ( *pCur++ == '\n' )
- i++;
-
- // create the AND gates
- pProgress = Bar_ProgressStart( stdout, nAnds );
- for ( i = 0; i < nAnds; i++ )
- {
- Bar_ProgressUpdate( pProgress, i, NULL );
- uLit = ((i + 1 + nInputs + nLatches) << 1);
- uLit1 = uLit - Ioa_ReadAigerDecode( &pCur );
- uLit0 = uLit1 - Ioa_ReadAigerDecode( &pCur );
-// assert( uLit1 > uLit0 );
- pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
- pNode1 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
- assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
- Vec_PtrPush( vNodes, Aig_And(pManNew, pNode0, pNode1) );
- }
- Bar_ProgressStop( pProgress );
-
- // remember the place where symbols begin
- pSymbols = pCur;
-
- // read the latch driver literals
- vDrivers = Vec_PtrAlloc( nLatches + nOutputs );
- pCur = pDrivers;
-// Aig_ManForEachLatchInput( pManNew, pObj, i )
- for ( i = 0; i < nLatches; i++ )
- {
- uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
- pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
-// Aig_ObjAddFanin( pObj, pNode0 );
- Vec_PtrPush( vDrivers, pNode0 );
- }
- // read the PO driver literals
-// Aig_ManForEachPo( pManNew, pObj, i )
- for ( i = 0; i < nOutputs; i++ )
- {
- uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
- pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
-// Aig_ObjAddFanin( pObj, pNode0 );
- Vec_PtrPush( vDrivers, pNode0 );
- }
-
-
- // create the POs
- for ( i = 0; i < nOutputs; i++ )
- Aig_ObjCreatePo( pManNew, Vec_PtrEntry(vDrivers, nLatches + i) );
- for ( i = 0; i < nLatches; i++ )
- Aig_ObjCreatePo( pManNew, Vec_PtrEntry(vDrivers, i) );
- Vec_PtrFree( vDrivers );
-
-/*
- // read the names if present
- pCur = pSymbols;
- if ( *pCur != 'c' )
- {
- int Counter = 0;
- while ( pCur < pContents + nFileSize && *pCur != 'c' )
- {
- // get the terminal type
- pType = pCur;
- if ( *pCur == 'i' )
- vTerms = pManNew->vPis;
- else if ( *pCur == 'l' )
- vTerms = pManNew->vBoxes;
- else if ( *pCur == 'o' )
- vTerms = pManNew->vPos;
- else
- {
- fprintf( stdout, "Wrong terminal type.\n" );
- return NULL;
- }
- // get the terminal number
- iTerm = atoi( ++pCur ); while ( *pCur++ != ' ' );
- // get the node
- if ( iTerm >= Vec_PtrSize(vTerms) )
- {
- fprintf( stdout, "The number of terminal is out of bound.\n" );
- return NULL;
- }
- pObj = Vec_PtrEntry( vTerms, iTerm );
- if ( *pType == 'l' )
- pObj = Aig_ObjFanout0(pObj);
- // assign the name
- pName = pCur; while ( *pCur++ != '\n' );
- // assign this name
- *(pCur-1) = 0;
- Aig_ObjAssignName( pObj, pName, NULL );
- if ( *pType == 'l' )
- {
- Aig_ObjAssignName( Aig_ObjFanin0(pObj), Aig_ObjName(pObj), "L" );
- Aig_ObjAssignName( Aig_ObjFanin0(Aig_ObjFanin0(pObj)), Aig_ObjName(pObj), "_in" );
- }
- // mark the node as named
- pObj->pCopy = (Aig_Obj_t *)Aig_ObjName(pObj);
- }
-
- // assign the remaining names
- Aig_ManForEachPi( pManNew, pObj, i )
- {
- if ( pObj->pCopy ) continue;
- Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
- Counter++;
- }
- Aig_ManForEachLatchOutput( pManNew, pObj, i )
- {
- if ( pObj->pCopy ) continue;
- Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
- Aig_ObjAssignName( Aig_ObjFanin0(pObj), Aig_ObjName(pObj), "L" );
- Aig_ObjAssignName( Aig_ObjFanin0(Aig_ObjFanin0(pObj)), Aig_ObjName(pObj), "_in" );
- Counter++;
- }
- Aig_ManForEachPo( pManNew, pObj, i )
- {
- if ( pObj->pCopy ) continue;
- Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
- Counter++;
- }
- if ( Counter )
- printf( "Ioa_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
- }
- else
- {
-// printf( "Ioa_ReadAiger(): I/O/register names are not given. Generating short names.\n" );
- Aig_ManShortNames( pManNew );
- }
-*/
-
- // skipping the comments
- free( pContents );
- Vec_PtrFree( vNodes );
-
- // remove the extra nodes
- Aig_ManCleanup( pManNew );
-
- // check the result
- if ( fCheck && !Aig_ManCheck( pManNew ) )
- {
- printf( "Ioa_ReadAiger: The network check has failed.\n" );
- Aig_ManStop( pManNew );
- return NULL;
- }
- return pManNew;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Extracts one unsigned AIG edge from the input buffer.]
-
- Description [This procedure is a slightly modified version of Armin Biere's
- procedure "unsigned decode (FILE * file)". ]
-
- SideEffects [Updates the current reading position.]
-
- SeeAlso []
-
-***********************************************************************/
-unsigned Ioa_ReadAigerDecode( char ** ppPos )
-{
- unsigned x = 0, i = 0;
- unsigned char ch;
-
-// while ((ch = getnoneofch (file)) & 0x80)
- while ((ch = *(*ppPos)++) & 0x80)
- x |= (ch & 0x7f) << (7 * i++);
-
- return x | (ch << (7 * i));
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/ioa/ioaUtil.c b/src/aig/ioa/ioaUtil.c
deleted file mode 100644
index 79dcca1e..00000000
--- a/src/aig/ioa/ioaUtil.c
+++ /dev/null
@@ -1,117 +0,0 @@
-/**CFile****************************************************************
-
- FileName [ioaUtil.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Command processing package.]
-
- Synopsis [Procedures to read binary AIGER format developed by
- Armin Biere, Johannes Kepler University (http://fmv.jku.at/)]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - December 16, 2006.]
-
- Revision [$Id: ioaUtil.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "ioa.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Returns the file size.]
-
- Description [The file should be closed.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ioa_FileSize( char * pFileName )
-{
- FILE * pFile;
- int nFileSize;
- pFile = fopen( pFileName, "r" );
- if ( pFile == NULL )
- {
- printf( "Ioa_FileSize(): The file is unavailable (absent or open).\n" );
- return 0;
- }
- fseek( pFile, 0, SEEK_END );
- nFileSize = ftell( pFile );
- fclose( pFile );
- return nFileSize;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-char * Ioa_FileNameGeneric( char * FileName )
-{
- char * pDot;
- char * pUnd;
- char * pRes;
-
- // find the generic name of the file
- pRes = Aig_UtilStrsav( FileName );
- // find the pointer to the "." symbol in the file name
-// pUnd = strstr( FileName, "_" );
- pUnd = NULL;
- pDot = strstr( FileName, "." );
- if ( pUnd )
- pRes[pUnd - FileName] = 0;
- else if ( pDot )
- pRes[pDot - FileName] = 0;
- return pRes;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns the time stamp.]
-
- Description [The file should be closed.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-char * Ioa_TimeStamp()
-{
- static char Buffer[100];
- char * TimeStamp;
- time_t ltime;
- // get the current time
- time( &ltime );
- TimeStamp = asctime( localtime( &ltime ) );
- TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
- strcpy( Buffer, TimeStamp );
- return Buffer;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/ioa/ioaWriteAig.c b/src/aig/ioa/ioaWriteAig.c
deleted file mode 100644
index a6c23fd4..00000000
--- a/src/aig/ioa/ioaWriteAig.c
+++ /dev/null
@@ -1,292 +0,0 @@
-/**CFile****************************************************************
-
- FileName [ioaWriteAiger.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Command processing package.]
-
- Synopsis [Procedures to write binary AIGER format developed by
- Armin Biere, Johannes Kepler University (http://fmv.jku.at/)]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - December 16, 2006.]
-
- Revision [$Id: ioaWriteAiger.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "ioa.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/*
- The following is taken from the AIGER format description,
- which can be found at http://fmv.jku.at/aiger
-*/
-
-
-/*
- The AIGER And-Inverter Graph (AIG) Format Version 20061129
- ----------------------------------------------------------
- Armin Biere, Johannes Kepler University, 2006
-
- This report describes the AIG file format as used by the AIGER library.
- The purpose of this report is not only to motivate and document the
- format, but also to allow independent implementations of writers and
- readers by giving precise and unambiguous definitions.
-
- ...
-
-Introduction
-
- The name AIGER contains as one part the acronym AIG of And-Inverter
- Graphs and also if pronounced in German sounds like the name of the
- 'Eiger', a mountain in the Swiss alps. This choice should emphasize the
- origin of this format. It was first openly discussed at the Alpine
- Verification Meeting 2006 in Ascona as a way to provide a simple, compact
- file format for a model checking competition affiliated to CAV 2007.
-
- ...
-
-Binary Format Definition
-
- The binary format is semantically a subset of the ASCII format with a
- slightly different syntax. The binary format may need to reencode
- literals, but translating a file in binary format into ASCII format and
- then back in to binary format will result in the same file.
-
- The main differences of the binary format to the ASCII format are as
- follows. After the header the list of input literals and all the
- current state literals of a latch can be omitted. Furthermore the
- definitions of the AND gates are binary encoded. However, the symbol
- table and the comment section are as in the ASCII format.
-
- The header of an AIGER file in binary format has 'aig' as format
- identifier, but otherwise is identical to the ASCII header. The standard
- file extension for the binary format is therefore '.aig'.
-
- A header for the binary format is still in ASCII encoding:
-
- aig M I L O A
-
- Constants, variables and literals are handled in the same way as in the
- ASCII format. The first simplifying restriction is on the variable
- indices of inputs and latches. The variable indices of inputs come first,
- followed by the pseudo-primary inputs of the latches and then the variable
- indices of all LHS of AND gates:
-
- input variable indices 1, 2, ... , I
- latch variable indices I+1, I+2, ... , (I+L)
- AND variable indices I+L+1, I+L+2, ... , (I+L+A) == M
-
- The corresponding unsigned literals are
-
- input literals 2, 4, ... , 2*I
- latch literals 2*I+2, 2*I+4, ... , 2*(I+L)
- AND literals 2*(I+L)+2, 2*(I+L)+4, ... , 2*(I+L+A) == 2*M
-
- All literals have to be defined, and therefore 'M = I + L + A'. With this
- restriction it becomes possible that the inputs and the current state
- literals of the latches do not have to be listed explicitly. Therefore,
- after the header only the list of 'L' next state literals follows, one per
- latch on a single line, and then the 'O' outputs, again one per line.
-
- In the binary format we assume that the AND gates are ordered and respect
- the child parent relation. AND gates with smaller literals on the LHS
- come first. Therefore we can assume that the literals on the right-hand
- side of a definition of an AND gate are smaller than the LHS literal.
- Furthermore we can sort the literals on the RHS, such that the larger
- literal comes first. A definition thus consists of three literals
-
- lhs rhs0 rhs1
-
- with 'lhs' even and 'lhs > rhs0 >= rhs1'. Also the variable indices are
- pairwise different to avoid combinational self loops. Since the LHS
- indices of the definitions are all consecutive (as even integers),
- the binary format does not have to keep 'lhs'. In addition, we can use
- the order restriction and only write the differences 'delta0' and 'delta1'
- instead of 'rhs0' and 'rhs1', with
-
- delta0 = lhs - rhs0, delta1 = rhs0 - rhs1
-
- The differences will all be strictly positive, and in practice often very
- small. We can take advantage of this fact by the simple little-endian
- encoding of unsigned integers of the next section. After the binary delta
- encoding of the RHSs of all AND gates, the optional symbol table and
- optional comment section start in the same format as in the ASCII case.
-
- ...
-
-*/
-
-static unsigned Ioa_ObjMakeLit( int Var, int fCompl ) { return (Var << 1) | fCompl; }
-static unsigned Ioa_ObjAigerNum( Aig_Obj_t * pObj ) { return (unsigned)pObj->pData; }
-static void Ioa_ObjSetAigerNum( Aig_Obj_t * pObj, unsigned Num ) { pObj->pData = (void *)Num; }
-
-int Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Writes the AIG in the binary AIGER format.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols )
-{
- Bar_Progress_t * pProgress;
- FILE * pFile;
- Aig_Obj_t * pObj, * pDriver;
- int i, nNodes, Pos, nBufferSize;
- unsigned char * pBuffer;
- unsigned uLit0, uLit1, uLit;
-
-// assert( Aig_ManIsStrash(pMan) );
- // start the output stream
- pFile = fopen( pFileName, "wb" );
- if ( pFile == NULL )
- {
- fprintf( stdout, "Ioa_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
- return;
- }
-/*
- Aig_ManForEachLatch( pMan, pObj, i )
- if ( !Aig_LatchIsInit0(pObj) )
- {
- fprintf( stdout, "Ioa_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
- return;
- }
-*/
- // set the node numbers to be used in the output file
- nNodes = 0;
- Ioa_ObjSetAigerNum( Aig_ManConst1(pMan), nNodes++ );
- Aig_ManForEachPi( pMan, pObj, i )
- Ioa_ObjSetAigerNum( pObj, nNodes++ );
- Aig_ManForEachNode( pMan, pObj, i )
- Ioa_ObjSetAigerNum( pObj, nNodes++ );
-
- // write the header "M I L O A" where M = I + L + A
- fprintf( pFile, "aig %u %u %u %u %u\n",
- Aig_ManPiNum(pMan) + Aig_ManNodeNum(pMan),
- Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan),
- Aig_ManRegNum(pMan),
- Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan),
- Aig_ManNodeNum(pMan) );
-
- // if the driver node is a constant, we need to complement the literal below
- // because, in the AIGER format, literal 0/1 is represented as number 0/1
- // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
-
- // write latch drivers
- Aig_ManForEachLiSeq( pMan, pObj, i )
- {
- pDriver = Aig_ObjFanin0(pObj);
- fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
- }
-
- // write PO drivers
- Aig_ManForEachPoSeq( pMan, pObj, i )
- {
- pDriver = Aig_ObjFanin0(pObj);
- fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
- }
-
- // write the nodes into the buffer
- Pos = 0;
- nBufferSize = 6 * Aig_ManNodeNum(pMan) + 100; // skeptically assuming 3 chars per one AIG edge
- pBuffer = ALLOC( char, nBufferSize );
- pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pMan) );
- Aig_ManForEachNode( pMan, pObj, i )
- {
- Bar_ProgressUpdate( pProgress, i, NULL );
- uLit = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pObj), 0 );
- uLit0 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) );
- uLit1 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) );
- assert( uLit0 < uLit1 );
- Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 );
- Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
- if ( Pos > nBufferSize - 10 )
- {
- printf( "Ioa_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
- fclose( pFile );
- return;
- }
- }
- assert( Pos < nBufferSize );
- Bar_ProgressStop( pProgress );
-
- // write the buffer
- fwrite( pBuffer, 1, Pos, pFile );
- free( pBuffer );
-/*
- // write the symbol table
- if ( fWriteSymbols )
- {
- // write PIs
- Aig_ManForEachPi( pMan, pObj, i )
- fprintf( pFile, "i%d %s\n", i, Aig_ObjName(pObj) );
- // write latches
- Aig_ManForEachLatch( pMan, pObj, i )
- fprintf( pFile, "l%d %s\n", i, Aig_ObjName(Aig_ObjFanout0(pObj)) );
- // write POs
- Aig_ManForEachPo( pMan, pObj, i )
- fprintf( pFile, "o%d %s\n", i, Aig_ObjName(pObj) );
- }
-*/
- // write the comment
- fprintf( pFile, "c\n" );
- if ( pMan->pName )
- fprintf( pFile, ".model %s\n", pMan->pName );
- fprintf( pFile, "This file was produced by the AIG package in ABC on %s\n", Ioa_TimeStamp() );
- fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
- fclose( pFile );
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds one unsigned AIG edge to the output buffer.]
-
- Description [This procedure is a slightly modified version of Armin Biere's
- procedure "void encode (FILE * file, unsigned x)" ]
-
- SideEffects [Returns the current writing position.]
-
- SeeAlso []
-
-***********************************************************************/
-int Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x )
-{
- unsigned char ch;
- while (x & ~0x7f)
- {
- ch = (x & 0x7f) | 0x80;
-// putc (ch, file);
- pBuffer[Pos++] = ch;
- x >>= 7;
- }
- ch = x;
-// putc (ch, file);
- pBuffer[Pos++] = ch;
- return Pos;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/ioa/module.make b/src/aig/ioa/module.make
deleted file mode 100644
index 66b4a0d5..00000000
--- a/src/aig/ioa/module.make
+++ /dev/null
@@ -1,3 +0,0 @@
-SRC += src/aig/ioa/ioaReadAig.c \
- src/aig/ioa/ioaWriteAig.c \
- src/aig/ioa/ioaUtil.c
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-17 13:13:04 +0000