abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
ioWriteAiger.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [ioWriteAiger.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Command processing package.]
8 
9  Synopsis [Procedures to write binary AIGER format developed by
10  Armin Biere, Johannes Kepler University (http://fmv.jku.at/)]
11 
12  Author [Alan Mishchenko]
13 
14  Affiliation [UC Berkeley]
15 
16  Date [Ver. 1.0. Started - December 16, 2006.]
17 
18  Revision [$Id: ioWriteAiger.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $]
19 
20 ***********************************************************************/
21 
22 // The code in this file is developed in collaboration with Mark Jarvin of Toronto.
23 
24 #include <stdio.h>
25 #include <stdlib.h>
26 #include <string.h>
27 #include <assert.h>
28 
29 #include "misc/bzlib/bzlib.h"
30 #include "misc/zlib/zlib.h"
31 #include "ioAbc.h"
32 
33 
34 
35 ABC_NAMESPACE_IMPL_START
36 
37 
38 #ifdef _WIN32
39 #define vsnprintf _vsnprintf
40 #endif
41 
42 ////////////////////////////////////////////////////////////////////////
43 /// DECLARATIONS ///
44 ////////////////////////////////////////////////////////////////////////
45 
46 /*
47  The following is taken from the AIGER format description,
48  which can be found at http://fmv.jku.at/aiger
49 */
50 
51 
52 /*
53  The AIGER And-Inverter Graph (AIG) Format Version 20061129
54  ----------------------------------------------------------
55  Armin Biere, Johannes Kepler University, 2006
56 
57  This report describes the AIG file format as used by the AIGER library.
58  The purpose of this report is not only to motivate and document the
59  format, but also to allow independent implementations of writers and
60  readers by giving precise and unambiguous definitions.
61 
62  ...
63 
64 Introduction
65 
66  The name AIGER contains as one part the acronym AIG of And-Inverter
67  Graphs and also if pronounced in German sounds like the name of the
68  'Eiger', a mountain in the Swiss alps. This choice should emphasize the
69  origin of this format. It was first openly discussed at the Alpine
70  Verification Meeting 2006 in Ascona as a way to provide a simple, compact
71  file format for a model checking competition affiliated to CAV 2007.
72 
73  ...
74 
75 Binary Format Definition
76 
77  The binary format is semantically a subset of the ASCII format with a
78  slightly different syntax. The binary format may need to reencode
79  literals, but translating a file in binary format into ASCII format and
80  then back in to binary format will result in the same file.
81 
82  The main differences of the binary format to the ASCII format are as
83  follows. After the header the list of input literals and all the
84  current state literals of a latch can be omitted. Furthermore the
85  definitions of the AND gates are binary encoded. However, the symbol
86  table and the comment section are as in the ASCII format.
87 
88  The header of an AIGER file in binary format has 'aig' as format
89  identifier, but otherwise is identical to the ASCII header. The standard
90  file extension for the binary format is therefore '.aig'.
91 
92  A header for the binary format is still in ASCII encoding:
93 
94  aig M I L O A
95 
96  Constants, variables and literals are handled in the same way as in the
97  ASCII format. The first simplifying restriction is on the variable
98  indices of inputs and latches. The variable indices of inputs come first,
99  followed by the pseudo-primary inputs of the latches and then the variable
100  indices of all LHS of AND gates:
101 
102  input variable indices 1, 2, ... , I
103  latch variable indices I+1, I+2, ... , (I+L)
104  AND variable indices I+L+1, I+L+2, ... , (I+L+A) == M
105 
106  The corresponding unsigned literals are
107 
108  input literals 2, 4, ... , 2*I
109  latch literals 2*I+2, 2*I+4, ... , 2*(I+L)
110  AND literals 2*(I+L)+2, 2*(I+L)+4, ... , 2*(I+L+A) == 2*M
111 
112  All literals have to be defined, and therefore 'M = I + L + A'. With this
113  restriction it becomes possible that the inputs and the current state
114  literals of the latches do not have to be listed explicitly. Therefore,
115  after the header only the list of 'L' next state literals follows, one per
116  latch on a single line, and then the 'O' outputs, again one per line.
117 
118  In the binary format we assume that the AND gates are ordered and respect
119  the child parent relation. AND gates with smaller literals on the LHS
120  come first. Therefore we can assume that the literals on the right-hand
121  side of a definition of an AND gate are smaller than the LHS literal.
122  Furthermore we can sort the literals on the RHS, such that the larger
123  literal comes first. A definition thus consists of three literals
124 
125  lhs rhs0 rhs1
126 
127  with 'lhs' even and 'lhs > rhs0 >= rhs1'. Also the variable indices are
128  pairwise different to avoid combinational self loops. Since the LHS
129  indices of the definitions are all consecutive (as even integers),
130  the binary format does not have to keep 'lhs'. In addition, we can use
131  the order restriction and only write the differences 'delta0' and 'delta1'
132  instead of 'rhs0' and 'rhs1', with
133 
134  delta0 = lhs - rhs0, delta1 = rhs0 - rhs1
135 
136  The differences will all be strictly positive, and in practice often very
137  small. We can take advantage of this fact by the simple little-endian
138  encoding of unsigned integers of the next section. After the binary delta
139  encoding of the RHSs of all AND gates, the optional symbol table and
140  optional comment section start in the same format as in the ASCII case.
141 
142  ...
143 
144 */
145 
146 static unsigned Io_ObjMakeLit( int Var, int fCompl ) { return (Var << 1) | fCompl; }
147 static unsigned Io_ObjAigerNum( Abc_Obj_t * pObj ) { return (unsigned)(ABC_PTRINT_T)pObj->pCopy; }
148 static void Io_ObjSetAigerNum( Abc_Obj_t * pObj, unsigned Num ) { pObj->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)Num; }
149 
150 ////////////////////////////////////////////////////////////////////////
151 /// FUNCTION DEFINITIONS ///
152 ////////////////////////////////////////////////////////////////////////
153 
154 /**Function*************************************************************
155 
156  Synopsis [Adds one unsigned AIG edge to the output buffer.]
157 
158  Description [This procedure is a slightly modified version of Armin Biere's
159  procedure "void encode (FILE * file, unsigned x)" ]
160 
161  SideEffects [Returns the current writing position.]
162 
163  SeeAlso []
164 
165 ***********************************************************************/
166 int Io_WriteAigerEncode( unsigned char * pBuffer, int Pos, unsigned x )
167 {
168  unsigned char ch;
169  while (x & ~0x7f)
170  {
171  ch = (x & 0x7f) | 0x80;
172 // putc (ch, file);
173  pBuffer[Pos++] = ch;
174  x >>= 7;
175  }
176  ch = x;
177 // putc (ch, file);
178  pBuffer[Pos++] = ch;
179  return Pos;
180 }
181 
182 /**Function*************************************************************
183 
184  Synopsis [Create the array of literals to be written.]
185 
186  Description []
187 
188  SideEffects []
189 
190  SeeAlso []
191 
192 ***********************************************************************/
193 Vec_Int_t * Io_WriteAigerLiterals( Abc_Ntk_t * pNtk )
194 {
195  Vec_Int_t * vLits;
196  Abc_Obj_t * pObj, * pDriver;
197  int i;
198  vLits = Vec_IntAlloc( Abc_NtkCoNum(pNtk) );
199  Abc_NtkForEachLatchInput( pNtk, pObj, i )
200  {
201  pDriver = Abc_ObjFanin0(pObj);
202  Vec_IntPush( vLits, Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
203  }
204  Abc_NtkForEachPo( pNtk, pObj, i )
205  {
206  pDriver = Abc_ObjFanin0(pObj);
207  Vec_IntPush( vLits, Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
208  }
209  return vLits;
210 }
211 
212 /**Function*************************************************************
213 
214  Synopsis [Creates the binary encoded array of literals.]
215 
216  Description []
217 
218  SideEffects []
219 
220  SeeAlso []
221 
222 ***********************************************************************/
223 Vec_Str_t * Io_WriteEncodeLiterals( Vec_Int_t * vLits )
224 {
225  Vec_Str_t * vBinary;
226  int Pos = 0, Lit, LitPrev, Diff, i;
227  vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) );
228  LitPrev = Vec_IntEntry( vLits, 0 );
229  Pos = Io_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, LitPrev );
230  Vec_IntForEachEntryStart( vLits, Lit, i, 1 )
231  {
232  Diff = Lit - LitPrev;
233  Diff = (Lit < LitPrev)? -Diff : Diff;
234  Diff = (Diff << 1) | (int)(Lit < LitPrev);
235  Pos = Io_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, Diff );
236  LitPrev = Lit;
237  if ( Pos + 10 > vBinary->nCap )
238  Vec_StrGrow( vBinary, vBinary->nCap+1 );
239  }
240  vBinary->nSize = Pos;
241 /*
242  // verify
243  {
244  extern Vec_Int_t * Io_WriteDecodeLiterals( char ** ppPos, int nEntries );
245  char * pPos = Vec_StrArray( vBinary );
246  Vec_Int_t * vTemp = Io_WriteDecodeLiterals( &pPos, Vec_IntSize(vLits) );
247  for ( i = 0; i < Vec_IntSize(vLits); i++ )
248  {
249  int Entry1 = Vec_IntEntry(vLits,i);
250  int Entry2 = Vec_IntEntry(vTemp,i);
251  assert( Entry1 == Entry2 );
252  }
253  }
254 */
255  return vBinary;
256 }
257 
258 /**Function*************************************************************
259 
260  Synopsis [Writes the AIG in the binary AIGER format.]
261 
262  Description []
263 
264  SideEffects []
265 
266  SeeAlso []
267 
268 ***********************************************************************/
269 void Io_WriteAiger_old( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact )
270 {
271  ProgressBar * pProgress;
272  FILE * pFile;
273  Abc_Obj_t * pObj, * pDriver, * pLatch;
274  int i, nNodes, nBufferSize, Pos, fExtended;
275  unsigned char * pBuffer;
276  unsigned uLit0, uLit1, uLit;
277 
278  fExtended = Abc_NtkConstrNum(pNtk);
279 
280  assert( Abc_NtkIsStrash(pNtk) );
281  Abc_NtkForEachLatch( pNtk, pObj, i )
282  if ( !Abc_LatchIsInit0(pObj) )
283  {
284  if ( !fCompact )
285  {
286  fExtended = 1;
287  break;
288  }
289  fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
290  return;
291  }
292 
293  // start the output stream
294  pFile = fopen( pFileName, "wb" );
295  if ( pFile == NULL )
296  {
297  fprintf( stdout, "Io_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
298  return;
299  }
300 
301  // set the node numbers to be used in the output file
302  nNodes = 0;
303  Io_ObjSetAigerNum( Abc_AigConst1(pNtk), nNodes++ );
304  Abc_NtkForEachCi( pNtk, pObj, i )
305  Io_ObjSetAigerNum( pObj, nNodes++ );
306  Abc_AigForEachAnd( pNtk, pObj, i )
307  Io_ObjSetAigerNum( pObj, nNodes++ );
308 
309  // write the header "M I L O A" where M = I + L + A
310  fprintf( pFile, "aig%s %u %u %u %u %u",
311  fCompact? "2" : "",
312  Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk),
313  Abc_NtkPiNum(pNtk),
314  Abc_NtkLatchNum(pNtk),
315  fExtended ? 0 : Abc_NtkPoNum(pNtk),
316  Abc_NtkNodeNum(pNtk) );
317  // write the extended header "B C J F"
318  if ( fExtended )
319  fprintf( pFile, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) );
320  fprintf( pFile, "\n" );
321 
322  // if the driver node is a constant, we need to complement the literal below
323  // because, in the AIGER format, literal 0/1 is represented as number 0/1
324  // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
325 
326  Abc_NtkInvertConstraints( pNtk );
327  if ( !fCompact )
328  {
329  // write latch drivers
330  Abc_NtkForEachLatch( pNtk, pLatch, i )
331  {
332  pObj = Abc_ObjFanin0(pLatch);
333  pDriver = Abc_ObjFanin0(pObj);
334  uLit = Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) );
335  if ( Abc_LatchIsInit0(pLatch) )
336  fprintf( pFile, "%u\n", uLit );
337  else if ( Abc_LatchIsInit1(pLatch) )
338  fprintf( pFile, "%u 1\n", uLit );
339  else
340  {
341  // Both None and DC are written as 'uninitialized' e.g. a free boolean value
342  assert( Abc_LatchIsInitNone(pLatch) || Abc_LatchIsInitDc(pLatch) );
343  fprintf( pFile, "%u %u\n", uLit, Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanout0(pLatch)), 0 ) );
344  }
345  }
346  // write PO drivers
347  Abc_NtkForEachPo( pNtk, pObj, i )
348  {
349  pDriver = Abc_ObjFanin0(pObj);
350  fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
351  }
352  }
353  else
354  {
355  Vec_Int_t * vLits = Io_WriteAigerLiterals( pNtk );
356  Vec_Str_t * vBinary = Io_WriteEncodeLiterals( vLits );
357  fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile );
358  Vec_StrFree( vBinary );
359  Vec_IntFree( vLits );
360  }
361  Abc_NtkInvertConstraints( pNtk );
362 
363  // write the nodes into the buffer
364  Pos = 0;
365  nBufferSize = 6 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge
366  pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
367  pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
368  Abc_AigForEachAnd( pNtk, pObj, i )
369  {
370  Extra_ProgressBarUpdate( pProgress, i, NULL );
371  uLit = Io_ObjMakeLit( Io_ObjAigerNum(pObj), 0 );
372  uLit0 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin0(pObj)), Abc_ObjFaninC0(pObj) );
373  uLit1 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin1(pObj)), Abc_ObjFaninC1(pObj) );
374  if ( uLit0 > uLit1 )
375  {
376  unsigned Temp = uLit0;
377  uLit0 = uLit1;
378  uLit1 = Temp;
379  }
380  assert( uLit1 < uLit );
381  Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit - uLit1) );
382  Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) );
383  if ( Pos > nBufferSize - 10 )
384  {
385  printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
386  fclose( pFile );
387  return;
388  }
389  }
390  assert( Pos < nBufferSize );
391  Extra_ProgressBarStop( pProgress );
392 
393  // write the buffer
394  fwrite( pBuffer, 1, Pos, pFile );
395  ABC_FREE( pBuffer );
396 
397  // write the symbol table
398  if ( fWriteSymbols )
399  {
400  // write PIs
401  Abc_NtkForEachPi( pNtk, pObj, i )
402  fprintf( pFile, "i%d %s\n", i, Abc_ObjName(pObj) );
403  // write latches
404  Abc_NtkForEachLatch( pNtk, pObj, i )
405  fprintf( pFile, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) );
406  // write POs
407  Abc_NtkForEachPo( pNtk, pObj, i )
408  if ( !fExtended )
409  fprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) );
410  else if ( i < Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) )
411  fprintf( pFile, "b%d %s\n", i, Abc_ObjName(pObj) );
412  else
413  fprintf( pFile, "c%d %s\n", i - (Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk)), Abc_ObjName(pObj) );
414  }
415 
416  // write the comment
417  fprintf( pFile, "c\n" );
418  if ( pNtk->pName && strlen(pNtk->pName) > 0 )
419  fprintf( pFile, ".model %s\n", pNtk->pName );
420  fprintf( pFile, "This file was produced by ABC on %s\n", Extra_TimeStamp() );
421  fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
422  fclose( pFile );
423 }
424 
425 /**Function*************************************************************
426 
427  Synopsis [Writes the AIG in the binary AIGER format.]
428 
429  Description []
430 
431  SideEffects []
432 
433  SeeAlso []
434 
435 ***********************************************************************/
436 void Io_WriteAigerGz( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
437 {
438  ProgressBar * pProgress;
439  gzFile pFile;
440  Abc_Obj_t * pObj, * pDriver, * pLatch;
441  int i, nNodes, Pos, nBufferSize, fExtended;
442  unsigned char * pBuffer;
443  unsigned uLit0, uLit1, uLit;
444 
445  assert( Abc_NtkIsStrash(pNtk) );
446  // start the output stream
447  pFile = gzopen( pFileName, "wb" ); // if pFileName doesn't end in ".gz" then this acts as a passthrough to fopen
448  if ( pFile == NULL )
449  {
450  fprintf( stdout, "Io_WriteAigerGz(): Cannot open the output file \"%s\".\n", pFileName );
451  return;
452  }
453 
454  fExtended = Abc_NtkConstrNum(pNtk);
455 
456  // set the node numbers to be used in the output file
457  nNodes = 0;
458  Io_ObjSetAigerNum( Abc_AigConst1(pNtk), nNodes++ );
459  Abc_NtkForEachCi( pNtk, pObj, i )
460  Io_ObjSetAigerNum( pObj, nNodes++ );
461  Abc_AigForEachAnd( pNtk, pObj, i )
462  Io_ObjSetAigerNum( pObj, nNodes++ );
463 
464  // write the header "M I L O A" where M = I + L + A
465  gzprintf( pFile, "aig %u %u %u %u %u",
466  Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk),
467  Abc_NtkPiNum(pNtk),
468  Abc_NtkLatchNum(pNtk),
469  fExtended ? 0 : Abc_NtkPoNum(pNtk),
470  Abc_NtkNodeNum(pNtk) );
471  // write the extended header "B C J F"
472  if ( fExtended )
473  gzprintf( pFile, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) );
474  gzprintf( pFile, "\n" );
475 
476  // if the driver node is a constant, we need to complement the literal below
477  // because, in the AIGER format, literal 0/1 is represented as number 0/1
478  // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
479 
480  // write latch drivers
481  Abc_NtkInvertConstraints( pNtk );
482  Abc_NtkForEachLatch( pNtk, pLatch, i )
483  {
484  pObj = Abc_ObjFanin0(pLatch);
485  pDriver = Abc_ObjFanin0(pObj);
486  uLit = Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) );
487  if ( Abc_LatchIsInit0(pLatch) )
488  gzprintf( pFile, "%u\n", uLit );
489  else if ( Abc_LatchIsInit1(pLatch) )
490  gzprintf( pFile, "%u 1\n", uLit );
491  else
492  {
493  // Both None and DC are written as 'uninitialized' e.g. a free boolean value
494  assert( Abc_LatchIsInitNone(pLatch) || Abc_LatchIsInitDc(pLatch) );
495  gzprintf( pFile, "%u %u\n", uLit, Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanout0(pLatch)), 0 ) );
496  }
497  }
498  // write PO drivers
499  Abc_NtkForEachPo( pNtk, pObj, i )
500  {
501  pDriver = Abc_ObjFanin0(pObj);
502  gzprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
503  }
504  Abc_NtkInvertConstraints( pNtk );
505 
506  // write the nodes into the buffer
507  Pos = 0;
508  nBufferSize = 6 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge
509  pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
510  pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
511  Abc_AigForEachAnd( pNtk, pObj, i )
512  {
513  Extra_ProgressBarUpdate( pProgress, i, NULL );
514  uLit = Io_ObjMakeLit( Io_ObjAigerNum(pObj), 0 );
515  uLit0 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin0(pObj)), Abc_ObjFaninC0(pObj) );
516  uLit1 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin1(pObj)), Abc_ObjFaninC1(pObj) );
517  if ( uLit0 > uLit1 )
518  {
519  unsigned Temp = uLit0;
520  uLit0 = uLit1;
521  uLit1 = Temp;
522  }
523  assert( uLit1 < uLit );
524  Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 );
525  Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
526  if ( Pos > nBufferSize - 10 )
527  {
528  printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
529  gzclose( pFile );
530  return;
531  }
532  }
533  assert( Pos < nBufferSize );
534  Extra_ProgressBarStop( pProgress );
535 
536  // write the buffer
537  gzwrite(pFile, pBuffer, Pos);
538  ABC_FREE( pBuffer );
539 
540  // write the symbol table
541  if ( fWriteSymbols )
542  {
543  // write PIs
544  Abc_NtkForEachPi( pNtk, pObj, i )
545  gzprintf( pFile, "i%d %s\n", i, Abc_ObjName(pObj) );
546  // write latches
547  Abc_NtkForEachLatch( pNtk, pObj, i )
548  gzprintf( pFile, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) );
549  // write POs
550  Abc_NtkForEachPo( pNtk, pObj, i )
551  if ( !fExtended )
552  gzprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) );
553  else if ( i < Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) )
554  gzprintf( pFile, "b%d %s\n", i, Abc_ObjName(pObj) );
555  else
556  gzprintf( pFile, "c%d %s\n", i - (Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk)), Abc_ObjName(pObj) );
557  }
558 
559  // write the comment
560  gzprintf( pFile, "c\n" );
561  if ( pNtk->pName && strlen(pNtk->pName) > 0 )
562  gzprintf( pFile, ".model %s\n", pNtk->pName );
563  gzprintf( pFile, "This file was produced by ABC on %s\n", Extra_TimeStamp() );
564  gzprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
565  gzclose( pFile );
566 }
567 
568 
569 /**Function*************************************************************
570 
571  Synopsis [Procedure to write data into BZ2 file.]
572 
573  Description [Based on the vsnprintf() man page.]
574 
575  SideEffects []
576 
577  SeeAlso []
578 
579 ***********************************************************************/
580 typedef struct bz2file {
581  FILE * f;
582  BZFILE * b;
583  char * buf;
584  int nBytes;
585  int nBytesMax;
586 } bz2file;
587 
588 int fprintfBz2Aig( bz2file * b, char * fmt, ... ) {
589  if (b->b) {
590  char * newBuf;
591  int bzError;
592  va_list ap;
593  while (1) {
594  va_start(ap,fmt);
595  b->nBytes = vsnprintf(b->buf,b->nBytesMax,fmt,ap);
596  va_end(ap);
597  if (b->nBytes > -1 && b->nBytes < b->nBytesMax)
598  break;
599  if (b->nBytes > -1)
600  b->nBytesMax = b->nBytes + 1;
601  else
602  b->nBytesMax *= 2;
603  if ((newBuf = ABC_REALLOC( char,b->buf,b->nBytesMax )) == NULL)
604  return -1;
605  else
606  b->buf = newBuf;
607  }
608  BZ2_bzWrite( &bzError, b->b, b->buf, b->nBytes );
609  if (bzError == BZ_IO_ERROR) {
610  fprintf( stdout, "Ioa_WriteBlif(): I/O error writing to compressed stream.\n" );
611  return -1;
612  }
613  return b->nBytes;
614  } else {
615  int n;
616  va_list ap;
617  va_start(ap,fmt);
618  n = vfprintf( b->f, fmt, ap);
619  va_end(ap);
620  return n;
621  }
622 }
623 
624 /**Function*************************************************************
625 
626  Synopsis [Writes the AIG in the binary AIGER format.]
627 
628  Description []
629 
630  SideEffects []
631 
632  SeeAlso []
633 
634 ***********************************************************************/
635 void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact, int fUnique )
636 {
637  ProgressBar * pProgress;
638 // FILE * pFile;
639  Abc_Obj_t * pObj, * pDriver, * pLatch;
640  int i, nNodes, nBufferSize, bzError, Pos, fExtended;
641  unsigned char * pBuffer;
642  unsigned uLit0, uLit1, uLit;
643  bz2file b;
644 
645  // define unique writing
646  if ( fUnique )
647  {
648  fWriteSymbols = 0;
649  fCompact = 0;
650  }
651 
652  fExtended = Abc_NtkConstrNum(pNtk);
653 
654  // check that the network is valid
655  assert( Abc_NtkIsStrash(pNtk) );
656  Abc_NtkForEachLatch( pNtk, pObj, i )
657  if ( !Abc_LatchIsInit0(pObj) )
658  {
659  if ( !fCompact )
660  {
661  fExtended = 1;
662  break;
663  }
664  fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
665  return;
666  }
667 
668  // write the GZ file
669  if (!strncmp(pFileName+strlen(pFileName)-3,".gz",3))
670  {
671  Io_WriteAigerGz( pNtk, pFileName, fWriteSymbols );
672  return;
673  }
674 
675  memset(&b,0,sizeof(b));
676  b.nBytesMax = (1<<12);
677  b.buf = ABC_ALLOC( char,b.nBytesMax );
678 
679  // start the output stream
680  b.f = fopen( pFileName, "wb" );
681  if ( b.f == NULL )
682  {
683  fprintf( stdout, "Ioa_WriteBlif(): Cannot open the output file \"%s\".\n", pFileName );
684  ABC_FREE(b.buf);
685  return;
686  }
687  if (!strncmp(pFileName+strlen(pFileName)-4,".bz2",4)) {
688  b.b = BZ2_bzWriteOpen( &bzError, b.f, 9, 0, 0 );
689  if ( bzError != BZ_OK ) {
690  BZ2_bzWriteClose( &bzError, b.b, 0, NULL, NULL );
691  fprintf( stdout, "Ioa_WriteBlif(): Cannot start compressed stream.\n" );
692  fclose( b.f );
693  ABC_FREE(b.buf);
694  return;
695  }
696  }
697 
698  // set the node numbers to be used in the output file
699  nNodes = 0;
700  Io_ObjSetAigerNum( Abc_AigConst1(pNtk), nNodes++ );
701  Abc_NtkForEachCi( pNtk, pObj, i )
702  Io_ObjSetAigerNum( pObj, nNodes++ );
703  Abc_AigForEachAnd( pNtk, pObj, i )
704  Io_ObjSetAigerNum( pObj, nNodes++ );
705 
706  // write the header "M I L O A" where M = I + L + A
707  fprintfBz2Aig( &b, "aig%s %u %u %u %u %u",
708  fCompact? "2" : "",
709  Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk),
710  Abc_NtkPiNum(pNtk),
711  Abc_NtkLatchNum(pNtk),
712  fExtended ? 0 : Abc_NtkPoNum(pNtk),
713  Abc_NtkNodeNum(pNtk) );
714  // write the extended header "B C J F"
715  if ( fExtended )
716  fprintfBz2Aig( &b, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) );
717  fprintfBz2Aig( &b, "\n" );
718 
719  // if the driver node is a constant, we need to complement the literal below
720  // because, in the AIGER format, literal 0/1 is represented as number 0/1
721  // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
722 
723  Abc_NtkInvertConstraints( pNtk );
724  if ( !fCompact )
725  {
726  // write latch drivers
727  Abc_NtkForEachLatch( pNtk, pLatch, i )
728  {
729  pObj = Abc_ObjFanin0(pLatch);
730  pDriver = Abc_ObjFanin0(pObj);
731  uLit = Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) );
732  if ( Abc_LatchIsInit0(pLatch) )
733  fprintfBz2Aig( &b, "%u\n", uLit );
734  else if ( Abc_LatchIsInit1(pLatch) )
735  fprintfBz2Aig( &b, "%u 1\n", uLit );
736  else
737  {
738  // Both None and DC are written as 'uninitialized' e.g. a free boolean value
739  assert( Abc_LatchIsInitNone(pLatch) || Abc_LatchIsInitDc(pLatch) );
740  fprintfBz2Aig( &b, "%u %u\n", uLit, Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanout0(pLatch)), 0 ) );
741  }
742  }
743  // write PO drivers
744  Abc_NtkForEachPo( pNtk, pObj, i )
745  {
746  pDriver = Abc_ObjFanin0(pObj);
747  fprintfBz2Aig( &b, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
748  }
749  }
750  else
751  {
752  Vec_Int_t * vLits = Io_WriteAigerLiterals( pNtk );
753  Vec_Str_t * vBinary = Io_WriteEncodeLiterals( vLits );
754  if ( !b.b )
755  fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), b.f );
756  else
757  {
758  BZ2_bzWrite( &bzError, b.b, Vec_StrArray(vBinary), Vec_StrSize(vBinary) );
759  if (bzError == BZ_IO_ERROR) {
760  fprintf( stdout, "Io_WriteAiger(): I/O error writing to compressed stream.\n" );
761  fclose( b.f );
762  ABC_FREE(b.buf);
763  Vec_StrFree( vBinary );
764  return;
765  }
766  }
767  Vec_StrFree( vBinary );
768  Vec_IntFree( vLits );
769  }
770  Abc_NtkInvertConstraints( pNtk );
771 
772  // write the nodes into the buffer
773  Pos = 0;
774  nBufferSize = 6 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge
775  pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
776  pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
777  Abc_AigForEachAnd( pNtk, pObj, i )
778  {
779  Extra_ProgressBarUpdate( pProgress, i, NULL );
780  uLit = Io_ObjMakeLit( Io_ObjAigerNum(pObj), 0 );
781  uLit0 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin0(pObj)), Abc_ObjFaninC0(pObj) );
782  uLit1 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin1(pObj)), Abc_ObjFaninC1(pObj) );
783  if ( uLit0 > uLit1 )
784  {
785  unsigned Temp = uLit0;
786  uLit0 = uLit1;
787  uLit1 = Temp;
788  }
789  assert( uLit1 < uLit );
790  Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit - uLit1) );
791  Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) );
792  if ( Pos > nBufferSize - 10 )
793  {
794  printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
795  fclose( b.f );
796  ABC_FREE(b.buf);
797  Extra_ProgressBarStop( pProgress );
798  return;
799  }
800  }
801  assert( Pos < nBufferSize );
802  Extra_ProgressBarStop( pProgress );
803 
804  // write the buffer
805  if ( !b.b )
806  fwrite( pBuffer, 1, Pos, b.f );
807  else
808  {
809  BZ2_bzWrite( &bzError, b.b, pBuffer, Pos );
810  if (bzError == BZ_IO_ERROR) {
811  fprintf( stdout, "Io_WriteAiger(): I/O error writing to compressed stream.\n" );
812  fclose( b.f );
813  ABC_FREE(b.buf);
814  return;
815  }
816  }
817  ABC_FREE( pBuffer );
818 
819  // write the symbol table
820  if ( fWriteSymbols )
821  {
822  // write PIs
823  Abc_NtkForEachPi( pNtk, pObj, i )
824  fprintfBz2Aig( &b, "i%d %s\n", i, Abc_ObjName(pObj) );
825  // write latches
826  Abc_NtkForEachLatch( pNtk, pObj, i )
827  fprintfBz2Aig( &b, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) );
828  // write POs
829  Abc_NtkForEachPo( pNtk, pObj, i )
830  if ( !fExtended )
831  fprintfBz2Aig( &b, "o%d %s\n", i, Abc_ObjName(pObj) );
832  else if ( i < Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) )
833  fprintfBz2Aig( &b, "b%d %s\n", i, Abc_ObjName(pObj) );
834  else
835  fprintfBz2Aig( &b, "c%d %s\n", i - (Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk)), Abc_ObjName(pObj) );
836  }
837 
838  // write the comment
839  fprintfBz2Aig( &b, "c" );
840  if ( !fUnique )
841  {
842  if ( pNtk->pName && strlen(pNtk->pName) > 0 )
843  fprintfBz2Aig( &b, "\n%s%c", pNtk->pName, '\0' );
844  fprintfBz2Aig( &b, "\nThis file was written by ABC on %s\n", Extra_TimeStamp() );
845  fprintfBz2Aig( &b, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
846  }
847 
848  // close the file
849  if (b.b) {
850  BZ2_bzWriteClose( &bzError, b.b, 0, NULL, NULL );
851  if (bzError == BZ_IO_ERROR) {
852  fprintf( stdout, "Io_WriteAiger(): I/O error closing compressed stream.\n" );
853  fclose( b.f );
854  ABC_FREE(b.buf);
855  return;
856  }
857  }
858  fclose( b.f );
859  ABC_FREE(b.buf);
860 }
861 
862 ABC_NAMESPACE_IMPL_END
863 
864 #include "aig/gia/giaAig.h"
865 #include "aig/saig/saig.h"
866 
867 ABC_NAMESPACE_IMPL_START
868 
869 /**Function*************************************************************
870 
871  Synopsis [Writes the AIG in the binary AIGER format.]
872 
873  Description []
874 
875  SideEffects []
876 
877  SeeAlso []
878 
879 ***********************************************************************/
880 void Io_WriteAigerCex( Abc_Cex_t * pCex, Abc_Ntk_t * pNtk, void * pG, char * pFileName )
881 {
882  extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
883  FILE * pFile;
884  Aig_Man_t * pAig;
885  Aig_Obj_t * pObj, * pObj2;
886  Gia_Man_t * pGia = (Gia_Man_t *)pG;
887  int k, f, b;
888  assert( pCex != NULL );
889 
890  // derive AIG
891  if ( pNtk != NULL &&
892  Abc_NtkPiNum(pNtk) == pCex->nPis &&
893  Abc_NtkLatchNum(pNtk) == pCex->nRegs )
894  {
895  pAig = Abc_NtkToDar( pNtk, 0, 1 );
896  }
897  else if ( pGia != NULL &&
898  Gia_ManPiNum(pGia) == pCex->nPis &&
899  Gia_ManRegNum(pGia) == pCex->nRegs )
900  {
901  pAig = Gia_ManToAigSimple( pGia );
902  }
903  else
904  {
905  printf( "AIG parameters do not match those of the CEX.\n" );
906  return;
907  }
908 
909  // create output file
910  pFile = fopen( pFileName, "wb" );
911  fprintf( pFile, "1\n" );
912  b = pCex->nRegs;
913  for ( k = 0; k < pCex->nRegs; k++ )
914  fprintf( pFile, "0" );
915  fprintf( pFile, " " );
916  Aig_ManCleanMarkA( pAig );
917  for ( f = 0; f <= pCex->iFrame; f++ )
918  {
919  for ( k = 0; k < pCex->nPis; k++ )
920  {
921  fprintf( pFile, "%d", Abc_InfoHasBit(pCex->pData, b) );
922  Aig_ManCi( pAig, k )->fMarkA = Abc_InfoHasBit(pCex->pData, b++);
923  }
924  fprintf( pFile, " " );
925  Aig_ManForEachNode( pAig, pObj, k )
926  pObj->fMarkA = (Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj)) &
927  (Aig_ObjFanin1(pObj)->fMarkA ^ Aig_ObjFaninC1(pObj));
928  Aig_ManForEachCo( pAig, pObj, k )
929  pObj->fMarkA = (Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj));
930  Saig_ManForEachPo( pAig, pObj, k )
931  fprintf( pFile, "%d", pObj->fMarkA );
932  fprintf( pFile, " " );
933  Saig_ManForEachLi( pAig, pObj, k )
934  fprintf( pFile, "%d", pObj->fMarkA );
935  fprintf( pFile, "\n" );
936  if ( f == pCex->iFrame )
937  break;
938  Saig_ManForEachLi( pAig, pObj, k )
939  fprintf( pFile, "%d", pObj->fMarkA );
940  fprintf( pFile, " " );
941  Saig_ManForEachLiLo( pAig, pObj, pObj2, k )
942  pObj2->fMarkA = pObj->fMarkA;
943  }
944  assert( b == pCex->nBits );
945  fclose( pFile );
946  Aig_ManCleanMarkA( pAig );
947  Aig_ManStop( pAig );
948 }
949 
950 ////////////////////////////////////////////////////////////////////////
951 /// END OF FILE ///
952 ////////////////////////////////////////////////////////////////////////
953 
954 
955 ABC_NAMESPACE_IMPL_END
956 
memset
char * memset()
Abc_NtkInvertConstraints
ABC_DLL void Abc_NtkInvertConstraints(Abc_Ntk_t *pNtk)
Definition: abcUtil.c:2204
Abc_NtkIsStrash
static int Abc_NtkIsStrash(Abc_Ntk_t *pNtk)
Definition: abc.h:251
BZ2_bzWrite
void BZ_API() BZ2_bzWrite(int *bzerror, BZFILE *b, void *buf, int len)
Definition: bzlib.c:976
Io_WriteAigerCex
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START void Io_WriteAigerCex(Abc_Cex_t *pCex, Abc_Ntk_t *pNtk, void *pG, char *pFileName)
Definition: ioWriteAiger.c:880
Abc_ObjFanin1
static Abc_Obj_t * Abc_ObjFanin1(Abc_Obj_t *pObj)
Definition: abc.h:374
Io_ObjMakeLit
static ABC_NAMESPACE_IMPL_START unsigned Io_ObjMakeLit(int Var, int fCompl)
DECLARATIONS ///.
Definition: ioWriteAiger.c:146
Gia_ManToAigSimple
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
Abc_LatchIsInitNone
static int Abc_LatchIsInitNone(Abc_Obj_t *pLatch)
Definition: abc.h:421
Abc_NtkObjNumMax
static int Abc_NtkObjNumMax(Abc_Ntk_t *pNtk)
Definition: abc.h:284
Abc_AigConst1
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
Definition: abcAig.c:683
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
BZ2_bzWriteClose
void BZ_API() BZ2_bzWriteClose(int *bzerror, BZFILE *b, int abandon, unsigned int *nbytes_in, unsigned int *nbytes_out)
Definition: bzlib.c:1021
Abc_ObjFaninC1
static int Abc_ObjFaninC1(Abc_Obj_t *pObj)
Definition: abc.h:378
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
bz2file::nBytes
int nBytes
Definition: ioWriteAiger.c:584
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Vec_StrArray
static char * Vec_StrArray(Vec_Str_t *p)
Definition: vecStr.h:272
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition: abc_global.h:233
Pos
ush Pos
Definition: deflate.h:88
Abc_Ntk_t_
Definition: abc.h:153
Io_WriteEncodeLiterals
Vec_Str_t * Io_WriteEncodeLiterals(Vec_Int_t *vLits)
Definition: ioWriteAiger.c:223
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Abc_NtkLatchNum
static int Abc_NtkLatchNum(Abc_Ntk_t *pNtk)
Definition: abc.h:294
Abc_ObjFaninC0
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
Definition: abc.h:377
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition: aig.h:79
Io_WriteAiger
void Io_WriteAiger(Abc_Ntk_t *pNtk, char *pFileName, int fWriteSymbols, int fCompact, int fUnique)
Definition: ioWriteAiger.c:635
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Abc_LatchIsInit0
static int Abc_LatchIsInit0(Abc_Obj_t *pLatch)
Definition: abc.h:422
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
gzclose
ABC_NAMESPACE_IMPL_START int ZEXPORT gzclose(gzFile file)
Definition: gzclose.c:18
Vec_StrAlloc
static Vec_Str_t * Vec_StrAlloc(int nCap)
Definition: bblif.c:495
Io_WriteAigerEncode
int Io_WriteAigerEncode(unsigned char *pBuffer, int Pos, unsigned x)
FUNCTION DEFINITIONS ///.
Definition: ioWriteAiger.c:166
gzwrite
int ZEXPORT gzwrite(gzFile file, voidpc buf, unsigned len)
Definition: gzwrite.c:145
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
bz2file::f
FILE * f
Definition: ioWriteAiger.c:581
gzFile
voidp gzFile
Definition: zlib.h:1173
Abc_ObjFanin0
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
BZ2_bzWriteOpen
BZFILE *BZ_API() BZ2_bzWriteOpen(int *bzerror, FILE *f, int blockSize100k, int verbosity, int workFactor)
Definition: bzlib.c:928
Io_ObjAigerNum
static unsigned Io_ObjAigerNum(Abc_Obj_t *pObj)
Definition: ioWriteAiger.c:147
Abc_NtkCoNum
static int Abc_NtkCoNum(Abc_Ntk_t *pNtk)
Definition: abc.h:288
bz2file::nBytesMax
int nBytesMax
Definition: ioWriteAiger.c:585
Abc_Obj_t_
Definition: abc.h:128
Abc_AigForEachAnd
#define Abc_AigForEachAnd(pNtk, pNode, i)
Definition: abc.h:485
Abc_NtkNodeNum
static int Abc_NtkNodeNum(Abc_Ntk_t *pNtk)
Definition: abc.h:293
bz2file::b
BZFILE * b
Definition: ioWriteAiger.c:582
Vec_StrGrow
static void Vec_StrGrow(Vec_Str_t *p, int nCapMin)
Definition: vecStr.h:404
ProgressBarStruct
DECLARATIONS ///.
Definition: extraUtilProgress.c:32
bz2file
struct bz2file bz2file
Abc_Obj_t_::pCopy
Abc_Obj_t * pCopy
Definition: abc.h:148
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
BZ_OK
#define BZ_OK
Definition: bzlib.h:34
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
bz2file::buf
char * buf
Definition: ioWriteAiger.c:583
Abc_NtkToDar
Aig_Man_t * Abc_NtkToDar(Abc_Ntk_t *pNtk, int fExors, int fRegisters)
Definition: abcDar.c:233
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Vec_StrFree
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
Aig_ManCi
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Abc_LatchIsInitDc
static int Abc_LatchIsInitDc(Abc_Obj_t *pLatch)
Definition: abc.h:424
Io_WriteAigerLiterals
Vec_Int_t * Io_WriteAigerLiterals(Abc_Ntk_t *pNtk)
Definition: ioWriteAiger.c:193
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Abc_NtkForEachLatch
#define Abc_NtkForEachLatch(pNtk, pObj, i)
Definition: abc.h:497
Abc_LatchIsInit1
static int Abc_LatchIsInit1(Abc_Obj_t *pLatch)
Definition: abc.h:423
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
Extra_ProgressBarStop
void Extra_ProgressBarStop(ProgressBar *p)
Definition: extraUtilProgress.c:118
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Abc_NtkConstrNum
static int Abc_NtkConstrNum(Abc_Ntk_t *pNtk)
Definition: abc.h:299
gzprintf
int ZEXPORTVA gzprintf(gzFile file, const char *format, int a1, int a2, int a3, int a4, int a5, int a6, int a7, int a8, int a9, int a10, int a11, int a12, int a13, int a14, int a15, int a16, int a17, int a18, int a19, int a20)
Definition: gzwrite.c:347
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Vec_StrSize
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
Io_WriteAiger_old
void Io_WriteAiger_old(Abc_Ntk_t *pNtk, char *pFileName, int fWriteSymbols, int fCompact)
Definition: ioWriteAiger.c:269
gzopen
gzFile ZEXPORT gzopen(const char *path, const char *mode)
Definition: gzlib.c:198
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Abc_NtkForEachCi
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition: abc.h:515
Abc_NtkPoNum
static int Abc_NtkPoNum(Abc_Ntk_t *pNtk)
Definition: abc.h:286
Vec_Str_t_
Definition: bblif.c:47
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
Abc_NtkPiNum
static int Abc_NtkPiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:285
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
Vec_Str_t_::nSize
int nSize
Definition: bblif.c:50
Extra_TimeStamp
char * Extra_TimeStamp()
Definition: extraUtilFile.c:446
Abc_NtkForEachLatchInput
#define Abc_NtkForEachLatchInput(pNtk, pObj, i)
Definition: abc.h:500
Extra_ProgressBarStart
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition: extraUtilProgress.c:62
Aig_ManCleanMarkA
void Aig_ManCleanMarkA(Aig_Man_t *p)
Definition: aigUtil.c:148
Minisat::Var
int Var
Definition: SolverTypes.h:42
strncmp
int strncmp()
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Io_ObjSetAigerNum
static void Io_ObjSetAigerNum(Abc_Obj_t *pObj, unsigned Num)
Definition: ioWriteAiger.c:148
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
assert
#define assert(ex)
Definition: util_old.h:213
Extra_ProgressBarUpdate
static void Extra_ProgressBarUpdate(ProgressBar *p, int nItemsCur, char *pString)
Definition: extra.h:243
strlen
int strlen()
Io_WriteAigerGz
void Io_WriteAigerGz(Abc_Ntk_t *pNtk, char *pFileName, int fWriteSymbols)
Definition: ioWriteAiger.c:436
BZ_IO_ERROR
#define BZ_IO_ERROR
Definition: bzlib.h:44
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
fprintfBz2Aig
int fprintfBz2Aig(bz2file *b, char *fmt,...)
Definition: ioWriteAiger.c:588
Abc_NtkForEachPo
#define Abc_NtkForEachPo(pNtk, pPo, i)
Definition: abc.h:517
BZFILE
void BZFILE
Definition: bzlib.h:142
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Vec_Str_t_::nCap
int nCap
Definition: bblif.c:49
Abc_Ntk_t_::pName
char * pName
Definition: abc.h:158
Abc_ObjFanout0
static Abc_Obj_t * Abc_ObjFanout0(Abc_Obj_t *pObj)
Definition: abc.h:371
Abc_NtkForEachPi
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition: abc.h:513
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387