abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
abcSat.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [abcSat.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Network and node package.]
8 
9  Synopsis [Procedures to solve the miter using the internal SAT sat_solver.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: abcSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "base/abc/abc.h"
22 #include "base/main/main.h"
23 #include "base/cmd/cmd.h"
24 #include "sat/bsat/satSolver.h"
25 #include "misc/extra/extraBdd.h"
26 
27 ABC_NAMESPACE_IMPL_START
28 
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// DECLARATIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 static sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes );
35 extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
36 static int nMuxes;
37 
38 ////////////////////////////////////////////////////////////////////////
39 /// FUNCTION DEFINITIONS ///
40 ////////////////////////////////////////////////////////////////////////
41 
42 /**Function*************************************************************
43 
44  Synopsis [Attempts to solve the miter using an internal SAT sat_solver.]
45 
46  Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.]
47 
48  SideEffects []
49 
50  SeeAlso []
51 
52 ***********************************************************************/
53 int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fVerbose, ABC_INT64_T * pNumConfs, ABC_INT64_T * pNumInspects )
54 {
55  sat_solver * pSat;
56  lbool status;
57  int RetValue;
58  abctime clk;
59 
60  if ( pNumConfs )
61  *pNumConfs = 0;
62  if ( pNumInspects )
63  *pNumInspects = 0;
64 
65  assert( Abc_NtkLatchNum(pNtk) == 0 );
66 
67 // if ( Abc_NtkPoNum(pNtk) > 1 )
68 // fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
69 
70  // load clauses into the sat_solver
71  clk = Abc_Clock();
72  pSat = (sat_solver *)Abc_NtkMiterSatCreate( pNtk, 0 );
73  if ( pSat == NULL )
74  return 1;
75 //printf( "%d \n", pSat->clauses.size );
76 //sat_solver_delete( pSat );
77 //return 1;
78 
79 // printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
80 // ABC_PRT( "Time", Abc_Clock() - clk );
81 
82  // simplify the problem
83  clk = Abc_Clock();
84  status = sat_solver_simplify(pSat);
85 // printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
86 // ABC_PRT( "Time", Abc_Clock() - clk );
87  if ( status == 0 )
88  {
89  sat_solver_delete( pSat );
90 // printf( "The problem is UNSATISFIABLE after simplification.\n" );
91  return 1;
92  }
93 
94  // solve the miter
95  clk = Abc_Clock();
96  if ( fVerbose )
97  pSat->verbosity = 1;
98  status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
99  if ( status == l_Undef )
100  {
101 // printf( "The problem timed out.\n" );
102  RetValue = -1;
103  }
104  else if ( status == l_True )
105  {
106 // printf( "The problem is SATISFIABLE.\n" );
107  RetValue = 0;
108  }
109  else if ( status == l_False )
110  {
111 // printf( "The problem is UNSATISFIABLE.\n" );
112  RetValue = 1;
113  }
114  else
115  assert( 0 );
116 // ABC_PRT( "SAT sat_solver time", Abc_Clock() - clk );
117 // printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts );
118 
119  // if the problem is SAT, get the counterexample
120  if ( status == l_True )
121  {
122 // Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk );
123  Vec_Int_t * vCiIds = Abc_NtkGetCiSatVarNums( pNtk );
124  pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
125  Vec_IntFree( vCiIds );
126  }
127  // free the sat_solver
128  if ( fVerbose )
129  Sat_SolverPrintStats( stdout, pSat );
130 
131  if ( pNumConfs )
132  *pNumConfs = (int)pSat->stats.conflicts;
133  if ( pNumInspects )
134  *pNumInspects = (int)pSat->stats.inspects;
135 
136 sat_solver_store_write( pSat, "trace.cnf" );
137 sat_solver_store_free( pSat );
138 
139  sat_solver_delete( pSat );
140  return RetValue;
141 }
142 
143 /**Function*************************************************************
144 
145  Synopsis [Returns the array of CI IDs.]
146 
147  Description []
148 
149  SideEffects []
150 
151  SeeAlso []
152 
153 ***********************************************************************/
154 Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk )
155 {
156  Vec_Int_t * vCiIds;
157  Abc_Obj_t * pObj;
158  int i;
159  vCiIds = Vec_IntAlloc( Abc_NtkCiNum(pNtk) );
160  Abc_NtkForEachCi( pNtk, pObj, i )
161  Vec_IntPush( vCiIds, (int)(ABC_PTRINT_T)pObj->pCopy );
162  return vCiIds;
163 }
164 
165 
166 
167 /**Function*************************************************************
168 
169  Synopsis [Adds trivial clause.]
170 
171  Description []
172 
173  SideEffects []
174 
175  SeeAlso []
176 
177 ***********************************************************************/
178 int Abc_NtkClauseTriv( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
179 {
180 //printf( "Adding triv %d. %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->sat_solver_stats.clauses );
181  vVars->nSize = 0;
182  Vec_IntPush( vVars, toLitCond( (int)(ABC_PTRINT_T)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
183 // Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
184  return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
185 }
186 
187 /**Function*************************************************************
188 
189  Synopsis [Adds trivial clause.]
190 
191  Description []
192 
193  SideEffects []
194 
195  SeeAlso []
196 
197 ***********************************************************************/
198 int Abc_NtkClauseTop( sat_solver * pSat, Vec_Ptr_t * vNodes, Vec_Int_t * vVars )
199 {
200  Abc_Obj_t * pNode;
201  int i;
202 //printf( "Adding triv %d. %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->sat_solver_stats.clauses );
203  vVars->nSize = 0;
204  Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
205  Vec_IntPush( vVars, toLitCond( (int)(ABC_PTRINT_T)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
206 // Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
207  return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
208 }
209 
210 /**Function*************************************************************
211 
212  Synopsis [Adds trivial clause.]
213 
214  Description []
215 
216  SideEffects []
217 
218  SeeAlso []
219 
220 ***********************************************************************/
221 int Abc_NtkClauseAnd( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_Int_t * vVars )
222 {
223  int fComp1, Var, Var1, i;
224 //printf( "Adding AND %d. (%d) %d\n", pNode->Id, vSuper->nSize+1, (int)pSat->sat_solver_stats.clauses );
225 
226  assert( !Abc_ObjIsComplement( pNode ) );
227  assert( Abc_ObjIsNode( pNode ) );
228 
229 // nVars = sat_solver_nvars(pSat);
230  Var = (int)(ABC_PTRINT_T)pNode->pCopy;
231 // Var = pNode->Id;
232 
233 // assert( Var < nVars );
234  for ( i = 0; i < vSuper->nSize; i++ )
235  {
236  // get the predecessor nodes
237  // get the complemented attributes of the nodes
238  fComp1 = Abc_ObjIsComplement((Abc_Obj_t *)vSuper->pArray[i]);
239  // determine the variable numbers
240  Var1 = (int)(ABC_PTRINT_T)Abc_ObjRegular((Abc_Obj_t *)vSuper->pArray[i])->pCopy;
241 // Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->Id;
242 
243  // check that the variables are in the SAT manager
244 // assert( Var1 < nVars );
245 
246  // suppose the AND-gate is A * B = C
247  // add !A => !C or A + !C
248  // fprintf( pFile, "%d %d 0%c", Var1, -Var, 10 );
249  vVars->nSize = 0;
250  Vec_IntPush( vVars, toLitCond(Var1, fComp1) );
251  Vec_IntPush( vVars, toLitCond(Var, 1 ) );
252  if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
253  return 0;
254  }
255 
256  // add A & B => C or !A + !B + C
257 // fprintf( pFile, "%d %d %d 0%c", -Var1, -Var2, Var, 10 );
258  vVars->nSize = 0;
259  for ( i = 0; i < vSuper->nSize; i++ )
260  {
261  // get the predecessor nodes
262  // get the complemented attributes of the nodes
263  fComp1 = Abc_ObjIsComplement((Abc_Obj_t *)vSuper->pArray[i]);
264  // determine the variable numbers
265  Var1 = (int)(ABC_PTRINT_T)Abc_ObjRegular((Abc_Obj_t *)vSuper->pArray[i])->pCopy;
266 // Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->Id;
267  // add this variable to the array
268  Vec_IntPush( vVars, toLitCond(Var1, !fComp1) );
269  }
270  Vec_IntPush( vVars, toLitCond(Var, 0) );
271  return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
272 }
273 
274 /**Function*************************************************************
275 
276  Synopsis [Adds trivial clause.]
277 
278  Description []
279 
280  SideEffects []
281 
282  SeeAlso []
283 
284 ***********************************************************************/
285 int Abc_NtkClauseMux( sat_solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_Obj_t * pNodeT, Abc_Obj_t * pNodeE, Vec_Int_t * vVars )
286 {
287  int VarF, VarI, VarT, VarE, fCompT, fCompE;
288 //printf( "Adding mux %d. %d\n", pNode->Id, (int)pSat->sat_solver_stats.clauses );
289 
290  assert( !Abc_ObjIsComplement( pNode ) );
291  assert( Abc_NodeIsMuxType( pNode ) );
292  // get the variable numbers
293  VarF = (int)(ABC_PTRINT_T)pNode->pCopy;
294  VarI = (int)(ABC_PTRINT_T)pNodeC->pCopy;
295  VarT = (int)(ABC_PTRINT_T)Abc_ObjRegular(pNodeT)->pCopy;
296  VarE = (int)(ABC_PTRINT_T)Abc_ObjRegular(pNodeE)->pCopy;
297 // VarF = (int)pNode->Id;
298 // VarI = (int)pNodeC->Id;
299 // VarT = (int)Abc_ObjRegular(pNodeT)->Id;
300 // VarE = (int)Abc_ObjRegular(pNodeE)->Id;
301 
302  // get the complementation flags
303  fCompT = Abc_ObjIsComplement(pNodeT);
304  fCompE = Abc_ObjIsComplement(pNodeE);
305 
306  // f = ITE(i, t, e)
307  // i' + t' + f
308  // i' + t + f'
309  // i + e' + f
310  // i + e + f'
311  // create four clauses
312  vVars->nSize = 0;
313  Vec_IntPush( vVars, toLitCond(VarI, 1) );
314  Vec_IntPush( vVars, toLitCond(VarT, 1^fCompT) );
315  Vec_IntPush( vVars, toLitCond(VarF, 0) );
316  if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
317  return 0;
318  vVars->nSize = 0;
319  Vec_IntPush( vVars, toLitCond(VarI, 1) );
320  Vec_IntPush( vVars, toLitCond(VarT, 0^fCompT) );
321  Vec_IntPush( vVars, toLitCond(VarF, 1) );
322  if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
323  return 0;
324  vVars->nSize = 0;
325  Vec_IntPush( vVars, toLitCond(VarI, 0) );
326  Vec_IntPush( vVars, toLitCond(VarE, 1^fCompE) );
327  Vec_IntPush( vVars, toLitCond(VarF, 0) );
328  if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
329  return 0;
330  vVars->nSize = 0;
331  Vec_IntPush( vVars, toLitCond(VarI, 0) );
332  Vec_IntPush( vVars, toLitCond(VarE, 0^fCompE) );
333  Vec_IntPush( vVars, toLitCond(VarF, 1) );
334  if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
335  return 0;
336 
337  if ( VarT == VarE )
338  {
339 // assert( fCompT == !fCompE );
340  return 1;
341  }
342 
343  // two additional clauses
344  // t' & e' -> f' t + e + f'
345  // t & e -> f t' + e' + f
346  vVars->nSize = 0;
347  Vec_IntPush( vVars, toLitCond(VarT, 0^fCompT) );
348  Vec_IntPush( vVars, toLitCond(VarE, 0^fCompE) );
349  Vec_IntPush( vVars, toLitCond(VarF, 1) );
350  if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
351  return 0;
352  vVars->nSize = 0;
353  Vec_IntPush( vVars, toLitCond(VarT, 1^fCompT) );
354  Vec_IntPush( vVars, toLitCond(VarE, 1^fCompE) );
355  Vec_IntPush( vVars, toLitCond(VarF, 0) );
356  return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
357 }
358 
359 /**Function*************************************************************
360 
361  Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]
362 
363  Description []
364 
365  SideEffects []
366 
367  SeeAlso []
368 
369 ***********************************************************************/
370 int Abc_NtkCollectSupergate_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, int fFirst, int fStopAtMux )
371 {
372  int RetValue1, RetValue2, i;
373  // check if the node is visited
374  if ( Abc_ObjRegular(pNode)->fMarkB )
375  {
376  // check if the node occurs in the same polarity
377  for ( i = 0; i < vSuper->nSize; i++ )
378  if ( vSuper->pArray[i] == pNode )
379  return 1;
380  // check if the node is present in the opposite polarity
381  for ( i = 0; i < vSuper->nSize; i++ )
382  if ( vSuper->pArray[i] == Abc_ObjNot(pNode) )
383  return -1;
384  assert( 0 );
385  return 0;
386  }
387  // if the new node is complemented or a PI, another gate begins
388  if ( !fFirst )
389  if ( Abc_ObjIsComplement(pNode) || !Abc_ObjIsNode(pNode) || Abc_ObjFanoutNum(pNode) > 1 || (fStopAtMux && Abc_NodeIsMuxType(pNode)) )
390  {
391  Vec_PtrPush( vSuper, pNode );
392  Abc_ObjRegular(pNode)->fMarkB = 1;
393  return 0;
394  }
395  assert( !Abc_ObjIsComplement(pNode) );
396  assert( Abc_ObjIsNode(pNode) );
397  // go through the branches
398  RetValue1 = Abc_NtkCollectSupergate_rec( Abc_ObjChild0(pNode), vSuper, 0, fStopAtMux );
399  RetValue2 = Abc_NtkCollectSupergate_rec( Abc_ObjChild1(pNode), vSuper, 0, fStopAtMux );
400  if ( RetValue1 == -1 || RetValue2 == -1 )
401  return -1;
402  // return 1 if at least one branch has a duplicate
403  return RetValue1 || RetValue2;
404 }
405 
406 /**Function*************************************************************
407 
408  Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]
409 
410  Description []
411 
412  SideEffects []
413 
414  SeeAlso []
415 
416 ***********************************************************************/
417 void Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNodes )
418 {
419  int RetValue, i;
420  assert( !Abc_ObjIsComplement(pNode) );
421  // collect the nodes in the implication supergate
422  Vec_PtrClear( vNodes );
423  RetValue = Abc_NtkCollectSupergate_rec( pNode, vNodes, 1, fStopAtMux );
424  assert( vNodes->nSize > 1 );
425  // unmark the visited nodes
426  for ( i = 0; i < vNodes->nSize; i++ )
427  Abc_ObjRegular((Abc_Obj_t *)vNodes->pArray[i])->fMarkB = 0;
428  // if we found the node and its complement in the same implication supergate,
429  // return empty set of nodes (meaning that we should use constant-0 node)
430  if ( RetValue == -1 )
431  vNodes->nSize = 0;
432 }
433 
434 
435 /**Function*************************************************************
436 
437  Synopsis [Computes the factor of the node.]
438 
439  Description []
440 
441  SideEffects []
442 
443  SeeAlso []
444 
445 ***********************************************************************/
446 int Abc_NtkNodeFactor( Abc_Obj_t * pObj, int nLevelMax )
447 {
448 // nLevelMax = ((nLevelMax)/2)*3;
449  assert( (int)pObj->Level <= nLevelMax );
450 // return (int)(100000000.0 * pow(0.999, nLevelMax - pObj->Level));
451  return (int)(100000000.0 * (1 + 0.01 * pObj->Level));
452 // return (int)(100000000.0 / ((nLevelMax)/2)*3 - pObj->Level);
453 }
454 
455 /**Function*************************************************************
456 
457  Synopsis [Sets up the SAT sat_solver.]
458 
459  Description []
460 
461  SideEffects []
462 
463  SeeAlso []
464 
465 ***********************************************************************/
466 int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
467 {
468  Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE;
469  Vec_Ptr_t * vNodes, * vSuper;
470  Vec_Int_t * vVars;
471  int i, k, fUseMuxes = 1;
472 // int fOrderCiVarsFirst = 0;
473  int RetValue = 0;
474 
475  assert( Abc_NtkIsStrash(pNtk) );
476 
477  // clean the CI node pointers
478  Abc_NtkForEachCi( pNtk, pNode, i )
479  pNode->pCopy = NULL;
480 
481  // start the data structures
482  vNodes = Vec_PtrAlloc( 1000 ); // the nodes corresponding to vars in the sat_solver
483  vSuper = Vec_PtrAlloc( 100 ); // the nodes belonging to the given implication supergate
484  vVars = Vec_IntAlloc( 100 ); // the temporary array for variables in the clause
485 
486  // add the clause for the constant node
487  pNode = Abc_AigConst1(pNtk);
488  pNode->fMarkA = 1;
489  pNode->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)vNodes->nSize;
490  Vec_PtrPush( vNodes, pNode );
491  Abc_NtkClauseTriv( pSat, pNode, vVars );
492 /*
493  // add the PI variables first
494  Abc_NtkForEachCi( pNtk, pNode, i )
495  {
496  pNode->fMarkA = 1;
497  pNode->pCopy = (Abc_Obj_t *)vNodes->nSize;
498  Vec_PtrPush( vNodes, pNode );
499  }
500 */
501  // collect the nodes that need clauses and top-level assignments
502  Vec_PtrClear( vSuper );
503  Abc_NtkForEachCo( pNtk, pNode, i )
504  {
505  // get the fanin
506  pFanin = Abc_ObjFanin0(pNode);
507  // create the node's variable
508  if ( pFanin->fMarkA == 0 )
509  {
510  pFanin->fMarkA = 1;
511  pFanin->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)vNodes->nSize;
512  Vec_PtrPush( vNodes, pFanin );
513  }
514  // add the trivial clause
515  Vec_PtrPush( vSuper, Abc_ObjChild0(pNode) );
516  }
517  if ( !Abc_NtkClauseTop( pSat, vSuper, vVars ) )
518  goto Quits;
519 
520 
521  // add the clauses
522  Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
523  {
524  assert( !Abc_ObjIsComplement(pNode) );
525  if ( !Abc_AigNodeIsAnd(pNode) )
526  continue;
527 //printf( "%d ", pNode->Id );
528 
529  // add the clauses
530  if ( fUseMuxes && Abc_NodeIsMuxType(pNode) )
531  {
532  nMuxes++;
533 
534  pNodeC = Abc_NodeRecognizeMux( pNode, &pNodeT, &pNodeE );
535  Vec_PtrClear( vSuper );
536  Vec_PtrPush( vSuper, pNodeC );
537  Vec_PtrPush( vSuper, pNodeT );
538  Vec_PtrPush( vSuper, pNodeE );
539  // add the fanin nodes to explore
540  Vec_PtrForEachEntry( Abc_Obj_t *, vSuper, pFanin, k )
541  {
542  pFanin = Abc_ObjRegular(pFanin);
543  if ( pFanin->fMarkA == 0 )
544  {
545  pFanin->fMarkA = 1;
546  pFanin->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)vNodes->nSize;
547  Vec_PtrPush( vNodes, pFanin );
548  }
549  }
550  // add the clauses
551  if ( !Abc_NtkClauseMux( pSat, pNode, pNodeC, pNodeT, pNodeE, vVars ) )
552  goto Quits;
553  }
554  else
555  {
556  // get the supergate
557  Abc_NtkCollectSupergate( pNode, fUseMuxes, vSuper );
558  // add the fanin nodes to explore
559  Vec_PtrForEachEntry( Abc_Obj_t *, vSuper, pFanin, k )
560  {
561  pFanin = Abc_ObjRegular(pFanin);
562  if ( pFanin->fMarkA == 0 )
563  {
564  pFanin->fMarkA = 1;
565  pFanin->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)vNodes->nSize;
566  Vec_PtrPush( vNodes, pFanin );
567  }
568  }
569  // add the clauses
570  if ( vSuper->nSize == 0 )
571  {
572  if ( !Abc_NtkClauseTriv( pSat, Abc_ObjNot(pNode), vVars ) )
573 // if ( !Abc_NtkClauseTriv( pSat, pNode, vVars ) )
574  goto Quits;
575  }
576  else
577  {
578  if ( !Abc_NtkClauseAnd( pSat, pNode, vSuper, vVars ) )
579  goto Quits;
580  }
581  }
582  }
583 /*
584  // set preferred variables
585  if ( fOrderCiVarsFirst )
586  {
587  int * pPrefVars = ABC_ALLOC( int, Abc_NtkCiNum(pNtk) );
588  int nVars = 0;
589  Abc_NtkForEachCi( pNtk, pNode, i )
590  {
591  if ( pNode->fMarkA == 0 )
592  continue;
593  pPrefVars[nVars++] = (int)pNode->pCopy;
594  }
595  nVars = Abc_MinInt( nVars, 10 );
596  ASat_SolverSetPrefVars( pSat, pPrefVars, nVars );
597  }
598 */
599 /*
600  Abc_NtkForEachObj( pNtk, pNode, i )
601  {
602  if ( !pNode->fMarkA )
603  continue;
604  printf( "%10s : ", Abc_ObjName(pNode) );
605  printf( "%3d\n", (int)pNode->pCopy );
606  }
607  printf( "\n" );
608 */
609  RetValue = 1;
610 Quits :
611  // delete
612  Vec_IntFree( vVars );
613  Vec_PtrFree( vNodes );
614  Vec_PtrFree( vSuper );
615  return RetValue;
616 }
617 
618 /**Function*************************************************************
619 
620  Synopsis [Sets up the SAT sat_solver.]
621 
622  Description []
623 
624  SideEffects []
625 
626  SeeAlso []
627 
628 ***********************************************************************/
629 void * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes )
630 {
631  sat_solver * pSat;
632  Abc_Obj_t * pNode;
633  int RetValue, i; //, clk = Abc_Clock();
634 
635  assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsBddLogic(pNtk) );
636  if ( Abc_NtkIsBddLogic(pNtk) )
637  return Abc_NtkMiterSatCreateLogic(pNtk, fAllPrimes);
638 
639  nMuxes = 0;
640  pSat = sat_solver_new();
641 //sat_solver_store_alloc( pSat );
642  RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk );
643 sat_solver_store_mark_roots( pSat );
644 
645  Abc_NtkForEachObj( pNtk, pNode, i )
646  pNode->fMarkA = 0;
647 // ASat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
648  if ( RetValue == 0 )
649  {
650  sat_solver_delete(pSat);
651  return NULL;
652  }
653 // printf( "Ands = %6d. Muxes = %6d (%5.2f %%). ", Abc_NtkNodeNum(pNtk), nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
654 // ABC_PRT( "Creating sat_solver", Abc_Clock() - clk );
655  return pSat;
656 }
657 
658 
659 
660 
661 /**Function*************************************************************
662 
663  Synopsis [Adds clauses for the internal node.]
664 
665  Description []
666 
667  SideEffects []
668 
669  SeeAlso []
670 
671 ***********************************************************************/
672 int Abc_NodeAddClauses( sat_solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
673 {
674  Abc_Obj_t * pFanin;
675  int i, c, nFanins;
676  int RetValue;
677  char * pCube;
678 
679  nFanins = Abc_ObjFaninNum( pNode );
680  assert( nFanins == Abc_SopGetVarNum( pSop0 ) );
681 
682 // if ( nFanins == 0 )
683  if ( Cudd_Regular((Abc_Obj_t *)pNode->pData) == Cudd_ReadOne((DdManager *)pNode->pNtk->pManFunc) )
684  {
685  vVars->nSize = 0;
686 // if ( Abc_SopIsConst1(pSop1) )
687  if ( !Cudd_IsComplement(pNode->pData) )
688  Vec_IntPush( vVars, toLit(pNode->Id) );
689  else
690  Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) );
691  RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
692  if ( !RetValue )
693  {
694  printf( "The CNF is trivially UNSAT.\n" );
695  return 0;
696  }
697  return 1;
698  }
699 
700  // add clauses for the negative phase
701  for ( c = 0; ; c++ )
702  {
703  // get the cube
704  pCube = pSop0 + c * (nFanins + 3);
705  if ( *pCube == 0 )
706  break;
707  // add the clause
708  vVars->nSize = 0;
709  Abc_ObjForEachFanin( pNode, pFanin, i )
710  {
711  if ( pCube[i] == '0' )
712  Vec_IntPush( vVars, toLit(pFanin->Id) );
713  else if ( pCube[i] == '1' )
714  Vec_IntPush( vVars, lit_neg(toLit(pFanin->Id)) );
715  }
716  Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) );
717  RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
718  if ( !RetValue )
719  {
720  printf( "The CNF is trivially UNSAT.\n" );
721  return 0;
722  }
723  }
724 
725  // add clauses for the positive phase
726  for ( c = 0; ; c++ )
727  {
728  // get the cube
729  pCube = pSop1 + c * (nFanins + 3);
730  if ( *pCube == 0 )
731  break;
732  // add the clause
733  vVars->nSize = 0;
734  Abc_ObjForEachFanin( pNode, pFanin, i )
735  {
736  if ( pCube[i] == '0' )
737  Vec_IntPush( vVars, toLit(pFanin->Id) );
738  else if ( pCube[i] == '1' )
739  Vec_IntPush( vVars, lit_neg(toLit(pFanin->Id)) );
740  }
741  Vec_IntPush( vVars, toLit(pNode->Id) );
742  RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
743  if ( !RetValue )
744  {
745  printf( "The CNF is trivially UNSAT.\n" );
746  return 0;
747  }
748  }
749  return 1;
750 }
751 
752 /**Function*************************************************************
753 
754  Synopsis [Adds clauses for the PO node.]
755 
756  Description []
757 
758  SideEffects []
759 
760  SeeAlso []
761 
762 ***********************************************************************/
763 int Abc_NodeAddClausesTop( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
764 {
765  Abc_Obj_t * pFanin;
766  int RetValue;
767 
768  pFanin = Abc_ObjFanin0(pNode);
769  if ( Abc_ObjFaninC0(pNode) )
770  {
771  vVars->nSize = 0;
772  Vec_IntPush( vVars, toLit(pFanin->Id) );
773  Vec_IntPush( vVars, toLit(pNode->Id) );
774  RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
775  if ( !RetValue )
776  {
777  printf( "The CNF is trivially UNSAT.\n" );
778  return 0;
779  }
780 
781  vVars->nSize = 0;
782  Vec_IntPush( vVars, lit_neg(toLit(pFanin->Id)) );
783  Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) );
784  RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
785  if ( !RetValue )
786  {
787  printf( "The CNF is trivially UNSAT.\n" );
788  return 0;
789  }
790  }
791  else
792  {
793  vVars->nSize = 0;
794  Vec_IntPush( vVars, lit_neg(toLit(pFanin->Id)) );
795  Vec_IntPush( vVars, toLit(pNode->Id) );
796  RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
797  if ( !RetValue )
798  {
799  printf( "The CNF is trivially UNSAT.\n" );
800  return 0;
801  }
802 
803  vVars->nSize = 0;
804  Vec_IntPush( vVars, toLit(pFanin->Id) );
805  Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) );
806  RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
807  if ( !RetValue )
808  {
809  printf( "The CNF is trivially UNSAT.\n" );
810  return 0;
811  }
812  }
813 
814  vVars->nSize = 0;
815  Vec_IntPush( vVars, toLit(pNode->Id) );
816  RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
817  if ( !RetValue )
818  {
819  printf( "The CNF is trivially UNSAT.\n" );
820  return 0;
821  }
822  return 1;
823 }
824 
825 /**Function*************************************************************
826 
827  Synopsis [Sets up the SAT sat_solver.]
828 
829  Description []
830 
831  SideEffects []
832 
833  SeeAlso []
834 
835 ***********************************************************************/
836 sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes )
837 {
838  sat_solver * pSat;
839  Mem_Flex_t * pMmFlex;
840  Abc_Obj_t * pNode;
841  Vec_Str_t * vCube;
842  Vec_Int_t * vVars;
843  char * pSop0, * pSop1;
844  int i;
845 
846  assert( Abc_NtkIsBddLogic(pNtk) );
847 
848  // transfer the IDs to the copy field
849  Abc_NtkForEachPi( pNtk, pNode, i )
850  pNode->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)pNode->Id;
851 
852  // start the data structures
853  pSat = sat_solver_new();
854 sat_solver_store_alloc( pSat );
855  pMmFlex = Mem_FlexStart();
856  vCube = Vec_StrAlloc( 100 );
857  vVars = Vec_IntAlloc( 100 );
858 
859  // add clauses for each internal nodes
860  Abc_NtkForEachNode( pNtk, pNode, i )
861  {
862  // derive SOPs for both phases of the node
863  Abc_NodeBddToCnf( pNode, pMmFlex, vCube, fAllPrimes, &pSop0, &pSop1 );
864  // add the clauses to the sat_solver
865  if ( !Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ) )
866  {
867  sat_solver_delete( pSat );
868  pSat = NULL;
869  goto finish;
870  }
871  }
872  // add clauses for each PO
873  Abc_NtkForEachPo( pNtk, pNode, i )
874  {
875  if ( !Abc_NodeAddClausesTop( pSat, pNode, vVars ) )
876  {
877  sat_solver_delete( pSat );
878  pSat = NULL;
879  goto finish;
880  }
881  }
882 sat_solver_store_mark_roots( pSat );
883 
884 finish:
885  // delete
886  Vec_StrFree( vCube );
887  Vec_IntFree( vVars );
888  Mem_FlexStop( pMmFlex, 0 );
889  return pSat;
890 }
891 
892 
893 
894 /**Function*************************************************************
895 
896  Synopsis [Writes CNF for the sorter with N inputs asserting Q ones.]
897 
898  Description []
899 
900  SideEffects []
901 
902  SeeAlso []
903 
904 ***********************************************************************/
905 void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens )
906 {
907  char Command[100];
908  void * pAbc;
909  Abc_Ntk_t * pNtk;
910  Abc_Obj_t * pObj, * ppNodes[2], * ppRoots[2];
911  Vec_Ptr_t * vNodes;
912  FILE * pFile;
913  int i, Counter;
914 
915  if ( nQueens <= 0 && nQueens >= nVars )
916  {
917  printf( "The number of queens (Q = %d) should belong to the interval: 0 < Q < %d.\n", nQueens, nQueens);
918  return;
919  }
920  assert( nQueens > 0 && nQueens < nVars );
921  pAbc = Abc_FrameGetGlobalFrame();
922  // generate sorter
923  sprintf( Command, "gen -s -N %d sorter%d.blif", nVars, nVars );
924  if ( Cmd_CommandExecute( (Abc_Frame_t *)pAbc, Command ) )
925  {
926  fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
927  return;
928  }
929  // read the file
930  sprintf( Command, "read sorter%d.blif; strash", nVars );
931  if ( Cmd_CommandExecute( (Abc_Frame_t *)pAbc, Command ) )
932  {
933  fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
934  return;
935  }
936 
937  // get the current network
938  pNtk = Abc_FrameReadNtk((Abc_Frame_t *)pAbc);
939  // collect the nodes for the given two primary outputs
940  ppNodes[0] = Abc_NtkPo( pNtk, nVars - nQueens - 1 );
941  ppNodes[1] = Abc_NtkPo( pNtk, nVars - nQueens );
942  ppRoots[0] = Abc_ObjFanin0( ppNodes[0] );
943  ppRoots[1] = Abc_ObjFanin0( ppNodes[1] );
944  vNodes = Abc_NtkDfsNodes( pNtk, ppRoots, 2 );
945 
946  // assign CNF variables
947  Counter = 0;
948  Abc_NtkForEachObj( pNtk, pObj, i )
949  pObj->pCopy = (Abc_Obj_t *)~0;
950  Abc_NtkForEachPi( pNtk, pObj, i )
951  pObj->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)Counter++;
952  Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
953  pObj->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)Counter++;
954 
955 /*
956  OutVar = pCnf->pVarNums[ pObj->Id ];
957  pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
958  pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
959 
960  // positive phase
961  *pClas++ = pLits;
962  *pLits++ = 2 * OutVar;
963  *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj);
964  *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj);
965  // negative phase
966  *pClas++ = pLits;
967  *pLits++ = 2 * OutVar + 1;
968  *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj);
969  *pClas++ = pLits;
970  *pLits++ = 2 * OutVar + 1;
971  *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj);
972 */
973 
974  // add clauses for these nodes
975  pFile = fopen( pFileName, "w" );
976  fprintf( pFile, "c CNF for %d-bit sorter with %d bits set to 1 generated by ABC.\n", nVars, nQueens );
977  fprintf( pFile, "p cnf %d %d\n", Counter, 3 * Vec_PtrSize(vNodes) + 2 );
978  Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
979  {
980  // positive phase
981  fprintf( pFile, "%d %s%d %s%d 0\n", 1+(int)(ABC_PTRINT_T)pObj->pCopy,
982  Abc_ObjFaninC0(pObj)? "" : "-", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy,
983  Abc_ObjFaninC1(pObj)? "" : "-", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy );
984  // negative phase
985  fprintf( pFile, "-%d %s%d 0\n", 1+(int)(ABC_PTRINT_T)pObj->pCopy,
986  Abc_ObjFaninC0(pObj)? "-" : "", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy );
987  fprintf( pFile, "-%d %s%d 0\n", 1+(int)(ABC_PTRINT_T)pObj->pCopy,
988  Abc_ObjFaninC1(pObj)? "-" : "", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy );
989  }
990  Vec_PtrFree( vNodes );
991 
992 /*
993  *pClas++ = pLits;
994  *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
995 */
996  // assert the first literal to zero
997  fprintf( pFile, "%s%d 0\n",
998  Abc_ObjFaninC0(ppNodes[0])? "" : "-", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin0(ppNodes[0])->pCopy );
999  // assert the second literal to one
1000  fprintf( pFile, "%s%d 0\n",
1001  Abc_ObjFaninC0(ppNodes[1])? "-" : "", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin0(ppNodes[1])->pCopy );
1002  fclose( pFile );
1003 }
1004 
1005 
1006 ////////////////////////////////////////////////////////////////////////
1007 /// END OF FILE ///
1008 ////////////////////////////////////////////////////////////////////////
1009 
1010 
1011 ABC_NAMESPACE_IMPL_END
1012 
Abc_NtkIsStrash
static int Abc_NtkIsStrash(Abc_Ntk_t *pNtk)
Definition: abc.h:251
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Abc_ObjFanin1
static Abc_Obj_t * Abc_ObjFanin1(Abc_Obj_t *pObj)
Definition: abc.h:374
Abc_NtkMiterSatCreateInt
int Abc_NtkMiterSatCreateInt(sat_solver *pSat, Abc_Ntk_t *pNtk)
Definition: abcSat.c:466
Abc_Obj_t_::fMarkA
unsigned fMarkA
Definition: abc.h:134
lbool
char lbool
Definition: satVec.h:133
Abc_AigConst1
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
Definition: abcAig.c:683
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Abc_ObjFaninC1
static int Abc_ObjFaninC1(Abc_Obj_t *pObj)
Definition: abc.h:378
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Cmd_CommandExecute
int Cmd_CommandExecute(void *pAbc, char *pCommandLine)
l_Undef
#define l_Undef
Definition: SolverTypes.h:86
sat_solver_solve
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
Abc_Ntk_t_
Definition: abc.h:153
Abc_ObjFanoutNum
static int Abc_ObjFanoutNum(Abc_Obj_t *pObj)
Definition: abc.h:365
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Abc_ObjFaninNum
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
Definition: abc.h:364
Abc_NtkNodeFactor
int Abc_NtkNodeFactor(Abc_Obj_t *pObj, int nLevelMax)
Definition: abcSat.c:446
Abc_NtkLatchNum
static int Abc_NtkLatchNum(Abc_Ntk_t *pNtk)
Definition: abc.h:294
Abc_ObjFaninC0
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
Definition: abc.h:377
Abc_NtkMiterSatCreate
void * Abc_NtkMiterSatCreate(Abc_Ntk_t *pNtk, int fAllPrimes)
Definition: abcSat.c:629
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
l_True
#define l_True
Definition: SolverTypes.h:84
Mem_Flex_t_
Definition: mem.c:55
Abc_NtkCiNum
static int Abc_NtkCiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:287
Abc_NtkForEachCo
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition: abc.h:519
Abc_NtkMiterSatCreateLogic
static ABC_NAMESPACE_IMPL_START sat_solver * Abc_NtkMiterSatCreateLogic(Abc_Ntk_t *pNtk, int fAllPrimes)
DECLARATIONS ///.
Definition: abcSat.c:836
Vec_StrAlloc
static Vec_Str_t * Vec_StrAlloc(int nCap)
Definition: bblif.c:495
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
sat_solver_t::stats
stats_t stats
Definition: satSolver.h:156
Abc_NtkCollectSupergate_rec
int Abc_NtkCollectSupergate_rec(Abc_Obj_t *pNode, Vec_Ptr_t *vSuper, int fFirst, int fStopAtMux)
Definition: abcSat.c:370
Abc_NtkWriteSorterCnf
void Abc_NtkWriteSorterCnf(char *pFileName, int nVars, int nQueens)
Definition: abcSat.c:905
Abc_ObjFanin0
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
Abc_NodeAddClauses
int Abc_NodeAddClauses(sat_solver *pSat, char *pSop0, char *pSop1, Abc_Obj_t *pNode, Vec_Int_t *vVars)
Definition: abcSat.c:672
sat_solver_store_write
void sat_solver_store_write(sat_solver *s, char *pFileName)
Definition: satSolver.c:1922
Abc_Obj_t_::Level
unsigned Level
Definition: abc.h:142
Abc_Ntk_t_::pModel
int * pModel
Definition: abc.h:198
Abc_Obj_t_
Definition: abc.h:128
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
Abc_ObjChild0
static Abc_Obj_t * Abc_ObjChild0(Abc_Obj_t *pObj)
Definition: abc.h:383
Abc_Ntk_t_::pManFunc
void * pManFunc
Definition: abc.h:191
Abc_ObjIsNode
static int Abc_ObjIsNode(Abc_Obj_t *pObj)
Definition: abc.h:355
Mem_FlexStart
Mem_Flex_t * Mem_FlexStart()
Definition: mem.c:311
Abc_Frame_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Frame_t_ Abc_Frame_t
INCLUDES ///.
Definition: base/main/main.h:39
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
Abc_Obj_t_::pCopy
Abc_Obj_t * pCopy
Definition: abc.h:148
Abc_NodeIsMuxType
ABC_DLL int Abc_NodeIsMuxType(Abc_Obj_t *pNode)
Definition: abcUtil.c:1301
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
toLit
static lit toLit(int v)
Definition: satVec.h:142
Abc_NtkGetCiSatVarNums
Vec_Int_t * Abc_NtkGetCiSatVarNums(Abc_Ntk_t *pNtk)
Definition: abcSat.c:154
Vec_StrFree
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
sat_solver_store_alloc
void sat_solver_store_alloc(sat_solver *s)
Definition: satSolver.c:1916
Abc_NtkClauseMux
int Abc_NtkClauseMux(sat_solver *pSat, Abc_Obj_t *pNode, Abc_Obj_t *pNodeC, Abc_Obj_t *pNodeT, Abc_Obj_t *pNodeE, Vec_Int_t *vVars)
Definition: abcSat.c:285
nMuxes
static int nMuxes
Definition: abcSat.c:36
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Abc_FrameGetGlobalFrame
void * Abc_FrameGetGlobalFrame()
Definition: mainFrame.c:593
if
if(last==0)
Definition: sparse_int.h:34
Abc_AigNodeIsAnd
static int Abc_AigNodeIsAnd(Abc_Obj_t *pNode)
Definition: abc.h:397
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
sprintf
char * sprintf()
Counter
static int Counter
Definition: extraBddMisc.c:1877
Abc_NtkForEachNode
#define Abc_NtkForEachNode(pNtk, pNode, i)
Definition: abc.h:461
Mem_FlexStop
void Mem_FlexStop(Mem_Flex_t *p, int fVerbose)
Definition: mem.c:343
stats_t::inspects
ABC_INT64_T inspects
Definition: satVec.h:154
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Abc_NtkClauseTriv
int Abc_NtkClauseTriv(sat_solver *pSat, Abc_Obj_t *pNode, Vec_Int_t *vVars)
Definition: abcSat.c:178
sat_solver_store_mark_roots
void sat_solver_store_mark_roots(sat_solver *s)
Definition: satSolver.c:1939
Abc_FrameReadNtk
ABC_DLL Abc_Ntk_t * Abc_FrameReadNtk(Abc_Frame_t *p)
Definition: mainFrame.c:282
stats_t::conflicts
ABC_INT64_T conflicts
Definition: satVec.h:154
Cudd_ReadOne
DdNode * Cudd_ReadOne(DdManager *dd)
Definition: cuddAPI.c:987
sat_solver_simplify
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
Abc_ObjRegular
static Abc_Obj_t * Abc_ObjRegular(Abc_Obj_t *p)
Definition: abc.h:323
Abc_Obj_t_::pNtk
Abc_Ntk_t * pNtk
Definition: abc.h:130
Abc_Obj_t_::fMarkB
unsigned fMarkB
Definition: abc.h:135
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Abc_NtkPo
static Abc_Obj_t * Abc_NtkPo(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:316
Abc_NtkForEachCi
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition: abc.h:515
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Vec_Str_t_
Definition: bblif.c:47
Abc_ObjForEachFanin
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition: abc.h:524
Abc_NtkClauseTop
int Abc_NtkClauseTop(sat_solver *pSat, Vec_Ptr_t *vNodes, Vec_Int_t *vVars)
Definition: abcSat.c:198
Abc_NtkClauseAnd
int Abc_NtkClauseAnd(sat_solver *pSat, Abc_Obj_t *pNode, Vec_Ptr_t *vSuper, Vec_Int_t *vVars)
Definition: abcSat.c:221
Abc_NtkIsBddLogic
static int Abc_NtkIsBddLogic(Abc_Ntk_t *pNtk)
Definition: abc.h:265
Abc_Obj_t_::Id
int Id
Definition: abc.h:132
Abc_NtkMiterSat
int Abc_NtkMiterSat(Abc_Ntk_t *pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fVerbose, ABC_INT64_T *pNumConfs, ABC_INT64_T *pNumInspects)
FUNCTION DEFINITIONS ///.
Definition: abcSat.c:53
sat_solver_store_free
void sat_solver_store_free(sat_solver *s)
Definition: satSolver.c:1927
l_False
#define l_False
Definition: SolverTypes.h:85
Minisat::Var
int Var
Definition: SolverTypes.h:42
Abc_SopGetVarNum
ABC_DLL int Abc_SopGetVarNum(char *pSop)
Definition: abcSop.c:536
sat_solver_t
Definition: satSolver.h:91
Abc_NodeBddToCnf
ABC_DLL void Abc_NodeBddToCnf(Abc_Obj_t *pNode, Mem_Flex_t *pMmMan, Vec_Str_t *vCube, int fAllPrimes, char **ppSop0, char **ppSop1)
Definition: abcFunc.c:490
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Abc_ObjNot
static Abc_Obj_t * Abc_ObjNot(Abc_Obj_t *p)
Definition: abc.h:324
Abc_Obj_t_::pData
void * pData
Definition: abc.h:145
Abc_NtkDfsNodes
ABC_DLL Vec_Ptr_t * Abc_NtkDfsNodes(Abc_Ntk_t *pNtk, Abc_Obj_t **ppNodes, int nNodes)
Definition: abcDfs.c:120
Sat_SolverPrintStats
void Sat_SolverPrintStats(FILE *pFile, sat_solver *p)
Definition: satUtil.c:188
Abc_NtkForEachPo
#define Abc_NtkForEachPo(pNtk, pPo, i)
Definition: abc.h:517
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Abc_ObjIsComplement
static int Abc_ObjIsComplement(Abc_Obj_t *p)
Definition: abc.h:322
Abc_NtkCollectSupergate
void Abc_NtkCollectSupergate(Abc_Obj_t *pNode, int fStopAtMux, Vec_Ptr_t *vNodes)
Definition: abcSat.c:417
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Abc_NtkForEachObj
#define Abc_NtkForEachObj(pNtk, pObj, i)
ITERATORS ///.
Definition: abc.h:446
sat_solver_t::verbosity
int verbosity
Definition: satSolver.h:153
Abc_ObjChild1
static Abc_Obj_t * Abc_ObjChild1(Abc_Obj_t *pObj)
Definition: abc.h:384
Sat_SolverGetModel
int * Sat_SolverGetModel(sat_solver *p, int *pVars, int nVars)
Definition: satUtil.c:266
Abc_NodeRecognizeMux
ABC_DLL Abc_Obj_t * Abc_NodeRecognizeMux(Abc_Obj_t *pNode, Abc_Obj_t **ppNodeT, Abc_Obj_t **ppNodeE)
Definition: abcUtil.c:1389
Abc_NtkForEachPi
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition: abc.h:513
Abc_NodeAddClausesTop
int Abc_NodeAddClausesTop(sat_solver *pSat, Abc_Obj_t *pNode, Vec_Int_t *vVars)
Definition: abcSat.c:763
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223