abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
ifTune.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [ifTune.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [FPGA mapping based on priority cuts.]
8 
9  Synopsis [Library tuning.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - November 21, 2006.]
16 
17  Revision [$Id: ifTune.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "if.h"
22 #include "aig/gia/giaAig.h"
23 #include "sat/bsat/satStore.h"
24 #include "sat/cnf/cnf.h"
25 #include "misc/extra/extra.h"
26 #include "bool/kit/kit.h"
27 
28 ABC_NAMESPACE_IMPL_START
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// DECLARATIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 #define IFN_INS 11
35 #define IFN_WRD (IFN_INS > 6 ? 1 << (IFN_INS-6) : 1)
36 #define IFN_PAR 1024
37 
38 // network types
39 typedef enum {
40  IFN_DSD_NONE = 0, // 0: unknown
41  IFN_DSD_CONST0, // 1: constant
42  IFN_DSD_VAR, // 2: variable
43  IFN_DSD_AND, // 3: AND
44  IFN_DSD_XOR, // 4: XOR
45  IFN_DSD_MUX, // 5: MUX
46  IFN_DSD_PRIME // 6: PRIME
47 } Ifn_DsdType_t;
48 
49 // object types
50 static char * Ifn_Symbs[16] = {
51  NULL, // 0: unknown
52  "const", // 1: constant
53  "var", // 2: variable
54  "()", // 3: AND
55  "[]", // 4: XOR
56  "<>", // 5: MUX
57  "{}" // 6: PRIME
58 };
59 
60 typedef struct Ifn_Obj_t_ Ifn_Obj_t;
61 struct Ifn_Obj_t_
62 {
63  unsigned Type : 3; // node type
64  unsigned nFanins : 5; // fanin counter
65  unsigned iFirst : 8; // first parameter
66  unsigned Var : 16; // current variable
67  int Fanins[IFN_INS]; // fanin IDs
68 };
69 struct Ifn_Ntk_t_
70 {
71  // cell structure
72  int nInps; // inputs
73  int nObjs; // objects
74  Ifn_Obj_t Nodes[2*IFN_INS]; // nodes
75  // constraints
76  int pConstr[IFN_INS]; // constraint pairs
77  int nConstr; // number of pairs
78  // user data
79  int nVars; // variables
80  int nWords; // truth table words
81  int nParsVNum; // selection parameters per variable
82  int nParsVIni; // first selection parameter
83  int nPars; // total parameters
84  word * pTruth; // user truth table
85  // matching procedures
86  int Values[IFN_PAR]; // variable values
87  word pTtElems[IFN_INS*IFN_WRD]; // elementary truth tables
88  word pTtObjs[2*IFN_INS*IFN_WRD]; // object truth tables
89 };
90 
91 static inline word * Ifn_ElemTruth( Ifn_Ntk_t * p, int i ) { return p->pTtElems + i * Abc_TtWordNum(p->nInps); }
92 static inline word * Ifn_ObjTruth( Ifn_Ntk_t * p, int i ) { return p->pTtObjs + i * p->nWords; }
93 
94 // variable ordering
95 // - primary inputs [0; p->nInps)
96 // - internal nodes [p->nInps; p->nObjs)
97 // - configuration params [p->nObjs; p->nParsVIni)
98 // - variable selection params [p->nParsVIni; p->pPars)
99 
100 ////////////////////////////////////////////////////////////////////////
101 /// FUNCTION DEFINITIONS ///
102 ////////////////////////////////////////////////////////////////////////
103 
104 /**Function*************************************************************
105 
106  Synopsis [Prepare network to check the given function.]
107 
108  Description []
109 
110  SideEffects []
111 
112  SeeAlso []
113 
114 ***********************************************************************/
115 int Ifn_Prepare( Ifn_Ntk_t * p, word * pTruth, int nVars )
116 {
117  int i, fVerbose = 0;
118  assert( nVars <= p->nInps );
119  p->pTruth = pTruth;
120  p->nVars = nVars;
121  p->nWords = Abc_TtWordNum(nVars);
122  p->nPars = p->nObjs;
123  for ( i = p->nInps; i < p->nObjs; i++ )
124  {
125  if ( p->Nodes[i].Type != IFN_DSD_PRIME )
126  continue;
127  p->Nodes[i].iFirst = p->nPars;
128  p->nPars += (1 << p->Nodes[i].nFanins);
129  if ( fVerbose )
130  printf( "Node %d Start %d Vars %d\n", i, p->Nodes[i].iFirst, (1 << p->Nodes[i].nFanins) );
131  }
132  if ( fVerbose )
133  printf( "Groups start %d\n", p->nPars );
134  p->nParsVIni = p->nPars;
135  p->nParsVNum = Abc_Base2Log(nVars);
136  p->nPars += p->nParsVNum * p->nInps;
137  assert( p->nPars <= IFN_PAR );
138  memset( p->Values, 0xFF, sizeof(int) * p->nPars );
139  return p->nPars;
140 }
141 void Ifn_NtkPrint( Ifn_Ntk_t * p )
142 {
143  int i, k;
144  if ( p == NULL )
145  printf( "String is empty.\n" );
146  if ( p == NULL )
147  return;
148  for ( i = p->nInps; i < p->nObjs; i++ )
149  {
150  printf( "%c=", 'a'+i );
151  printf( "%c", Ifn_Symbs[p->Nodes[i].Type][0] );
152  for ( k = 0; k < (int)p->Nodes[i].nFanins; k++ )
153  printf( "%c", 'a'+p->Nodes[i].Fanins[k] );
154  printf( "%c", Ifn_Symbs[p->Nodes[i].Type][1] );
155  printf( ";" );
156  }
157  printf( "\n" );
158 }
159 int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p )
160 {
161  int i, LutSize = 0;
162  for ( i = p->nInps; i < p->nObjs; i++ )
163  if ( p->Nodes[i].Type == IFN_DSD_PRIME )
164  LutSize = Abc_MaxInt( LutSize, (int)p->Nodes[i].nFanins );
165  return LutSize;
166 }
167 int Ifn_NtkInputNum( Ifn_Ntk_t * p )
168 {
169  return p->nInps;
170 }
171 
172 /**Function*************************************************************
173 
174  Synopsis []
175 
176  Description []
177 
178  SideEffects []
179 
180  SeeAlso []
181 
182 ***********************************************************************/
183 int Ifn_ErrorMessage( const char * format, ... )
184 {
185  char * pMessage;
186  va_list args;
187  va_start( args, format );
188  pMessage = vnsprintf( format, args );
189  va_end( args );
190  printf( "%s", pMessage );
191  ABC_FREE( pMessage );
192  return 0;
193 }
194 int Inf_ManOpenSymb( char * pStr )
195 {
196  if ( pStr[0] == '(' )
197  return 3;
198  if ( pStr[0] == '[' )
199  return 4;
200  if ( pStr[0] == '<' )
201  return 5;
202  if ( pStr[0] == '{' )
203  return 6;
204  return 0;
205 }
206 int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs )
207 {
208  int i, nNodes = 0, Marks[32] = {0}, MaxVar = -1;
209  for ( i = 0; pStr[i]; i++ )
210  {
211  if ( Inf_ManOpenSymb(pStr+i) )
212  nNodes++;
213  if ( pStr[i] == ';' ||
214  pStr[i] == '(' || pStr[i] == ')' ||
215  pStr[i] == '[' || pStr[i] == ']' ||
216  pStr[i] == '<' || pStr[i] == '>' ||
217  pStr[i] == '{' || pStr[i] == '}' )
218  continue;
219  if ( pStr[i] >= 'A' && pStr[i] <= 'Z' )
220  continue;
221  if ( pStr[i] >= 'a' && pStr[i] <= 'z' )
222  {
223  MaxVar = Abc_MaxInt( MaxVar, (int)(pStr[i] - 'a') );
224  Marks[pStr[i] - 'a'] = 1;
225  continue;
226  }
227  return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] );
228  }
229  for ( i = 0; i <= MaxVar; i++ )
230  if ( Marks[i] == 0 )
231  return Ifn_ErrorMessage( "String \"%s\" has no symbol \'%c\'.\n", pStr, 'a' + i );
232  *pnInps = MaxVar + 1;
233  *pnObjs = MaxVar + 1 + nNodes;
234  return 1;
235 }
236 static inline char * Ifn_NtkParseFindClosingParanthesis( char * pStr, char Open, char Close )
237 {
238  int Counter = 0;
239  assert( *pStr == Open );
240  for ( ; *pStr; pStr++ )
241  {
242  if ( *pStr == Open )
243  Counter++;
244  if ( *pStr == Close )
245  Counter--;
246  if ( Counter == 0 )
247  return pStr;
248  }
249  return NULL;
250 }
251 int Ifn_NtkParseInt_rec( char * pStr, Ifn_Ntk_t * p, char ** ppFinal, int * piNode )
252 {
253  Ifn_Obj_t * pObj;
254  int nFanins = 0, pFanins[IFN_INS];
255  int Type = Inf_ManOpenSymb( pStr );
256  char * pLim = Ifn_NtkParseFindClosingParanthesis( pStr++, Ifn_Symbs[Type][0], Ifn_Symbs[Type][1] );
257  *ppFinal = NULL;
258  if ( pLim == NULL )
259  return Ifn_ErrorMessage( "For symbol \'%c\' cannot find matching symbol \'%c\'.\n", Ifn_Symbs[Type][0], Ifn_Symbs[Type][1] );
260  while ( pStr < pLim )
261  {
262  assert( nFanins < IFN_INS );
263  if ( pStr[0] >= 'a' && pStr[0] <= 'z' )
264  pFanins[nFanins++] = pStr[0] - 'a', pStr++;
265  else if ( Inf_ManOpenSymb(pStr) )
266  {
267  if ( !Ifn_NtkParseInt_rec( pStr, p, &pStr, piNode ) )
268  return 0;
269  pFanins[nFanins++] = *piNode - 1;
270  }
271  else
272  return Ifn_ErrorMessage( "Substring \"%s\" contans unrecognized symbol \'%c\'.\n", pStr, pStr[0] );
273  }
274  assert( pStr == pLim );
275  pObj = p->Nodes + (*piNode)++;
276  pObj->Type = Type;
277  assert( pObj->nFanins == 0 );
278  pObj->nFanins = nFanins;
279  memcpy( pObj->Fanins, pFanins, sizeof(int) * nFanins );
280  *ppFinal = pLim + 1;
281  if ( Type == IFN_DSD_MUX && nFanins != 3 )
282  return Ifn_ErrorMessage( "MUX should have exactly three fanins.\n" );
283  return 1;
284 }
285 int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p )
286 {
287  char * pFinal; int iNode;
288  if ( !Ifn_ManStrCheck(pStr, &p->nInps, &p->nObjs) )
289  return 0;
290  if ( p->nInps > IFN_INS )
291  return Ifn_ErrorMessage( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS );
292  assert( p->nInps > 1 && p->nInps < p->nObjs && p->nInps <= IFN_INS && p->nObjs < 2*IFN_INS );
293  if ( !Inf_ManOpenSymb(pStr) )
294  return Ifn_ErrorMessage( "The first symbol should be one of the symbols: (, [, <, {.\n" );
295  iNode = p->nInps;
296  if ( !Ifn_NtkParseInt_rec( pStr, p, &pFinal, &iNode ) )
297  return 0;
298  if ( pFinal[0] && pFinal[0] != ';' )
299  return Ifn_ErrorMessage( "The last symbol should be \';\'.\n" );
300  if ( iNode != p->nObjs )
301  return Ifn_ErrorMessage( "Mismatch in the number of nodes.\n" );
302  return 1;
303 }
304 
305 /**Function*************************************************************
306 
307  Synopsis []
308 
309  Description []
310 
311  SideEffects []
312 
313  SeeAlso []
314 
315 ***********************************************************************/
316 int Ifn_ManStrType2( char * pStr )
317 {
318  int i;
319  for ( i = 0; pStr[i]; i++ )
320  if ( pStr[i] == '=' )
321  return 1;
322  return 0;
323 }
324 int Ifn_ManStrCheck2( char * pStr, int * pnInps, int * pnObjs )
325 {
326  int i, Marks[32] = {0}, MaxVar = 0, MaxDef = 0;
327  for ( i = 0; pStr[i]; i++ )
328  {
329  if ( pStr[i] == '=' || pStr[i] == ';' ||
330  pStr[i] == '(' || pStr[i] == ')' ||
331  pStr[i] == '[' || pStr[i] == ']' ||
332  pStr[i] == '<' || pStr[i] == '>' ||
333  pStr[i] == '{' || pStr[i] == '}' )
334  continue;
335  if ( pStr[i] >= 'A' && pStr[i] <= 'Z' )
336  continue;
337  if ( pStr[i] >= 'a' && pStr[i] <= 'z' )
338  {
339  if ( pStr[i+1] == '=' )
340  Marks[pStr[i] - 'a'] = 2, MaxDef = Abc_MaxInt(MaxDef, pStr[i] - 'a');
341  continue;
342  }
343  return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] );
344  }
345  for ( i = 0; pStr[i]; i++ )
346  {
347  if ( pStr[i] == '=' || pStr[i] == ';' ||
348  pStr[i] == '(' || pStr[i] == ')' ||
349  pStr[i] == '[' || pStr[i] == ']' ||
350  pStr[i] == '<' || pStr[i] == '>' ||
351  pStr[i] == '{' || pStr[i] == '}' )
352  continue;
353  if ( pStr[i] >= 'A' && pStr[i] <= 'Z' )
354  continue;
355  if ( pStr[i] >= 'a' && pStr[i] <= 'z' )
356  {
357  if ( pStr[i+1] != '=' && Marks[pStr[i] - 'a'] != 2 )
358  Marks[pStr[i] - 'a'] = 1, MaxVar = Abc_MaxInt(MaxVar, pStr[i] - 'a');
359  continue;
360  }
361  return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] );
362  }
363  MaxVar++;
364  MaxDef++;
365  for ( i = 0; i < MaxDef; i++ )
366  if ( Marks[i] == 0 )
367  return Ifn_ErrorMessage( "String \"%s\" has no symbol \'%c\'.\n", pStr, 'a' + i );
368  for ( i = 0; i < MaxVar; i++ )
369  if ( Marks[i] == 2 )
370  return Ifn_ErrorMessage( "String \"%s\" has definition of input variable \'%c\'.\n", pStr, 'a' + i );
371  for ( i = MaxVar; i < MaxDef; i++ )
372  if ( Marks[i] == 1 )
373  return Ifn_ErrorMessage( "String \"%s\" has no definition for internal variable \'%c\'.\n", pStr, 'a' + i );
374  *pnInps = MaxVar;
375  *pnObjs = MaxDef;
376  return 1;
377 }
378 int Ifn_NtkParseInt2( char * pStr, Ifn_Ntk_t * p )
379 {
380  int i, k, n, f, nFans, iFan;
381  if ( !Ifn_ManStrCheck2(pStr, &p->nInps, &p->nObjs) )
382  return 0;
383  if ( p->nInps > IFN_INS )
384  return Ifn_ErrorMessage( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS );
385  assert( p->nInps > 1 && p->nInps < p->nObjs && p->nInps <= IFN_INS && p->nObjs < 2*IFN_INS );
386  for ( i = p->nInps; i < p->nObjs; i++ )
387  {
388  char Next = 0;
389  for ( k = 0; pStr[k]; k++ )
390  if ( pStr[k] == 'a' + i && pStr[k+1] == '=' )
391  break;
392  if ( pStr[k] == 0 )
393  return Ifn_ErrorMessage( "Cannot find definition of signal \'%c\'.\n", 'a' + i );
394  if ( pStr[k+2] == '(' )
395  p->Nodes[i].Type = IFN_DSD_AND, Next = ')';
396  else if ( pStr[k+2] == '[' )
397  p->Nodes[i].Type = IFN_DSD_XOR, Next = ']';
398  else if ( pStr[k+2] == '<' )
399  p->Nodes[i].Type = IFN_DSD_MUX, Next = '>';
400  else if ( pStr[k+2] == '{' )
401  p->Nodes[i].Type = IFN_DSD_PRIME, Next = '}';
402  else
403  return Ifn_ErrorMessage( "Cannot find openning operation symbol in the defition of of signal \'%c\'.\n", 'a' + i );
404  for ( n = k + 3; pStr[n]; n++ )
405  if ( pStr[n] == Next )
406  break;
407  if ( pStr[n] == 0 )
408  return Ifn_ErrorMessage( "Cannot find closing operation symbol in the defition of of signal \'%c\'.\n", 'a' + i );
409  nFans = n - k - 3;
410  if ( nFans < 1 || nFans > 8 )
411  return Ifn_ErrorMessage( "Cannot find matching operation symbol in the defition of of signal \'%c\'.\n", 'a' + i );
412  for ( f = 0; f < nFans; f++ )
413  {
414  iFan = pStr[k + 3 + f] - 'a';
415  if ( iFan < 0 || iFan >= i )
416  return Ifn_ErrorMessage( "Fanin number %d is signal %d is out of range.\n", f, 'a' + i );
417  p->Nodes[i].Fanins[f] = iFan;
418  }
419  p->Nodes[i].nFanins = nFans;
420  }
421  return 1;
422 }
423 void Ifn_NtkParseConstraints( char * pStr, Ifn_Ntk_t * p )
424 {
425  int i, k;
426  // parse constraints
427  p->nConstr = 0;
428  for ( i = 0; i < p->nInps; i++ )
429  for ( k = 0; pStr[k]; k++ )
430  if ( pStr[k] == 'A' + i && pStr[k-1] == ';' )
431  {
432  p->pConstr[p->nConstr++] = ((int)(pStr[k] - 'A') << 16) | (int)(pStr[k+1] - 'A');
433 // printf( "Added constraint (%c < %c)\n", pStr[k], pStr[k+1] );
434  }
435 // if ( p->nConstr )
436 // printf( "Total constraints = %d\n", p->nConstr );
437 }
438 
439 Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
440 {
441  Ifn_Ntk_t * p = ABC_CALLOC( Ifn_Ntk_t, 1 );
442  if ( Ifn_ManStrType2(pStr) )
443  {
444  if ( !Ifn_NtkParseInt2( pStr, p ) )
445  {
446  ABC_FREE( p );
447  return NULL;
448  }
449  }
450  else
451  {
452  if ( !Ifn_NtkParseInt( pStr, p ) )
453  {
454  ABC_FREE( p );
455  return NULL;
456  }
457  }
458  Ifn_NtkParseConstraints( pStr, p );
459  Abc_TtElemInit2( p->pTtElems, p->nInps );
460 // printf( "Finished parsing: " ); Ifn_NtkPrint(p);
461  return p;
462 }
463 
464 
465 
466 /**Function*************************************************************
467 
468  Synopsis [Derive AIG.]
469 
470  Description []
471 
472  SideEffects []
473 
474  SeeAlso []
475 
476 ***********************************************************************/
477 Gia_Man_t * Ifn_ManStrFindModel( Ifn_Ntk_t * p )
478 {
479  Gia_Man_t * pNew, * pTemp;
480  int i, k, iLit, * pVarMap = ABC_FALLOC( int, p->nParsVIni );
481  pNew = Gia_ManStart( 1000 );
482  pNew->pName = Abc_UtilStrsav( "model" );
483  Gia_ManHashStart( pNew );
484  for ( i = 0; i < p->nInps; i++ )
485  pVarMap[i] = Gia_ManAppendCi(pNew);
486  for ( i = p->nObjs; i < p->nParsVIni; i++ )
487  pVarMap[i] = Gia_ManAppendCi(pNew);
488  for ( i = p->nInps; i < p->nObjs; i++ )
489  {
490  int Type = p->Nodes[i].Type;
491  int nFans = p->Nodes[i].nFanins;
492  int * pFans = p->Nodes[i].Fanins;
493  int iFanin = p->Nodes[i].iFirst;
494  if ( Type == IFN_DSD_AND )
495  {
496  iLit = 1;
497  for ( k = 0; k < nFans; k++ )
498  iLit = Gia_ManHashAnd( pNew, iLit, pVarMap[pFans[k]] );
499  pVarMap[i] = iLit;
500  }
501  else if ( Type == IFN_DSD_XOR )
502  {
503  iLit = 0;
504  for ( k = 0; k < nFans; k++ )
505  iLit = Gia_ManHashXor( pNew, iLit, pVarMap[pFans[k]] );
506  pVarMap[i] = iLit;
507  }
508  else if ( Type == IFN_DSD_MUX )
509  {
510  assert( nFans == 3 );
511  pVarMap[i] = Gia_ManHashMux( pNew, pVarMap[pFans[0]], pVarMap[pFans[1]], pVarMap[pFans[2]] );
512  }
513  else if ( Type == IFN_DSD_PRIME )
514  {
515  int n, Step, pVarsData[256];
516  int nMints = (1 << nFans);
517  assert( nFans >= 1 && nFans <= 8 );
518  for ( k = 0; k < nMints; k++ )
519  pVarsData[k] = pVarMap[iFanin + k];
520  for ( Step = 1, k = 0; k < nFans; k++, Step <<= 1 )
521  for ( n = 0; n < nMints; n += Step << 1 )
522  pVarsData[n] = Gia_ManHashMux( pNew, pVarMap[pFans[k]], pVarsData[n+Step], pVarsData[n] );
523  assert( Step == nMints );
524  pVarMap[i] = pVarsData[0];
525  }
526  else assert( 0 );
527  }
528  Gia_ManAppendCo( pNew, pVarMap[p->nObjs-1] );
529  ABC_FREE( pVarMap );
530  pNew = Gia_ManCleanup( pTemp = pNew );
531  Gia_ManStop( pTemp );
532  assert( Gia_ManPiNum(pNew) == p->nParsVIni - (p->nObjs - p->nInps) );
533  assert( Gia_ManPoNum(pNew) == 1 );
534  return pNew;
535 }
536 // compute cofactors w.r.t. the first nIns variables
537 Gia_Man_t * Ifn_ManStrFindCofactors( int nIns, Gia_Man_t * p )
538 {
539  Gia_Man_t * pNew, * pTemp;
540  Gia_Obj_t * pObj;
541  int i, m, nMints = 1 << nIns;
542  pNew = Gia_ManStart( Gia_ManObjNum(p) );
543  pNew->pName = Abc_UtilStrsav( p->pName );
544  Gia_ManHashAlloc( pNew );
545  Gia_ManConst0(p)->Value = 0;
546  Gia_ManForEachCi( p, pObj, i )
547  if ( i >= nIns )
548  pObj->Value = Gia_ManAppendCi( pNew );
549  for ( m = 0; m < nMints; m++ )
550  {
551  Gia_ManForEachCi( p, pObj, i )
552  if ( i < nIns )
553  pObj->Value = ((m >> i) & 1);
554  Gia_ManForEachAnd( p, pObj, i )
555  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
556  Gia_ManForEachPo( p, pObj, i )
557  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
558  }
559  pNew = Gia_ManCleanup( pTemp = pNew );
560  Gia_ManStop( pTemp );
561  return pNew;
562 }
563 
564 /**Function*************************************************************
565 
566  Synopsis [Derive SAT solver.]
567 
568  Description []
569 
570  SideEffects []
571 
572  SeeAlso []
573 
574 ***********************************************************************/
575 static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
576 {
577  Cnf_Dat_t * pCnf;
578  Aig_Man_t * pAig = Gia_ManToAigSimple( p );
579  pAig->nRegs = 0;
580  pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
581  Aig_ManStop( pAig );
582  return pCnf;
583 }
584 sat_solver * Ifn_ManStrFindSolver( Gia_Man_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars )
585 {
586  sat_solver * pSat;
587  Gia_Obj_t * pObj;
588  Cnf_Dat_t * pCnf;
589  int i;
590  pCnf = Cnf_DeriveGiaRemapped( p );
591  // start the SAT solver
592  pSat = sat_solver_new();
593  sat_solver_setnvars( pSat, pCnf->nVars );
594  // add timeframe clauses
595  for ( i = 0; i < pCnf->nClauses; i++ )
596  if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
597  assert( 0 );
598  // inputs/outputs
599  *pvPiVars = Vec_IntAlloc( Gia_ManPiNum(p) );
600  Gia_ManForEachCi( p, pObj, i )
601  Vec_IntPush( *pvPiVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] );
602  *pvPoVars = Vec_IntAlloc( Gia_ManPoNum(p) );
603  Gia_ManForEachCo( p, pObj, i )
604  Vec_IntPush( *pvPoVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] );
605  Cnf_DataFree( pCnf );
606  return pSat;
607 }
608 sat_solver * Ifn_ManSatBuild( Ifn_Ntk_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars )
609 {
610  Gia_Man_t * p1, * p2;
611  sat_solver * pSat = NULL;
612  *pvPiVars = *pvPoVars = NULL;
613  p1 = Ifn_ManStrFindModel( p );
614 // Gia_AigerWrite( p1, "satbuild.aig", 0, 0 );
615  p2 = Ifn_ManStrFindCofactors( p->nInps, p1 );
616  Gia_ManStop( p1 );
617 // Gia_AigerWrite( p2, "satbuild2.aig", 0, 0 );
618  pSat = Ifn_ManStrFindSolver( p2, pvPiVars, pvPoVars );
619  Gia_ManStop( p2 );
620  return pSat;
621 }
622 void * If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars, Ifn_Ntk_t ** ppNtk )
623 {
624  Ifn_Ntk_t * p = Ifn_NtkParse( pStr );
625  Ifn_Prepare( p, NULL, p->nInps );
626  *ppNtk = p;
627  if ( p == NULL )
628  return NULL;
629 // Ifn_NtkPrint( p );
630  return Ifn_ManSatBuild( p, pvPiVars, pvPoVars );
631 }
632 
633 /**Function*************************************************************
634 
635  Synopsis []
636 
637  Description []
638 
639  SideEffects []
640 
641  SeeAlso []
642 
643 ***********************************************************************/
644 void Ifn_ManSatPrintPerm( char * pPerms, int nVars )
645 {
646  int i;
647  for ( i = 0; i < nVars; i++ )
648  printf( "%c", 'a' + pPerms[i] );
649  printf( "\n" );
650 }
651 int Ifn_ManSatCheckOne( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, int * pPerm, int nInps, Vec_Int_t * vLits )
652 {
653  int v, Value, m, mNew, nMints = (1 << nVars); // (1 << nInps);
654  assert( (1 << nInps) == Vec_IntSize(vPoVars) );
655  assert( nVars <= nInps );
656  // remap minterms
657  Vec_IntFill( vLits, Vec_IntSize(vPoVars), -1 );
658  for ( m = 0; m < nMints; m++ )
659  {
660  mNew = 0;
661  for ( v = 0; v < nInps; v++ )
662  {
663  assert( pPerm[v] < nVars );
664  if ( ((m >> pPerm[v]) & 1) )
665  mNew |= (1 << v);
666  }
667  assert( Vec_IntEntry(vLits, mNew) == -1 );
668  Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) );
669  }
670  // find assumptions
671  v = 0;
672  Vec_IntForEachEntry( vLits, Value, m )
673  if ( Value >= 0 )
674  Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(Vec_IntEntry(vPoVars, m), !Value) );
675  Vec_IntShrink( vLits, v );
676  // run SAT solver
677  Value = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
678  return (int)(Value == l_True);
679 }
680 void Ifn_ManSatDeriveOne( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vValues )
681 {
682  int i, iVar;
683  Vec_IntClear( vValues );
684  Vec_IntForEachEntry( vPiVars, iVar, i )
685  Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
686 }
687 int If_ManSatFindCofigBits( void * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, word * pTruth, int nVars, word Perm, int nInps, Vec_Int_t * vValues )
688 {
689  // extract permutation
690  int RetValue, i, pPerm[IF_MAX_FUNC_LUTSIZE];
691  assert( nInps <= IF_MAX_FUNC_LUTSIZE );
692  for ( i = 0; i < nInps; i++ )
693  {
694  pPerm[i] = Abc_TtGetHex( &Perm, i );
695  assert( pPerm[i] < nVars );
696  }
697  // perform SAT check
698  RetValue = Ifn_ManSatCheckOne( (sat_solver *)pSat, vPoVars, pTruth, nVars, pPerm, nInps, vValues );
699  Vec_IntClear( vValues );
700  if ( RetValue == 0 )
701  return 0;
702  Ifn_ManSatDeriveOne( pSat, vPiVars, vValues );
703  return 1;
704 }
705 int Ifn_ManSatFindCofigBitsTest( Ifn_Ntk_t * p, word * pTruth, int nVars, word Perm )
706 {
707  Vec_Int_t * vValues = Vec_IntAlloc( 100 );
708  Vec_Int_t * vPiVars, * vPoVars;
709  sat_solver * pSat = Ifn_ManSatBuild( p, &vPiVars, &vPoVars );
710  int RetValue = If_ManSatFindCofigBits( pSat, vPiVars, vPoVars, pTruth, nVars, Perm, p->nInps, vValues );
711  Vec_IntPrint( vValues );
712  // cleanup
713  sat_solver_delete( pSat );
714  Vec_IntFreeP( &vPiVars );
715  Vec_IntFreeP( &vPoVars );
716  Vec_IntFreeP( &vValues );
717  return RetValue;
718 }
719 
720 /**Function*************************************************************
721 
722  Synopsis [Derive GIA using programmable bits.]
723 
724  Description []
725 
726  SideEffects []
727 
728  SeeAlso []
729 
730 ***********************************************************************/
731 int If_ManSatDeriveGiaFromBits( void * pGia, Ifn_Ntk_t * p, Vec_Int_t * vValues, Vec_Int_t * vCover )
732 {
733  Gia_Man_t * pNew = (Gia_Man_t *)pGia;
734  int i, Id, k, iLit, iVar = 0, nVarsNew, pVarMap[1000];
735  assert( Gia_ManCiNum(pNew) == p->nInps && p->nParsVIni < 1000 );
736  Gia_ManForEachCiId( pNew, Id, i )
737  pVarMap[i] = Abc_Var2Lit( Id, 0 );
738  for ( i = p->nInps; i < p->nObjs; i++ )
739  {
740  int Type = p->Nodes[i].Type;
741  int nFans = p->Nodes[i].nFanins;
742  int * pFans = p->Nodes[i].Fanins;
743  //int iFanin = p->Nodes[i].iFirst;
744  assert( nFans <= 6 );
745  if ( Type == IFN_DSD_AND )
746  {
747  iLit = 1;
748  for ( k = 0; k < nFans; k++ )
749  iLit = Gia_ManHashAnd( pNew, iLit, pVarMap[pFans[k]] );
750  pVarMap[i] = iLit;
751  }
752  else if ( Type == IFN_DSD_XOR )
753  {
754  iLit = 0;
755  for ( k = 0; k < nFans; k++ )
756  iLit = Gia_ManHashXor( pNew, iLit, pVarMap[pFans[k]] );
757  pVarMap[i] = iLit;
758  }
759  else if ( Type == IFN_DSD_MUX )
760  {
761  assert( nFans == 3 );
762  pVarMap[i] = Gia_ManHashMux( pNew, pVarMap[pFans[0]], pVarMap[pFans[1]], pVarMap[pFans[2]] );
763  }
764  else if ( Type == IFN_DSD_PRIME )
765  {
766  int pFaninLits[16];
767  // collect truth table
768  word uTruth = 0;
769  int nMints = (1 << nFans);
770  for ( k = 0; k < nMints; k++ )
771  if ( Vec_IntEntry( vValues, iVar++ ) )
772  uTruth |= ((word)1 << k);
773  uTruth = Abc_Tt6Stretch( uTruth, nFans );
774  // collect function
775  for ( k = 0; k < nFans; k++ )
776  pFaninLits[k] = pVarMap[pFans[k]];
777  // implement the function
778  nVarsNew = Abc_TtMinBase( &uTruth, pFaninLits, nFans, 6 );
779  if ( nVarsNew == 0 )
780  pVarMap[i] = (int)(uTruth & 1);
781  else
782  {
783  extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
784  Vec_Int_t Leaves = { nVarsNew, nVarsNew, pFaninLits };
785  pVarMap[i] = Kit_TruthToGia( pNew, (unsigned *)&uTruth, nVarsNew, vCover, &Leaves, 1 ); // hashing enabled!!!
786  }
787  }
788  else assert( 0 );
789  }
790  assert( iVar == Vec_IntSize(vValues) );
791  return pVarMap[p->nObjs - 1];
792 }
793 
794 /**Function*************************************************************
795 
796  Synopsis [Derive truth table given the configulation values.]
797 
798  Description []
799 
800  SideEffects []
801 
802  SeeAlso []
803 
804 ***********************************************************************/
805 word * Ifn_NtkDeriveTruth( Ifn_Ntk_t * p, int * pValues )
806 {
807  int i, v, f, iVar, iStart;
808  // elementary variables
809  for ( i = 0; i < p->nInps; i++ )
810  {
811  // find variable
812  iStart = p->nParsVIni + i * p->nParsVNum;
813  for ( v = iVar = 0; v < p->nParsVNum; v++ )
814  if ( p->Values[iStart+v] )
815  iVar += (1 << v);
816  // assign variable
817  Abc_TtCopy( Ifn_ObjTruth(p, i), Ifn_ElemTruth(p, iVar), p->nWords, 0 );
818  }
819  // internal variables
820  for ( i = p->nInps; i < p->nObjs; i++ )
821  {
822  int nFans = p->Nodes[i].nFanins;
823  int * pFans = p->Nodes[i].Fanins;
824  word * pTruth = Ifn_ObjTruth( p, i );
825  if ( p->Nodes[i].Type == IFN_DSD_AND )
826  {
827  Abc_TtFill( pTruth, p->nWords );
828  for ( f = 0; f < nFans; f++ )
829  Abc_TtAnd( pTruth, pTruth, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 );
830  }
831  else if ( p->Nodes[i].Type == IFN_DSD_XOR )
832  {
833  Abc_TtClear( pTruth, p->nWords );
834  for ( f = 0; f < nFans; f++ )
835  Abc_TtXor( pTruth, pTruth, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 );
836  }
837  else if ( p->Nodes[i].Type == IFN_DSD_MUX )
838  {
839  assert( nFans == 3 );
840  Abc_TtMux( pTruth, Ifn_ObjTruth(p, pFans[0]), Ifn_ObjTruth(p, pFans[1]), Ifn_ObjTruth(p, pFans[2]), p->nWords );
841  }
842  else if ( p->Nodes[i].Type == IFN_DSD_PRIME )
843  {
844  int nValues = (1 << nFans);
845  word * pTemp = Ifn_ObjTruth(p, p->nObjs);
846  Abc_TtClear( pTruth, p->nWords );
847  for ( v = 0; v < nValues; v++ )
848  {
849  if ( pValues[p->Nodes[i].iFirst + v] == 0 )
850  continue;
851  Abc_TtFill( pTemp, p->nWords );
852  for ( f = 0; f < nFans; f++ )
853  if ( (v >> f) & 1 )
854  Abc_TtAnd( pTemp, pTemp, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 );
855  else
856  Abc_TtSharp( pTemp, pTemp, Ifn_ObjTruth(p, pFans[f]), p->nWords );
857  Abc_TtOr( pTruth, pTruth, pTemp, p->nWords );
858  }
859  }
860  else assert( 0 );
861 //Dau_DsdPrintFromTruth( pTruth, p->nVars );
862  }
863  return Ifn_ObjTruth(p, p->nObjs-1);
864 }
865 
866 /**Function*************************************************************
867 
868  Synopsis [Compute more or equal]
869 
870  Description []
871 
872  SideEffects []
873 
874  SeeAlso []
875 
876 ***********************************************************************/
877 void Ifn_TtComparisonConstr( word * pTruth, int nVars, int fMore, int fEqual )
878 {
879  word Cond[4], Equa[4], Temp[4];
880  word s_TtElems[8][4] = {
881  { ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA) },
882  { ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC) },
883  { ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0) },
884  { ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00) },
885  { ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000) },
886  { ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000) },
887  { ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF) },
888  { ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF) }
889  };
890  int i, nWords = Abc_TtWordNum(2*nVars);
891  assert( nVars > 0 && nVars <= 4 );
892  Abc_TtClear( pTruth, nWords );
893  Abc_TtFill( Equa, nWords );
894  for ( i = nVars - 1; i >= 0; i-- )
895  {
896  if ( fMore )
897  Abc_TtSharp( Cond, s_TtElems[2*i+1], s_TtElems[2*i+0], nWords );
898  else
899  Abc_TtSharp( Cond, s_TtElems[2*i+0], s_TtElems[2*i+1], nWords );
900  Abc_TtAnd( Temp, Equa, Cond, nWords, 0 );
901  Abc_TtOr( pTruth, pTruth, Temp, nWords );
902  Abc_TtXor( Temp, s_TtElems[2*i+0], s_TtElems[2*i+1], nWords, 1 );
903  Abc_TtAnd( Equa, Equa, Temp, nWords, 0 );
904  }
905  if ( fEqual )
906  Abc_TtNot( pTruth, nWords );
907 }
908 
909 /**Function*************************************************************
910 
911  Synopsis [Adds parameter constraints.]
912 
913  Description []
914 
915  SideEffects []
916 
917  SeeAlso []
918 
919 ***********************************************************************/
920 int Ifn_AddClause( sat_solver * pSat, int * pBeg, int * pEnd )
921 {
922  int fVerbose = 0;
923  int RetValue = sat_solver_addclause( pSat, pBeg, pEnd );
924  if ( fVerbose )
925  {
926  for ( ; pBeg < pEnd; pBeg++ )
927  printf( "%c%d ", Abc_LitIsCompl(*pBeg) ? '-':'+', Abc_Lit2Var(*pBeg) );
928  printf( "\n" );
929  }
930  return RetValue;
931 }
932 void Ifn_NtkAddConstrOne( sat_solver * pSat, Vec_Int_t * vCover, int * pVars, int nVars )
933 {
934  int RetValue, k, c, Cube, Literal, nLits, pLits[IFN_INS];
935  Vec_IntForEachEntry( vCover, Cube, c )
936  {
937  nLits = 0;
938  for ( k = 0; k < nVars; k++ )
939  {
940  Literal = 3 & (Cube >> (k << 1));
941  if ( Literal == 1 ) // '0' -> pos lit
942  pLits[nLits++] = Abc_Var2Lit(pVars[k], 0);
943  else if ( Literal == 2 ) // '1' -> neg lit
944  pLits[nLits++] = Abc_Var2Lit(pVars[k], 1);
945  else if ( Literal != 0 )
946  assert( 0 );
947  }
948  RetValue = Ifn_AddClause( pSat, pLits, pLits + nLits );
949  assert( RetValue );
950  }
951 }
952 void Ifn_NtkAddConstraints( Ifn_Ntk_t * p, sat_solver * pSat )
953 {
954  int fAddConstr = 1;
955  Vec_Int_t * vCover = Vec_IntAlloc( 0 );
956  word uTruth = Abc_Tt6Stretch( ~Abc_Tt6Mask(p->nVars), p->nParsVNum );
957  assert( p->nParsVNum <= 4 );
958  if ( uTruth )
959  {
960  int i, k, pVars[IFN_INS];
961  int RetValue = Kit_TruthIsop( (unsigned *)&uTruth, p->nParsVNum, vCover, 0 );
962  assert( RetValue == 0 );
963 // Dau_DsdPrintFromTruth( &uTruth, p->nParsVNum );
964  // add capacity constraints
965  for ( i = 0; i < p->nInps; i++ )
966  {
967  for ( k = 0; k < p->nParsVNum; k++ )
968  pVars[k] = p->nParsVIni + i * p->nParsVNum + k;
969  Ifn_NtkAddConstrOne( pSat, vCover, pVars, p->nParsVNum );
970  }
971  }
972  // ordering constraints
973  if ( fAddConstr && p->nConstr )
974  {
975  word pTruth[4];
976  int i, k, RetValue, pVars[2*IFN_INS];
977  int fForceDiff = (p->nVars == p->nInps);
978  Ifn_TtComparisonConstr( pTruth, p->nParsVNum, fForceDiff, fForceDiff );
979  RetValue = Kit_TruthIsop( (unsigned *)pTruth, 2*p->nParsVNum, vCover, 0 );
980  assert( RetValue == 0 );
981 // Kit_TruthIsopPrintCover( vCover, 2*p->nParsVNum, 0 );
982  for ( i = 0; i < p->nConstr; i++ )
983  {
984  int iVar1 = p->pConstr[i] >> 16;
985  int iVar2 = p->pConstr[i] & 0xFFFF;
986  for ( k = 0; k < p->nParsVNum; k++ )
987  {
988  pVars[2*k+0] = p->nParsVIni + iVar1 * p->nParsVNum + k;
989  pVars[2*k+1] = p->nParsVIni + iVar2 * p->nParsVNum + k;
990  }
991  Ifn_NtkAddConstrOne( pSat, vCover, pVars, 2*p->nParsVNum );
992 // printf( "added constraint with %d clauses for %d and %d\n", Vec_IntSize(vCover), iVar1, iVar2 );
993  }
994  }
995  Vec_IntFree( vCover );
996 }
997 
998 /**Function*************************************************************
999 
1000  Synopsis [Derive clauses given variable assignment.]
1001 
1002  Description []
1003 
1004  SideEffects []
1005 
1006  SeeAlso []
1007 
1008 ***********************************************************************/
1009 int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat )
1010 {
1011  int i, f, v, nLits, pLits[IFN_INS+2], pLits2[IFN_INS+2];
1012  // assign new variables
1013  int nSatVars = sat_solver_nvars(pSat);
1014  for ( i = 0; i < p->nObjs-1; i++ )
1015  p->Nodes[i].Var = nSatVars++;
1016  p->Nodes[p->nObjs-1].Var = 0xFFFF;
1017  sat_solver_setnvars( pSat, nSatVars );
1018  // verify variable values
1019  for ( i = 0; i < p->nVars; i++ )
1020  assert( pValues[i] != -1 );
1021  for ( i = p->nVars; i < p->nObjs-1; i++ )
1022  assert( pValues[i] == -1 );
1023  assert( pValues[p->nObjs-1] != -1 );
1024  // internal variables
1025 //printf( "\n" );
1026  for ( i = 0; i < p->nInps; i++ )
1027  {
1028  int iParStart = p->nParsVIni + i * p->nParsVNum;
1029  for ( v = 0; v < p->nVars; v++ )
1030  {
1031  // add output literal
1032  pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, pValues[v]==0 );
1033  // add clause literals
1034  for ( f = 0; f < p->nParsVNum; f++ )
1035  pLits[f+1] = Abc_Var2Lit( iParStart + f, (v >> f) & 1 );
1036  if ( !Ifn_AddClause( pSat, pLits, pLits+p->nParsVNum+1 ) )
1037  return 0;
1038  }
1039  }
1040 //printf( "\n" );
1041  for ( i = p->nInps; i < p->nObjs; i++ )
1042  {
1043  int nFans = p->Nodes[i].nFanins;
1044  int * pFans = p->Nodes[i].Fanins;
1045  if ( p->Nodes[i].Type == IFN_DSD_AND )
1046  {
1047  nLits = 0;
1048  pLits[nLits++] = Abc_Var2Lit( p->Nodes[i].Var, 0 );
1049  for ( f = 0; f < nFans; f++ )
1050  {
1051  pLits[nLits++] = Abc_Var2Lit( p->Nodes[pFans[f]].Var, 1 );
1052  // add small clause
1053  pLits2[0] = Abc_Var2Lit( p->Nodes[i].Var, 1 );
1054  pLits2[1] = Abc_Var2Lit( p->Nodes[pFans[f]].Var, 0 );
1055  if ( !Ifn_AddClause( pSat, pLits2, pLits2 + 2 ) )
1056  return 0;
1057  }
1058  // add big clause
1059  if ( !Ifn_AddClause( pSat, pLits, pLits + nLits ) )
1060  return 0;
1061  }
1062  else if ( p->Nodes[i].Type == IFN_DSD_XOR )
1063  {
1064  int m, nMints = (1 << (nFans+1));
1065  for ( m = 0; m < nMints; m++ )
1066  {
1067  // skip even
1068  int Count = 0;
1069  for ( v = 0; v <= nFans; v++ )
1070  Count += ((m >> v) & 1);
1071  if ( (Count & 1) == 0 )
1072  continue;
1073  // generate minterm
1074  pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, (m >> nFans) & 1 );
1075  for ( v = 0; v < nFans; v++ )
1076  pLits[v+1] = Abc_Var2Lit( p->Nodes[pFans[v]].Var, (m >> v) & 1 );
1077  if ( !Ifn_AddClause( pSat, pLits, pLits + nFans + 1 ) )
1078  return 0;
1079  }
1080  }
1081  else if ( p->Nodes[i].Type == IFN_DSD_MUX )
1082  {
1083  pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 0 );
1084  pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 1 ); // ctrl
1085  pLits[2] = Abc_Var2Lit( p->Nodes[pFans[1]].Var, 1 );
1086  if ( !Ifn_AddClause( pSat, pLits, pLits + 3 ) )
1087  return 0;
1088 
1089  pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 1 );
1090  pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 1 ); // ctrl
1091  pLits[2] = Abc_Var2Lit( p->Nodes[pFans[1]].Var, 0 );
1092  if ( !Ifn_AddClause( pSat, pLits, pLits + 3 ) )
1093  return 0;
1094 
1095  pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 0 );
1096  pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 0 ); // ctrl
1097  pLits[2] = Abc_Var2Lit( p->Nodes[pFans[2]].Var, 1 );
1098  if ( !Ifn_AddClause( pSat, pLits, pLits + 3 ) )
1099  return 0;
1100 
1101  pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 1 );
1102  pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 0 ); // ctrl
1103  pLits[2] = Abc_Var2Lit( p->Nodes[pFans[2]].Var, 0 );
1104  if ( !Ifn_AddClause( pSat, pLits, pLits + 3 ) )
1105  return 0;
1106  }
1107  else if ( p->Nodes[i].Type == IFN_DSD_PRIME )
1108  {
1109  int nValues = (1 << nFans);
1110  int iParStart = p->Nodes[i].iFirst;
1111  for ( v = 0; v < nValues; v++ )
1112  {
1113  nLits = 0;
1114  if ( pValues[i] == -1 )
1115  {
1116  pLits[nLits] = Abc_Var2Lit( p->Nodes[i].Var, 0 );
1117  pLits2[nLits] = Abc_Var2Lit( p->Nodes[i].Var, 1 );
1118  nLits++;
1119  }
1120  for ( f = 0; f < nFans; f++, nLits++ )
1121  pLits[nLits] = pLits2[nLits] = Abc_Var2Lit( p->Nodes[pFans[f]].Var, (v >> f) & 1 );
1122  pLits[nLits] = Abc_Var2Lit( iParStart + v, 1 );
1123  pLits2[nLits] = Abc_Var2Lit( iParStart + v, 0 );
1124  nLits++;
1125  if ( pValues[i] != 0 )
1126  {
1127  if ( !Ifn_AddClause( pSat, pLits2, pLits2 + nLits ) )
1128  return 0;
1129  }
1130  if ( pValues[i] != 1 )
1131  {
1132  if ( !Ifn_AddClause( pSat, pLits, pLits + nLits ) )
1133  return 0;
1134  }
1135  }
1136  }
1137  else assert( 0 );
1138 //printf( "\n" );
1139  }
1140  return 1;
1141 }
1142 
1143 /**Function*************************************************************
1144 
1145  Synopsis [Returns the minterm number for which there is a mismatch.]
1146 
1147  Description []
1148 
1149  SideEffects []
1150 
1151  SeeAlso []
1152 
1153 ***********************************************************************/
1154 void Ifn_NtkMatchPrintStatus( sat_solver * p, int Iter, int status, int iMint, int Value, abctime clk )
1155 {
1156  printf( "Iter = %5d ", Iter );
1157  printf( "Mint = %5d ", iMint );
1158  printf( "Value = %2d ", Value );
1159  printf( "Var = %6d ", sat_solver_nvars(p) );
1160  printf( "Cla = %6d ", sat_solver_nclauses(p) );
1161  printf( "Conf = %6d ", sat_solver_nconflicts(p) );
1162  if ( status == l_False )
1163  printf( "status = unsat" );
1164  else if ( status == l_True )
1165  printf( "status = sat " );
1166  else
1167  printf( "status = undec" );
1168  Abc_PrintTime( 1, "Time", clk );
1169 }
1170 void Ifn_NtkMatchPrintConfig( Ifn_Ntk_t * p, sat_solver * pSat )
1171 {
1172  int v, i;
1173  for ( v = p->nObjs; v < p->nPars; v++ )
1174  {
1175  for ( i = p->nInps; i < p->nObjs; i++ )
1176  if ( p->Nodes[i].Type == IFN_DSD_PRIME && (int)p->Nodes[i].iFirst == v )
1177  break;
1178  if ( i < p->nObjs )
1179  printf( " " );
1180  else if ( v >= p->nParsVIni && (v - p->nParsVIni) % p->nParsVNum == 0 )
1181  printf( " %d=", (v - p->nParsVIni) / p->nParsVNum );
1182  printf( "%d", sat_solver_var_value(pSat, v) );
1183  }
1184 }
1185 word Ifn_NtkMatchCollectPerm( Ifn_Ntk_t * p, sat_solver * pSat )
1186 {
1187  word Perm = 0;
1188  int i, v, Mint;
1189  assert( p->nParsVNum <= 4 );
1190  for ( i = 0; i < p->nInps; i++ )
1191  {
1192  for ( Mint = v = 0; v < p->nParsVNum; v++ )
1193  if ( sat_solver_var_value(pSat, p->nParsVIni + i * p->nParsVNum + v) )
1194  Mint |= (1 << v);
1195  Abc_TtSetHex( &Perm, i, Mint );
1196  }
1197  return Perm;
1198 }
1199 void Ifn_NtkMatchPrintPerm( word Perm, int nInps )
1200 {
1201  int i;
1202  assert( nInps <= 16 );
1203  for ( i = 0; i < nInps; i++ )
1204  printf( "%c", 'a' + Abc_TtGetHex(&Perm, i) );
1205  printf( "\n" );
1206 }
1207 int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pPerm )
1208 {
1209  word * pTruth1;
1210  int RetValue = 0;
1211  int nIterMax = (1<<nVars);
1212  int i, v, status, iMint = 0;
1213  abctime clk = Abc_Clock();
1214 // abctime clkTru = 0, clkSat = 0, clk2;
1215  sat_solver * pSat = sat_solver_new();
1216  Ifn_Prepare( p, pTruth, nVars );
1217  sat_solver_setnvars( pSat, p->nPars );
1218  Ifn_NtkAddConstraints( p, pSat );
1219  if ( fVeryVerbose )
1220  Ifn_NtkMatchPrintStatus( pSat, 0, l_True, -1, -1, Abc_Clock() - clk );
1221  if ( pPerm ) *pPerm = 0;
1222  for ( i = 0; i < nIterMax; i++ )
1223  {
1224  // get variable assignment
1225  for ( v = 0; v < p->nObjs; v++ )
1226  p->Values[v] = v < p->nVars ? (iMint >> v) & 1 : -1;
1227  p->Values[p->nObjs-1] = Abc_TtGetBit( pTruth, iMint );
1228  // derive clauses
1229  if ( !Ifn_NtkAddClauses( p, p->Values, pSat ) )
1230  break;
1231  // find assignment of parameters
1232 // clk2 = Abc_Clock();
1233  status = sat_solver_solve( pSat, NULL, NULL, nConfls, 0, 0, 0 );
1234 // clkSat += Abc_Clock() - clk2;
1235  if ( fVeryVerbose )
1236  Ifn_NtkMatchPrintStatus( pSat, i+1, status, iMint, p->Values[p->nObjs-1], Abc_Clock() - clk );
1237  if ( status != l_True )
1238  break;
1239  // collect assignment
1240  for ( v = p->nObjs; v < p->nPars; v++ )
1241  p->Values[v] = sat_solver_var_value(pSat, v);
1242  // find truth table
1243 // clk2 = Abc_Clock();
1244  pTruth1 = Ifn_NtkDeriveTruth( p, p->Values );
1245 // clkTru += Abc_Clock() - clk2;
1246  Abc_TtXor( pTruth1, pTruth1, p->pTruth, p->nWords, 0 );
1247  // find mismatch if present
1248  iMint = Abc_TtFindFirstBit( pTruth1, p->nVars );
1249  if ( iMint == -1 )
1250  {
1251  if ( pPerm )
1252  *pPerm = Ifn_NtkMatchCollectPerm( p, pSat );
1253 /*
1254  if ( pPerm )
1255  {
1256  int RetValue = Ifn_ManSatFindCofigBitsTest( p, pTruth, nVars, *pPerm );
1257  Ifn_NtkMatchPrintPerm( *pPerm, p->nInps );
1258  if ( RetValue == 0 )
1259  printf( "Verification failed.\n" );
1260  }
1261 */
1262  RetValue = 1;
1263  break;
1264  }
1265  }
1266  assert( i < nIterMax );
1267  if ( fVerbose )
1268  {
1269  printf( "%s Iter =%4d. Confl = %6d. ", RetValue ? "yes":"no ", i, sat_solver_nconflicts(pSat) );
1270  if ( RetValue )
1271  Ifn_NtkMatchPrintConfig( p, pSat );
1272  printf( "\n" );
1273  }
1274  sat_solver_delete( pSat );
1275 // Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1276 // Abc_PrintTime( 1, "Sat", clkSat );
1277 // Abc_PrintTime( 1, "Tru", clkTru );
1278  return RetValue;
1279 }
1280 
1281 /**Function*************************************************************
1282 
1283  Synopsis []
1284 
1285  Description []
1286 
1287  SideEffects []
1288 
1289  SeeAlso []
1290 
1291 ***********************************************************************/
1292 void Ifn_NtkRead()
1293 {
1294  int RetValue;
1295  int nVars = 8;
1296 // word * pTruth = Dau_DsdToTruth( "(abcdefghi)", nVars );
1297  word * pTruth = Dau_DsdToTruth( "1008{(1008{(ab)cde}f)ghi}", nVars );
1298 // word * pTruth = Dau_DsdToTruth( "18{(1008{(ab)cde}f)gh}", nVars );
1299 // word * pTruth = Dau_DsdToTruth( "1008{(1008{[ab]cde}f)ghi}", nVars );
1300 // word * pTruth = Dau_DsdToTruth( "(abcd)", nVars );
1301 // word * pTruth = Dau_DsdToTruth( "(abc)", nVars );
1302 // word * pTruth = Dau_DsdToTruth( "18{(1008{(ab)cde}f)gh}", nVars );
1303 // char * pStr = "e={abc};f={ed};";
1304 // char * pStr = "d={ab};e={cd};";
1305 // char * pStr = "j=(ab);k={jcde};l=(kf);m={lghi};";
1306 // char * pStr = "i={abc};j={ide};k={ifg};l={jkh};";
1307 // char * pStr = "h={abcde};i={abcdf};j=<ghi>;";
1308 // char * pStr = "g=<abc>;h=<ade>;i={fgh};";
1309 // char * pStr = "i=<abc>;j=(def);k=[gh];l={ijk};";
1310  char * pStr = "{({(ab)cde}f)ghi};AB;CD;DE;GH;HI";
1311  Ifn_Ntk_t * p = Ifn_NtkParse( pStr );
1312  word Perm = 0;
1313  if ( p == NULL )
1314  return;
1315  Ifn_NtkPrint( p );
1316  Dau_DsdPrintFromTruth( pTruth, nVars );
1317  // get the given function
1318  RetValue = Ifn_NtkMatch( p, pTruth, nVars, 0, 1, 1, &Perm );
1319  ABC_FREE( p );
1320 }
1321 
1322 ////////////////////////////////////////////////////////////////////////
1323 /// END OF FILE ///
1324 ////////////////////////////////////////////////////////////////////////
1325 
1326 
1327 ABC_NAMESPACE_IMPL_END
1328 
Ifn_Obj_t_
Definition: ifTune.c:61
memset
char * memset()
Abc_TtSharp
static void Abc_TtSharp(word *pOut, word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:241
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Inf_ManOpenSymb
int Inf_ManOpenSymb(char *pStr)
Definition: ifTune.c:194
Ifn_Ntk_t_::pTruth
word * pTruth
Definition: ifTune.c:84
Ifn_TtComparisonConstr
void Ifn_TtComparisonConstr(word *pTruth, int nVars, int fMore, int fEqual)
Definition: ifTune.c:877
Ifn_Obj_t_::nFanins
unsigned nFanins
Definition: ifTune.c:64
Ifn_Obj_t_::Fanins
int Fanins[IFN_INS]
Definition: ifTune.c:67
Ifn_Ntk_t_::pTtObjs
word pTtObjs[2 *IFN_INS *IFN_WRD]
Definition: ifTune.c:88
Ifn_NtkAddClauses
int Ifn_NtkAddClauses(Ifn_Ntk_t *p, int *pValues, sat_solver *pSat)
Definition: ifTune.c:1009
Ifn_Ntk_t_::Nodes
Ifn_Obj_t Nodes[2 *IFN_INS]
Definition: ifTune.c:74
Abc_TtMinBase
static int Abc_TtMinBase(word *pTruth, int *pVars, int nVars, int nVarsAll)
Definition: utilTruth.h:1395
Ifn_Prepare
int Ifn_Prepare(Ifn_Ntk_t *p, word *pTruth, int nVars)
FUNCTION DEFINITIONS ///.
Definition: ifTune.c:115
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManToAigSimple
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
Ifn_NtkParseInt
int Ifn_NtkParseInt(char *pStr, Ifn_Ntk_t *p)
Definition: ifTune.c:285
Ifn_NtkParseInt_rec
int Ifn_NtkParseInt_rec(char *pStr, Ifn_Ntk_t *p, char **ppFinal, int *piNode)
Definition: ifTune.c:251
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
IFN_PAR
#define IFN_PAR
Definition: ifTune.c:36
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Cnf_Derive
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Ifn_NtkParseFindClosingParanthesis
static char * Ifn_NtkParseFindClosingParanthesis(char *pStr, char Open, char Close)
Definition: ifTune.c:236
Gia_ManAppendCo
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Gia_ManHashXor
int Gia_ManHashXor(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:658
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Ifn_ManSatBuild
sat_solver * Ifn_ManSatBuild(Ifn_Ntk_t *p, Vec_Int_t **pvPiVars, Vec_Int_t **pvPoVars)
Definition: ifTune.c:608
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Ifn_NtkMatchPrintStatus
void Ifn_NtkMatchPrintStatus(sat_solver *p, int Iter, int status, int iMint, int Value, abctime clk)
Definition: ifTune.c:1154
Ifn_Ntk_t_::pConstr
int pConstr[IFN_INS]
Definition: ifTune.c:76
Cnf_Dat_t_::nClauses
int nClauses
Definition: cnf.h:61
sat_solver_solve
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
Ifn_Ntk_t_::nParsVIni
int nParsVIni
Definition: ifTune.c:82
Ifn_NtkMatch
int Ifn_NtkMatch(Ifn_Ntk_t *p, word *pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word *pPerm)
Definition: ifTune.c:1207
Ifn_NtkMatchCollectPerm
word Ifn_NtkMatchCollectPerm(Ifn_Ntk_t *p, sat_solver *pSat)
Definition: ifTune.c:1185
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Cnf_Dat_t_::nVars
int nVars
Definition: cnf.h:59
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Abc_TtClear
static void Abc_TtClear(word *pOut, int nWords)
Definition: utilTruth.h:197
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Ifn_ErrorMessage
int Ifn_ErrorMessage(const char *format,...)
Definition: ifTune.c:183
Abc_TtFindFirstBit
static int Abc_TtFindFirstBit(word *pIn, int nVars)
Definition: utilTruth.h:1516
sat_solver_nconflicts
int sat_solver_nconflicts(sat_solver *s)
Definition: satSolver.c:1908
Ifn_Ntk_t_::pTtElems
word pTtElems[IFN_INS *IFN_WRD]
Definition: ifTune.c:87
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition: cnf.h:63
Ifn_ManStrCheck2
int Ifn_ManStrCheck2(char *pStr, int *pnInps, int *pnObjs)
Definition: ifTune.c:324
Dau_DsdPrintFromTruth
void Dau_DsdPrintFromTruth(word *pTruth, int nVarsInit)
Definition: dauDsd.c:1968
memcpy
char * memcpy()
Ifn_DsdType_t
Ifn_DsdType_t
Definition: ifTune.c:39
Ifn_NtkAddConstraints
void Ifn_NtkAddConstraints(Ifn_Ntk_t *p, sat_solver *pSat)
Definition: ifTune.c:952
l_True
#define l_True
Definition: SolverTypes.h:84
Abc_TtOr
static void Abc_TtOr(word *pOut, word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:247
Ifn_Ntk_t_::nInps
int nInps
Definition: ifTune.c:72
Ifn_Ntk_t_::nVars
int nVars
Definition: ifTune.c:79
Dau_DsdToTruth
word * Dau_DsdToTruth(char *p, int nVars)
Definition: dauDsd.c:609
Ifn_ManSatDeriveOne
void Ifn_ManSatDeriveOne(sat_solver *pSat, Vec_Int_t *vPiVars, Vec_Int_t *vValues)
Definition: ifTune.c:680
Ifn_NtkInputNum
int Ifn_NtkInputNum(Ifn_Ntk_t *p)
Definition: ifTune.c:167
Ifn_ManSatCheckOne
int Ifn_ManSatCheckOne(sat_solver *pSat, Vec_Int_t *vPoVars, word *pTruth, int nVars, int *pPerm, int nInps, Vec_Int_t *vLits)
Definition: ifTune.c:651
Ifn_Ntk_t_
Definition: ifTune.c:69
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_TtGetBit
static int Abc_TtGetBit(word *p, int i)
MACRO DEFINITIONS ///.
Definition: utilTruth.h:149
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Cnf_Dat_t_
Definition: cnf.h:56
Abc_TtGetHex
static int Abc_TtGetHex(word *p, int k)
Definition: utilTruth.h:154
nWords
int nWords
Definition: abcNpn.c:127
Ifn_NtkLutSizeMax
int Ifn_NtkLutSizeMax(Ifn_Ntk_t *p)
Definition: ifTune.c:159
Ifn_NtkRead
void Ifn_NtkRead()
Definition: ifTune.c:1292
Cnf_DeriveGiaRemapped
static Cnf_Dat_t * Cnf_DeriveGiaRemapped(Gia_Man_t *p)
Definition: ifTune.c:575
Gia_Obj_t_
Definition: gia.h:75
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
IFN_WRD
#define IFN_WRD
Definition: ifTune.c:35
Ifn_Ntk_t_::nConstr
int nConstr
Definition: ifTune.c:77
Gia_ManForEachCiId
#define Gia_ManForEachCiId(p, Id, i)
Definition: gia.h:1018
Ifn_ManStrType2
int Ifn_ManStrType2(char *pStr)
Definition: ifTune.c:316
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Ifn_Obj_t_::Var
unsigned Var
Definition: ifTune.c:66
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Ifn_ManStrFindSolver
sat_solver * Ifn_ManStrFindSolver(Gia_Man_t *p, Vec_Int_t **pvPiVars, Vec_Int_t **pvPoVars)
Definition: ifTune.c:584
If_ManSatFindCofigBits
int If_ManSatFindCofigBits(void *pSat, Vec_Int_t *vPiVars, Vec_Int_t *vPoVars, word *pTruth, int nVars, word Perm, int nInps, Vec_Int_t *vValues)
Definition: ifTune.c:687
Ifn_Ntk_t_::nObjs
int nObjs
Definition: ifTune.c:73
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Abc_TtFill
static void Abc_TtFill(word *pOut, int nWords)
Definition: utilTruth.h:203
Ifn_Symbs
static char * Ifn_Symbs[16]
Definition: ifTune.c:50
Cnf_Dat_t_::pClauses
int ** pClauses
Definition: cnf.h:62
Abc_TtCopy
static void Abc_TtCopy(word *pOut, word *pIn, int nWords, int fCompl)
Definition: utilTruth.h:221
Ifn_NtkParseConstraints
void Ifn_NtkParseConstraints(char *pStr, Ifn_Ntk_t *p)
Definition: ifTune.c:423
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Ifn_Ntk_t_::nParsVNum
int nParsVNum
Definition: ifTune.c:81
Ifn_NtkParse
Ifn_Ntk_t * Ifn_NtkParse(char *pStr)
Definition: ifTune.c:439
IFN_INS
#define IFN_INS
DECLARATIONS ///.
Definition: ifTune.c:34
Kit_TruthIsop
int Kit_TruthIsop(unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
FUNCTION DEFINITIONS ///.
Definition: kitIsop.c:55
Gia_ObjFanin1Copy
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
vnsprintf
char * vnsprintf(const char *format, va_list args)
Definition: utilFile.c:168
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Gia_ManHashMux
int Gia_ManHashMux(Gia_Man_t *p, int iCtrl, int iData1, int iData0)
Definition: giaHash.c:677
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
Abc_Tt6Stretch
static word Abc_Tt6Stretch(word t, int nVars)
Definition: utilTruth.h:708
Gia_ManHashStart
void Gia_ManHashStart(Gia_Man_t *p)
Definition: giaHash.c:117
If_ManSatBuildFromCell
void * If_ManSatBuildFromCell(char *pStr, Vec_Int_t **pvPiVars, Vec_Int_t **pvPoVars, Ifn_Ntk_t **ppNtk)
Definition: ifTune.c:622
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Ifn_Ntk_t_::nWords
int nWords
Definition: ifTune.c:80
IF_MAX_FUNC_LUTSIZE
#define IF_MAX_FUNC_LUTSIZE
Definition: if.h:54
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Ifn_NtkParseInt2
int Ifn_NtkParseInt2(char *pStr, Ifn_Ntk_t *p)
Definition: ifTune.c:378
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Counter
static int Counter
Definition: extraBddMisc.c:1877
Ifn_Obj_t_::iFirst
unsigned iFirst
Definition: ifTune.c:65
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Ifn_NtkAddConstrOne
void Ifn_NtkAddConstrOne(sat_solver *pSat, Vec_Int_t *vCover, int *pVars, int nVars)
Definition: ifTune.c:932
Ifn_ManStrCheck
int Ifn_ManStrCheck(char *pStr, int *pnInps, int *pnObjs)
Definition: ifTune.c:206
Ifn_Ntk_t_::Values
int Values[IFN_PAR]
Definition: ifTune.c:86
pPerm
static int pPerm[13719]
Definition: rwrTemp.c:32
Gia_ObjFanin0Copy
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
Kit_TruthToGia
ABC_NAMESPACE_IMPL_START int Kit_TruthToGia(Gia_Man_t *pMan, unsigned *pTruth, int nVars, Vec_Int_t *vMemory, Vec_Int_t *vLeaves, int fHash)
DECLARATIONS ///.
Definition: kitHop.c:80
Ifn_AddClause
int Ifn_AddClause(sat_solver *pSat, int *pBeg, int *pEnd)
Definition: ifTune.c:920
Abc_Tt6Mask
static word Abc_Tt6Mask(int nBits)
Definition: utilTruth.h:184
sat_solver_nclauses
int sat_solver_nclauses(sat_solver *s)
Definition: satSolver.c:1902
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Ifn_NtkDeriveTruth
word * Ifn_NtkDeriveTruth(Ifn_Ntk_t *p, int *pValues)
Definition: ifTune.c:805
Ifn_ManStrFindModel
Gia_Man_t * Ifn_ManStrFindModel(Ifn_Ntk_t *p)
Definition: ifTune.c:477
Gia_ManCiNum
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Ifn_ManStrFindCofactors
Gia_Man_t * Ifn_ManStrFindCofactors(int nIns, Gia_Man_t *p)
Definition: ifTune.c:537
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Ifn_ElemTruth
static word * Ifn_ElemTruth(Ifn_Ntk_t *p, int i)
Definition: ifTune.c:91
Abc_TtWordNum
static int Abc_TtWordNum(int nVars)
Definition: utilTruth.h:169
Abc_TtSetHex
static void Abc_TtSetHex(word *p, int k, int d)
Definition: utilTruth.h:155
Ifn_NtkPrint
void Ifn_NtkPrint(Ifn_Ntk_t *p)
Definition: ifTune.c:141
Vec_IntShrink
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Abc_TtMux
static void Abc_TtMux(word *pOut, word *pCtrl, word *pIn1, word *pIn0, int nWords)
Definition: utilTruth.h:263
Gia_Man_t_
Definition: gia.h:95
Abc_Base2Log
static int Abc_Base2Log(unsigned n)
Definition: abc_global.h:251
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
Abc_TtElemInit2
static void Abc_TtElemInit2(word *pTtElems, int nVars)
Definition: utilTruth.h:344
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
l_False
#define l_False
Definition: SolverTypes.h:85
Ifn_ManSatFindCofigBitsTest
int Ifn_ManSatFindCofigBitsTest(Ifn_Ntk_t *p, word *pTruth, int nVars, word Perm)
Definition: ifTune.c:705
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
Ifn_NtkMatchPrintConfig
void Ifn_NtkMatchPrintConfig(Ifn_Ntk_t *p, sat_solver *pSat)
Definition: ifTune.c:1170
sat_solver_t
Definition: satSolver.h:91
Ifn_ManSatPrintPerm
void Ifn_ManSatPrintPerm(char *pPerms, int nVars)
Definition: ifTune.c:644
assert
#define assert(ex)
Definition: util_old.h:213
Ifn_ObjTruth
static word * Ifn_ObjTruth(Ifn_Ntk_t *p, int i)
Definition: ifTune.c:92
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Vec_IntPrint
static void Vec_IntPrint(Vec_Int_t *vVec)
Definition: vecInt.h:1803
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
Ifn_Ntk_t_::nPars
int nPars
Definition: ifTune.c:83
Ifn_NtkMatchPrintPerm
void Ifn_NtkMatchPrintPerm(word Perm, int nInps)
Definition: ifTune.c:1199
Abc_TtAnd
static void Abc_TtAnd(word *pOut, word *pIn1, word *pIn2, int nWords, int fCompl)
Definition: utilTruth.h:231
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_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
If_ManSatDeriveGiaFromBits
int If_ManSatDeriveGiaFromBits(void *pGia, Ifn_Ntk_t *p, Vec_Int_t *vValues, Vec_Int_t *vCover)
Definition: ifTune.c:731
Abc_TtXor
static void Abc_TtXor(word *pOut, word *pIn1, word *pIn2, int nWords, int fCompl)
Definition: utilTruth.h:253
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Abc_TtNot
static void Abc_TtNot(word *pOut, int nWords)
Definition: utilTruth.h:215
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Ifn_Obj_t_::Type
unsigned Type
Definition: ifTune.c:63
ABC_FALLOC
#define ABC_FALLOC(type, num)
Definition: abc_global.h:231