abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cnfFast.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [cnfFast.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [AIG-to-CNF conversion.]
8 
9  Synopsis []
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - April 28, 2007.]
16 
17  Revision [$Id: cnfFast.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "cnf.h"
22 #include "bool/kit/kit.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [Detects multi-input gate rooted at this node.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 void Cnf_CollectLeaves_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fStopCompl )
46 {
47  if ( pRoot != pObj && (pObj->fMarkA || (fStopCompl && Aig_IsComplement(pObj))) )
48  {
49  Vec_PtrPushUnique( vSuper, fStopCompl ? pObj : Aig_Regular(pObj) );
50  return;
51  }
52  assert( Aig_ObjIsNode(pObj) );
53  if ( fStopCompl )
54  {
55  Cnf_CollectLeaves_rec( pRoot, Aig_ObjChild0(pObj), vSuper, 1 );
56  Cnf_CollectLeaves_rec( pRoot, Aig_ObjChild1(pObj), vSuper, 1 );
57  }
58  else
59  {
60  Cnf_CollectLeaves_rec( pRoot, Aig_ObjFanin0(pObj), vSuper, 0 );
61  Cnf_CollectLeaves_rec( pRoot, Aig_ObjFanin1(pObj), vSuper, 0 );
62  }
63 }
64 
65 /**Function*************************************************************
66 
67  Synopsis [Detects multi-input gate rooted at this node.]
68 
69  Description []
70 
71  SideEffects []
72 
73  SeeAlso []
74 
75 ***********************************************************************/
76 void Cnf_CollectLeaves( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper, int fStopCompl )
77 {
78  assert( !Aig_IsComplement(pRoot) );
79  Vec_PtrClear( vSuper );
80  Cnf_CollectLeaves_rec( pRoot, pRoot, vSuper, fStopCompl );
81 }
82 
83 /**Function*************************************************************
84 
85  Synopsis [Collects nodes inside the cone.]
86 
87  Description []
88 
89  SideEffects []
90 
91  SeeAlso []
92 
93 ***********************************************************************/
94 void Cnf_CollectVolume_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
95 {
96  if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
97  return;
98  Aig_ObjSetTravIdCurrent( p, pObj );
99  assert( Aig_ObjIsNode(pObj) );
100  Cnf_CollectVolume_rec( p, Aig_ObjFanin0(pObj), vNodes );
101  Cnf_CollectVolume_rec( p, Aig_ObjFanin1(pObj), vNodes );
102  Vec_PtrPush( vNodes, pObj );
103 }
104 
105 /**Function*************************************************************
106 
107  Synopsis [Collects nodes inside the cone.]
108 
109  Description []
110 
111  SideEffects []
112 
113  SeeAlso []
114 
115 ***********************************************************************/
116 void Cnf_CollectVolume( Aig_Man_t * p, Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes )
117 {
118  Aig_Obj_t * pObj;
119  int i;
120  Aig_ManIncrementTravId( p );
121  Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
122  Aig_ObjSetTravIdCurrent( p, pObj );
123  Vec_PtrClear( vNodes );
124  Cnf_CollectVolume_rec( p, pRoot, vNodes );
125 }
126 
127 /**Function*************************************************************
128 
129  Synopsis [Derive truth table.]
130 
131  Description []
132 
133  SideEffects []
134 
135  SeeAlso []
136 
137 ***********************************************************************/
138 word Cnf_CutDeriveTruth( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes )
139 {
140  static word Truth6[6] = {
141  ABC_CONST(0xAAAAAAAAAAAAAAAA),
142  ABC_CONST(0xCCCCCCCCCCCCCCCC),
143  ABC_CONST(0xF0F0F0F0F0F0F0F0),
144  ABC_CONST(0xFF00FF00FF00FF00),
145  ABC_CONST(0xFFFF0000FFFF0000),
146  ABC_CONST(0xFFFFFFFF00000000)
147  };
148  static word C[2] = { 0, ~(word)0 };
149  static word S[256];
150  Aig_Obj_t * pObj = NULL;
151  int i;
152  assert( Vec_PtrSize(vLeaves) <= 6 && Vec_PtrSize(vNodes) > 0 );
153  assert( Vec_PtrSize(vLeaves) + Vec_PtrSize(vNodes) <= 256 );
154  Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
155  {
156  pObj->iData = i;
157  S[pObj->iData] = Truth6[i];
158  }
159  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
160  {
161  pObj->iData = Vec_PtrSize(vLeaves) + i;
162  S[pObj->iData] = (S[Aig_ObjFanin0(pObj)->iData] ^ C[Aig_ObjFaninC0(pObj)]) &
163  (S[Aig_ObjFanin1(pObj)->iData] ^ C[Aig_ObjFaninC1(pObj)]);
164  }
165  return S[pObj->iData];
166 }
167 
168 
169 /**Function*************************************************************
170 
171  Synopsis [Collects nodes inside the cone.]
172 
173  Description []
174 
175  SideEffects []
176 
177  SeeAlso []
178 
179 ***********************************************************************/
180 static inline int Cnf_ObjGetLit( Vec_Int_t * vMap, Aig_Obj_t * pObj, int fCompl )
181 {
182  int iSatVar = vMap ? Vec_IntEntry(vMap, Aig_ObjId(pObj)) : Aig_ObjId(pObj);
183  assert( iSatVar > 0 );
184  return iSatVar + iSatVar + fCompl;
185 }
186 
187 /**Function*************************************************************
188 
189  Synopsis [Collects nodes inside the cone.]
190 
191  Description []
192 
193  SideEffects []
194 
195  SeeAlso []
196 
197 ***********************************************************************/
198 void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot,
199  Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Int_t * vMap, Vec_Int_t * vCover, Vec_Int_t * vClauses )
200 {
201  Aig_Obj_t * pLeaf;
202  int c, k, Cube, OutLit, RetValue;
203  word Truth;
204  assert( pRoot->fMarkA );
205 
206  Vec_IntClear( vClauses );
207 
208  OutLit = Cnf_ObjGetLit( vMap, pRoot, 0 );
209  // detect cone
210  Cnf_CollectLeaves( pRoot, vLeaves, 0 );
211  Cnf_CollectVolume( p, pRoot, vLeaves, vNodes );
212  assert( pRoot == Vec_PtrEntryLast(vNodes) );
213  // check if this is an AND-gate
214  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pLeaf, k )
215  {
216  if ( Aig_ObjFaninC0(pLeaf) && !Aig_ObjFanin0(pLeaf)->fMarkA )
217  break;
218  if ( Aig_ObjFaninC1(pLeaf) && !Aig_ObjFanin1(pLeaf)->fMarkA )
219  break;
220  }
221  if ( k == Vec_PtrSize(vNodes) )
222  {
223  Cnf_CollectLeaves( pRoot, vLeaves, 1 );
224  // write big clause
225  Vec_IntPush( vClauses, 0 );
226  Vec_IntPush( vClauses, OutLit );
227  Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k )
228  Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, Aig_Regular(pLeaf), !Aig_IsComplement(pLeaf)) );
229  // write small clauses
230  Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k )
231  {
232  Vec_IntPush( vClauses, 0 );
233  Vec_IntPush( vClauses, OutLit ^ 1 );
234  Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, Aig_Regular(pLeaf), Aig_IsComplement(pLeaf)) );
235  }
236  return;
237  }
238  if ( Vec_PtrSize(vLeaves) > 6 )
239  printf( "FastCnfGeneration: Internal error!!!\n" );
240  assert( Vec_PtrSize(vLeaves) <= 6 );
241 
242  Truth = Cnf_CutDeriveTruth( p, vLeaves, vNodes );
243  if ( Truth == 0 || Truth == ~(word)0 )
244  {
245  Vec_IntPush( vClauses, 0 );
246  Vec_IntPush( vClauses, (Truth == 0) ? (OutLit ^ 1) : OutLit );
247  return;
248  }
249 
250  RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
251  assert( RetValue >= 0 );
252 
253  Vec_IntForEachEntry( vCover, Cube, c )
254  {
255  Vec_IntPush( vClauses, 0 );
256  Vec_IntPush( vClauses, OutLit );
257  for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 )
258  {
259  if ( (Cube & 3) == 0 )
260  continue;
261  assert( (Cube & 3) != 3 );
262  Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, (Aig_Obj_t *)Vec_PtrEntry(vLeaves,k), (Cube&3)!=1) );
263  }
264  }
265 
266  Truth = ~Truth;
267 
268  RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
269  assert( RetValue >= 0 );
270  Vec_IntForEachEntry( vCover, Cube, c )
271  {
272  Vec_IntPush( vClauses, 0 );
273  Vec_IntPush( vClauses, OutLit ^ 1 );
274  for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 )
275  {
276  if ( (Cube & 3) == 0 )
277  continue;
278  assert( (Cube & 3) != 3 );
279  Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, (Aig_Obj_t *)Vec_PtrEntry(vLeaves,k), (Cube&3)!=1) );
280  }
281  }
282 }
283 
284 
285 
286 /**Function*************************************************************
287 
288  Synopsis [Marks AIG for CNF computation.]
289 
290  Description []
291 
292  SideEffects []
293 
294  SeeAlso []
295 
296 ***********************************************************************/
297 void Cnf_DeriveFastMark( Aig_Man_t * p )
298 {
299  Vec_Int_t * vSupps;
300  Vec_Ptr_t * vLeaves, * vNodes;
301  Aig_Obj_t * pObj, * pTemp, * pObjC, * pObj0, * pObj1;
302  int i, k, nFans, Counter;
303 
304  vLeaves = Vec_PtrAlloc( 100 );
305  vNodes = Vec_PtrAlloc( 100 );
306  vSupps = Vec_IntStart( Aig_ManObjNumMax(p) );
307 
308  // mark CIs
309  Aig_ManForEachCi( p, pObj, i )
310  pObj->fMarkA = 1;
311 
312  // mark CO drivers
313  Aig_ManForEachCo( p, pObj, i )
314  Aig_ObjFanin0(pObj)->fMarkA = 1;
315 
316  // mark MUX/XOR nodes
317  Aig_ManForEachNode( p, pObj, i )
318  {
319  assert( !pObj->fMarkB );
320  if ( !Aig_ObjIsMuxType(pObj) )
321  continue;
322  pObj0 = Aig_ObjFanin0(pObj);
323  if ( pObj0->fMarkB || Aig_ObjRefs(pObj0) > 1 )
324  continue;
325  pObj1 = Aig_ObjFanin1(pObj);
326  if ( pObj1->fMarkB || Aig_ObjRefs(pObj1) > 1 )
327  continue;
328  // mark nodes
329  pObj->fMarkB = 1;
330  pObj0->fMarkB = 1;
331  pObj1->fMarkB = 1;
332  // mark inputs and outputs
333  pObj->fMarkA = 1;
334  Aig_ObjFanin0(pObj0)->fMarkA = 1;
335  Aig_ObjFanin1(pObj0)->fMarkA = 1;
336  Aig_ObjFanin0(pObj1)->fMarkA = 1;
337  Aig_ObjFanin1(pObj1)->fMarkA = 1;
338  }
339 
340  // mark nodes with multiple fanouts and pointed to by complemented edges
341  Aig_ManForEachNode( p, pObj, i )
342  {
343  // mark nodes with many fanouts
344  if ( Aig_ObjRefs(pObj) > 1 )
345  pObj->fMarkA = 1;
346  // mark nodes pointed to by a complemented edge
347  if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFanin0(pObj)->fMarkB )
348  Aig_ObjFanin0(pObj)->fMarkA = 1;
349  if ( Aig_ObjFaninC1(pObj) && !Aig_ObjFanin1(pObj)->fMarkB )
350  Aig_ObjFanin1(pObj)->fMarkA = 1;
351  }
352 
353  // compute supergate size for internal marked nodes
354  Aig_ManForEachNode( p, pObj, i )
355  {
356  if ( !pObj->fMarkA )
357  continue;
358  if ( pObj->fMarkB )
359  {
360  if ( !Aig_ObjIsMuxType(pObj) )
361  continue;
362  pObjC = Aig_ObjRecognizeMux( pObj, &pObj1, &pObj0 );
363  pObj0 = Aig_Regular(pObj0);
364  pObj1 = Aig_Regular(pObj1);
365  assert( pObj0->fMarkA );
366  assert( pObj1->fMarkA );
367 // if ( pObj0 == pObj1 )
368 // continue;
369  nFans = 1 + (pObj0 == pObj1);
370  if ( !pObj0->fMarkB && !Aig_ObjIsCi(pObj0) && Aig_ObjRefs(pObj0) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj0)) < 3 )
371  {
372  pObj0->fMarkA = 0;
373  continue;
374  }
375  if ( !pObj1->fMarkB && !Aig_ObjIsCi(pObj1) && Aig_ObjRefs(pObj1) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj1)) < 3 )
376  {
377  pObj1->fMarkA = 0;
378  continue;
379  }
380  continue;
381  }
382 
383  Cnf_CollectLeaves( pObj, vLeaves, 1 );
384  Vec_IntWriteEntry( vSupps, Aig_ObjId(pObj), Vec_PtrSize(vLeaves) );
385  if ( Vec_PtrSize(vLeaves) >= 6 )
386  continue;
387  Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pTemp, k )
388  {
389  pTemp = Aig_Regular(pTemp);
390  assert( pTemp->fMarkA );
391  if ( pTemp->fMarkB || Aig_ObjIsCi(pTemp) || Aig_ObjRefs(pTemp) > 1 )
392  continue;
393  assert( Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) > 0 );
394  if ( Vec_PtrSize(vLeaves) - 1 + Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) > 6 )
395  continue;
396  pTemp->fMarkA = 0;
397  Vec_IntWriteEntry( vSupps, Aig_ObjId(pObj), 6 );
398 //printf( "%d %d ", Vec_PtrSize(vLeaves), Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) );
399  break;
400  }
401  }
402  Aig_ManCleanMarkB( p );
403 
404  // check CO drivers
405  Counter = 0;
406  Aig_ManForEachCo( p, pObj, i )
407  Counter += !Aig_ObjFanin0(pObj)->fMarkA;
408  if ( Counter )
409  printf( "PO-driver rule is violated %d times.\n", Counter );
410 
411  // check that the AND-gates are fine
412  Counter = 0;
413  Aig_ManForEachNode( p, pObj, i )
414  {
415  assert( pObj->fMarkB == 0 );
416  if ( !pObj->fMarkA )
417  continue;
418  Cnf_CollectLeaves( pObj, vLeaves, 0 );
419  if ( Vec_PtrSize(vLeaves) <= 6 )
420  continue;
421  Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
422  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pTemp, k )
423  {
424  if ( Aig_ObjFaninC0(pTemp) && !Aig_ObjFanin0(pTemp)->fMarkA )
425  Counter++;
426  if ( Aig_ObjFaninC1(pTemp) && !Aig_ObjFanin1(pTemp)->fMarkA )
427  Counter++;
428  }
429  }
430  if ( Counter )
431  printf( "AND-gate rule is violated %d times.\n", Counter );
432 
433  Vec_PtrFree( vLeaves );
434  Vec_PtrFree( vNodes );
435  Vec_IntFree( vSupps );
436 }
437 
438 
439 /**Function*************************************************************
440 
441  Synopsis [Counts the number of clauses.]
442 
443  Description []
444 
445  SideEffects []
446 
447  SeeAlso []
448 
449 ***********************************************************************/
450 int Cnf_CutCountClauses( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Int_t * vCover )
451 {
452  word Truth;
453  Aig_Obj_t * pObj;
454  int i, RetValue, nSize = 0;
455  if ( Vec_PtrSize(vLeaves) > 6 )
456  {
457  // make sure this is an AND gate
458  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
459  {
460  if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFanin0(pObj)->fMarkA )
461  printf( "Unusual 1!\n" );
462  if ( Aig_ObjFaninC1(pObj) && !Aig_ObjFanin1(pObj)->fMarkA )
463  printf( "Unusual 2!\n" );
464  continue;
465 
466  assert( !Aig_ObjFaninC0(pObj) || Aig_ObjFanin0(pObj)->fMarkA );
467  assert( !Aig_ObjFaninC1(pObj) || Aig_ObjFanin1(pObj)->fMarkA );
468  }
469  return Vec_PtrSize(vLeaves) + 1;
470  }
471  Truth = Cnf_CutDeriveTruth( p, vLeaves, vNodes );
472 
473  RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
474  assert( RetValue >= 0 );
475  nSize += Vec_IntSize(vCover);
476 
477  Truth = ~Truth;
478 
479  RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
480  assert( RetValue >= 0 );
481  nSize += Vec_IntSize(vCover);
482  return nSize;
483 }
484 
485 /**Function*************************************************************
486 
487  Synopsis [Counts the size of the CNF, assuming marks are set.]
488 
489  Description []
490 
491  SideEffects []
492 
493  SeeAlso []
494 
495 ***********************************************************************/
496 int Cnf_CountCnfSize( Aig_Man_t * p )
497 {
498  Vec_Ptr_t * vLeaves, * vNodes;
499  Vec_Int_t * vCover;
500  Aig_Obj_t * pObj;
501  int nVars = 0, nClauses = 0;
502  int i, nSize;
503 
504  vLeaves = Vec_PtrAlloc( 100 );
505  vNodes = Vec_PtrAlloc( 100 );
506  vCover = Vec_IntAlloc( 1 << 16 );
507 
508  Aig_ManForEachObj( p, pObj, i )
509  nVars += pObj->fMarkA;
510 
511  Aig_ManForEachNode( p, pObj, i )
512  {
513  if ( !pObj->fMarkA )
514  continue;
515  Cnf_CollectLeaves( pObj, vLeaves, 0 );
516  Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
517  assert( pObj == Vec_PtrEntryLast(vNodes) );
518 
519  nSize = Cnf_CutCountClauses( p, vLeaves, vNodes, vCover );
520 // printf( "%d(%d) ", Vec_PtrSize(vLeaves), nSize );
521 
522  nClauses += nSize;
523  }
524 // printf( "\n" );
525  printf( "Vars = %d Clauses = %d\n", nVars, nClauses );
526 
527  Vec_PtrFree( vLeaves );
528  Vec_PtrFree( vNodes );
529  Vec_IntFree( vCover );
530  return nClauses;
531 }
532 
533 /**Function*************************************************************
534 
535  Synopsis [Derives CNF from the marked AIG.]
536 
537  Description [Assumes that marking is such that when we traverse from each
538  marked node, the logic cone has 6 inputs or less, or it is a multi-input AND.]
539 
540  SideEffects []
541 
542  SeeAlso []
543 
544 ***********************************************************************/
545 Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs )
546 {
547  Cnf_Dat_t * pCnf;
548  Vec_Int_t * vLits, * vClas, * vMap, * vTemp;
549  Vec_Ptr_t * vLeaves, * vNodes;
550  Vec_Int_t * vCover;
551  Aig_Obj_t * pObj;
552  int i, k, nVars, Entry, OutLit, DriLit;
553 
554  vLits = Vec_IntAlloc( 1 << 16 );
555  vClas = Vec_IntAlloc( 1 << 12 );
556  vMap = Vec_IntStartFull( Aig_ManObjNumMax(p) );
557 
558  // assign variables for the outputs
559  nVars = 1;
560  if ( nOutputs )
561  {
562  if ( Aig_ManRegNum(p) == 0 )
563  {
564  assert( nOutputs == Aig_ManCoNum(p) );
565  Aig_ManForEachCo( p, pObj, i )
566  Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ );
567  }
568  else
569  {
570  assert( nOutputs == Aig_ManRegNum(p) );
571  Aig_ManForEachLiSeq( p, pObj, i )
572  Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ );
573  }
574  }
575  // assign variables to the internal nodes
576  Aig_ManForEachNodeReverse( p, pObj, i )
577  if ( pObj->fMarkA )
578  Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ );
579  // assign variables to the PIs and constant node
580  Aig_ManForEachCi( p, pObj, i )
581  Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ );
582  Vec_IntWriteEntry( vMap, Aig_ObjId(Aig_ManConst1(p)), nVars++ );
583 
584  // create clauses
585  vLeaves = Vec_PtrAlloc( 100 );
586  vNodes = Vec_PtrAlloc( 100 );
587  vCover = Vec_IntAlloc( 1 << 16 );
588  vTemp = Vec_IntAlloc( 100 );
589  Aig_ManForEachNodeReverse( p, pObj, i )
590  {
591  if ( !pObj->fMarkA )
592  continue;
593  Cnf_ComputeClauses( p, pObj, vLeaves, vNodes, vMap, vCover, vTemp );
594  Vec_IntForEachEntry( vTemp, Entry, k )
595  {
596  if ( Entry == 0 )
597  Vec_IntPush( vClas, Vec_IntSize(vLits) );
598  else
599  Vec_IntPush( vLits, Entry );
600  }
601  }
602  Vec_PtrFree( vLeaves );
603  Vec_PtrFree( vNodes );
604  Vec_IntFree( vCover );
605  Vec_IntFree( vTemp );
606 
607  // create clauses for the outputs
608  Aig_ManForEachCo( p, pObj, i )
609  {
610  DriLit = Cnf_ObjGetLit( vMap, Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj) );
611  if ( i < Aig_ManCoNum(p) - nOutputs )
612  {
613  Vec_IntPush( vClas, Vec_IntSize(vLits) );
614  Vec_IntPush( vLits, DriLit );
615  }
616  else
617  {
618  OutLit = Cnf_ObjGetLit( vMap, pObj, 0 );
619  // first clause
620  Vec_IntPush( vClas, Vec_IntSize(vLits) );
621  Vec_IntPush( vLits, OutLit );
622  Vec_IntPush( vLits, DriLit ^ 1 );
623  // second clause
624  Vec_IntPush( vClas, Vec_IntSize(vLits) );
625  Vec_IntPush( vLits, OutLit ^ 1 );
626  Vec_IntPush( vLits, DriLit );
627  }
628  }
629 
630  // write the constant literal
631  OutLit = Cnf_ObjGetLit( vMap, Aig_ManConst1(p), 0 );
632  Vec_IntPush( vClas, Vec_IntSize(vLits) );
633  Vec_IntPush( vLits, OutLit );
634 
635  // create structure
636  pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
637  pCnf->pMan = p;
638  pCnf->nVars = nVars;
639  pCnf->nLiterals = Vec_IntSize( vLits );
640  pCnf->nClauses = Vec_IntSize( vClas );
641  pCnf->pClauses = ABC_ALLOC( int *, pCnf->nClauses + 1 );
642  pCnf->pClauses[0] = Vec_IntReleaseArray( vLits );
643  Vec_IntForEachEntry( vClas, Entry, i )
644  pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
645  pCnf->pClauses[pCnf->nClauses] = pCnf->pClauses[0] + pCnf->nLiterals;
646  pCnf->pVarNums = Vec_IntReleaseArray( vMap );
647 
648  // cleanup
649  Vec_IntFree( vLits );
650  Vec_IntFree( vClas );
651  Vec_IntFree( vMap );
652  return pCnf;
653 }
654 
655 /**Function*************************************************************
656 
657  Synopsis [Fast CNF computation.]
658 
659  Description []
660 
661  SideEffects []
662 
663  SeeAlso []
664 
665 ***********************************************************************/
666 Cnf_Dat_t * Cnf_DeriveFast( Aig_Man_t * p, int nOutputs )
667 {
668  Cnf_Dat_t * pCnf = NULL;
669  abctime clk;//, clkTotal = Abc_Clock();
670 // printf( "\n" );
671  Aig_ManCleanMarkAB( p );
672  // create initial marking
673  clk = Abc_Clock();
674  Cnf_DeriveFastMark( p );
675 // Abc_PrintTime( 1, "Marking", Abc_Clock() - clk );
676  // compute CNF size
677  clk = Abc_Clock();
678  pCnf = Cnf_DeriveFastClauses( p, nOutputs );
679 // Abc_PrintTime( 1, "Clauses", Abc_Clock() - clk );
680  // derive the resulting CNF
681  Aig_ManCleanMarkA( p );
682 // Abc_PrintTime( 1, "TOTAL ", Abc_Clock() - clkTotal );
683 
684 // printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. \n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
685 
686 // Cnf_DataFree( pCnf );
687 // pCnf = NULL;
688  return pCnf;
689 }
690 
691 ////////////////////////////////////////////////////////////////////////
692 /// END OF FILE ///
693 ////////////////////////////////////////////////////////////////////////
694 
695 
696 ABC_NAMESPACE_IMPL_END
697 
Cnf_ObjGetLit
static int Cnf_ObjGetLit(Vec_Int_t *vMap, Aig_Obj_t *pObj, int fCompl)
Definition: cnfFast.c:180
Cnf_CollectLeaves_rec
ABC_NAMESPACE_IMPL_START void Cnf_CollectLeaves_rec(Aig_Obj_t *pRoot, Aig_Obj_t *pObj, Vec_Ptr_t *vSuper, int fStopCompl)
DECLARATIONS ///.
Definition: cnfFast.c:45
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Aig_ObjChild0
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_PtrPushUnique
static int Vec_PtrPushUnique(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:656
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Cnf_Dat_t_::nClauses
int nClauses
Definition: cnf.h:61
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition: aig.h:80
Cnf_CollectVolume
void Cnf_CollectVolume(Aig_Man_t *p, Aig_Obj_t *pRoot, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes)
Definition: cnfFast.c:116
Cnf_Dat_t_::nVars
int nVars
Definition: cnf.h:59
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Cnf_DeriveFastClauses
Cnf_Dat_t * Cnf_DeriveFastClauses(Aig_Man_t *p, int nOutputs)
Definition: cnfFast.c:545
Aig_ManCleanMarkB
void Aig_ManCleanMarkB(Aig_Man_t *p)
Definition: aigUtil.c:167
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition: cnf.h:63
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition: aig.h:79
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Cnf_CutCountClauses
int Cnf_CutCountClauses(Aig_Man_t *p, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes, Vec_Int_t *vCover)
Definition: cnfFast.c:450
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Cnf_Dat_t_::pMan
Aig_Man_t * pMan
Definition: cnf.h:58
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Cnf_Dat_t_
Definition: cnf.h:56
Vec_IntStartFull
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Cnf_CollectVolume_rec
void Cnf_CollectVolume_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Definition: cnfFast.c:94
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Cnf_Dat_t_::pClauses
int ** pClauses
Definition: cnf.h:62
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Aig_ObjRecognizeMux
Aig_Obj_t * Aig_ObjRecognizeMux(Aig_Obj_t *pObj, Aig_Obj_t **ppObjT, Aig_Obj_t **ppObjE)
Definition: aigUtil.c:387
Vec_PtrEntryLast
static void * Vec_PtrEntryLast(Vec_Ptr_t *p)
Definition: vecPtr.h:413
Kit_TruthIsop
int Kit_TruthIsop(unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
FUNCTION DEFINITIONS ///.
Definition: kitIsop.c:55
Cnf_CollectLeaves
void Cnf_CollectLeaves(Aig_Obj_t *pRoot, Vec_Ptr_t *vSuper, int fStopCompl)
Definition: cnfFast.c:76
Cnf_ComputeClauses
void Cnf_ComputeClauses(Aig_Man_t *p, Aig_Obj_t *pRoot, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes, Vec_Int_t *vMap, Vec_Int_t *vCover, Vec_Int_t *vClauses)
Definition: cnfFast.c:198
Truth6
static word Truth6[6]
Definition: ifDec07.c:52
Cnf_CountCnfSize
int Cnf_CountCnfSize(Aig_Man_t *p)
Definition: cnfFast.c:496
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
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Aig_ObjChild1
static Aig_Obj_t * Aig_ObjChild1(Aig_Obj_t *pObj)
Definition: aig.h:311
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Counter
static int Counter
Definition: extraBddMisc.c:1877
Cnf_CutDeriveTruth
word Cnf_CutDeriveTruth(Aig_Man_t *p, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes)
Definition: cnfFast.c:138
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Aig_Obj_t_::iData
int iData
Definition: aig.h:88
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
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
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
Aig_ManCleanMarkAB
void Aig_ManCleanMarkAB(Aig_Man_t *p)
Definition: aigUtil.c:186
Aig_ObjIsMuxType
int Aig_ObjIsMuxType(Aig_Obj_t *pObj)
Definition: aigUtil.c:307
Aig_ManCleanMarkA
void Aig_ManCleanMarkA(Aig_Man_t *p)
Definition: aigUtil.c:148
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Aig_ManForEachLiSeq
#define Aig_ManForEachLiSeq(p, pObj, i)
Definition: aig.h:447
Aig_ManForEachNodeReverse
#define Aig_ManForEachNodeReverse(p, pObj, i)
Definition: aig.h:415
Aig_ObjRefs
static int Aig_ObjRefs(Aig_Obj_t *pObj)
Definition: aig.h:300
Cnf_DeriveFast
Cnf_Dat_t * Cnf_DeriveFast(Aig_Man_t *p, int nOutputs)
Definition: cnfFast.c:666
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Cnf_Dat_t_::nLiterals
int nLiterals
Definition: cnf.h:60
Cnf_DeriveFastMark
void Cnf_DeriveFastMark(Aig_Man_t *p)
Definition: cnfFast.c:297
Vec_IntReleaseArray
static int * Vec_IntReleaseArray(Vec_Int_t *p)
Definition: extraZddTrunc.c:89
S
static shot S[256]
Definition: kitPerm.c:40
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223