ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
cnfFast.c
Go to the documentation of this file.
1
20
21#include "cnf.h"
22#include "bool/kit/kit.h"
23
24ABC_NAMESPACE_IMPL_START
25
29
33
45void 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
76void 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
94void 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
116void 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
138word 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
180static 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
198void 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
297void 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
450int 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
496int 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
545Cnf_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
666Cnf_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
694
695
696ABC_NAMESPACE_IMPL_END
697
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition abc_global.h:240
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Aig_ObjRecognizeMux
Aig_Obj_t * Aig_ObjRecognizeMux(Aig_Obj_t *pObj, Aig_Obj_t **ppObjT, Aig_Obj_t **ppObjE)
Definition aigUtil.c:387
Aig_ManCleanMarkB
void Aig_ManCleanMarkB(Aig_Man_t *p)
Definition aigUtil.c:167
Aig_ManCleanMarkA
void Aig_ManCleanMarkA(Aig_Man_t *p)
Definition aigUtil.c:148
Aig_ManForEachNodeReverse
#define Aig_ManForEachNodeReverse(p, pObj, i)
Definition aig.h:415
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition aig.h:403
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigUtil.c:44
Aig_ManForEachLiSeq
#define Aig_ManForEachLiSeq(p, pObj, i)
Definition aig.h:447
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Aig_ManCleanMarkAB
void Aig_ManCleanMarkAB(Aig_Man_t *p)
Definition aigUtil.c:186
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
Aig_ObjIsMuxType
int Aig_ObjIsMuxType(Aig_Obj_t *pObj)
Definition aigUtil.c:307
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cnf_DeriveFast
Cnf_Dat_t * Cnf_DeriveFast(Aig_Man_t *p, int nOutputs)
Definition cnfFast.c:666
Cnf_CountCnfSize
int Cnf_CountCnfSize(Aig_Man_t *p)
Definition cnfFast.c:496
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
Cnf_CutDeriveTruth
word Cnf_CutDeriveTruth(Aig_Man_t *p, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes)
Definition cnfFast.c:138
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_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
Cnf_CollectVolume_rec
void Cnf_CollectVolume_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Definition cnfFast.c:94
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
Cnf_CollectLeaves
void Cnf_CollectLeaves(Aig_Obj_t *pRoot, Vec_Ptr_t *vSuper, int fStopCompl)
Definition cnfFast.c:76
Cnf_DeriveFastClauses
Cnf_Dat_t * Cnf_DeriveFastClauses(Aig_Man_t *p, int nOutputs)
Definition cnfFast.c:545
Cnf_DeriveFastMark
void Cnf_DeriveFastMark(Aig_Man_t *p)
Definition cnfFast.c:297
Cnf_Dat_t
struct Cnf_Dat_t_ Cnf_Dat_t
Definition cnf.h:52
p
Cube * p
Definition exorList.c:222
Cube
struct cube Cube
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Kit_TruthIsop
int Kit_TruthIsop(unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
Definition kitIsop.c:134
Aig_Obj_t_::iData
int iData
Definition aig.h:88
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition aig.h:80
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition aig.h:79
Cnf_Dat_t_::nVars
int nVars
Definition cnf.h:59
Cnf_Dat_t_::nLiterals
int nLiterals
Definition cnf.h:60
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition cnf.h:63
Cnf_Dat_t_::pClauses
int ** pClauses
Definition cnf.h:62
Cnf_Dat_t_::nClauses
int nClauses
Definition cnf.h:61
Cnf_Dat_t_::pMan
Aig_Man_t * pMan
Definition cnf.h:58
assert
#define assert(ex)
Definition util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55