abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
kitPla.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [kitPla.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Computation kit.]
8 
9  Synopsis [Manipulating SOP in the form of a C-string.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - Dec 6, 2006.]
16 
17  Revision [$Id: kitPla.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "kit.h"
22 #include "aig/aig/aig.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 /**Function*************************************************************
36 
37  Synopsis [Checks if the cover is constant 0.]
38 
39  Description []
40 
41  SideEffects []
42 
43  SeeAlso []
44 
45 ***********************************************************************/
46 int Kit_PlaIsConst0( char * pSop )
47 {
48  return pSop[0] == ' ' && pSop[1] == '0';
49 }
50 
51 /**Function*************************************************************
52 
53  Synopsis [Checks if the cover is constant 1.]
54 
55  Description []
56 
57  SideEffects []
58 
59  SeeAlso []
60 
61 ***********************************************************************/
62 int Kit_PlaIsConst1( char * pSop )
63 {
64  return pSop[0] == ' ' && pSop[1] == '1';
65 }
66 
67 /**Function*************************************************************
68 
69  Synopsis [Checks if the cover is a buffer.]
70 
71  Description []
72 
73  SideEffects []
74 
75  SeeAlso []
76 
77 ***********************************************************************/
78 int Kit_PlaIsBuf( char * pSop )
79 {
80  if ( pSop[4] != 0 )
81  return 0;
82  if ( (pSop[0] == '1' && pSop[2] == '1') || (pSop[0] == '0' && pSop[2] == '0') )
83  return 1;
84  return 0;
85 }
86 
87 /**Function*************************************************************
88 
89  Synopsis [Checks if the cover is an inverter.]
90 
91  Description []
92 
93  SideEffects []
94 
95  SeeAlso []
96 
97 ***********************************************************************/
98 int Kit_PlaIsInv( char * pSop )
99 {
100  if ( pSop[4] != 0 )
101  return 0;
102  if ( (pSop[0] == '0' && pSop[2] == '1') || (pSop[0] == '1' && pSop[2] == '0') )
103  return 1;
104  return 0;
105 }
106 
107 /**Function*************************************************************
108 
109  Synopsis [Reads the number of variables in the cover.]
110 
111  Description []
112 
113  SideEffects []
114 
115  SeeAlso []
116 
117 ***********************************************************************/
118 int Kit_PlaGetVarNum( char * pSop )
119 {
120  char * pCur;
121  for ( pCur = pSop; *pCur != '\n'; pCur++ )
122  if ( *pCur == 0 )
123  return -1;
124  return pCur - pSop - 2;
125 }
126 
127 /**Function*************************************************************
128 
129  Synopsis [Reads the number of cubes in the cover.]
130 
131  Description []
132 
133  SideEffects []
134 
135  SeeAlso []
136 
137 ***********************************************************************/
138 int Kit_PlaGetCubeNum( char * pSop )
139 {
140  char * pCur;
141  int nCubes = 0;
142  if ( pSop == NULL )
143  return 0;
144  for ( pCur = pSop; *pCur; pCur++ )
145  nCubes += (*pCur == '\n');
146  return nCubes;
147 }
148 
149 /**Function*************************************************************
150 
151  Synopsis []
152 
153  Description []
154 
155  SideEffects []
156 
157  SeeAlso []
158 
159 ***********************************************************************/
160 int Kit_PlaIsComplement( char * pSop )
161 {
162  char * pCur;
163  for ( pCur = pSop; *pCur; pCur++ )
164  if ( *pCur == '\n' )
165  return (int)(*(pCur - 1) == '0' || *(pCur - 1) == 'n');
166  assert( 0 );
167  return 0;
168 }
169 
170 /**Function*************************************************************
171 
172  Synopsis []
173 
174  Description []
175 
176  SideEffects []
177 
178  SeeAlso []
179 
180 ***********************************************************************/
181 void Kit_PlaComplement( char * pSop )
182 {
183  char * pCur;
184  for ( pCur = pSop; *pCur; pCur++ )
185  if ( *pCur == '\n' )
186  {
187  if ( *(pCur - 1) == '0' )
188  *(pCur - 1) = '1';
189  else if ( *(pCur - 1) == '1' )
190  *(pCur - 1) = '0';
191  else if ( *(pCur - 1) == 'x' )
192  *(pCur - 1) = 'n';
193  else if ( *(pCur - 1) == 'n' )
194  *(pCur - 1) = 'x';
195  else
196  assert( 0 );
197  }
198 }
199 
200 /**Function*************************************************************
201 
202  Synopsis [Creates the constant 1 cover with the given number of variables and cubes.]
203 
204  Description []
205 
206  SideEffects []
207 
208  SeeAlso []
209 
210 ***********************************************************************/
211 char * Kit_PlaStart( void * p, int nCubes, int nVars )
212 {
213  Aig_MmFlex_t * pMan = (Aig_MmFlex_t *)p;
214  char * pSopCover, * pCube;
215  int i, Length;
216 
217  Length = nCubes * (nVars + 3);
218  pSopCover = Aig_MmFlexEntryFetch( pMan, Length + 1 );
219  memset( pSopCover, '-', Length );
220  pSopCover[Length] = 0;
221 
222  for ( i = 0; i < nCubes; i++ )
223  {
224  pCube = pSopCover + i * (nVars + 3);
225  pCube[nVars + 0] = ' ';
226  pCube[nVars + 1] = '1';
227  pCube[nVars + 2] = '\n';
228  }
229  return pSopCover;
230 }
231 
232 /**Function*************************************************************
233 
234  Synopsis [Creates the cover from the ISOP computed from TT.]
235 
236  Description []
237 
238  SideEffects []
239 
240  SeeAlso []
241 
242 ***********************************************************************/
243 char * Kit_PlaCreateFromIsop( void * p, int nVars, Vec_Int_t * vCover )
244 {
245  Aig_MmFlex_t * pMan = (Aig_MmFlex_t *)p;
246  char * pSop, * pCube;
247  int i, k, Entry, Literal;
248  assert( Vec_IntSize(vCover) > 0 );
249  if ( Vec_IntSize(vCover) == 0 )
250  return NULL;
251  // start the cover
252  pSop = Kit_PlaStart( pMan, Vec_IntSize(vCover), nVars );
253  // create cubes
254  Vec_IntForEachEntry( vCover, Entry, i )
255  {
256  pCube = pSop + i * (nVars + 3);
257  for ( k = 0; k < nVars; k++ )
258  {
259  Literal = 3 & (Entry >> (k << 1));
260  if ( Literal == 1 )
261  pCube[k] = '0';
262  else if ( Literal == 2 )
263  pCube[k] = '1';
264  else if ( Literal != 0 )
265  assert( 0 );
266  }
267  }
268  return pSop;
269 }
270 
271 /**Function*************************************************************
272 
273  Synopsis [Creates the cover from the ISOP computed from TT.]
274 
275  Description []
276 
277  SideEffects []
278 
279  SeeAlso []
280 
281 ***********************************************************************/
282 void Kit_PlaToIsop( char * pSop, Vec_Int_t * vCover )
283 {
284  char * pCube;
285  int k, nVars, Entry;
286  nVars = Kit_PlaGetVarNum( pSop );
287  assert( nVars > 0 );
288  // create cubes
289  Vec_IntClear( vCover );
290  for ( pCube = pSop; *pCube; pCube += nVars + 3 )
291  {
292  Entry = 0;
293  for ( k = nVars - 1; k >= 0; k-- )
294  if ( pCube[k] == '0' )
295  Entry = (Entry << 2) | 1;
296  else if ( pCube[k] == '1' )
297  Entry = (Entry << 2) | 2;
298  else if ( pCube[k] == '-' )
299  Entry = (Entry << 2);
300  else
301  assert( 0 );
302  Vec_IntPush( vCover, Entry );
303  }
304 }
305 
306 /**Function*************************************************************
307 
308  Synopsis [Allocates memory and copies the SOP into it.]
309 
310  Description []
311 
312  SideEffects []
313 
314  SeeAlso []
315 
316 ***********************************************************************/
317 char * Kit_PlaStoreSop( void * p, char * pSop )
318 {
319  Aig_MmFlex_t * pMan = (Aig_MmFlex_t *)p;
320  char * pStore;
321  pStore = Aig_MmFlexEntryFetch( pMan, strlen(pSop) + 1 );
322  strcpy( pStore, pSop );
323  return pStore;
324 }
325 
326 /**Function*************************************************************
327 
328  Synopsis [Transforms truth table into the SOP.]
329 
330  Description []
331 
332  SideEffects []
333 
334  SeeAlso []
335 
336 ***********************************************************************/
337 char * Kit_PlaFromTruth( void * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover )
338 {
339  Aig_MmFlex_t * pMan = (Aig_MmFlex_t *)p;
340  char * pSop;
341  int RetValue;
342  if ( Kit_TruthIsConst0(pTruth, nVars) )
343  return Kit_PlaStoreSop( pMan, " 0\n" );
344  if ( Kit_TruthIsConst1(pTruth, nVars) )
345  return Kit_PlaStoreSop( pMan, " 1\n" );
346  RetValue = Kit_TruthIsop( pTruth, nVars, vCover, 0 ); // 1 );
347  assert( RetValue == 0 || RetValue == 1 );
348  pSop = Kit_PlaCreateFromIsop( pMan, nVars, vCover );
349  if ( RetValue )
350  Kit_PlaComplement( pSop );
351  return pSop;
352 }
353 
354 
355 /**Function*************************************************************
356 
357  Synopsis [Creates the cover from the ISOP computed from TT.]
358 
359  Description []
360 
361  SideEffects []
362 
363  SeeAlso []
364 
365 ***********************************************************************/
366 char * Kit_PlaFromIsop( Vec_Str_t * vStr, int nVars, Vec_Int_t * vCover )
367 {
368  int i, k, Entry, Literal;
369  assert( Vec_IntSize(vCover) > 0 );
370  if ( Vec_IntSize(vCover) == 0 )
371  return NULL;
372  Vec_StrClear( vStr );
373  Vec_IntForEachEntry( vCover, Entry, i )
374  {
375  for ( k = 0; k < nVars; k++ )
376  {
377  Literal = 3 & (Entry >> (k << 1));
378  if ( Literal == 1 )
379  Vec_StrPush( vStr, '0' );
380  else if ( Literal == 2 )
381  Vec_StrPush( vStr, '1' );
382  else if ( Literal == 0 )
383  Vec_StrPush( vStr, '-' );
384  else
385  assert( 0 );
386  }
387  Vec_StrPush( vStr, ' ' );
388  Vec_StrPush( vStr, '1' );
389  Vec_StrPush( vStr, '\n' );
390  }
391  Vec_StrPush( vStr, '\0' );
392  return Vec_StrArray( vStr );
393 }
394 
395 /**Function*************************************************************
396 
397  Synopsis [Creates the SOP from TT.]
398 
399  Description []
400 
401  SideEffects []
402 
403  SeeAlso []
404 
405 ***********************************************************************/
406 char * Kit_PlaFromTruthNew( unsigned * pTruth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vStr )
407 {
408  char * pResult;
409  // transform truth table into the SOP
410  int RetValue = Kit_TruthIsop( pTruth, nVars, vCover, 1 );
411  assert( RetValue == 0 || RetValue == 1 );
412  // check the case of constant cover
413  if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover,0) == 0) )
414  {
415  assert( RetValue == 0 );
416  Vec_StrClear( vStr );
417  Vec_StrAppend( vStr, (Vec_IntSize(vCover) == 0) ? " 0\n" : " 1\n" );
418  Vec_StrPush( vStr, '\0' );
419  return Vec_StrArray( vStr );
420  }
421  pResult = Kit_PlaFromIsop( vStr, nVars, vCover );
422  if ( RetValue )
423  Kit_PlaComplement( pResult );
424  if ( nVars < 6 )
425  assert( pTruth[0] == (unsigned)Kit_PlaToTruth6(pResult, nVars) );
426  else if ( nVars == 6 )
427  assert( *((ABC_UINT64_T*)pTruth) == Kit_PlaToTruth6(pResult, nVars) );
428  return pResult;
429 }
430 
431 /**Function*************************************************************
432 
433  Synopsis [Converts SOP into a truth table.]
434 
435  Description []
436 
437  SideEffects []
438 
439  SeeAlso []
440 
441 ***********************************************************************/
442 ABC_UINT64_T Kit_PlaToTruth6( char * pSop, int nVars )
443 {
444  static ABC_UINT64_T Truth[8] = {
445  ABC_CONST(0xAAAAAAAAAAAAAAAA),
446  ABC_CONST(0xCCCCCCCCCCCCCCCC),
447  ABC_CONST(0xF0F0F0F0F0F0F0F0),
448  ABC_CONST(0xFF00FF00FF00FF00),
449  ABC_CONST(0xFFFF0000FFFF0000),
450  ABC_CONST(0xFFFFFFFF00000000),
451  ABC_CONST(0x0000000000000000),
452  ABC_CONST(0xFFFFFFFFFFFFFFFF)
453  };
454  ABC_UINT64_T valueAnd, valueOr = Truth[6];
455  int v, lit = 0;
456  assert( nVars < 7 );
457  do {
458  valueAnd = Truth[7];
459  for ( v = 0; v < nVars; v++, lit++ )
460  {
461  if ( pSop[lit] == '1' )
462  valueAnd &= Truth[v];
463  else if ( pSop[lit] == '0' )
464  valueAnd &= ~Truth[v];
465  else if ( pSop[lit] != '-' )
466  assert( 0 );
467  }
468  valueOr |= valueAnd;
469  assert( pSop[lit] == ' ' );
470  lit++;
471  lit++;
472  assert( pSop[lit] == '\n' );
473  lit++;
474  } while ( pSop[lit] );
475  if ( Kit_PlaIsComplement(pSop) )
476  valueOr = ~valueOr;
477  return valueOr;
478 }
479 
480 /**Fnction*************************************************************
481 
482  Synopsis [Converting SOP into a truth table.]
483 
484  Description [The SOP is represented as a C-string, as documented in
485  file "bblif.h". The truth table is returned as a bit-string composed
486  of 2^nVars bits. For functions of less than 6 variables, the full
487  machine word is returned. (The truth table looks as if the function
488  had 5 variables.) The use of this procedure should be limited to
489  Boolean functions with no more than 16 inputs.]
490 
491  SideEffects []
492 
493  SeeAlso []
494 
495 ***********************************************************************/
496 void Kit_PlaToTruth( char * pSop, int nVars, Vec_Ptr_t * vVars, unsigned * pTemp, unsigned * pTruth )
497 {
498  int v, c, nCubes, fCompl = 0;
499  assert( pSop != NULL );
500  assert( nVars >= 0 );
501  if ( strlen(pSop) % (nVars + 3) != 0 )
502  {
503  printf( "Kit_PlaToTruth(): SOP is represented incorrectly.\n" );
504  return;
505  }
506  // iterate through the cubes
507  Kit_TruthClear( pTruth, nVars );
508  nCubes = strlen(pSop) / (nVars + 3);
509  for ( c = 0; c < nCubes; c++ )
510  {
511  fCompl = (pSop[nVars+1] == '0');
512  Kit_TruthFill( pTemp, nVars );
513  // iterate through the literals of the cube
514  for ( v = 0; v < nVars; v++ )
515  if ( pSop[v] == '1' )
516  Kit_TruthAnd( pTemp, pTemp, (unsigned *)Vec_PtrEntry(vVars, v), nVars );
517  else if ( pSop[v] == '0' )
518  Kit_TruthSharp( pTemp, pTemp, (unsigned *)Vec_PtrEntry(vVars, v), nVars );
519  // add cube to storage
520  Kit_TruthOr( pTruth, pTruth, pTemp, nVars );
521  // go to the next cube
522  pSop += (nVars + 3);
523  }
524  if ( fCompl )
525  Kit_TruthNot( pTruth, pTruth, nVars );
526 }
527 
528 
529 ////////////////////////////////////////////////////////////////////////
530 /// END OF FILE ///
531 ////////////////////////////////////////////////////////////////////////
532 
533 
534 ABC_NAMESPACE_IMPL_END
535 
memset
char * memset()
Kit_PlaStart
char * Kit_PlaStart(void *p, int nCubes, int nVars)
Definition: kitPla.c:211
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Kit_TruthFill
static void Kit_TruthFill(unsigned *pOut, int nVars)
Definition: kit.h:367
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Kit_PlaStoreSop
char * Kit_PlaStoreSop(void *p, char *pSop)
Definition: kitPla.c:317
Vec_StrArray
static char * Vec_StrArray(Vec_Str_t *p)
Definition: vecStr.h:272
Kit_PlaGetVarNum
int Kit_PlaGetVarNum(char *pSop)
Definition: kitPla.c:118
Kit_PlaIsComplement
int Kit_PlaIsComplement(char *pSop)
Definition: kitPla.c:160
Aig_MmFlexEntryFetch
char * Aig_MmFlexEntryFetch(Aig_MmFlex_t *p, int nBytes)
Definition: aigMem.c:366
Vec_StrClear
static void Vec_StrClear(Vec_Str_t *p)
Definition: vecStr.h:519
Kit_PlaIsInv
int Kit_PlaIsInv(char *pSop)
Definition: kitPla.c:98
Kit_TruthIsConst0
static int Kit_TruthIsConst0(unsigned *pIn, int nVars)
Definition: kit.h:315
Kit_PlaIsBuf
int Kit_PlaIsBuf(char *pSop)
Definition: kitPla.c:78
Vec_StrPush
static void Vec_StrPush(Vec_Str_t *p, char Entry)
Definition: vecStr.h:535
Kit_PlaFromTruthNew
char * Kit_PlaFromTruthNew(unsigned *pTruth, int nVars, Vec_Int_t *vCover, Vec_Str_t *vStr)
Definition: kitPla.c:406
lit
int lit
Definition: satVec.h:130
Aig_MmFlex_t_
Definition: aigMem.c:50
Kit_TruthAnd
static void Kit_TruthAnd(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:379
Kit_PlaFromIsop
char * Kit_PlaFromIsop(Vec_Str_t *vStr, int nVars, Vec_Int_t *vCover)
Definition: kitPla.c:366
Kit_TruthIsConst1
static int Kit_TruthIsConst1(unsigned *pIn, int nVars)
Definition: kit.h:323
Vec_StrAppend
static void Vec_StrAppend(Vec_Str_t *p, const char *pString)
Definition: vecStr.h:645
Kit_TruthIsop
int Kit_TruthIsop(unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
FUNCTION DEFINITIONS ///.
Definition: kitIsop.c:55
Kit_PlaIsConst1
int Kit_PlaIsConst1(char *pSop)
Definition: kitPla.c:62
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
Kit_PlaToTruth6
ABC_UINT64_T Kit_PlaToTruth6(char *pSop, int nVars)
Definition: kitPla.c:442
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Kit_TruthNot
static void Kit_TruthNot(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:373
strcpy
char * strcpy()
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Kit_TruthSharp
static void Kit_TruthSharp(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:397
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Kit_PlaCreateFromIsop
char * Kit_PlaCreateFromIsop(void *p, int nVars, Vec_Int_t *vCover)
Definition: kitPla.c:243
Truth
static ABC_NAMESPACE_IMPL_START word Truth[8]
DECLARATIONS ///.
Definition: giaShrink6.c:32
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Kit_PlaToTruth
void Kit_PlaToTruth(char *pSop, int nVars, Vec_Ptr_t *vVars, unsigned *pTemp, unsigned *pTruth)
Definition: kitPla.c:496
Vec_Str_t_
Definition: bblif.c:47
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
Kit_PlaGetCubeNum
int Kit_PlaGetCubeNum(char *pSop)
Definition: kitPla.c:138
Kit_PlaFromTruth
char * Kit_PlaFromTruth(void *p, unsigned *pTruth, int nVars, Vec_Int_t *vCover)
Definition: kitPla.c:337
Kit_PlaToIsop
void Kit_PlaToIsop(char *pSop, Vec_Int_t *vCover)
Definition: kitPla.c:282
assert
#define assert(ex)
Definition: util_old.h:213
strlen
int strlen()
Kit_PlaIsConst0
ABC_NAMESPACE_IMPL_START int Kit_PlaIsConst0(char *pSop)
DECLARATIONS ///.
Definition: kitPla.c:46
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Kit_TruthClear
static void Kit_TruthClear(unsigned *pOut, int nVars)
Definition: kit.h:361
Kit_TruthOr
static void Kit_TruthOr(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:385
Kit_PlaComplement
void Kit_PlaComplement(char *pSop)
Definition: kitPla.c:181