abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cnfMan.c
Go to the documentation of this file.
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 
33 static inline int Cnf_Lit2Var( int Lit ) { return (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+1; }
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 [Writes CNF into a file.]
197 
198  Description []
199 
200  SideEffects []
201 
202  SeeAlso []
203 
204 ***********************************************************************/
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 }
218 
219 /**Function*************************************************************
220 
221  Synopsis [Writes CNF into a file.]
222 
223  Description []
224 
225  SideEffects []
226 
227  SeeAlso []
228 
229 ***********************************************************************/
230 void Cnf_DataFlipLastLiteral( Cnf_Dat_t * p )
231 {
232  p->pClauses[0][p->nLiterals-1] = lit_neg( p->pClauses[0][p->nLiterals-1] );
233 }
234 
235 /**Function*************************************************************
236 
237  Synopsis [Writes CNF into a file.]
238 
239  Description []
240 
241  SideEffects []
242 
243  SeeAlso []
244 
245 ***********************************************************************/
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, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 
memset
char * memset()
Cnf_DataWriteIntoSolver
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:463
Cnf_Lit2Var
static ABC_NAMESPACE_IMPL_START int Cnf_Lit2Var(int Lit)
DECLARATIONS ///.
Definition: cnfMan.c:33
Cnf_DataWriteIntoSolverInt
void * Cnf_DataWriteIntoSolverInt(void *pSolver, Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:370
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
Cnf_DataAddXorClause
int Cnf_DataAddXorClause(void *pSat, int iVarA, int iVarB, int iVarC)
Definition: cnfMan.c:688
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Cnf_Dat_t_::nClauses
int nClauses
Definition: cnf.h:61
lit_var
static int lit_var(lit l)
Definition: satVec.h:145
sat_solver2_delete
void sat_solver2_delete(sat_solver2 *s)
Definition: satSolver2.c:1225
sat_solver2_t
Definition: satSolver2.h:90
Cnf_Dat_t_::nVars
int nVars
Definition: cnf.h:59
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Cnf_Dat_t_::vMapping
Vec_Int_t * vMapping
Definition: cnf.h:67
Cnf_Dat_t_::pClaPols
unsigned char * pClaPols
Definition: cnf.h:66
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Cnf_DataDup
Cnf_Dat_t * Cnf_DataDup(Cnf_Dat_t *p)
Definition: cnfMan.c:157
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition: cnf.h:63
memcpy
char * memcpy()
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
gzclose
ABC_NAMESPACE_IMPL_START int ZEXPORT gzclose(gzFile file)
Definition: gzclose.c:18
sat_solver2_new
sat_solver2 * sat_solver2_new(void)
Definition: satSolver2.c:1109
Abc_TruthWordNum
static int Abc_TruthWordNum(int nVars)
Definition: abc_global.h:256
sat_solver2_addclause
int sat_solver2_addclause(sat_solver2 *s, lit *begin, lit *end, int Id)
Definition: satSolver2.c:1287
Cnf_Dat_t_::pMan
Aig_Man_t * pMan
Definition: cnf.h:58
Cnf_Dat_t_
Definition: cnf.h:56
gzFile
voidp gzFile
Definition: zlib.h:1173
sat_solver2_setnvars
void sat_solver2_setnvars(sat_solver2 *s, int n)
Definition: satSolver2.c:1170
lit
int lit
Definition: satVec.h:130
Cnf_DataWriteAndClauses
int Cnf_DataWriteAndClauses(void *p, Cnf_Dat_t *pCnf)
Definition: cnfMan.c:627
Cnf_Dat_t_::pObj2Clause
int * pObj2Clause
Definition: cnf.h:64
Cnf_DataLift
void Cnf_DataLift(Cnf_Dat_t *p, int nVarsPlus)
Definition: cnfMan.c:205
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Cnf_DataWriteIntoSolver2
void * Cnf_DataWriteIntoSolver2(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:479
Cnf_ReadMsops
void Cnf_ReadMsops(char **ppSopSizes, char ***ppSops)
FUNCTION DEFINITIONS ///.
Definition: cnfData.c:4537
Cnf_Dat_t_::pClauses
int ** pClauses
Definition: cnf.h:62
Cnf_Lit2Var2
static int Cnf_Lit2Var2(int Lit)
Definition: cnfMan.c:34
Cnf_DataPrint
void Cnf_DataPrint(Cnf_Dat_t *p, int fReadable)
Definition: cnfMan.c:246
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
sat_solver2_simplify
int sat_solver2_simplify(sat_solver2 *s)
Definition: satSolver2.c:996
Aig_ManForEachLiLoSeq
#define Aig_ManForEachLiLoSeq(p, pObjLi, pObjLo, k)
Definition: aig.h:450
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
gzprintf
int ZEXPORTVA gzprintf(gzFile file, const char *format, int a1, int a2, int a3, int a4, int a5, int a6, int a7, int a8, int a9, int a10, int a11, int a12, int a13, int a14, int a15, int a16, int a17, int a18, int a19, int a20)
Definition: gzwrite.c:347
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Cnf_ManStart
Cnf_Man_t * Cnf_ManStart()
FUNCTION DEFINITIONS ///.
Definition: cnfMan.c:51
Cnf_DataWriteOrClause2
int Cnf_DataWriteOrClause2(void *p, Cnf_Dat_t *pCnf)
Definition: cnfMan.c:599
gzopen
gzFile ZEXPORT gzopen(const char *path, const char *mode)
Definition: gzlib.c:198
sat_solver_simplify
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
Cnf_DataWriteIntoFileGz
void Cnf_DataWriteIntoFileGz(Cnf_Dat_t *p, char *pFileName, int fReadable, Vec_Int_t *vForAlls, Vec_Int_t *vExists)
Definition: cnfMan.c:271
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Cnf_DataTranformPolarity
void Cnf_DataTranformPolarity(Cnf_Dat_t *pCnf, int fTransformPos)
Definition: cnfMan.c:652
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Aig_MmFlexStart
Aig_MmFlex_t * Aig_MmFlexStart()
Definition: aigMem.c:305
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Aig_MmFlexStop
void Aig_MmFlexStop(Aig_MmFlex_t *p, int fVerbose)
Definition: aigMem.c:337
Aig_ManForEachLoSeq
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition: aig.h:441
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
strncmp
int strncmp()
sat_solver_t
Definition: satSolver.h:91
Cnf_DataAlloc
Cnf_Dat_t * Cnf_DataAlloc(Aig_Man_t *pAig, int nVars, int nClauses, int nLiterals)
Definition: cnfMan.c:126
assert
#define assert(ex)
Definition: util_old.h:213
strlen
int strlen()
Cnf_DataFlipLastLiteral
void Cnf_DataFlipLastLiteral(Cnf_Dat_t *p)
Definition: cnfMan.c:230
Cnf_ManStop
void Cnf_ManStop(Cnf_Man_t *p)
Definition: cnfMan.c:82
Cnf_DataWriteIntoFile
void Cnf_DataWriteIntoFile(Cnf_Dat_t *p, char *pFileName, int fReadable, Vec_Int_t *vForAlls, Vec_Int_t *vExists)
Definition: cnfMan.c:318
Cnf_DataCollectPiSatNums
Vec_Int_t * Cnf_DataCollectPiSatNums(Cnf_Dat_t *pCnf, Aig_Man_t *p)
Definition: cnfMan.c:104
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Cnf_Man_t
typedefABC_NAMESPACE_HEADER_START struct Cnf_Man_t_ Cnf_Man_t
INCLUDES ///.
Definition: cnf.h:51
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_DataWriteOrClause
int Cnf_DataWriteOrClause(void *p, Cnf_Dat_t *pCnf)
Definition: cnfMan.c:571
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Cnf_Dat_t_::pObj2Count
int * pObj2Count
Definition: cnf.h:65