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 ***********************************************************************/
Cnf_CollectLeaves_rec(Aig_Obj_t * pRoot,Aig_Obj_t * pObj,Vec_Ptr_t * vSuper,int fStopCompl)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 ***********************************************************************/
Cnf_CollectLeaves(Aig_Obj_t * pRoot,Vec_Ptr_t * vSuper,int fStopCompl)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 ***********************************************************************/
Cnf_CollectVolume_rec(Aig_Man_t * p,Aig_Obj_t * pObj,Vec_Ptr_t * vNodes)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 ***********************************************************************/
Cnf_CollectVolume(Aig_Man_t * p,Aig_Obj_t * pRoot,Vec_Ptr_t * vLeaves,Vec_Ptr_t * vNodes)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 ***********************************************************************/
Cnf_CutDeriveTruth(Aig_Man_t * p,Vec_Ptr_t * vLeaves,Vec_Ptr_t * vNodes)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 ***********************************************************************/
Cnf_ObjGetLit(Vec_Int_t * vMap,Aig_Obj_t * pObj,int fCompl)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 ***********************************************************************/
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)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 ***********************************************************************/
Cnf_DeriveFastMark(Aig_Man_t * p)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 ***********************************************************************/
Cnf_CutCountClauses(Aig_Man_t * p,Vec_Ptr_t * vLeaves,Vec_Ptr_t * vNodes,Vec_Int_t * vCover)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 ***********************************************************************/
Cnf_CountCnfSize(Aig_Man_t * p)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 ***********************************************************************/
Cnf_DeriveFastClauses(Aig_Man_t * p,int nOutputs)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 ***********************************************************************/
Cnf_DeriveFast(Aig_Man_t * p,int nOutputs)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
698