abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaAiger.c File Reference
#include "gia.h"
#include "misc/tim/tim.h"
#include "base/main/main.h"

Go to the source code of this file.

Macros

#define XAIG_VERBOSE   0
 

Functions

void Gia_FileFixName (char *pFileName)
 DECLARATIONS ///. More...
 
char * Gia_FileNameGeneric (char *FileName)
 
int Gia_FileSize (char *pFileName)
 FUNCTION DECLARATIONS ///. More...
 
void Gia_FileWriteBufferSize (FILE *pFile, int nSize)
 
Vec_Int_tGia_AigerCollectLiterals (Gia_Man_t *p)
 
Vec_Int_tGia_AigerReadLiterals (unsigned char **ppPos, int nEntries)
 
Vec_Str_tGia_AigerWriteLiterals (Vec_Int_t *vLits)
 
Gia_Man_tGia_AigerReadFromMemory (char *pContents, int nFileSize, int fSkipStrash, int fCheck)
 
Gia_Man_tGia_AigerRead (char *pFileName, int fSkipStrash, int fCheck)
 
Vec_Str_tGia_AigerWriteIntoMemoryStr (Gia_Man_t *p)
 
Vec_Str_tGia_AigerWriteIntoMemoryStrPart (Gia_Man_t *p, Vec_Int_t *vCis, Vec_Int_t *vAnds, Vec_Int_t *vCos, int nRegs)
 
void Gia_AigerWrite (Gia_Man_t *pInit, char *pFileName, int fWriteSymbols, int fCompact)
 
void Gia_DumpAiger (Gia_Man_t *p, char *pFilePrefix, int iFileNum, int nFileNumDigits)
 
void Gia_AigerWriteSimple (Gia_Man_t *pInit, char *pFileName)
 

Macro Definition Documentation

#define XAIG_VERBOSE   0

CFile****************************************************************

FileName [giaAiger.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [Procedures to read/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 - June 20, 2005.]

Revision [

Id:
giaAiger.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 28 of file giaAiger.c.

Function Documentation

Vec_Int_t* Gia_AigerCollectLiterals ( Gia_Man_t p)

Function*************************************************************

Synopsis [Create the array of literals to be written.]

Description []

SideEffects []

SeeAlso []

Definition at line 97 of file giaAiger.c.

98 {
99  Vec_Int_t * vLits;
100  Gia_Obj_t * pObj;
101  int i;
102  vLits = Vec_IntAlloc( Gia_ManPoNum(p) );
103  Gia_ManForEachRi( p, pObj, i )
104  Vec_IntPush( vLits, Gia_ObjFaninLit0p(p, pObj) );
105  Gia_ManForEachPo( p, pObj, i )
106  Vec_IntPush( vLits, Gia_ObjFaninLit0p(p, pObj) );
107  return vLits;
108 }
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static int Gia_ObjFaninLit0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:469
Definition: gia.h:75
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
Gia_Man_t* Gia_AigerRead ( char *  pFileName,
int  fSkipStrash,
int  fCheck 
)

Function*************************************************************

Synopsis [Reads the AIG in the binary AIGER format.]

Description []

SideEffects []

SeeAlso []

Definition at line 821 of file giaAiger.c.

822 {
823  FILE * pFile;
824  Gia_Man_t * pNew;
825  char * pName, * pContents;
826  int nFileSize;
827  int RetValue;
828 
829  // read the file into the buffer
830  Gia_FileFixName( pFileName );
831  nFileSize = Gia_FileSize( pFileName );
832  pFile = fopen( pFileName, "rb" );
833  pContents = ABC_ALLOC( char, nFileSize );
834  RetValue = fread( pContents, nFileSize, 1, pFile );
835  fclose( pFile );
836 
837  pNew = Gia_AigerReadFromMemory( pContents, nFileSize, fSkipStrash, fCheck );
838  ABC_FREE( pContents );
839  if ( pNew )
840  {
841  ABC_FREE( pNew->pName );
842  pName = Gia_FileNameGeneric( pFileName );
843  pNew->pName = Abc_UtilStrsav( pName );
844  ABC_FREE( pName );
845 
846  assert( pNew->pSpec == NULL );
847  pNew->pSpec = Abc_UtilStrsav( pFileName );
848  }
849  return pNew;
850 }
void Gia_FileFixName(char *pFileName)
DECLARATIONS ///.
Definition: giaAiger.c:49
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
int Gia_FileSize(char *pFileName)
FUNCTION DECLARATIONS ///.
Definition: giaAiger.c:64
char * pName
Definition: gia.h:97
char * pSpec
Definition: gia.h:98
char * Gia_FileNameGeneric(char *FileName)
Definition: giaAiger.c:56
#define ABC_FREE(obj)
Definition: abc_global.h:232
Definition: gia.h:95
#define assert(ex)
Definition: util_old.h:213
Gia_Man_t * Gia_AigerReadFromMemory(char *pContents, int nFileSize, int fSkipStrash, int fCheck)
Definition: giaAiger.c:176
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Gia_Man_t* Gia_AigerReadFromMemory ( char *  pContents,
int  nFileSize,
int  fSkipStrash,
int  fCheck 
)

Function*************************************************************

Synopsis [Reads the AIG in the binary AIGER format.]

Description []

SideEffects []

SeeAlso []

Definition at line 176 of file giaAiger.c.

177 {
178  Gia_Man_t * pNew, * pTemp;
179  Vec_Int_t * vLits = NULL, * vPoTypes = NULL;
180  Vec_Int_t * vNodes, * vDrivers, * vInits = NULL;
181  int iObj, iNode0, iNode1, fHieOnly = 0;
182  int nTotal, nInputs, nOutputs, nLatches, nAnds, i;
183  int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
184  unsigned char * pDrivers, * pSymbols, * pCur;
185  unsigned uLit0, uLit1, uLit;
186 
187  // read the parameters (M I L O A + B C J F)
188  pCur = (unsigned char *)pContents; while ( *pCur != ' ' ) pCur++; pCur++;
189  // read the number of objects
190  nTotal = atoi( (const char *)pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
191  // read the number of inputs
192  nInputs = atoi( (const char *)pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
193  // read the number of latches
194  nLatches = atoi( (const char *)pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
195  // read the number of outputs
196  nOutputs = atoi( (const char *)pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
197  // read the number of nodes
198  nAnds = atoi( (const char *)pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
199  if ( *pCur == ' ' )
200  {
201 // assert( nOutputs == 0 );
202  // read the number of properties
203  pCur++;
204  nBad = atoi( (const char *)pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
205  nOutputs += nBad;
206  }
207  if ( *pCur == ' ' )
208  {
209  // read the number of properties
210  pCur++;
211  nConstr = atoi( (const char *)pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
212  nOutputs += nConstr;
213  }
214  if ( *pCur == ' ' )
215  {
216  // read the number of properties
217  pCur++;
218  nJust = atoi( (const char *)pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
219  nOutputs += nJust;
220  }
221  if ( *pCur == ' ' )
222  {
223  // read the number of properties
224  pCur++;
225  nFair = atoi( (const char *)pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
226  nOutputs += nFair;
227  }
228  if ( *pCur != '\n' )
229  {
230  fprintf( stdout, "The parameter line is in a wrong format.\n" );
231  return NULL;
232  }
233  pCur++;
234 
235  // check the parameters
236  if ( nTotal != nInputs + nLatches + nAnds )
237  {
238  fprintf( stdout, "The number of objects does not match.\n" );
239  return NULL;
240  }
241  if ( nJust || nFair )
242  {
243  fprintf( stdout, "Reading AIGER files with liveness properties is currently not supported.\n" );
244  return NULL;
245  }
246 
247  if ( nConstr )
248  {
249  if ( nConstr == 1 )
250  fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
251  else
252  fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
253  }
254 
255  // allocate the empty AIG
256  pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
257  pNew->nConstrs = nConstr;
258 
259  // prepare the array of nodes
260  vNodes = Vec_IntAlloc( 1 + nTotal );
261  Vec_IntPush( vNodes, 0 );
262 
263  // create the PIs
264  for ( i = 0; i < nInputs + nLatches; i++ )
265  {
266  iObj = Gia_ManAppendCi(pNew);
267  Vec_IntPush( vNodes, iObj );
268  }
269 
270  // remember the beginning of latch/PO literals
271  pDrivers = pCur;
272  if ( pContents[3] == ' ' ) // standard AIGER
273  {
274  // scroll to the beginning of the binary data
275  for ( i = 0; i < nLatches + nOutputs; )
276  if ( *pCur++ == '\n' )
277  i++;
278  }
279  else // modified AIGER
280  {
281  vLits = Gia_AigerReadLiterals( &pCur, nLatches + nOutputs );
282  }
283 
284  // create the AND gates
285  if ( !fSkipStrash )
286  Gia_ManHashAlloc( pNew );
287  for ( i = 0; i < nAnds; i++ )
288  {
289  uLit = ((i + 1 + nInputs + nLatches) << 1);
290  uLit1 = uLit - Gia_AigerReadUnsigned( &pCur );
291  uLit0 = uLit1 - Gia_AigerReadUnsigned( &pCur );
292 // assert( uLit1 > uLit0 );
293  iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
294  iNode1 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
295  assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches );
296  if ( fSkipStrash )
297  {
298  if ( iNode0 == iNode1 )
299  Vec_IntPush( vNodes, Gia_ManAppendBuf(pNew, iNode0) );
300  else
301  Vec_IntPush( vNodes, Gia_ManAppendAnd(pNew, iNode0, iNode1) );
302  }
303  else
304  Vec_IntPush( vNodes, Gia_ManHashAnd(pNew, iNode0, iNode1) );
305  }
306  if ( !fSkipStrash )
307  Gia_ManHashStop( pNew );
308 
309  // remember the place where symbols begin
310  pSymbols = pCur;
311 
312  // read the latch driver literals
313  vDrivers = Vec_IntAlloc( nLatches + nOutputs );
314  if ( pContents[3] == ' ' ) // standard AIGER
315  {
316  vInits = Vec_IntAlloc( nLatches );
317  pCur = pDrivers;
318  for ( i = 0; i < nLatches; i++ )
319  {
320  uLit0 = atoi( (char *)pCur );
321  while ( *pCur != ' ' && *pCur != '\n' )
322  pCur++;
323  if ( *pCur == ' ' )
324  {
325  pCur++;
326  Vec_IntPush( vInits, atoi( (char *)pCur ) );
327  while ( *pCur++ != '\n' );
328  }
329  else
330  {
331  pCur++;
332  Vec_IntPush( vInits, 0 );
333  }
334  iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
335  Vec_IntPush( vDrivers, iNode0 );
336  }
337  // read the PO driver literals
338  for ( i = 0; i < nOutputs; i++ )
339  {
340  uLit0 = atoi( (char *)pCur ); while ( *pCur++ != '\n' );
341  iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
342  Vec_IntPush( vDrivers, iNode0 );
343  }
344 
345  }
346  else
347  {
348  // read the latch driver literals
349  for ( i = 0; i < nLatches; i++ )
350  {
351  uLit0 = Vec_IntEntry( vLits, i );
352  iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
353  Vec_IntPush( vDrivers, iNode0 );
354  }
355  // read the PO driver literals
356  for ( i = 0; i < nOutputs; i++ )
357  {
358  uLit0 = Vec_IntEntry( vLits, i+nLatches );
359  iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
360  Vec_IntPush( vDrivers, iNode0 );
361  }
362  Vec_IntFree( vLits );
363  }
364 
365  // create the POs
366  for ( i = 0; i < nOutputs; i++ )
367  Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, nLatches + i) );
368  for ( i = 0; i < nLatches; i++ )
369  Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, i) );
370  Vec_IntFree( vDrivers );
371 
372  // create the latches
373  Gia_ManSetRegNum( pNew, nLatches );
374 
375  // read signal names if they are of the special type
376  pCur = pSymbols;
377  if ( pCur < (unsigned char *)pContents + nFileSize && *pCur != 'c' )
378  {
379  int fBreakUsed = 0;
380  unsigned char * pCurOld = pCur;
381  pNew->vUserPiIds = Vec_IntStartFull( nInputs );
382  pNew->vUserPoIds = Vec_IntStartFull( nOutputs );
383  pNew->vUserFfIds = Vec_IntStartFull( nLatches );
384  while ( pCur < (unsigned char *)pContents + nFileSize && *pCur != 'c' )
385  {
386  int iTerm;
387  char * pType = (char *)pCur;
388  // check terminal type
389  if ( *pCur != 'i' && *pCur != 'o' && *pCur != 'l' )
390  {
391 // fprintf( stdout, "Wrong terminal type.\n" );
392  fBreakUsed = 1;
393  break;
394  }
395  // get terminal number
396  iTerm = atoi( (char *)++pCur ); while ( *pCur++ != ' ' );
397  // skip spaces
398  while ( *pCur == ' ' )
399  pCur++;
400  // decode the user numbers:
401  // flops are named: @l<num>
402  // PIs are named: @i<num>
403  // POs are named: @o<num>
404  if ( *pCur++ != '@' )
405  {
406  fBreakUsed = 1;
407  break;
408  }
409  if ( *pCur == 'i' && *pType == 'i' )
410  Vec_IntWriteEntry( pNew->vUserPiIds, iTerm, atoi((char *)pCur+1) );
411  else if ( *pCur == 'o' && *pType == 'o' )
412  Vec_IntWriteEntry( pNew->vUserPoIds, iTerm, atoi((char *)pCur+1) );
413  else if ( *pCur == 'l' && *pType == 'l' )
414  Vec_IntWriteEntry( pNew->vUserFfIds, iTerm, atoi((char *)pCur+1) );
415  else
416  {
417  fprintf( stdout, "Wrong name format.\n" );
418  fBreakUsed = 1;
419  break;
420  }
421  // skip digits
422  while ( *pCur++ != '\n' );
423  }
424  // in case of abnormal termination, remove the arrays
425  if ( fBreakUsed )
426  {
427  unsigned char * pName;
428  int Entry, nInvars, nConstr, iTerm;
429 
430  Vec_Int_t * vPoNames = Vec_IntStartFull( nOutputs );
431 
432  Vec_IntFreeP( &pNew->vUserPiIds );
433  Vec_IntFreeP( &pNew->vUserPoIds );
434  Vec_IntFreeP( &pNew->vUserFfIds );
435 
436  // try to figure out signal names
437  fBreakUsed = 0;
438  pCur = (unsigned char *)pCurOld;
439  while ( pCur < (unsigned char *)pContents + nFileSize && *pCur != 'c' )
440  {
441  // get the terminal type
442  if ( *pCur == 'i' || *pCur == 'l' )
443  {
444  // skip till the end of the line
445  while ( *pCur++ != '\n' );
446  *(pCur-1) = 0;
447  continue;
448  }
449  if ( *pCur != 'o' )
450  {
451 // fprintf( stdout, "Wrong terminal type.\n" );
452  fBreakUsed = 1;
453  break;
454  }
455  // get the terminal number
456  iTerm = atoi( (char *)++pCur ); while ( *pCur++ != ' ' );
457  // get the node
458  if ( iTerm < 0 || iTerm >= nOutputs )
459  {
460  fprintf( stdout, "The output number (%d) is out of range.\n", iTerm );
461  fBreakUsed = 1;
462  break;
463  }
464  if ( Vec_IntEntry(vPoNames, iTerm) != ~0 )
465  {
466  fprintf( stdout, "The output number (%d) is listed twice.\n", iTerm );
467  fBreakUsed = 1;
468  break;
469  }
470 
471  // get the name
472  pName = pCur; while ( *pCur++ != '\n' );
473  *(pCur-1) = 0;
474  // assign the name
475  Vec_IntWriteEntry( vPoNames, iTerm, pName - (unsigned char *)pContents );
476  }
477 
478  // check that all names are assigned
479  if ( !fBreakUsed )
480  {
481  nInvars = nConstr = 0;
482  vPoTypes = Vec_IntStart( Gia_ManPoNum(pNew) );
483  Vec_IntForEachEntry( vPoNames, Entry, i )
484  {
485  if ( Entry == ~0 )
486  continue;
487  if ( strncmp( pContents+Entry, "constraint:", 11 ) == 0 )
488  {
489  Vec_IntWriteEntry( vPoTypes, i, 1 );
490  nConstr++;
491  }
492  if ( strncmp( pContents+Entry, "invariant:", 10 ) == 0 )
493  {
494  Vec_IntWriteEntry( vPoTypes, i, 2 );
495  nInvars++;
496  }
497  }
498  if ( nConstr )
499  fprintf( stdout, "Recognized and added %d constraints.\n", nConstr );
500  if ( nInvars )
501  fprintf( stdout, "Recognized and skipped %d invariants.\n", nInvars );
502  if ( nConstr == 0 && nInvars == 0 )
503  Vec_IntFreeP( &vPoTypes );
504  }
505  Vec_IntFree( vPoNames );
506  }
507  }
508 
509 
510  // check if there are other types of information to read
511  if ( pCur + 1 < (unsigned char *)pContents + nFileSize && *pCur == 'c' )
512  {
513  int fVerbose = XAIG_VERBOSE;
514  Vec_Str_t * vStr;
515  unsigned char * pCurTemp;
516  pCur++;
517  // skip new line if present
518 // if ( *pCur == '\n' )
519 // pCur++;
520  while ( pCur < (unsigned char *)pContents + nFileSize )
521  {
522  // read extra AIG
523  if ( *pCur == 'a' )
524  {
525  pCur++;
526  vStr = Vec_StrStart( Gia_AigerReadInt(pCur) ); pCur += 4;
527  memcpy( Vec_StrArray(vStr), pCur, Vec_StrSize(vStr) );
528  pCur += Vec_StrSize(vStr);
529  pNew->pAigExtra = Gia_AigerReadFromMemory( Vec_StrArray(vStr), Vec_StrSize(vStr), 0, 0 );
530  Vec_StrFree( vStr );
531  if ( fVerbose ) printf( "Finished reading extension \"a\".\n" );
532  }
533  // read number of constraints
534  else if ( *pCur == 'c' )
535  {
536  pCur++;
537  assert( Gia_AigerReadInt(pCur) == 4 ); pCur += 4;
538  pNew->nConstrs = Gia_AigerReadInt( pCur ); pCur += 4;
539  if ( fVerbose ) printf( "Finished reading extension \"c\".\n" );
540  }
541  // read delay information
542  else if ( *pCur == 'd' )
543  {
544  pCur++;
545  assert( Gia_AigerReadInt(pCur) == 4 ); pCur += 4;
546  pNew->nAnd2Delay = Gia_AigerReadInt(pCur); pCur += 4;
547  if ( fVerbose ) printf( "Finished reading extension \"d\".\n" );
548  }
549  else if ( *pCur == 'i' )
550  {
551  pCur++;
552  nInputs = Gia_AigerReadInt(pCur)/4; pCur += 4;
553  pNew->vInArrs = Vec_FltStart( nInputs );
554  memcpy( Vec_FltArray(pNew->vInArrs), pCur, 4*nInputs ); pCur += 4*nInputs;
555  if ( fVerbose ) printf( "Finished reading extension \"i\".\n" );
556  }
557  else if ( *pCur == 'o' )
558  {
559  pCur++;
560  nOutputs = Gia_AigerReadInt(pCur)/4; pCur += 4;
561  pNew->vOutReqs = Vec_FltStart( nOutputs );
562  memcpy( Vec_FltArray(pNew->vOutReqs), pCur, 4*nOutputs ); pCur += 4*nOutputs;
563  if ( fVerbose ) printf( "Finished reading extension \"o\".\n" );
564  }
565  // read equivalence classes
566  else if ( *pCur == 'e' )
567  {
568  extern Gia_Rpr_t * Gia_AigerReadEquivClasses( unsigned char ** ppPos, int nSize );
569  pCur++;
570  pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4;
571  pNew->pReprs = Gia_AigerReadEquivClasses( &pCur, Gia_ManObjNum(pNew) );
572  pNew->pNexts = Gia_ManDeriveNexts( pNew );
573  assert( pCur == pCurTemp );
574  if ( fVerbose ) printf( "Finished reading extension \"e\".\n" );
575  }
576  // read flop classes
577  else if ( *pCur == 'f' )
578  {
579  pCur++;
580  assert( Gia_AigerReadInt(pCur) == 4*Gia_ManRegNum(pNew) ); pCur += 4;
581  pNew->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pNew) );
582  memcpy( Vec_IntArray(pNew->vFlopClasses), pCur, 4*Gia_ManRegNum(pNew) ); pCur += 4*Gia_ManRegNum(pNew);
583  if ( fVerbose ) printf( "Finished reading extension \"f\".\n" );
584  }
585  // read gate classes
586  else if ( *pCur == 'g' )
587  {
588  pCur++;
589  assert( Gia_AigerReadInt(pCur) == 4*Gia_ManObjNum(pNew) ); pCur += 4;
590  pNew->vGateClasses = Vec_IntStart( Gia_ManObjNum(pNew) );
591  memcpy( Vec_IntArray(pNew->vGateClasses), pCur, 4*Gia_ManObjNum(pNew) ); pCur += 4*Gia_ManObjNum(pNew);
592  if ( fVerbose ) printf( "Finished reading extension \"g\".\n" );
593  }
594  // read hierarchy information
595  else if ( *pCur == 'h' )
596  {
597  pCur++;
598  vStr = Vec_StrStart( Gia_AigerReadInt(pCur) ); pCur += 4;
599  memcpy( Vec_StrArray(vStr), pCur, Vec_StrSize(vStr) );
600  pCur += Vec_StrSize(vStr);
601  pNew->pManTime = Tim_ManLoad( vStr, 1 );
602  Vec_StrFree( vStr );
603  fHieOnly = 1;
604  if ( fVerbose ) printf( "Finished reading extension \"h\".\n" );
605  }
606  // read packing
607  else if ( *pCur == 'k' )
608  {
609  extern Vec_Int_t * Gia_AigerReadPacking( unsigned char ** ppPos, int nSize );
610  int nSize;
611  pCur++;
612  nSize = Gia_AigerReadInt(pCur);
613  pCurTemp = pCur + nSize + 4; pCur += 4;
614  pNew->vPacking = Gia_AigerReadPacking( &pCur, nSize );
615  assert( pCur == pCurTemp );
616  if ( fVerbose ) printf( "Finished reading extension \"k\".\n" );
617  }
618  // read mapping
619  else if ( *pCur == 'm' )
620  {
621  extern int * Gia_AigerReadMapping( unsigned char ** ppPos, int nSize );
622  extern int * Gia_AigerReadMappingSimple( unsigned char ** ppPos, int nSize );
623  extern Vec_Int_t * Gia_AigerReadMappingDoc( unsigned char ** ppPos, int nObjs );
624  int nSize;
625  pCur++;
626  nSize = Gia_AigerReadInt(pCur);
627  pCurTemp = pCur + nSize + 4; pCur += 4;
628  pNew->vMapping = Gia_AigerReadMappingDoc( &pCur, Gia_ManObjNum(pNew) );
629  assert( pCur == pCurTemp );
630  if ( fVerbose ) printf( "Finished reading extension \"m\".\n" );
631  }
632  // read model name
633  else if ( *pCur == 'n' )
634  {
635  pCur++;
636  if ( (*pCur >= 'a' && *pCur <= 'z') || (*pCur >= 'A' && *pCur <= 'Z') || (*pCur >= '0' && *pCur <= '9') )
637  {
638  pNew->pName = Abc_UtilStrsav( (char *)pCur ); pCur += strlen(pNew->pName) + 1;
639  }
640  else
641  {
642  pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4;
643  ABC_FREE( pNew->pName );
644  pNew->pName = Abc_UtilStrsav( (char *)pCur ); pCur += strlen(pNew->pName) + 1;
645  assert( pCur == pCurTemp );
646  }
647  }
648  // read placement
649  else if ( *pCur == 'p' )
650  {
651  Gia_Plc_t * pPlacement;
652  pCur++;
653  pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4;
654  pPlacement = ABC_ALLOC( Gia_Plc_t, Gia_ManObjNum(pNew) );
655  memcpy( pPlacement, pCur, 4*Gia_ManObjNum(pNew) ); pCur += 4*Gia_ManObjNum(pNew);
656  assert( pCur == pCurTemp );
657  pNew->pPlacement = pPlacement;
658  if ( fVerbose ) printf( "Finished reading extension \"p\".\n" );
659  }
660  // read register classes
661  else if ( *pCur == 'r' )
662  {
663  int i, nRegs;
664  pCur++;
665  nRegs = Gia_AigerReadInt(pCur)/4; pCur += 4;
666  pNew->vRegClasses = Vec_IntAlloc( nRegs );
667  for ( i = 0; i < nRegs; i++ )
668  Vec_IntPush( pNew->vRegClasses, Gia_AigerReadInt(pCur) ), pCur += 4;
669  if ( fVerbose ) printf( "Finished reading extension \"r\".\n" );
670  }
671  // read choices
672  else if ( *pCur == 'q' )
673  {
674  int i, nPairs, iRepr, iNode;
675  assert( !Gia_ManHasChoices(pNew) );
676  pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(pNew) );
677  pCur++;
678  pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4;
679  nPairs = Gia_AigerReadInt(pCur); pCur += 4;
680  for ( i = 0; i < nPairs; i++ )
681  {
682  iRepr = Gia_AigerReadInt(pCur); pCur += 4;
683  iNode = Gia_AigerReadInt(pCur); pCur += 4;
684  pNew->pSibls[iRepr] = iNode;
685  assert( iRepr > iNode );
686  }
687  assert( pCur == pCurTemp );
688  if ( fVerbose ) printf( "Finished reading extension \"q\".\n" );
689  }
690  // read switching activity
691  else if ( *pCur == 'u' )
692  {
693  unsigned char * pSwitching;
694  pCur++;
695  pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4;
696  pSwitching = ABC_ALLOC( unsigned char, Gia_ManObjNum(pNew) );
697  memcpy( pSwitching, pCur, Gia_ManObjNum(pNew) ); pCur += Gia_ManObjNum(pNew);
698  assert( pCur == pCurTemp );
699  if ( fVerbose ) printf( "Finished reading extension \"s\".\n" );
700  }
701  // read timing manager
702  else if ( *pCur == 't' )
703  {
704  pCur++;
705  vStr = Vec_StrStart( Gia_AigerReadInt(pCur) ); pCur += 4;
706  memcpy( Vec_StrArray(vStr), pCur, Vec_StrSize(vStr) ); pCur += Vec_StrSize(vStr);
707  pNew->pManTime = Tim_ManLoad( vStr, 0 );
708  Vec_StrFree( vStr );
709  if ( fVerbose ) printf( "Finished reading extension \"t\".\n" );
710  }
711  // read object classes
712  else if ( *pCur == 'v' )
713  {
714  pCur++;
715  pNew->vObjClasses = Vec_IntStart( Gia_AigerReadInt(pCur)/4 ); pCur += 4;
716  memcpy( Vec_IntArray(pNew->vObjClasses), pCur, 4*Vec_IntSize(pNew->vObjClasses) );
717  pCur += 4*Vec_IntSize(pNew->vObjClasses);
718  if ( fVerbose ) printf( "Finished reading extension \"v\".\n" );
719  }
720  else break;
721  }
722  }
723 
724  // skipping the comments
725  Vec_IntFree( vNodes );
726 
727  // update polarity of the additional outputs
728  if ( nBad || nConstr || nJust || nFair )
729  Gia_ManInvertConstraints( pNew );
730 
731  // clean the PO drivers
732  if ( vPoTypes )
733  {
734  pNew = Gia_ManDupWithConstraints( pTemp = pNew, vPoTypes );
735  Gia_ManStop( pTemp );
736  Vec_IntFreeP( &vPoTypes );
737  }
738 
739  if ( !fSkipStrash && Gia_ManHasDangling(pNew) )
740  {
741  Tim_Man_t * pManTime;
742  Vec_Int_t * vFlopMap, * vGateMap, * vObjMap;
743  vFlopMap = pNew->vFlopClasses; pNew->vFlopClasses = NULL;
744  vGateMap = pNew->vGateClasses; pNew->vGateClasses = NULL;
745  vObjMap = pNew->vObjClasses; pNew->vObjClasses = NULL;
746  pManTime = (Tim_Man_t *)pNew->pManTime; pNew->pManTime = NULL;
747  pNew = Gia_ManCleanup( pTemp = pNew );
748  if ( (vGateMap || vObjMap) && (Gia_ManObjNum(pNew) < Gia_ManObjNum(pTemp)) )
749  printf( "Cleanup removed objects after reading. Old gate/object abstraction maps are invalid!\n" );
750  Gia_ManStop( pTemp );
751  pNew->vFlopClasses = vFlopMap;
752  pNew->vGateClasses = vGateMap;
753  pNew->vObjClasses = vObjMap;
754  pNew->pManTime = pManTime;
755  }
756 
757  if ( fHieOnly )
758  {
759 // Tim_ManPrint( (Tim_Man_t *)pNew->pManTime );
760  if ( Abc_FrameReadLibBox() == NULL )
761  printf( "Warning: Creating unit-delay box delay tables because box library is not available.\n" );
763  }
764  Vec_FltFreeP( &pNew->vInArrs );
765  Vec_FltFreeP( &pNew->vOutReqs );
766 /*
767  // check the result
768  if ( fCheck && !Gia_ManCheck( pNew ) )
769  {
770  printf( "Gia_AigerRead: The network check has failed.\n" );
771  Gia_ManStop( pNew );
772  return NULL;
773  }
774 */
775 
776  if ( vInits && Vec_IntSum(vInits) )
777  {
778  char * pInit = ABC_ALLOC( char, Vec_IntSize(vInits) + 1 );
779  Gia_Obj_t * pObj;
780  int i;
781  assert( Vec_IntSize(vInits) == Gia_ManRegNum(pNew) );
782  Gia_ManForEachRo( pNew, pObj, i )
783  {
784  if ( Vec_IntEntry(vInits, i) == 0 )
785  pInit[i] = '0';
786  else if ( Vec_IntEntry(vInits, i) == 1 )
787  pInit[i] = '1';
788  else
789  {
790  assert( Vec_IntEntry(vInits, i) == Abc_Var2Lit(Gia_ObjId(pNew, pObj), 0) );
791  // unitialized value of the latch is the latch literal according to http://fmv.jku.at/hwmcc11/beyond1.pdf
792  pInit[i] = 'X';
793  }
794  }
795  pInit[i] = 0;
796  pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 1 );
797  pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
798  Gia_ManStop( pTemp );
799  ABC_FREE( pInit );
800  }
801  Vec_IntFreeP( &vInits );
802  if ( !fSkipStrash && pNew->vMapping )
803  {
804  Abc_Print( 0, "Structural hashing enabled while reading AIGER invalidated the mapping. Consider using \"&r -s\".\n" );
805  Vec_IntFreeP( &pNew->vMapping );
806  }
807  return pNew;
808 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
static int Gia_ManAppendAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: gia.h:592
Vec_Int_t * vUserFfIds
Definition: gia.h:159
void Gia_ManInvertConstraints(Gia_Man_t *pAig)
Definition: giaUtil.c:1415
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_Man_t * pAigExtra
Definition: gia.h:149
int * pNexts
Definition: gia.h:122
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_Int_t * vRegClasses
Definition: gia.h:144
static char * Vec_StrArray(Vec_Str_t *p)
Definition: vecStr.h:272
Vec_Int_t * vObjClasses
Definition: gia.h:142
int * pSibls
Definition: gia.h:123
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Vec_Int_t * vFlopClasses
Definition: gia.h:140
char * memcpy()
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
#define XAIG_VERBOSE
Definition: giaAiger.c:28
static float * Vec_FltArray(Vec_Flt_t *p)
Definition: vecFlt.h:274
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
ABC_NAMESPACE_IMPL_START Gia_Rpr_t * Gia_AigerReadEquivClasses(unsigned char **ppPos, int nSize)
DECLARATIONS ///.
Definition: giaAigerExt.c:45
Vec_Int_t * vPacking
Definition: gia.h:133
int * Gia_AigerReadMapping(unsigned char **ppPos, int nSize)
Definition: giaAigerExt.c:143
Vec_Int_t * Gia_AigerReadLiterals(unsigned char **ppPos, int nEntries)
Definition: giaAiger.c:109
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
static void Vec_FltFreeP(Vec_Flt_t **p)
Definition: vecFlt.h:235
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Definition: gia.h:75
Gia_Man_t * Gia_ManDupZeroUndc(Gia_Man_t *p, char *pInit, int fVerbose)
Definition: giaDup.c:2390
int Gia_ManHasDangling(Gia_Man_t *p)
Definition: giaUtil.c:1155
static int Gia_ManHasChoices(Gia_Man_t *p)
Definition: gia.h:397
void Tim_ManCreate(Tim_Man_t *p, void *pLib, Vec_Flt_t *vInArrs, Vec_Flt_t *vOutReqs)
Definition: timMan.c:403
static Vec_Flt_t * Vec_FltStart(int nSize)
Definition: vecFlt.h:101
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
static int Gia_AigerReadInt(unsigned char *pPos)
Definition: gia.h:827
int nConstrs
Definition: gia.h:117
char * pName
Definition: gia.h:97
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
Vec_Int_t * vGateClasses
Definition: gia.h:141
static int Gia_ManAppendBuf(Gia_Man_t *p, int iLit)
Definition: gia.h:694
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
ABC_DLL void * Abc_FrameReadLibBox()
Definition: mainFrame.c:55
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
static Vec_Str_t * Vec_StrStart(int nSize)
Definition: vecStr.h:95
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Vec_Flt_t * vOutReqs
Definition: gia.h:151
void * pManTime
Definition: gia.h:165
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
int * Gia_ManDeriveNexts(Gia_Man_t *p)
Definition: giaEquiv.c:97
Vec_Int_t * Gia_AigerReadMappingDoc(unsigned char **ppPos, int nObjs)
Definition: giaAigerExt.c:245
Vec_Int_t * vUserPiIds
Definition: gia.h:157
int nAnd2Delay
Definition: gia.h:173
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static int Vec_IntSum(Vec_Int_t *p)
Definition: vecInt.h:1137
#define ABC_FREE(obj)
Definition: abc_global.h:232
Definition: gia.h:95
Gia_Plc_t * pPlacement
Definition: gia.h:148
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
int strncmp()
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
int * Gia_AigerReadMappingSimple(unsigned char **ppPos, int nSize)
Definition: giaAigerExt.c:219
Gia_Rpr_t * pReprs
Definition: gia.h:121
#define assert(ex)
Definition: util_old.h:213
int strlen()
Definition: gia.h:66
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
static unsigned Gia_AigerReadUnsigned(unsigned char **ppPos)
Definition: gia.h:840
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
Vec_Int_t * vMapping
Definition: gia.h:131
Gia_Man_t * Gia_AigerReadFromMemory(char *pContents, int nFileSize, int fSkipStrash, int fCheck)
Definition: giaAiger.c:176
Definition: gia.h:56
Tim_Man_t * Tim_ManLoad(Vec_Str_t *p, int fHieOnly)
Definition: timDump.c:112
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
Vec_Int_t * vUserPoIds
Definition: gia.h:158
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Gia_Man_t * Gia_ManDupWithConstraints(Gia_Man_t *p, Vec_Int_t *vPoTypes)
Definition: giaDup.c:2627
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Vec_Int_t * Gia_AigerReadPacking(unsigned char **ppPos, int nSize)
Definition: giaAigerExt.c:302
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
int nTotal
DECLARATIONS ///.
Definition: cutTruth.c:37
Vec_Flt_t * vInArrs
Definition: gia.h:150
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Vec_Int_t* Gia_AigerReadLiterals ( unsigned char **  ppPos,
int  nEntries 
)

Definition at line 109 of file giaAiger.c.

110 {
111  Vec_Int_t * vLits;
112  int Lit, LitPrev, Diff, i;
113  vLits = Vec_IntAlloc( nEntries );
114  LitPrev = Gia_AigerReadUnsigned( ppPos );
115  Vec_IntPush( vLits, LitPrev );
116  for ( i = 1; i < nEntries; i++ )
117  {
118 // Diff = Lit - LitPrev;
119 // Diff = (Lit < LitPrev)? -Diff : Diff;
120 // Diff = ((2 * Diff) << 1) | (int)(Lit < LitPrev);
121  Diff = Gia_AigerReadUnsigned( ppPos );
122  Diff = (Diff & 1)? -(Diff >> 1) : Diff >> 1;
123  Lit = Diff + LitPrev;
124  Vec_IntPush( vLits, Lit );
125  LitPrev = Lit;
126  }
127  return vLits;
128 }
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static unsigned Gia_AigerReadUnsigned(unsigned char **ppPos)
Definition: gia.h:840
void Gia_AigerWrite ( Gia_Man_t pInit,
char *  pFileName,
int  fWriteSymbols,
int  fCompact 
)

Function*************************************************************

Synopsis [Writes the AIG in the binary AIGER format.]

Description []

SideEffects []

SeeAlso []

Definition at line 1024 of file giaAiger.c.

1025 {
1026  int fVerbose = XAIG_VERBOSE;
1027  FILE * pFile;
1028  Gia_Man_t * p;
1029  Gia_Obj_t * pObj;
1030  Vec_Str_t * vStrExt;
1031  int i, nBufferSize, Pos;
1032  unsigned char * pBuffer;
1033  unsigned uLit0, uLit1, uLit;
1034  assert( pInit->nXors == 0 && pInit->nMuxes == 0 );
1035 
1036  if ( Gia_ManCoNum(pInit) == 0 )
1037  {
1038  printf( "AIG cannot be written because it has no POs.\n" );
1039  return;
1040  }
1041 
1042  // start the output stream
1043  pFile = fopen( pFileName, "wb" );
1044  if ( pFile == NULL )
1045  {
1046  fprintf( stdout, "Gia_AigerWrite(): Cannot open the output file \"%s\".\n", pFileName );
1047  return;
1048  }
1049 
1050  // create normalized AIG
1051  if ( !Gia_ManIsNormalized(pInit) )
1052  {
1053 // printf( "Gia_AigerWrite(): Normalizing AIG for writing.\n" );
1054  p = Gia_ManDupNormalize( pInit );
1055  Gia_ManTransferMapping( p, pInit );
1056  Gia_ManTransferPacking( p, pInit );
1057  Gia_ManTransferTiming( p, pInit );
1058  p->vNamesIn = pInit->vNamesIn; pInit->vNamesIn = NULL;
1059  p->vNamesOut = pInit->vNamesOut; pInit->vNamesOut = NULL;
1060  p->nConstrs = pInit->nConstrs; pInit->nConstrs = 0;
1061  }
1062  else
1063  p = pInit;
1064 
1065  // write the header "M I L O A" where M = I + L + A
1066  fprintf( pFile, "aig%s %u %u %u %u %u",
1067  fCompact? "2" : "",
1068  Gia_ManCiNum(p) + Gia_ManAndNum(p),
1069  Gia_ManPiNum(p),
1070  Gia_ManRegNum(p),
1071  Gia_ManConstrNum(p) ? 0 : Gia_ManPoNum(p),
1072  Gia_ManAndNum(p) );
1073  // write the extended header "B C J F"
1074  if ( Gia_ManConstrNum(p) )
1075  fprintf( pFile, " %u %u", Gia_ManPoNum(p) - Gia_ManConstrNum(p), Gia_ManConstrNum(p) );
1076  fprintf( pFile, "\n" );
1077 
1079  if ( !fCompact )
1080  {
1081  // write latch drivers
1082  Gia_ManForEachRi( p, pObj, i )
1083  fprintf( pFile, "%u\n", Gia_ObjFaninLit0p(p, pObj) );
1084  // write PO drivers
1085  Gia_ManForEachPo( p, pObj, i )
1086  fprintf( pFile, "%u\n", Gia_ObjFaninLit0p(p, pObj) );
1087  }
1088  else
1089  {
1090  Vec_Int_t * vLits = Gia_AigerCollectLiterals( p );
1091  Vec_Str_t * vBinary = Gia_AigerWriteLiterals( vLits );
1092  fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile );
1093  Vec_StrFree( vBinary );
1094  Vec_IntFree( vLits );
1095  }
1097 
1098  // write the nodes into the buffer
1099  Pos = 0;
1100  nBufferSize = 8 * Gia_ManAndNum(p) + 100; // skeptically assuming 3 chars per one AIG edge
1101  pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
1102  Gia_ManForEachAnd( p, pObj, i )
1103  {
1104  uLit = Abc_Var2Lit( i, 0 );
1105  uLit0 = Gia_ObjFaninLit0( pObj, i );
1106  uLit1 = Gia_ObjFaninLit1( pObj, i );
1107  assert( Gia_ManBufNum(p) || uLit0 < uLit1 );
1108  Pos = Gia_AigerWriteUnsignedBuffer( pBuffer, Pos, uLit - uLit1 );
1109  Pos = Gia_AigerWriteUnsignedBuffer( pBuffer, Pos, uLit1 - uLit0 );
1110  if ( Pos > nBufferSize - 10 )
1111  {
1112  printf( "Gia_AigerWrite(): AIGER generation has failed because the allocated buffer is too small.\n" );
1113  fclose( pFile );
1114  if ( p != pInit )
1115  Gia_ManStop( p );
1116  return;
1117  }
1118  }
1119  assert( Pos < nBufferSize );
1120 
1121  // write the buffer
1122  fwrite( pBuffer, 1, Pos, pFile );
1123  ABC_FREE( pBuffer );
1124 
1125  // write the symbol table
1126  if ( p->vNamesIn && p->vNamesOut )
1127  {
1128  assert( Vec_PtrSize(p->vNamesIn) == Gia_ManCiNum(p) );
1129  assert( Vec_PtrSize(p->vNamesOut) == Gia_ManCoNum(p) );
1130  // write PIs
1131  Gia_ManForEachPi( p, pObj, i )
1132  fprintf( pFile, "i%d %s\n", i, (char *)Vec_PtrEntry(p->vNamesIn, i) );
1133  // write latches
1134  Gia_ManForEachRo( p, pObj, i )
1135  fprintf( pFile, "l%d %s\n", i, (char *)Vec_PtrEntry(p->vNamesIn, Gia_ManPiNum(p) + i) );
1136  // write POs
1137  Gia_ManForEachPo( p, pObj, i )
1138  fprintf( pFile, "o%d %s\n", i, (char *)Vec_PtrEntry(p->vNamesOut, i) );
1139  }
1140 
1141  // write the comment
1142 // fprintf( pFile, "c\n" );
1143  fprintf( pFile, "c" );
1144 
1145  // write additional AIG
1146  if ( p->pAigExtra )
1147  {
1148  fprintf( pFile, "a" );
1149  vStrExt = Gia_AigerWriteIntoMemoryStr( p->pAigExtra );
1150  Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1151  fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1152  Vec_StrFree( vStrExt );
1153  if ( fVerbose ) printf( "Finished writing extension \"a\".\n" );
1154  }
1155  // write constraints
1156  if ( p->nConstrs )
1157  {
1158  fprintf( pFile, "c" );
1159  Gia_FileWriteBufferSize( pFile, 4 );
1160  Gia_FileWriteBufferSize( pFile, p->nConstrs );
1161  }
1162  // write timing information
1163  if ( p->nAnd2Delay )
1164  {
1165  fprintf( pFile, "d" );
1166  Gia_FileWriteBufferSize( pFile, 4 );
1167  Gia_FileWriteBufferSize( pFile, p->nAnd2Delay );
1168  }
1169  if ( p->pManTime )
1170  {
1171  float * pTimes;
1172  pTimes = Tim_ManGetArrTimes( (Tim_Man_t *)p->pManTime );
1173  if ( pTimes )
1174  {
1175  fprintf( pFile, "i" );
1176  Gia_FileWriteBufferSize( pFile, 4*Tim_ManPiNum((Tim_Man_t *)p->pManTime) );
1177  fwrite( pTimes, 1, 4*Tim_ManPiNum((Tim_Man_t *)p->pManTime), pFile );
1178  ABC_FREE( pTimes );
1179  if ( fVerbose ) printf( "Finished writing extension \"i\".\n" );
1180  }
1181  pTimes = Tim_ManGetReqTimes( (Tim_Man_t *)p->pManTime );
1182  if ( pTimes )
1183  {
1184  fprintf( pFile, "o" );
1185  Gia_FileWriteBufferSize( pFile, 4*Tim_ManPoNum((Tim_Man_t *)p->pManTime) );
1186  fwrite( pTimes, 1, 4*Tim_ManPoNum((Tim_Man_t *)p->pManTime), pFile );
1187  ABC_FREE( pTimes );
1188  if ( fVerbose ) printf( "Finished writing extension \"o\".\n" );
1189  }
1190  }
1191  // write equivalences
1192  if ( p->pReprs && p->pNexts )
1193  {
1194  extern Vec_Str_t * Gia_WriteEquivClasses( Gia_Man_t * p );
1195  fprintf( pFile, "e" );
1196  vStrExt = Gia_WriteEquivClasses( p );
1197  Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1198  fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1199  Vec_StrFree( vStrExt );
1200  }
1201  // write flop classes
1202  if ( p->vFlopClasses )
1203  {
1204  fprintf( pFile, "f" );
1205  Gia_FileWriteBufferSize( pFile, 4*Gia_ManRegNum(p) );
1206  assert( Vec_IntSize(p->vFlopClasses) == Gia_ManRegNum(p) );
1207  fwrite( Vec_IntArray(p->vFlopClasses), 1, 4*Gia_ManRegNum(p), pFile );
1208  }
1209  // write gate classes
1210  if ( p->vGateClasses )
1211  {
1212  fprintf( pFile, "g" );
1213  Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) );
1214  assert( Vec_IntSize(p->vGateClasses) == Gia_ManObjNum(p) );
1215  fwrite( Vec_IntArray(p->vGateClasses), 1, 4*Gia_ManObjNum(p), pFile );
1216  }
1217  // write hierarchy info
1218  if ( p->pManTime )
1219  {
1220  fprintf( pFile, "h" );
1221  vStrExt = Tim_ManSave( (Tim_Man_t *)p->pManTime, 1 );
1222  Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1223  fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1224  Vec_StrFree( vStrExt );
1225  if ( fVerbose ) printf( "Finished writing extension \"h\".\n" );
1226  }
1227  // write packing
1228  if ( p->vPacking )
1229  {
1230  extern Vec_Str_t * Gia_WritePacking( Vec_Int_t * vPacking );
1231  fprintf( pFile, "k" );
1232  vStrExt = Gia_WritePacking( p->vPacking );
1233  Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1234  fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1235  Vec_StrFree( vStrExt );
1236  if ( fVerbose ) printf( "Finished writing extension \"k\".\n" );
1237  }
1238  // write mapping
1239  if ( Gia_ManHasMapping(p) )
1240  {
1241  extern Vec_Str_t * Gia_AigerWriteMapping( Gia_Man_t * p );
1244  fprintf( pFile, "m" );
1245  vStrExt = Gia_AigerWriteMappingDoc( p );
1246  Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1247  fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1248  Vec_StrFree( vStrExt );
1249  if ( fVerbose ) printf( "Finished writing extension \"m\".\n" );
1250  }
1251  // write placement
1252  if ( p->pPlacement )
1253  {
1254  fprintf( pFile, "p" );
1255  Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) );
1256  fwrite( p->pPlacement, 1, 4*Gia_ManObjNum(p), pFile );
1257  }
1258  // write register classes
1259  if ( p->vRegClasses )
1260  {
1261  int i;
1262  fprintf( pFile, "r" );
1263  Gia_FileWriteBufferSize( pFile, 4*Vec_IntSize(p->vRegClasses) );
1264  for ( i = 0; i < Vec_IntSize(p->vRegClasses); i++ )
1265  Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vRegClasses, i) );
1266  }
1267  // write choices
1268  if ( Gia_ManHasChoices(p) )
1269  {
1270  int i, nPairs = 0;
1271  fprintf( pFile, "q" );
1272  for ( i = 0; i < Gia_ManObjNum(p); i++ )
1273  nPairs += (Gia_ObjSibl(p, i) > 0);
1274  Gia_FileWriteBufferSize( pFile, 4*(nPairs * 2 + 1) );
1275  Gia_FileWriteBufferSize( pFile, nPairs );
1276  for ( i = 0; i < Gia_ManObjNum(p); i++ )
1277  if ( Gia_ObjSibl(p, i) )
1278  {
1279  assert( i > Gia_ObjSibl(p, i) );
1280  Gia_FileWriteBufferSize( pFile, i );
1281  Gia_FileWriteBufferSize( pFile, Gia_ObjSibl(p, i) );
1282  }
1283  if ( fVerbose ) printf( "Finished writing extension \"q\".\n" );
1284  }
1285  // write switching activity
1286  if ( p->pSwitching )
1287  {
1288  fprintf( pFile, "u" );
1290  fwrite( p->pSwitching, 1, Gia_ManObjNum(p), pFile );
1291  }
1292 /*
1293  // write timing information
1294  if ( p->pManTime )
1295  {
1296  fprintf( pFile, "t" );
1297  vStrExt = Tim_ManSave( (Tim_Man_t *)p->pManTime, 0 );
1298  Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1299  fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1300  Vec_StrFree( vStrExt );
1301  }
1302 */
1303  // write object classes
1304  if ( p->vObjClasses )
1305  {
1306  fprintf( pFile, "v" );
1307  Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) );
1308  assert( Vec_IntSize(p->vObjClasses) == Gia_ManObjNum(p) );
1309  fwrite( Vec_IntArray(p->vObjClasses), 1, 4*Gia_ManObjNum(p), pFile );
1310  }
1311  // write name
1312  if ( p->pName )
1313  {
1314  fprintf( pFile, "n" );
1315  Gia_FileWriteBufferSize( pFile, strlen(p->pName)+1 );
1316  fwrite( p->pName, 1, strlen(p->pName), pFile );
1317  fprintf( pFile, "%c", '\0' );
1318  }
1319  // write comments
1320  fprintf( pFile, "\nThis file was produced by the GIA package in ABC on %s\n", Gia_TimeStamp() );
1321  fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
1322  fclose( pFile );
1323  if ( p != pInit )
1324  {
1325  pInit->pManTime = p->pManTime; p->pManTime = NULL;
1326  pInit->vNamesIn = p->vNamesIn; p->vNamesIn = NULL;
1327  pInit->vNamesOut = p->vNamesOut; p->vNamesOut = NULL;
1328  Gia_ManStop( p );
1329  }
1330 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
static int Gia_ObjFaninLit0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:466
void Gia_ManInvertConstraints(Gia_Man_t *pAig)
Definition: giaUtil.c:1415
Vec_Str_t * Tim_ManSave(Tim_Man_t *p, int fHieOnly)
FUNCTION DEFINITIONS ///.
Definition: timDump.c:46
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static char * Vec_StrArray(Vec_Str_t *p)
Definition: vecStr.h:272
static int Gia_ObjFaninLit0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:469
ush Pos
Definition: deflate.h:88
Vec_Str_t * Gia_AigerWriteMappingDoc(Gia_Man_t *p)
Definition: giaAigerExt.c:267
static int Gia_ManConstrNum(Gia_Man_t *p)
Definition: gia.h:395
char * Gia_TimeStamp()
Definition: giaUtil.c:101
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
#define XAIG_VERBOSE
Definition: giaAiger.c:28
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Definition: gia.h:75
static int Gia_ManHasChoices(Gia_Man_t *p)
Definition: gia.h:397
int nXors
Definition: gia.h:105
int Tim_ManPiNum(Tim_Man_t *p)
Definition: timMan.c:688
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
static int Gia_ObjSibl(Gia_Man_t *p, int Id)
Definition: gia.h:893
Vec_Str_t * Gia_AigerWriteMappingSimple(Gia_Man_t *p)
Definition: giaAigerExt.c:226
Vec_Int_t * Gia_AigerCollectLiterals(Gia_Man_t *p)
Definition: giaAiger.c:97
int nConstrs
Definition: gia.h:117
static int Gia_ObjFaninLit1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:467
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
Gia_Man_t * Gia_ManDupNormalize(Gia_Man_t *p)
Definition: giaTim.c:134
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Vec_Str_t * Gia_AigerWriteMapping(Gia_Man_t *p)
Definition: giaAigerExt.c:201
if(last==0)
Definition: sparse_int.h:34
else
Definition: sparse_int.h:55
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Vec_Str_t * Gia_WriteEquivClasses(Gia_Man_t *p)
Definition: giaAigerExt.c:118
void * pManTime
Definition: gia.h:165
void Gia_ManTransferTiming(Gia_Man_t *p, Gia_Man_t *pGia)
Definition: giaIf.c:1912
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Vec_Ptr_t * vNamesOut
Definition: gia.h:156
float * Tim_ManGetReqTimes(Tim_Man_t *p)
Definition: timMan.c:494
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static int Gia_ManHasMapping(Gia_Man_t *p)
Definition: gia.h:951
void Gia_FileWriteBufferSize(FILE *pFile, int nSize)
Definition: giaAiger.c:79
#define ABC_FREE(obj)
Definition: abc_global.h:232
Definition: gia.h:95
int Gia_ManIsNormalized(Gia_Man_t *p)
Definition: giaTim.c:109
static int Gia_ManBufNum(Gia_Man_t *p)
Definition: gia.h:392
void Gia_ManTransferPacking(Gia_Man_t *p, Gia_Man_t *pGia)
Definition: giaIf.c:1878
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
void Gia_ManTransferMapping(Gia_Man_t *p, Gia_Man_t *pGia)
Definition: giaIf.c:1855
#define assert(ex)
Definition: util_old.h:213
int strlen()
Vec_Str_t * Gia_AigerWriteIntoMemoryStr(Gia_Man_t *p)
Definition: giaAiger.c:866
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
Vec_Ptr_t * vNamesIn
Definition: gia.h:155
static int Gia_AigerWriteUnsignedBuffer(unsigned char *pBuffer, int Pos, unsigned x)
Definition: gia.h:872
Vec_Str_t * Gia_WritePacking(Vec_Int_t *vPacking)
Definition: giaAigerExt.c:311
float * Tim_ManGetArrTimes(Tim_Man_t *p)
Definition: timMan.c:479
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
int nMuxes
Definition: gia.h:106
int Tim_ManPoNum(Tim_Man_t *p)
Definition: timMan.c:694
Vec_Str_t * Gia_AigerWriteLiterals(Vec_Int_t *vLits)
Definition: giaAiger.c:129
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Vec_Str_t* Gia_AigerWriteIntoMemoryStr ( Gia_Man_t p)

Function*************************************************************

Synopsis [Writes the AIG in into the memory buffer.]

Description [The resulting buffer constains the AIG in AIGER format. The resulting buffer should be deallocated by the user.]

SideEffects []

SeeAlso []

Definition at line 866 of file giaAiger.c.

867 {
868  Vec_Str_t * vBuffer;
869  Gia_Obj_t * pObj;
870  int nNodes = 0, i, uLit, uLit0, uLit1;
871  // set the node numbers to be used in the output file
872  Gia_ManConst0(p)->Value = nNodes++;
873  Gia_ManForEachCi( p, pObj, i )
874  pObj->Value = nNodes++;
875  Gia_ManForEachAnd( p, pObj, i )
876  pObj->Value = nNodes++;
877 
878  // write the header "M I L O A" where M = I + L + A
879  vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) );
880  Vec_StrPrintStr( vBuffer, "aig " );
881  Vec_StrPrintNum( vBuffer, Gia_ManCandNum(p) );
882  Vec_StrPrintStr( vBuffer, " " );
883  Vec_StrPrintNum( vBuffer, Gia_ManPiNum(p) );
884  Vec_StrPrintStr( vBuffer, " " );
885  Vec_StrPrintNum( vBuffer, Gia_ManRegNum(p) );
886  Vec_StrPrintStr( vBuffer, " " );
887  Vec_StrPrintNum( vBuffer, Gia_ManPoNum(p) );
888  Vec_StrPrintStr( vBuffer, " " );
889  Vec_StrPrintNum( vBuffer, Gia_ManAndNum(p) );
890  Vec_StrPrintStr( vBuffer, "\n" );
891 
892  // write latch drivers
893  Gia_ManForEachRi( p, pObj, i )
894  {
895  uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
896  Vec_StrPrintNum( vBuffer, uLit );
897  Vec_StrPrintStr( vBuffer, "\n" );
898  }
899 
900  // write PO drivers
901  Gia_ManForEachPo( p, pObj, i )
902  {
903  uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
904  Vec_StrPrintNum( vBuffer, uLit );
905  Vec_StrPrintStr( vBuffer, "\n" );
906  }
907  // write the nodes into the buffer
908  Gia_ManForEachAnd( p, pObj, i )
909  {
910  uLit = Abc_Var2Lit( Gia_ObjValue(pObj), 0 );
911  uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
912  uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) );
913  assert( uLit0 != uLit1 );
914  if ( uLit0 > uLit1 )
915  {
916  int Temp = uLit0;
917  uLit0 = uLit1;
918  uLit1 = Temp;
919  }
920  Gia_AigerWriteUnsigned( vBuffer, uLit - uLit1 );
921  Gia_AigerWriteUnsigned( vBuffer, uLit1 - uLit0 );
922  }
923  Vec_StrPrintStr( vBuffer, "c" );
924  return vBuffer;
925 }
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
static void Vec_StrPrintNum(Vec_Str_t *p, int Num)
Definition: vecStr.h:575
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
static int Gia_ObjValue(Gia_Obj_t *pObj)
Definition: gia.h:413
static Vec_Str_t * Vec_StrAlloc(int nCap)
Definition: bblif.c:495
static void Gia_AigerWriteUnsigned(Vec_Str_t *vStr, unsigned x)
Definition: gia.h:848
Definition: gia.h:75
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
static int Gia_ManCandNum(Gia_Man_t *p)
Definition: gia.h:394
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
static void Vec_StrPrintStr(Vec_Str_t *p, const char *pStr)
Definition: vecStr.h:627
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Vec_Str_t* Gia_AigerWriteIntoMemoryStrPart ( Gia_Man_t p,
Vec_Int_t vCis,
Vec_Int_t vAnds,
Vec_Int_t vCos,
int  nRegs 
)

Function*************************************************************

Synopsis [Writes the AIG in into the memory buffer.]

Description [The resulting buffer constains the AIG in AIGER format. The CI/CO/AND nodes are assumed to be ordered according to some rule. The resulting buffer should be deallocated by the user.]

SideEffects [Note that in vCos, PIs are order first, followed by latches!]

SeeAlso []

Definition at line 940 of file giaAiger.c.

941 {
942  Vec_Str_t * vBuffer;
943  Gia_Obj_t * pObj;
944  int nNodes = 0, i, uLit, uLit0, uLit1;
945  // set the node numbers to be used in the output file
946  Gia_ManConst0(p)->Value = nNodes++;
947  Gia_ManForEachObjVec( vCis, p, pObj, i )
948  {
949  assert( Gia_ObjIsCi(pObj) );
950  pObj->Value = nNodes++;
951  }
952  Gia_ManForEachObjVec( vAnds, p, pObj, i )
953  {
954  assert( Gia_ObjIsAnd(pObj) );
955  pObj->Value = nNodes++;
956  }
957 
958  // write the header "M I L O A" where M = I + L + A
959  vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) );
960  Vec_StrPrintStr( vBuffer, "aig " );
961  Vec_StrPrintNum( vBuffer, Vec_IntSize(vCis) + Vec_IntSize(vAnds) );
962  Vec_StrPrintStr( vBuffer, " " );
963  Vec_StrPrintNum( vBuffer, Vec_IntSize(vCis) - nRegs );
964  Vec_StrPrintStr( vBuffer, " " );
965  Vec_StrPrintNum( vBuffer, nRegs );
966  Vec_StrPrintStr( vBuffer, " " );
967  Vec_StrPrintNum( vBuffer, Vec_IntSize(vCos) - nRegs );
968  Vec_StrPrintStr( vBuffer, " " );
969  Vec_StrPrintNum( vBuffer, Vec_IntSize(vAnds) );
970  Vec_StrPrintStr( vBuffer, "\n" );
971 
972  // write latch drivers
973  Gia_ManForEachObjVec( vCos, p, pObj, i )
974  {
975  assert( Gia_ObjIsCo(pObj) );
976  if ( i < Vec_IntSize(vCos) - nRegs )
977  continue;
978  uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
979  Vec_StrPrintNum( vBuffer, uLit );
980  Vec_StrPrintStr( vBuffer, "\n" );
981  }
982  // write output drivers
983  Gia_ManForEachObjVec( vCos, p, pObj, i )
984  {
985  assert( Gia_ObjIsCo(pObj) );
986  if ( i >= Vec_IntSize(vCos) - nRegs )
987  continue;
988  uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
989  Vec_StrPrintNum( vBuffer, uLit );
990  Vec_StrPrintStr( vBuffer, "\n" );
991  }
992 
993  // write the nodes into the buffer
994  Gia_ManForEachObjVec( vAnds, p, pObj, i )
995  {
996  uLit = Abc_Var2Lit( Gia_ObjValue(pObj), 0 );
997  uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
998  uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) );
999  assert( uLit0 != uLit1 );
1000  if ( uLit0 > uLit1 )
1001  {
1002  int Temp = uLit0;
1003  uLit0 = uLit1;
1004  uLit1 = Temp;
1005  }
1006  Gia_AigerWriteUnsigned( vBuffer, uLit - uLit1 );
1007  Gia_AigerWriteUnsigned( vBuffer, uLit1 - uLit0 );
1008  }
1009  Vec_StrPrintStr( vBuffer, "c" );
1010  return vBuffer;
1011 }
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
static void Vec_StrPrintNum(Vec_Str_t *p, int Num)
Definition: vecStr.h:575
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
static int Gia_ObjValue(Gia_Obj_t *pObj)
Definition: gia.h:413
static Vec_Str_t * Vec_StrAlloc(int nCap)
Definition: bblif.c:495
static void Gia_AigerWriteUnsigned(Vec_Str_t *vStr, unsigned x)
Definition: gia.h:848
Definition: gia.h:75
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
static void Vec_StrPrintStr(Vec_Str_t *p, const char *pStr)
Definition: vecStr.h:627
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Vec_Str_t* Gia_AigerWriteLiterals ( Vec_Int_t vLits)

Definition at line 129 of file giaAiger.c.

130 {
131  Vec_Str_t * vBinary;
132  int Pos = 0, Lit, LitPrev, Diff, i;
133  vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) );
134  LitPrev = Vec_IntEntry( vLits, 0 );
135  Pos = Gia_AigerWriteUnsignedBuffer( (unsigned char *)Vec_StrArray(vBinary), Pos, LitPrev );
136  Vec_IntForEachEntryStart( vLits, Lit, i, 1 )
137  {
138  Diff = Lit - LitPrev;
139  Diff = (Lit < LitPrev)? -Diff : Diff;
140  Diff = (Diff << 1) | (int)(Lit < LitPrev);
141  Pos = Gia_AigerWriteUnsignedBuffer( (unsigned char *)Vec_StrArray(vBinary), Pos, Diff );
142  LitPrev = Lit;
143  if ( Pos + 10 > vBinary->nCap )
144  Vec_StrGrow( vBinary, vBinary->nCap+1 );
145  }
146  vBinary->nSize = Pos;
147 /*
148  // verify
149  {
150  extern Vec_Int_t * Gia_AigerReadLiterals( char ** ppPos, int nEntries );
151  char * pPos = Vec_StrArray( vBinary );
152  Vec_Int_t * vTemp = Gia_AigerReadLiterals( &pPos, Vec_IntSize(vLits) );
153  for ( i = 0; i < Vec_IntSize(vLits); i++ )
154  {
155  int Entry1 = Vec_IntEntry(vLits,i);
156  int Entry2 = Vec_IntEntry(vTemp,i);
157  assert( Entry1 == Entry2 );
158  }
159  Vec_IntFree( vTemp );
160  }
161 */
162  return vBinary;
163 }
static char * Vec_StrArray(Vec_Str_t *p)
Definition: vecStr.h:272
ush Pos
Definition: deflate.h:88
static Vec_Str_t * Vec_StrAlloc(int nCap)
Definition: bblif.c:495
static void Vec_StrGrow(Vec_Str_t *p, int nCapMin)
Definition: vecStr.h:404
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
int nSize
Definition: bblif.c:50
static int Gia_AigerWriteUnsignedBuffer(unsigned char *pBuffer, int Pos, unsigned x)
Definition: gia.h:872
int nCap
Definition: bblif.c:49
void Gia_AigerWriteSimple ( Gia_Man_t pInit,
char *  pFileName 
)

Function*************************************************************

Synopsis [Writes the AIG in the binary AIGER format.]

Description []

SideEffects []

SeeAlso []

Definition at line 1361 of file giaAiger.c.

1362 {
1363  FILE * pFile;
1364  Vec_Str_t * vStr;
1365  if ( Gia_ManPoNum(pInit) == 0 )
1366  {
1367  printf( "Gia_AigerWriteSimple(): AIG cannot be written because it has no POs.\n" );
1368  return;
1369  }
1370  // start the output stream
1371  pFile = fopen( pFileName, "wb" );
1372  if ( pFile == NULL )
1373  {
1374  fprintf( stdout, "Gia_AigerWriteSimple(): Cannot open the output file \"%s\".\n", pFileName );
1375  return;
1376  }
1377  // write the buffer
1378  vStr = Gia_AigerWriteIntoMemoryStr( pInit );
1379  fwrite( Vec_StrArray(vStr), 1, Vec_StrSize(vStr), pFile );
1380  Vec_StrFree( vStr );
1381  fclose( pFile );
1382 }
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
static char * Vec_StrArray(Vec_Str_t *p)
Definition: vecStr.h:272
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
Vec_Str_t * Gia_AigerWriteIntoMemoryStr(Gia_Man_t *p)
Definition: giaAiger.c:866
void Gia_DumpAiger ( Gia_Man_t p,
char *  pFilePrefix,
int  iFileNum,
int  nFileNumDigits 
)

Function*************************************************************

Synopsis [Writes the AIG in the binary AIGER format.]

Description []

SideEffects []

SeeAlso []

Definition at line 1343 of file giaAiger.c.

1344 {
1345  char Buffer[100];
1346  sprintf( Buffer, "%s%0*d.aig", pFilePrefix, nFileNumDigits, iFileNum );
1347  Gia_AigerWrite( p, Buffer, 0, 0 );
1348 }
char * sprintf()
void Gia_AigerWrite(Gia_Man_t *pInit, char *pFileName, int fWriteSymbols, int fCompact)
Definition: giaAiger.c:1024
void Gia_FileFixName ( char *  pFileName)

DECLARATIONS ///.

FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 49 of file giaAiger.c.

50 {
51  char * pName;
52  for ( pName = pFileName; *pName; pName++ )
53  if ( *pName == '>' )
54  *pName = '\\';
55 }
char* Gia_FileNameGeneric ( char *  FileName)

Definition at line 56 of file giaAiger.c.

57 {
58  char * pDot, * pRes;
59  pRes = Abc_UtilStrsav( FileName );
60  if ( (pDot = strrchr( pRes, '.' )) )
61  *pDot = 0;
62  return pRes;
63 }
char * strrchr()
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
int Gia_FileSize ( char *  pFileName)

FUNCTION DECLARATIONS ///.

Definition at line 64 of file giaAiger.c.

65 {
66  FILE * pFile;
67  int nFileSize;
68  pFile = fopen( pFileName, "r" );
69  if ( pFile == NULL )
70  {
71  printf( "Gia_FileSize(): The file is unavailable (absent or open).\n" );
72  return 0;
73  }
74  fseek( pFile, 0, SEEK_END );
75  nFileSize = ftell( pFile );
76  fclose( pFile );
77  return nFileSize;
78 }
#define SEEK_END
Definition: zconf.h:392
void Gia_FileWriteBufferSize ( FILE *  pFile,
int  nSize 
)

Definition at line 79 of file giaAiger.c.

80 {
81  unsigned char Buffer[5];
82  Gia_AigerWriteInt( Buffer, nSize );
83  fwrite( Buffer, 1, 4, pFile );
84 }
static void Gia_AigerWriteInt(unsigned char *pPos, int Value)
Definition: gia.h:834