1 /**CFile****************************************************************
2
3 FileName [cnfMan.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: cnfMan.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "cnf.h"
22 #include "sat/bsat/satSolver.h"
23 #include "sat/bsat/satSolver2.h"
24 #include "misc/zlib/zlib.h"
25
26 ABC_NAMESPACE_IMPL_START
27
28
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32
Cnf_Lit2Var(int Lit)33 static inline int Cnf_Lit2Var( int Lit ) { return (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+1; }
Cnf_Lit2Var2(int Lit)34 static inline int Cnf_Lit2Var2( int Lit ) { return (Lit & 1)? -(Lit >> 1) : (Lit >> 1); }
35
36 ////////////////////////////////////////////////////////////////////////
37 /// FUNCTION DEFINITIONS ///
38 ////////////////////////////////////////////////////////////////////////
39
40 /**Function*************************************************************
41
42 Synopsis [Starts the fraiging manager.]
43
44 Description []
45
46 SideEffects []
47
48 SeeAlso []
49
50 ***********************************************************************/
Cnf_ManStart()51 Cnf_Man_t * Cnf_ManStart()
52 {
53 Cnf_Man_t * p;
54 int i;
55 // allocate the manager
56 p = ABC_ALLOC( Cnf_Man_t, 1 );
57 memset( p, 0, sizeof(Cnf_Man_t) );
58 // derive internal data structures
59 Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
60 // allocate memory manager for cuts
61 p->pMemCuts = Aig_MmFlexStart();
62 p->nMergeLimit = 10;
63 // allocate temporary truth tables
64 p->pTruths[0] = ABC_ALLOC( unsigned, 4 * Abc_TruthWordNum(p->nMergeLimit) );
65 for ( i = 1; i < 4; i++ )
66 p->pTruths[i] = p->pTruths[i-1] + Abc_TruthWordNum(p->nMergeLimit);
67 p->vMemory = Vec_IntAlloc( 1 << 18 );
68 return p;
69 }
70
71 /**Function*************************************************************
72
73 Synopsis [Stops the fraiging manager.]
74
75 Description []
76
77 SideEffects []
78
79 SeeAlso []
80
81 ***********************************************************************/
Cnf_ManStop(Cnf_Man_t * p)82 void Cnf_ManStop( Cnf_Man_t * p )
83 {
84 Vec_IntFree( p->vMemory );
85 ABC_FREE( p->pTruths[0] );
86 Aig_MmFlexStop( p->pMemCuts, 0 );
87 ABC_FREE( p->pSopSizes );
88 ABC_FREE( p->pSops[1] );
89 ABC_FREE( p->pSops );
90 ABC_FREE( p );
91 }
92
93 /**Function*************************************************************
94
95 Synopsis [Returns the array of CI IDs.]
96
97 Description []
98
99 SideEffects []
100
101 SeeAlso []
102
103 ***********************************************************************/
Cnf_DataCollectPiSatNums(Cnf_Dat_t * pCnf,Aig_Man_t * p)104 Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
105 {
106 Vec_Int_t * vCiIds;
107 Aig_Obj_t * pObj;
108 int i;
109 vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
110 Aig_ManForEachCi( p, pObj, i )
111 Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
112 return vCiIds;
113 }
114
115 /**Function*************************************************************
116
117 Synopsis [Allocates the new CNF.]
118
119 Description []
120
121 SideEffects []
122
123 SeeAlso []
124
125 ***********************************************************************/
Cnf_DataAlloc(Aig_Man_t * pAig,int nVars,int nClauses,int nLiterals)126 Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals )
127 {
128 Cnf_Dat_t * pCnf;
129 int i;
130 pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
131 memset( pCnf, 0, sizeof(Cnf_Dat_t) );
132 pCnf->pMan = pAig;
133 pCnf->nVars = nVars;
134 pCnf->nClauses = nClauses;
135 pCnf->nLiterals = nLiterals;
136 pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
137 pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
138 pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
139 pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(pAig) );
140 // memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(pAig) );
141 for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
142 pCnf->pVarNums[i] = -1;
143 return pCnf;
144 }
145
146 /**Function*************************************************************
147
148 Synopsis [Allocates the new CNF.]
149
150 Description []
151
152 SideEffects []
153
154 SeeAlso []
155
156 ***********************************************************************/
Cnf_DataDup(Cnf_Dat_t * p)157 Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p )
158 {
159 Cnf_Dat_t * pCnf;
160 int i;
161 pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses, p->nLiterals );
162 memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
163 memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
164 for ( i = 1; i < p->nClauses; i++ )
165 pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
166 return pCnf;
167 }
168
169 /**Function*************************************************************
170
171 Synopsis []
172
173 Description []
174
175 SideEffects []
176
177 SeeAlso []
178
179 ***********************************************************************/
Cnf_DataFree(Cnf_Dat_t * p)180 void Cnf_DataFree( Cnf_Dat_t * p )
181 {
182 if ( p == NULL )
183 return;
184 Vec_IntFreeP( &p->vMapping );
185 ABC_FREE( p->pClaPols );
186 ABC_FREE( p->pObj2Clause );
187 ABC_FREE( p->pObj2Count );
188 ABC_FREE( p->pClauses[0] );
189 ABC_FREE( p->pClauses );
190 ABC_FREE( p->pVarNums );
191 ABC_FREE( p );
192 }
193
194 /**Function*************************************************************
195
196 Synopsis []
197
198 Description []
199
200 SideEffects []
201
202 SeeAlso []
203
204 ***********************************************************************/
Cnf_DataLift(Cnf_Dat_t * p,int nVarsPlus)205 void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus )
206 {
207 Aig_Obj_t * pObj;
208 int v;
209 if ( p->pMan )
210 {
211 Aig_ManForEachObj( p->pMan, pObj, v )
212 if ( p->pVarNums[pObj->Id] >= 0 )
213 p->pVarNums[pObj->Id] += nVarsPlus;
214 }
215 for ( v = 0; v < p->nLiterals; v++ )
216 p->pClauses[0][v] += 2*nVarsPlus;
217 }
Cnf_DataCollectFlipLits(Cnf_Dat_t * p,int iFlipVar,Vec_Int_t * vFlips)218 void Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar, Vec_Int_t * vFlips )
219 {
220 int v;
221 assert( p->pMan == NULL );
222 Vec_IntClear( vFlips );
223 for ( v = 0; v < p->nLiterals; v++ )
224 if ( Abc_Lit2Var(p->pClauses[0][v]) == iFlipVar )
225 Vec_IntPush( vFlips, v );
226 }
Cnf_DataLiftAndFlipLits(Cnf_Dat_t * p,int nVarsPlus,Vec_Int_t * vLits)227 void Cnf_DataLiftAndFlipLits( Cnf_Dat_t * p, int nVarsPlus, Vec_Int_t * vLits )
228 {
229 int i, iLit;
230 assert( p->pMan == NULL );
231 Vec_IntForEachEntry( vLits, iLit, i )
232 p->pClauses[0][iLit] = Abc_LitNot(p->pClauses[0][iLit]) + 2*nVarsPlus;
233 }
234
235 /**Function*************************************************************
236
237 Synopsis []
238
239 Description []
240
241 SideEffects []
242
243 SeeAlso []
244
245 ***********************************************************************/
Cnf_DataPrint(Cnf_Dat_t * p,int fReadable)246 void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable )
247 {
248 FILE * pFile = stdout;
249 int * pLit, * pStop, i;
250 fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
251 for ( i = 0; i < p->nClauses; i++ )
252 {
253 for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
254 fprintf( pFile, "%s%d ", Abc_LitIsCompl(*pLit) ? "-":"", fReadable? Abc_Lit2Var(*pLit) : Abc_Lit2Var(*pLit)+1 );
255 fprintf( pFile, "\n" );
256 }
257 fprintf( pFile, "\n" );
258 }
259
260 /**Function*************************************************************
261
262 Synopsis [Writes CNF into a file.]
263
264 Description []
265
266 SideEffects []
267
268 SeeAlso []
269
270 ***********************************************************************/
Cnf_DataWriteIntoFileGz(Cnf_Dat_t * p,char * pFileName,int fReadable,Vec_Int_t * vForAlls,Vec_Int_t * vExists)271 void Cnf_DataWriteIntoFileGz( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vForAlls, Vec_Int_t * vExists )
272 {
273 gzFile pFile;
274 int * pLit, * pStop, i, VarId;
275 pFile = gzopen( pFileName, "wb" );
276 if ( pFile == NULL )
277 {
278 printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" );
279 return;
280 }
281 gzprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
282 gzprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
283 if ( vForAlls )
284 {
285 gzprintf( pFile, "a " );
286 Vec_IntForEachEntry( vForAlls, VarId, i )
287 gzprintf( pFile, "%d ", fReadable? VarId : VarId+1 );
288 gzprintf( pFile, "0\n" );
289 }
290 if ( vExists )
291 {
292 gzprintf( pFile, "e " );
293 Vec_IntForEachEntry( vExists, VarId, i )
294 gzprintf( pFile, "%d ", fReadable? VarId : VarId+1 );
295 gzprintf( pFile, "0\n" );
296 }
297 for ( i = 0; i < p->nClauses; i++ )
298 {
299 for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
300 gzprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
301 gzprintf( pFile, "0\n" );
302 }
303 gzprintf( pFile, "\n" );
304 gzclose( pFile );
305 }
306
307 /**Function*************************************************************
308
309 Synopsis [Writes CNF into a file.]
310
311 Description []
312
313 SideEffects []
314
315 SeeAlso []
316
317 ***********************************************************************/
Cnf_DataWriteIntoFile(Cnf_Dat_t * p,char * pFileName,int fReadable,Vec_Int_t * vForAlls,Vec_Int_t * vExists)318 void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vForAlls, Vec_Int_t * vExists )
319 {
320 FILE * pFile;
321 int * pLit, * pStop, i, VarId;
322 if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) )
323 {
324 Cnf_DataWriteIntoFileGz( p, pFileName, fReadable, vForAlls, vExists );
325 return;
326 }
327 pFile = fopen( pFileName, "w" );
328 if ( pFile == NULL )
329 {
330 printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" );
331 return;
332 }
333 fprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
334 fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
335 if ( vForAlls )
336 {
337 fprintf( pFile, "a " );
338 Vec_IntForEachEntry( vForAlls, VarId, i )
339 fprintf( pFile, "%d ", fReadable? VarId : VarId+1 );
340 fprintf( pFile, "0\n" );
341 }
342 if ( vExists )
343 {
344 fprintf( pFile, "e " );
345 Vec_IntForEachEntry( vExists, VarId, i )
346 fprintf( pFile, "%d ", fReadable? VarId : VarId+1 );
347 fprintf( pFile, "0\n" );
348 }
349 for ( i = 0; i < p->nClauses; i++ )
350 {
351 for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
352 fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
353 fprintf( pFile, "0\n" );
354 }
355 fprintf( pFile, "\n" );
356 fclose( pFile );
357 }
358
359 /**Function*************************************************************
360
361 Synopsis [Writes CNF into a file.]
362
363 Description []
364
365 SideEffects []
366
367 SeeAlso []
368
369 ***********************************************************************/
Cnf_DataWriteIntoSolverInt(void * pSolver,Cnf_Dat_t * p,int nFrames,int fInit)370 void * Cnf_DataWriteIntoSolverInt( void * pSolver, Cnf_Dat_t * p, int nFrames, int fInit )
371 {
372 sat_solver * pSat = (sat_solver *)pSolver;
373 int i, f, status;
374 assert( nFrames > 0 );
375 assert( pSat );
376 // pSat = sat_solver_new();
377 sat_solver_setnvars( pSat, p->nVars * nFrames );
378 for ( i = 0; i < p->nClauses; i++ )
379 {
380 if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
381 {
382 sat_solver_delete( pSat );
383 return NULL;
384 }
385 }
386 if ( nFrames > 1 )
387 {
388 Aig_Obj_t * pObjLo, * pObjLi;
389 int nLitsAll, * pLits, Lits[2];
390 nLitsAll = 2 * p->nVars;
391 pLits = p->pClauses[0];
392 for ( f = 1; f < nFrames; f++ )
393 {
394 // add equality of register inputs/outputs for different timeframes
395 Aig_ManForEachLiLoSeq( p->pMan, pObjLi, pObjLo, i )
396 {
397 Lits[0] = (f-1)*nLitsAll + toLitCond( p->pVarNums[pObjLi->Id], 0 );
398 Lits[1] = f *nLitsAll + toLitCond( p->pVarNums[pObjLo->Id], 1 );
399 if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
400 {
401 sat_solver_delete( pSat );
402 return NULL;
403 }
404 Lits[0]++;
405 Lits[1]--;
406 if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
407 {
408 sat_solver_delete( pSat );
409 return NULL;
410 }
411 }
412 // add clauses for the next timeframe
413 for ( i = 0; i < p->nLiterals; i++ )
414 pLits[i] += nLitsAll;
415 for ( i = 0; i < p->nClauses; i++ )
416 {
417 if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
418 {
419 sat_solver_delete( pSat );
420 return NULL;
421 }
422 }
423 }
424 // return literals to their original state
425 nLitsAll = (f-1) * nLitsAll;
426 for ( i = 0; i < p->nLiterals; i++ )
427 pLits[i] -= nLitsAll;
428 }
429 if ( fInit )
430 {
431 Aig_Obj_t * pObjLo;
432 int Lits[1];
433 Aig_ManForEachLoSeq( p->pMan, pObjLo, i )
434 {
435 Lits[0] = toLitCond( p->pVarNums[pObjLo->Id], 1 );
436 if ( !sat_solver_addclause( pSat, Lits, Lits + 1 ) )
437 {
438 sat_solver_delete( pSat );
439 return NULL;
440 }
441 }
442 }
443 status = sat_solver_simplify(pSat);
444 if ( status == 0 )
445 {
446 sat_solver_delete( pSat );
447 return NULL;
448 }
449 return pSat;
450 }
451
452 /**Function*************************************************************
453
454 Synopsis [Writes CNF into a file.]
455
456 Description []
457
458 SideEffects []
459
460 SeeAlso []
461
462 ***********************************************************************/
Cnf_DataWriteIntoSolver(Cnf_Dat_t * p,int nFrames,int fInit)463 void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
464 {
465 return Cnf_DataWriteIntoSolverInt( sat_solver_new(), p, nFrames, fInit );
466 }
467
468 /**Function*************************************************************
469
470 Synopsis [Writes CNF into a file.]
471
472 Description []
473
474 SideEffects []
475
476 SeeAlso []
477
478 ***********************************************************************/
Cnf_DataWriteIntoSolver2(Cnf_Dat_t * p,int nFrames,int fInit)479 void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit )
480 {
481 sat_solver2 * pSat;
482 int i, f, status;
483 assert( nFrames > 0 );
484 pSat = sat_solver2_new();
485 sat_solver2_setnvars( pSat, p->nVars * nFrames );
486 for ( i = 0; i < p->nClauses; i++ )
487 {
488 if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1], 0 ) )
489 {
490 sat_solver2_delete( pSat );
491 return NULL;
492 }
493 }
494 if ( nFrames > 1 )
495 {
496 Aig_Obj_t * pObjLo, * pObjLi;
497 int nLitsAll, * pLits, Lits[2];
498 nLitsAll = 2 * p->nVars;
499 pLits = p->pClauses[0];
500 for ( f = 1; f < nFrames; f++ )
501 {
502 // add equality of register inputs/outputs for different timeframes
503 Aig_ManForEachLiLoSeq( p->pMan, pObjLi, pObjLo, i )
504 {
505 Lits[0] = (f-1)*nLitsAll + toLitCond( p->pVarNums[pObjLi->Id], 0 );
506 Lits[1] = f *nLitsAll + toLitCond( p->pVarNums[pObjLo->Id], 1 );
507 if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) )
508 {
509 sat_solver2_delete( pSat );
510 return NULL;
511 }
512 Lits[0]++;
513 Lits[1]--;
514 if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) )
515 {
516 sat_solver2_delete( pSat );
517 return NULL;
518 }
519 }
520 // add clauses for the next timeframe
521 for ( i = 0; i < p->nLiterals; i++ )
522 pLits[i] += nLitsAll;
523 for ( i = 0; i < p->nClauses; i++ )
524 {
525 if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1], 0 ) )
526 {
527 sat_solver2_delete( pSat );
528 return NULL;
529 }
530 }
531 }
532 // return literals to their original state
533 nLitsAll = (f-1) * nLitsAll;
534 for ( i = 0; i < p->nLiterals; i++ )
535 pLits[i] -= nLitsAll;
536 }
537 if ( fInit )
538 {
539 Aig_Obj_t * pObjLo;
540 int Lits[1];
541 Aig_ManForEachLoSeq( p->pMan, pObjLo, i )
542 {
543 Lits[0] = toLitCond( p->pVarNums[pObjLo->Id], 1 );
544 if ( !sat_solver2_addclause( pSat, Lits, Lits + 1, 0 ) )
545 {
546 sat_solver2_delete( pSat );
547 return NULL;
548 }
549 }
550 }
551 status = sat_solver2_simplify(pSat);
552 if ( status == 0 )
553 {
554 sat_solver2_delete( pSat );
555 return NULL;
556 }
557 return pSat;
558 }
559
560 /**Function*************************************************************
561
562 Synopsis [Adds the OR-clause.]
563
564 Description []
565
566 SideEffects []
567
568 SeeAlso []
569
570 ***********************************************************************/
Cnf_DataWriteOrClause(void * p,Cnf_Dat_t * pCnf)571 int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf )
572 {
573 sat_solver * pSat = (sat_solver *)p;
574 Aig_Obj_t * pObj;
575 int i, * pLits;
576 pLits = ABC_ALLOC( int, Aig_ManCoNum(pCnf->pMan) );
577 Aig_ManForEachCo( pCnf->pMan, pObj, i )
578 pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
579 if ( !sat_solver_addclause( pSat, pLits, pLits + Aig_ManCoNum(pCnf->pMan) ) )
580 {
581 ABC_FREE( pLits );
582 return 0;
583 }
584 ABC_FREE( pLits );
585 return 1;
586 }
587
588 /**Function*************************************************************
589
590 Synopsis [Adds the OR-clause.]
591
592 Description []
593
594 SideEffects []
595
596 SeeAlso []
597
598 ***********************************************************************/
Cnf_DataWriteOrClause2(void * p,Cnf_Dat_t * pCnf)599 int Cnf_DataWriteOrClause2( void * p, Cnf_Dat_t * pCnf )
600 {
601 sat_solver2 * pSat = (sat_solver2 *)p;
602 Aig_Obj_t * pObj;
603 int i, * pLits;
604 pLits = ABC_ALLOC( int, Aig_ManCoNum(pCnf->pMan) );
605 Aig_ManForEachCo( pCnf->pMan, pObj, i )
606 pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
607 if ( !sat_solver2_addclause( pSat, pLits, pLits + Aig_ManCoNum(pCnf->pMan), 0 ) )
608 {
609 ABC_FREE( pLits );
610 return 0;
611 }
612 ABC_FREE( pLits );
613 return 1;
614 }
615
616 /**Function*************************************************************
617
618 Synopsis [Adds the OR-clause.]
619
620 Description []
621
622 SideEffects []
623
624 SeeAlso []
625
626 ***********************************************************************/
Cnf_DataWriteAndClauses(void * p,Cnf_Dat_t * pCnf)627 int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf )
628 {
629 sat_solver * pSat = (sat_solver *)p;
630 Aig_Obj_t * pObj;
631 int i, Lit;
632 Aig_ManForEachCo( pCnf->pMan, pObj, i )
633 {
634 Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
635 if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
636 return 0;
637 }
638 return 1;
639 }
640
641 /**Function*************************************************************
642
643 Synopsis [Transforms polarity of the internal veriables.]
644
645 Description []
646
647 SideEffects []
648
649 SeeAlso []
650
651 ***********************************************************************/
Cnf_DataTranformPolarity(Cnf_Dat_t * pCnf,int fTransformPos)652 void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf, int fTransformPos )
653 {
654 Aig_Obj_t * pObj;
655 int * pVarToPol;
656 int i, iVar;
657 // create map from the variable number to its polarity
658 pVarToPol = ABC_CALLOC( int, pCnf->nVars );
659 Aig_ManForEachObj( pCnf->pMan, pObj, i )
660 {
661 if ( !fTransformPos && Aig_ObjIsCo(pObj) )
662 continue;
663 if ( pCnf->pVarNums[pObj->Id] >= 0 )
664 pVarToPol[ pCnf->pVarNums[pObj->Id] ] = pObj->fPhase;
665 }
666 // transform literals
667 for ( i = 0; i < pCnf->nLiterals; i++ )
668 {
669 iVar = lit_var(pCnf->pClauses[0][i]);
670 assert( iVar < pCnf->nVars );
671 if ( pVarToPol[iVar] )
672 pCnf->pClauses[0][i] = lit_neg( pCnf->pClauses[0][i] );
673 }
674 ABC_FREE( pVarToPol );
675 }
676
677 /**Function*************************************************************
678
679 Synopsis [Adds constraints for the two-input AND-gate.]
680
681 Description []
682
683 SideEffects []
684
685 SeeAlso []
686
687 ***********************************************************************/
Cnf_DataAddXorClause(void * pSat,int iVarA,int iVarB,int iVarC)688 int Cnf_DataAddXorClause( void * pSat, int iVarA, int iVarB, int iVarC )
689 {
690 lit Lits[3];
691 assert( iVarA > 0 && iVarB > 0 && iVarC > 0 );
692
693 Lits[0] = toLitCond( iVarA, 1 );
694 Lits[1] = toLitCond( iVarB, 1 );
695 Lits[2] = toLitCond( iVarC, 1 );
696 if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) )
697 return 0;
698
699 Lits[0] = toLitCond( iVarA, 1 );
700 Lits[1] = toLitCond( iVarB, 0 );
701 Lits[2] = toLitCond( iVarC, 0 );
702 if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) )
703 return 0;
704
705 Lits[0] = toLitCond( iVarA, 0 );
706 Lits[1] = toLitCond( iVarB, 1 );
707 Lits[2] = toLitCond( iVarC, 0 );
708 if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) )
709 return 0;
710
711 Lits[0] = toLitCond( iVarA, 0 );
712 Lits[1] = toLitCond( iVarB, 0 );
713 Lits[2] = toLitCond( iVarC, 1 );
714 if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) )
715 return 0;
716
717 return 1;
718 }
719
720 ////////////////////////////////////////////////////////////////////////
721 /// END OF FILE ///
722 ////////////////////////////////////////////////////////////////////////
723
724
725 ABC_NAMESPACE_IMPL_END
726
727