ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
cnfWrite.c
Go to the documentation of this file.
1
20
21#include "cnf.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
29
33
45Vec_Int_t * Cnf_ManWriteCnfMapping( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
46{
47 Vec_Int_t * vResult;
48 Aig_Obj_t * pObj;
49 Cnf_Cut_t * pCut;
50 int i, k, nOffset;
51 nOffset = Aig_ManObjNumMax(p->pManAig);
52 vResult = Vec_IntStart( nOffset );
53 Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
54 {
55 assert( Aig_ObjIsNode(pObj) );
56 pCut = Cnf_ObjBestCut( pObj );
57 assert( pCut->nFanins < 5 );
58 Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), nOffset );
59 Vec_IntPush( vResult, *Cnf_CutTruth(pCut) );
60 for ( k = 0; k < pCut->nFanins; k++ )
61 Vec_IntPush( vResult, pCut->pFanins[k] );
62 for ( ; k < 4; k++ )
63 Vec_IntPush( vResult, -1 );
64 nOffset += 5;
65 }
66 return vResult;
67}
68
69
70
82void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover )
83{
84 int Lits[4], Cube, iCube, i, b;
85 Vec_IntClear( vCover );
86 for ( i = 0; i < nCubes; i++ )
87 {
88 Cube = pSop[i];
89 for ( b = 0; b < 4; b++ )
90 {
91 if ( Cube % 3 == 0 )
92 Lits[b] = 1;
93 else if ( Cube % 3 == 1 )
94 Lits[b] = 2;
95 else
96 Lits[b] = 0;
97 Cube = Cube / 3;
98 }
99 iCube = 0;
100 for ( b = 0; b < 4; b++ )
101 iCube = (iCube << 2) | Lits[b];
102 Vec_IntPush( vCover, iCube );
103 }
104}
105
117int Cnf_SopCountLiterals( char * pSop, int nCubes )
118{
119 int nLits = 0, Cube, i, b;
120 for ( i = 0; i < nCubes; i++ )
121 {
122 Cube = pSop[i];
123 for ( b = 0; b < 4; b++ )
124 {
125 if ( Cube % 3 != 2 )
126 nLits++;
127 Cube = Cube / 3;
128 }
129 }
130 return nLits;
131}
132
144int Cnf_IsopCountLiterals( Vec_Int_t * vIsop, int nVars )
145{
146 int nLits = 0, Cube, i, b;
147 Vec_IntForEachEntry( vIsop, Cube, i )
148 {
149 for ( b = 0; b < nVars; b++ )
150 {
151 if ( (Cube & 3) == 1 || (Cube & 3) == 2 )
152 nLits++;
153 Cube >>= 2;
154 }
155 }
156 return nLits;
157}
158
170int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int * pLiterals )
171{
172 int nLits = nVars, b;
173 for ( b = 0; b < nVars; b++ )
174 {
175 if ( (Cube & 3) == 1 ) // value 0 --> write positive literal
176 *pLiterals++ = 2 * pVars[b];
177 else if ( (Cube & 3) == 2 ) // value 1 --> write negative literal
178 *pLiterals++ = 2 * pVars[b] + 1;
179 else
180 nLits--;
181 Cube >>= 2;
182 }
183 return nLits;
184}
185
199Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
200{
201 int fChangeVariableOrder = 0; // should be set to 0 to improve performance
202 Aig_Obj_t * pObj;
203 Cnf_Dat_t * pCnf;
204 Cnf_Cut_t * pCut;
205 Vec_Int_t * vCover, * vSopTemp;
206 int OutVar, PoVar, pVars[32], * pLits, ** pClas;
207 unsigned uTruth;
208 int i, k, nLiterals, nClauses, Cube, Number;
209
210 // count the number of literals and clauses
211 nLiterals = 1 + Aig_ManCoNum( p->pManAig ) + 3 * nOutputs;
212 nClauses = 1 + Aig_ManCoNum( p->pManAig ) + nOutputs;
213 Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
214 {
215 assert( Aig_ObjIsNode(pObj) );
216 pCut = Cnf_ObjBestCut( pObj );
217
218 // positive polarity of the cut
219 if ( pCut->nFanins < 5 )
220 {
221 uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
222 nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
223 assert( p->pSopSizes[uTruth] >= 0 );
224 nClauses += p->pSopSizes[uTruth];
225 }
226 else
227 {
228 nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]);
229 nClauses += Vec_IntSize(pCut->vIsop[1]);
230 }
231 // negative polarity of the cut
232 if ( pCut->nFanins < 5 )
233 {
234 uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
235 nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
236 assert( p->pSopSizes[uTruth] >= 0 );
237 nClauses += p->pSopSizes[uTruth];
238 }
239 else
240 {
241 nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
242 nClauses += Vec_IntSize(pCut->vIsop[0]);
243 }
244//printf( "%d ", nClauses-(1 + Aig_ManCoNum( p->pManAig )) );
245 }
246//printf( "\n" );
247
248 // allocate CNF
249 pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
250 pCnf->pMan = p->pManAig;
251 pCnf->nLiterals = nLiterals;
252 pCnf->nClauses = nClauses;
253 pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
254 pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
255 pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
256 // create room for variable numbers
257 pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
258// memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p->pManAig) );
259 for ( i = 0; i < Aig_ManObjNumMax(p->pManAig); i++ )
260 pCnf->pVarNums[i] = -1;
261
262 if ( !fChangeVariableOrder )
263 {
264 // assign variables to the last (nOutputs) POs
265 Number = 1;
266 if ( nOutputs )
267 {
268 if ( Aig_ManRegNum(p->pManAig) == 0 )
269 {
270 assert( nOutputs == Aig_ManCoNum(p->pManAig) );
271 Aig_ManForEachCo( p->pManAig, pObj, i )
272 pCnf->pVarNums[pObj->Id] = Number++;
273 }
274 else
275 {
276 assert( nOutputs == Aig_ManRegNum(p->pManAig) );
277 Aig_ManForEachLiSeq( p->pManAig, pObj, i )
278 pCnf->pVarNums[pObj->Id] = Number++;
279 }
280 }
281 // assign variables to the internal nodes
282 Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
283 pCnf->pVarNums[pObj->Id] = Number++;
284 // assign variables to the PIs and constant node
285 Aig_ManForEachCi( p->pManAig, pObj, i )
286 pCnf->pVarNums[pObj->Id] = Number++;
287 pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number++;
288 pCnf->nVars = Number;
289 }
290 else
291 {
292 // assign variables to the last (nOutputs) POs
293 Number = Aig_ManObjNumMax(p->pManAig) + 1;
294 pCnf->nVars = Number + 1;
295 if ( nOutputs )
296 {
297 if ( Aig_ManRegNum(p->pManAig) == 0 )
298 {
299 assert( nOutputs == Aig_ManCoNum(p->pManAig) );
300 Aig_ManForEachCo( p->pManAig, pObj, i )
301 pCnf->pVarNums[pObj->Id] = Number--;
302 }
303 else
304 {
305 assert( nOutputs == Aig_ManRegNum(p->pManAig) );
306 Aig_ManForEachLiSeq( p->pManAig, pObj, i )
307 pCnf->pVarNums[pObj->Id] = Number--;
308 }
309 }
310 // assign variables to the internal nodes
311 Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
312 pCnf->pVarNums[pObj->Id] = Number--;
313 // assign variables to the PIs and constant node
314 Aig_ManForEachCi( p->pManAig, pObj, i )
315 pCnf->pVarNums[pObj->Id] = Number--;
316 pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number--;
317 assert( Number >= 0 );
318 }
319
320 // assign the clauses
321 vSopTemp = Vec_IntAlloc( 1 << 16 );
322 pLits = pCnf->pClauses[0];
323 pClas = pCnf->pClauses;
324 Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
325 {
326 pCut = Cnf_ObjBestCut( pObj );
327
328 // save variables of this cut
329 OutVar = pCnf->pVarNums[ pObj->Id ];
330 for ( k = 0; k < (int)pCut->nFanins; k++ )
331 {
332 pVars[k] = pCnf->pVarNums[ pCut->pFanins[k] ];
333 assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) );
334 }
335
336 // positive polarity of the cut
337 if ( pCut->nFanins < 5 )
338 {
339 uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
340 Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
341 vCover = vSopTemp;
342 }
343 else
344 vCover = pCut->vIsop[1];
345 Vec_IntForEachEntry( vCover, Cube, k )
346 {
347 *pClas++ = pLits;
348 *pLits++ = 2 * OutVar;
349 pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
350 }
351
352 // negative polarity of the cut
353 if ( pCut->nFanins < 5 )
354 {
355 uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
356 Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
357 vCover = vSopTemp;
358 }
359 else
360 vCover = pCut->vIsop[0];
361 Vec_IntForEachEntry( vCover, Cube, k )
362 {
363 *pClas++ = pLits;
364 *pLits++ = 2 * OutVar + 1;
365 pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
366 }
367 }
368 Vec_IntFree( vSopTemp );
369
370 // write the constant literal
371 OutVar = pCnf->pVarNums[ Aig_ManConst1(p->pManAig)->Id ];
372 assert( OutVar <= Aig_ManObjNumMax(p->pManAig) );
373 *pClas++ = pLits;
374 *pLits++ = 2 * OutVar;
375
376 // write the output literals
377 Aig_ManForEachCo( p->pManAig, pObj, i )
378 {
379 OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
380 if ( i < Aig_ManCoNum(p->pManAig) - nOutputs )
381 {
382 *pClas++ = pLits;
383 *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
384 }
385 else
386 {
387 PoVar = pCnf->pVarNums[ pObj->Id ];
388 // first clause
389 *pClas++ = pLits;
390 *pLits++ = 2 * PoVar;
391 *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj);
392 // second clause
393 *pClas++ = pLits;
394 *pLits++ = 2 * PoVar + 1;
395 *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
396 }
397 }
398
399 // verify that the correct number of literals and clauses was written
400 assert( pLits - pCnf->pClauses[0] == nLiterals );
401 assert( pClas - pCnf->pClauses == nClauses );
402//Cnf_DataPrint( pCnf, 1 );
403 return pCnf;
404}
405
406
419Cnf_Dat_t * Cnf_ManWriteCnfOther( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
420{
421 Aig_Obj_t * pObj;
422 Cnf_Dat_t * pCnf;
423 Cnf_Cut_t * pCut;
424 Vec_Int_t * vCover, * vSopTemp;
425 int OutVar, PoVar, pVars[32], * pLits, ** pClas;
426 unsigned uTruth;
427 int i, k, nLiterals, nClauses, Cube;
428
429 // count the number of literals and clauses
430 nLiterals = 1 + 4 * Aig_ManCoNum( p->pManAig );
431 nClauses = 1 + 2 * Aig_ManCoNum( p->pManAig );
432 Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
433 {
434 assert( Aig_ObjIsNode(pObj) );
435 pCut = Cnf_ObjBestCut( pObj );
436 // positive polarity of the cut
437 if ( pCut->nFanins < 5 )
438 {
439 uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
440 nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
441 assert( p->pSopSizes[uTruth] >= 0 );
442 nClauses += p->pSopSizes[uTruth];
443 }
444 else
445 {
446 nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]);
447 nClauses += Vec_IntSize(pCut->vIsop[1]);
448 }
449 // negative polarity of the cut
450 if ( pCut->nFanins < 5 )
451 {
452 uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
453 nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
454 assert( p->pSopSizes[uTruth] >= 0 );
455 nClauses += p->pSopSizes[uTruth];
456 }
457 else
458 {
459 nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
460 nClauses += Vec_IntSize(pCut->vIsop[0]);
461 }
462 }
463
464 // allocate CNF
465 pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
466 pCnf->pMan = p->pManAig;
467 pCnf->nLiterals = nLiterals;
468 pCnf->nClauses = nClauses;
469 pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
470 pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
471 pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
472 // create room for variable numbers
473 pCnf->pObj2Clause = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
474 pCnf->pObj2Count = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
475 for ( i = 0; i < Aig_ManObjNumMax(p->pManAig); i++ )
476 pCnf->pObj2Clause[i] = pCnf->pObj2Count[i] = -1;
477 pCnf->nVars = Aig_ManObjNumMax(p->pManAig);
478
479 // clear the PI counters
480 Aig_ManForEachCi( p->pManAig, pObj, i )
481 pCnf->pObj2Count[pObj->Id] = 0;
482
483 // assign the clauses
484 vSopTemp = Vec_IntAlloc( 1 << 16 );
485 pLits = pCnf->pClauses[0];
486 pClas = pCnf->pClauses;
487 Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
488 {
489 // remember the starting clause
490 pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses;
491 pCnf->pObj2Count[pObj->Id] = 0;
492
493 // get the best cut
494 pCut = Cnf_ObjBestCut( pObj );
495 // save variables of this cut
496 OutVar = pObj->Id;
497 for ( k = 0; k < (int)pCut->nFanins; k++ )
498 {
499 pVars[k] = pCut->pFanins[k];
500 assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) );
501 }
502
503 // positive polarity of the cut
504 if ( pCut->nFanins < 5 )
505 {
506 uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
507 Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
508 vCover = vSopTemp;
509 }
510 else
511 vCover = pCut->vIsop[1];
512 Vec_IntForEachEntry( vCover, Cube, k )
513 {
514 *pClas++ = pLits;
515 *pLits++ = 2 * OutVar;
516 pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
517 }
518 pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover);
519
520 // negative polarity of the cut
521 if ( pCut->nFanins < 5 )
522 {
523 uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
524 Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
525 vCover = vSopTemp;
526 }
527 else
528 vCover = pCut->vIsop[0];
529 Vec_IntForEachEntry( vCover, Cube, k )
530 {
531 *pClas++ = pLits;
532 *pLits++ = 2 * OutVar + 1;
533 pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
534 }
535 pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover);
536 }
537 Vec_IntFree( vSopTemp );
538
539 // write the output literals
540 Aig_ManForEachCo( p->pManAig, pObj, i )
541 {
542 // remember the starting clause
543 pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses;
544 pCnf->pObj2Count[pObj->Id] = 2;
545 // get variables
546 OutVar = Aig_ObjFanin0(pObj)->Id;
547 PoVar = pObj->Id;
548 // first clause
549 *pClas++ = pLits;
550 *pLits++ = 2 * PoVar;
551 *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj);
552 // second clause
553 *pClas++ = pLits;
554 *pLits++ = 2 * PoVar + 1;
555 *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
556 }
557
558 // remember the starting clause
559 pCnf->pObj2Clause[Aig_ManConst1(p->pManAig)->Id] = pClas - pCnf->pClauses;
560 pCnf->pObj2Count[Aig_ManConst1(p->pManAig)->Id] = 1;
561 // write the constant literal
562 OutVar = Aig_ManConst1(p->pManAig)->Id;
563 *pClas++ = pLits;
564 *pLits++ = 2 * OutVar;
565
566 // verify that the correct number of literals and clauses was written
567 assert( pLits - pCnf->pClauses[0] == nLiterals );
568 assert( pClas - pCnf->pClauses == nClauses );
569//Cnf_DataPrint( pCnf, 1 );
570 return pCnf;
571}
572
573
587Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs )
588{
589 Aig_Obj_t * pObj;
590 Cnf_Dat_t * pCnf;
591 int OutVar, PoVar, pVars[32], * pLits, ** pClas;
592 int i, nLiterals, nClauses, Number;
593
594 // count the number of literals and clauses
595 nLiterals = 1 + 7 * Aig_ManNodeNum(p) + Aig_ManCoNum( p ) + 3 * nOutputs;
596 nClauses = 1 + 3 * Aig_ManNodeNum(p) + Aig_ManCoNum( p ) + nOutputs;
597
598 // allocate CNF
599 pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
600 memset( pCnf, 0, sizeof(Cnf_Dat_t) );
601 pCnf->pMan = p;
602 pCnf->nLiterals = nLiterals;
603 pCnf->nClauses = nClauses;
604 pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
605 pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
606 pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
607
608 // create room for variable numbers
609 pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p) );
610// memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
611 for ( i = 0; i < Aig_ManObjNumMax(p); i++ )
612 pCnf->pVarNums[i] = -1;
613 // assign variables to the last (nOutputs) POs
614 Number = 1;
615 if ( nOutputs )
616 {
617// assert( nOutputs == Aig_ManRegNum(p) );
618// Aig_ManForEachLiSeq( p, pObj, i )
619// pCnf->pVarNums[pObj->Id] = Number++;
620 Aig_ManForEachCo( p, pObj, i )
621 pCnf->pVarNums[pObj->Id] = Number++;
622 }
623 // assign variables to the internal nodes
624 Aig_ManForEachNode( p, pObj, i )
625 pCnf->pVarNums[pObj->Id] = Number++;
626 // assign variables to the PIs and constant node
627 Aig_ManForEachCi( p, pObj, i )
628 pCnf->pVarNums[pObj->Id] = Number++;
629 pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++;
630 pCnf->nVars = Number;
631/*
632 // print CNF numbers
633 printf( "SAT numbers of each node:\n" );
634 Aig_ManForEachObj( p, pObj, i )
635 printf( "%d=%d ", pObj->Id, pCnf->pVarNums[pObj->Id] );
636 printf( "\n" );
637*/
638 // assign the clauses
639 pLits = pCnf->pClauses[0];
640 pClas = pCnf->pClauses;
641 Aig_ManForEachNode( p, pObj, i )
642 {
643 OutVar = pCnf->pVarNums[ pObj->Id ];
644 pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
645 pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
646
647 // positive phase
648 *pClas++ = pLits;
649 *pLits++ = 2 * OutVar;
650 *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj);
651 *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj);
652 // negative phase
653 *pClas++ = pLits;
654 *pLits++ = 2 * OutVar + 1;
655 *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj);
656 *pClas++ = pLits;
657 *pLits++ = 2 * OutVar + 1;
658 *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj);
659 }
660
661 // write the constant literal
662 OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ];
663 assert( OutVar <= Aig_ManObjNumMax(p) );
664 *pClas++ = pLits;
665 *pLits++ = 2 * OutVar;
666
667 // write the output literals
668 Aig_ManForEachCo( p, pObj, i )
669 {
670 OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
671 if ( i < Aig_ManCoNum(p) - nOutputs )
672 {
673 *pClas++ = pLits;
674 *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
675 }
676 else
677 {
678 PoVar = pCnf->pVarNums[ pObj->Id ];
679 // first clause
680 *pClas++ = pLits;
681 *pLits++ = 2 * PoVar;
682 *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj);
683 // second clause
684 *pClas++ = pLits;
685 *pLits++ = 2 * PoVar + 1;
686 *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
687 }
688 }
689
690 // verify that the correct number of literals and clauses was written
691 assert( pLits - pCnf->pClauses[0] == nLiterals );
692 assert( pClas - pCnf->pClauses == nClauses );
693 return pCnf;
694}
695
709Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p )
710{
711 Aig_Obj_t * pObj;
712 Cnf_Dat_t * pCnf;
713 int OutVar, PoVar, pVars[32], * pLits, ** pClas;
714 int i, nLiterals, nClauses, Number;
715
716 // count the number of literals and clauses
717 nLiterals = 1 + 7 * Aig_ManNodeNum(p) + 5 * Aig_ManCoNum(p);
718 nClauses = 1 + 3 * Aig_ManNodeNum(p) + 3 * Aig_ManCoNum(p);
719
720 // allocate CNF
721 pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
722 memset( pCnf, 0, sizeof(Cnf_Dat_t) );
723 pCnf->pMan = p;
724 pCnf->nLiterals = nLiterals;
725 pCnf->nClauses = nClauses;
726 pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
727 pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
728 pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
729
730 // create room for variable numbers
731 pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p) );
732// memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
733 for ( i = 0; i < Aig_ManObjNumMax(p); i++ )
734 pCnf->pVarNums[i] = -1;
735 // assign variables to the last (nOutputs) POs
736 Number = 1;
737 Aig_ManForEachCo( p, pObj, i )
738 pCnf->pVarNums[pObj->Id] = Number++;
739 // assign variables to the internal nodes
740 Aig_ManForEachNode( p, pObj, i )
741 pCnf->pVarNums[pObj->Id] = Number++;
742 // assign variables to the PIs and constant node
743 Aig_ManForEachCi( p, pObj, i )
744 pCnf->pVarNums[pObj->Id] = Number++;
745 pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++;
746 pCnf->nVars = Number;
747 // assign the clauses
748 pLits = pCnf->pClauses[0];
749 pClas = pCnf->pClauses;
750 Aig_ManForEachNode( p, pObj, i )
751 {
752 OutVar = pCnf->pVarNums[ pObj->Id ];
753 pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
754 pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
755
756 // positive phase
757 *pClas++ = pLits;
758 *pLits++ = 2 * OutVar;
759 *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj);
760 *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj);
761 // negative phase
762 *pClas++ = pLits;
763 *pLits++ = 2 * OutVar + 1;
764 *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj);
765 *pClas++ = pLits;
766 *pLits++ = 2 * OutVar + 1;
767 *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj);
768 }
769
770 // write the constant literal
771 OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ];
772 assert( OutVar <= Aig_ManObjNumMax(p) );
773 *pClas++ = pLits;
774 *pLits++ = 2 * OutVar;
775
776 // write the output literals
777 Aig_ManForEachCo( p, pObj, i )
778 {
779 OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
780 PoVar = pCnf->pVarNums[ pObj->Id ];
781 // first clause
782 *pClas++ = pLits;
783 *pLits++ = 2 * PoVar;
784 *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj);
785 // second clause
786 *pClas++ = pLits;
787 *pLits++ = 2 * PoVar + 1;
788 *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
789 // final clause (init-state is always 0 -> set the output to 0)
790 *pClas++ = pLits;
791 *pLits++ = 2 * PoVar + 1;
792 }
793
794 // verify that the correct number of literals and clauses was written
795 assert( pLits - pCnf->pClauses[0] == nLiterals );
796 assert( pClas - pCnf->pClauses == nClauses );
797 return pCnf;
798}
799
803
804
805ABC_NAMESPACE_IMPL_END
806
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_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_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_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cnf_DeriveSimple
Cnf_Dat_t * Cnf_DeriveSimple(Aig_Man_t *p, int nOutputs)
Definition cnfWrite.c:587
Cnf_IsopWriteCube
int Cnf_IsopWriteCube(int Cube, int nVars, int *pVars, int *pLiterals)
Definition cnfWrite.c:170
Cnf_ManWriteCnfOther
Cnf_Dat_t * Cnf_ManWriteCnfOther(Cnf_Man_t *p, Vec_Ptr_t *vMapped)
Definition cnfWrite.c:419
Cnf_ManWriteCnfMapping
ABC_NAMESPACE_IMPL_START Vec_Int_t * Cnf_ManWriteCnfMapping(Cnf_Man_t *p, Vec_Ptr_t *vMapped)
DECLARATIONS ///.
Definition cnfWrite.c:45
Cnf_IsopCountLiterals
int Cnf_IsopCountLiterals(Vec_Int_t *vIsop, int nVars)
Definition cnfWrite.c:144
Cnf_SopConvertToVector
void Cnf_SopConvertToVector(char *pSop, int nCubes, Vec_Int_t *vCover)
Definition cnfWrite.c:82
Cnf_ManWriteCnf
Cnf_Dat_t * Cnf_ManWriteCnf(Cnf_Man_t *p, Vec_Ptr_t *vMapped, int nOutputs)
Definition cnfWrite.c:199
Cnf_DeriveSimpleForRetiming
Cnf_Dat_t * Cnf_DeriveSimpleForRetiming(Aig_Man_t *p)
Definition cnfWrite.c:709
Cnf_SopCountLiterals
int Cnf_SopCountLiterals(char *pSop, int nCubes)
Definition cnfWrite.c:117
Cnf_Man_t
typedefABC_NAMESPACE_HEADER_START struct Cnf_Man_t_ Cnf_Man_t
INCLUDES ///.
Definition cnf.h:51
Cnf_Dat_t
struct Cnf_Dat_t_ Cnf_Dat_t
Definition cnf.h:52
Cnf_Cut_t
struct Cnf_Cut_t_ Cnf_Cut_t
Definition cnf.h:53
p
Cube * p
Definition exorList.c:222
Cube
struct cube Cube
Aig_Obj_t_::Id
int Id
Definition aig.h:85
Cnf_Cut_t_::vIsop
Vec_Int_t * vIsop[2]
Definition cnf.h:76
Cnf_Cut_t_::nFanins
char nFanins
Definition cnf.h:73
Cnf_Cut_t_::pFanins
int pFanins[0]
Definition cnf.h:77
Cnf_Dat_t_::nVars
int nVars
Definition cnf.h:59
Cnf_Dat_t_::pObj2Count
int * pObj2Count
Definition cnf.h:65
Cnf_Dat_t_::pObj2Clause
int * pObj2Clause
Definition cnf.h:64
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
memset
char * memset()
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