Version abc80130

5 files changed, 0 insertions, 944 deletions

diff --git a/src/aig/ioa/ioa.h b/src/aig/ioa/ioa.h
deleted file mode 100644
index e697a729..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, int fCompact );
-/*=== 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 498cdd30..00000000
--- a/src/aig/ioa/ioaReadAig.c
+++ /dev/null
@@ -1,366 +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                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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));
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Decodes the encoded array of literals.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Ioa_WriteDecodeLiterals( char ** ppPos, int nEntries )
-{
-    Vec_Int_t * vLits;
-    int Lit, LitPrev, Diff, i;
-    vLits = Vec_IntAlloc( nEntries );
-    LitPrev = Ioa_ReadAigerDecode( ppPos );
-    Vec_IntPush( vLits, LitPrev );
-    for ( i = 1; i < nEntries; i++ )
-    {
-//        Diff = Lit - LitPrev;
-//        Diff = (Lit < LitPrev)? -Diff : Diff;
-//        Diff = ((2 * Diff) << 1) | (int)(Lit < LitPrev);
-        Diff = Ioa_ReadAigerDecode( ppPos );
-        Diff = (Diff & 1)? -(Diff >> 1) : Diff >> 1;
-        Lit  = Diff + LitPrev;
-        Vec_IntPush( vLits, Lit );
-        LitPrev = Lit;
-    }
-    return vLits;
-}
-
-
-/**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_Int_t * vLits = NULL;
-    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 || (pContents[3] != ' ' && pContents[3] != '2') )
-    {
-        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;
-    if ( pContents[3] == ' ' ) // standard AIGER
-    {
-        // scroll to the beginning of the binary data
-        for ( i = 0; i < nLatches + nOutputs; )
-            if ( *pCur++ == '\n' )
-                i++;
-    }
-    else // modified AIGER
-    {
-        vLits = Ioa_WriteDecodeLiterals( &pCur, nLatches + nOutputs );
-    }
-
-    // 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 );
-    if ( pContents[3] == ' ' ) // standard AIGER
-    {
-        pCur = pDrivers;
-        for ( i = 0; i < nLatches; i++ )
-        {
-            uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
-            pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
-            Vec_PtrPush( vDrivers, pNode0 );
-        }
-        // read the PO driver literals
-        for ( i = 0; i < nOutputs; i++ )
-        {
-            uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
-            pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
-            Vec_PtrPush( vDrivers, pNode0 );
-        }
-
-    }
-    else
-    {
-        // read the latch driver literals
-        for ( i = 0; i < nLatches; i++ )
-        {
-            uLit0 = Vec_IntEntry( vLits, i );
-            pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
-            Vec_PtrPush( vDrivers, pNode0 );
-        }
-        // read the PO driver literals
-        for ( i = 0; i < nOutputs; i++ )
-        {
-            uLit0 = Vec_IntEntry( vLits, i+nLatches );
-            pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
-            Vec_PtrPush( vDrivers, pNode0 );
-        }
-        Vec_IntFree( vLits );
-    }
-
-    // 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;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       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 166dca4b..00000000
--- a/src/aig/ioa/ioaWriteAig.c
+++ /dev/null
@@ -1,378 +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 int      Ioa_ObjMakeLit( int Var, int fCompl )                 { return (Var << 1) | fCompl;  }
-static int      Ioa_ObjAigerNum( Aig_Obj_t * pObj )                   { return pObj->iData;          }
-static void     Ioa_ObjSetAigerNum( Aig_Obj_t * pObj, unsigned Num )  { pObj->iData = Num;           }
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Create the array of literals to be written.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Ioa_WriteAigerLiterals( Aig_Man_t * pMan )
-{
-    Vec_Int_t * vLits;
-    Aig_Obj_t * pObj, * pDriver;
-    int i;
-    vLits = Vec_IntAlloc( Aig_ManPoNum(pMan) );
-    Aig_ManForEachLiSeq( pMan, pObj, i )
-    {
-        pDriver = Aig_ObjFanin0(pObj);
-        Vec_IntPush( vLits, Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
-    }
-    Aig_ManForEachPoSeq( pMan, pObj, i )
-    {
-        pDriver = Aig_ObjFanin0(pObj);
-        Vec_IntPush( vLits, Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
-    }
-    return vLits;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the binary encoded array of literals.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Str_t * Ioa_WriteEncodeLiterals( Vec_Int_t * vLits )
-{
-    Vec_Str_t * vBinary;
-    int Pos = 0, Lit, LitPrev, Diff, i;
-    vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) );
-    LitPrev = Vec_IntEntry( vLits, 0 );
-    Pos = Ioa_WriteAigerEncode( Vec_StrArray(vBinary), Pos, LitPrev ); 
-    Vec_IntForEachEntryStart( vLits, Lit, i, 1 )
-    {
-        Diff = Lit - LitPrev;
-        Diff = (Lit < LitPrev)? -Diff : Diff;
-        Diff = (Diff << 1) | (int)(Lit < LitPrev);
-        Pos = Ioa_WriteAigerEncode( Vec_StrArray(vBinary), Pos, Diff );
-        LitPrev = Lit;
-        if ( Pos + 10 > vBinary->nCap )
-            Vec_StrGrow( vBinary, vBinary->nCap+1 );
-    }
-    vBinary->nSize = Pos;
-/*
-    // verify
-    {
-        extern Vec_Int_t * Ioa_WriteDecodeLiterals( char ** ppPos, int nEntries );
-        char * pPos = Vec_StrArray( vBinary );
-        Vec_Int_t * vTemp = Ioa_WriteDecodeLiterals( &pPos, Vec_IntSize(vLits) );
-        for ( i = 0; i < Vec_IntSize(vLits); i++ )
-        {
-            int Entry1 = Vec_IntEntry(vLits,i);
-            int Entry2 = Vec_IntEntry(vTemp,i);
-            assert( Entry1 == Entry2 );
-        }
-        Vec_IntFree( vTemp );
-    }
-*/
-    return vBinary;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Writes the AIG in the binary AIGER format.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact )
-{
-//    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%s %u %u %u %u %u\n", 
-        fCompact? "2" : "",
-        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
-
-    if ( !fCompact ) 
-    {
-        // 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) ) );
-        }
-    }
-    else
-    {
-        Vec_Int_t * vLits = Ioa_WriteAigerLiterals( pMan );
-        Vec_Str_t * vBinary = Ioa_WriteEncodeLiterals( vLits );
-        fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile );
-        Vec_StrFree( vBinary );
-        Vec_IntFree( vLits );
-    }
-
-    // write the nodes into the buffer
-    Pos = 0;
-    nBufferSize = 6 * Aig_ManNodeNum(pMan) + 100; // skeptically assuming 3 chars per one AIG edge
-    pBuffer = ALLOC( unsigned 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, (unsigned)(uLit  - uLit1) );
-        Pos = Ioa_WriteAigerEncode( pBuffer, Pos, (unsigned)(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 on %s\n", Ioa_TimeStamp() );
-    fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
-    fclose( pFile );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       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