abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaSweeper.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [giaSweeper.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Scalable AIG package.]
8 
9  Synopsis [Incremental SAT sweeper.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: giaSweeper.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "gia.h"
22 #include "base/main/main.h"
23 #include "sat/bsat/satSolver.h"
24 #include "proof/ssc/ssc.h"
25 
26 ABC_NAMESPACE_IMPL_START
27 
28 /*
29 
30 SAT sweeping/equivalence checking requires the following steps:
31 - Creating probes
32  These APIs should be called for all internal points in the logic, which may be used as
33  - nodes representing conditions to be used as constraints
34  - nodes representing functions to be equivalence checked
35  - nodes representing functions needed by the user at the end of SAT sweeping
36  Creating new probe using Gia_SweeperProbeCreate(): int Gia_SweeperProbeCreate( Gia_Man_t * p, int iLit );
37  Delete existing probe using Gia_SweeperProbeDelete(): int Gia_SweeperProbeDelete( Gia_Man_t * p, int ProbeId );
38  Update existing probe using Gia_SweeperProbeUpdate(): int Gia_SweeperProbeUpdate( Gia_Man_t * p, int ProbeId, int iLit );
39  Comments:
40  - a probe is identified by its 0-based ID, which is returned by above procedures
41  - GIA literal of the probe is returned by int Gia_SweeperProbeLit( Gia_Man_t * p, int ProbeId )
42 - Adding/removing conditions on the current path by calling Gia_SweeperCondPush() and Gia_SweeperCondPop()
43  extern void Gia_SweeperCondPush( Gia_Man_t * p, int ProbeId );
44  extern void Gia_SweeperCondPop( Gia_Man_t * p );
45 - Performing equivalence checking by calling int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 )
46  (resource limits, such as the number of conflicts, will be controllable by dedicated GIA APIs)
47 - The resulting AIG to be returned to the user by calling Gia_SweeperExtractUserLogic()
48  Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vOutNames )
49 
50 */
51 
52 ////////////////////////////////////////////////////////////////////////
53 /// DECLARATIONS ///
54 ////////////////////////////////////////////////////////////////////////
55 
56 typedef struct Swp_Man_t_ Swp_Man_t;
57 struct Swp_Man_t_
58 {
59  Gia_Man_t * pGia; // GIA manager under construction
60  int nConfMax; // conflict limit in seconds
61  int nTimeOut; // runtime limit in seconds
62  Vec_Int_t * vProbes; // probes
63  Vec_Int_t * vCondProbes; // conditions as probes
64  Vec_Int_t * vCondAssump; // conditions as SAT solver literals
65  // equivalence checking
66  sat_solver * pSat; // SAT solver
67  Vec_Int_t * vId2Lit; // mapping of Obj IDs into SAT literal
68  Vec_Int_t * vFront; // temporary frontier
69  Vec_Int_t * vFanins; // temporary fanins
70  Vec_Int_t * vCexSwp; // sweeper counter-example
71  Vec_Int_t * vCexUser; // user-visible counter-example
72  int nSatVars; // counter of SAT variables
73  // statistics
74  int nSatCalls;
75  int nSatCallsSat;
76  int nSatCallsUnsat;
77  int nSatCallsUndec;
78  int nSatProofs;
79  abctime timeStart;
80  abctime timeTotal;
81  abctime timeCnf;
82  abctime timeSat;
83  abctime timeSatSat;
84  abctime timeSatUnsat;
85  abctime timeSatUndec;
86 };
87 
88 static inline int Swp_ManObj2Lit( Swp_Man_t * p, int Id ) { return Vec_IntGetEntry( p->vId2Lit, Id ); }
89 static inline int Swp_ManLit2Lit( Swp_Man_t * p, int Lit ) { assert( Vec_IntEntry(p->vId2Lit, Abc_Lit2Var(Lit)) ); return Abc_Lit2LitL( Vec_IntArray(p->vId2Lit), Lit ); }
90 static inline void Swp_ManSetObj2Lit( Swp_Man_t * p, int Id, int Lit ) { assert( Lit > 0 ); Vec_IntSetEntry( p->vId2Lit, Id, Lit ); }
91 
92 ////////////////////////////////////////////////////////////////////////
93 /// FUNCTION DEFINITIONS ///
94 ////////////////////////////////////////////////////////////////////////
95 
96 /**Function*************************************************************
97 
98  Synopsis [Creating/deleting the manager.]
99 
100  Description []
101 
102  SideEffects []
103 
104  SeeAlso []
105 
106 ***********************************************************************/
107 static inline Swp_Man_t * Swp_ManStart( Gia_Man_t * pGia )
108 {
109  Swp_Man_t * p;
110  int Lit;
111  assert( pGia->pHTable != NULL );
112  pGia->pData = p = ABC_CALLOC( Swp_Man_t, 1 );
113  p->pGia = pGia;
114  p->nConfMax = 1000;
115  p->vProbes = Vec_IntAlloc( 100 );
116  p->vCondProbes = Vec_IntAlloc( 100 );
117  p->vCondAssump = Vec_IntAlloc( 100 );
118  p->vId2Lit = Vec_IntAlloc( 10000 );
119  p->vFront = Vec_IntAlloc( 100 );
120  p->vFanins = Vec_IntAlloc( 100 );
121  p->vCexSwp = Vec_IntAlloc( 100 );
122  p->pSat = sat_solver_new();
123  p->nSatVars = 1;
124  sat_solver_setnvars( p->pSat, 1000 );
125  Swp_ManSetObj2Lit( p, 0, (Lit = Abc_Var2Lit(p->nSatVars++, 0)) );
126  Lit = Abc_LitNot(Lit);
127  sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
128  p->timeStart = Abc_Clock();
129  return p;
130 }
131 static inline void Swp_ManStop( Gia_Man_t * pGia )
132 {
133  Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
134  sat_solver_delete( p->pSat );
135  Vec_IntFree( p->vFanins );
136  Vec_IntFree( p->vCexSwp );
137  Vec_IntFree( p->vId2Lit );
138  Vec_IntFree( p->vFront );
139  Vec_IntFree( p->vProbes );
140  Vec_IntFree( p->vCondProbes );
141  Vec_IntFree( p->vCondAssump );
142  ABC_FREE( p );
143  pGia->pData = NULL;
144 }
145 Gia_Man_t * Gia_SweeperStart( Gia_Man_t * pGia )
146 {
147  if ( pGia == NULL )
148  pGia = Gia_ManStart( 10000 );
149  if ( pGia->pHTable == NULL )
150  Gia_ManHashStart( pGia );
151  // recompute fPhase and fMark1 to mark multiple fanout nodes if AIG is already defined!!!
152 
153  Swp_ManStart( pGia );
154  pGia->fSweeper = 1;
155  return pGia;
156 }
157 void Gia_SweeperStop( Gia_Man_t * pGia )
158 {
159  pGia->fSweeper = 0;
160  Swp_ManStop( pGia );
161  Gia_ManHashStop( pGia );
162 // Gia_ManStop( pGia );
163 }
164 int Gia_SweeperIsRunning( Gia_Man_t * pGia )
165 {
166  return (pGia->pData != NULL);
167 }
168 double Gia_SweeperMemUsage( Gia_Man_t * pGia )
169 {
170  Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
171  double nMem = sizeof(Swp_Man_t);
172  nMem += Vec_IntCap(p->vProbes);
173  nMem += Vec_IntCap(p->vCondProbes);
174  nMem += Vec_IntCap(p->vCondAssump);
175  nMem += Vec_IntCap(p->vId2Lit);
176  nMem += Vec_IntCap(p->vFront);
177  nMem += Vec_IntCap(p->vFanins);
178  nMem += Vec_IntCap(p->vCexSwp);
179  return 4.0 * nMem;
180 }
181 void Gia_SweeperPrintStats( Gia_Man_t * pGia )
182 {
183  Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
184  double nMemSwp = Gia_SweeperMemUsage(pGia);
185  double nMemGia = (double)Gia_ManObjNum(pGia)*(sizeof(Gia_Obj_t) + sizeof(int));
186  double nMemSat = sat_solver_memory(p->pSat);
187  double nMemTot = nMemSwp + nMemGia + nMemSat;
188  printf( "SAT sweeper statistics:\n" );
189  printf( "Memory usage:\n" );
190  ABC_PRMP( "Sweeper ", nMemSwp, nMemTot );
191  ABC_PRMP( "AIG manager ", nMemGia, nMemTot );
192  ABC_PRMP( "SAT solver ", nMemSat, nMemTot );
193  ABC_PRMP( "TOTAL ", nMemTot, nMemTot );
194  printf( "Runtime usage:\n" );
195  p->timeTotal = Abc_Clock() - p->timeStart;
196  ABC_PRTP( "CNF construction", p->timeCnf, p->timeTotal );
197  ABC_PRTP( "SAT solving ", p->timeSat, p->timeTotal );
198  ABC_PRTP( " Sat ", p->timeSatSat, p->timeTotal );
199  ABC_PRTP( " Unsat ", p->timeSatUnsat, p->timeTotal );
200  ABC_PRTP( " Undecided ", p->timeSatUndec, p->timeTotal );
201  ABC_PRTP( "TOTAL RUNTIME ", p->timeTotal, p->timeTotal );
202  printf( "GIA: " );
203  Gia_ManPrintStats( pGia, NULL );
204  printf( "SAT calls = %d. Sat = %d. Unsat = %d. Undecided = %d. Proofs = %d.\n",
205  p->nSatCalls, p->nSatCallsSat, p->nSatCallsUnsat, p->nSatCallsUndec, p->nSatProofs );
206  Sat_SolverPrintStats( stdout, p->pSat );
207 }
208 
209 /**Function*************************************************************
210 
211  Synopsis [Setting resource limits.]
212 
213  Description []
214 
215  SideEffects []
216 
217  SeeAlso []
218 
219 ***********************************************************************/
220 void Gia_SweeperSetConflictLimit( Gia_Man_t * p, int nConfMax )
221 {
222  Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
223  pSwp->nConfMax = nConfMax;
224 }
225 void Gia_SweeperSetRuntimeLimit( Gia_Man_t * p, int nSeconds )
226 {
227  Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
228  pSwp->nTimeOut = nSeconds;
229 }
230 Vec_Int_t * Gia_SweeperGetCex( Gia_Man_t * p )
231 {
232  Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
233  assert( pSwp->vCexUser == NULL || Vec_IntSize(pSwp->vCexUser) == Gia_ManPiNum(p) );
234  return pSwp->vCexUser;
235 }
236 
237 /**Function*************************************************************
238 
239  Synopsis []
240 
241  Description []
242 
243  SideEffects []
244 
245  SeeAlso []
246 
247 ***********************************************************************/
248 // create new probe
249 int Gia_SweeperProbeCreate( Gia_Man_t * p, int iLit )
250 {
251  Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
252  int ProbeId = Vec_IntSize(pSwp->vProbes);
253  assert( iLit >= 0 );
254  Vec_IntPush( pSwp->vProbes, iLit );
255  return ProbeId;
256 }
257 // delete existing probe
258 int Gia_SweeperProbeDelete( Gia_Man_t * p, int ProbeId )
259 {
260  Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
261  int iLit = Vec_IntEntry(pSwp->vProbes, ProbeId);
262  assert( iLit >= 0 );
263  Vec_IntWriteEntry(pSwp->vProbes, ProbeId, -1);
264  return iLit;
265 }
266 // update existing probe
267 int Gia_SweeperProbeUpdate( Gia_Man_t * p, int ProbeId, int iLitNew )
268 {
269  Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
270  int iLit = Vec_IntEntry(pSwp->vProbes, ProbeId);
271  assert( iLit >= 0 );
272  Vec_IntWriteEntry(pSwp->vProbes, ProbeId, iLitNew);
273  return iLit;
274 }
275 // returns literal associated with the probe
276 int Gia_SweeperProbeLit( Gia_Man_t * p, int ProbeId )
277 {
278  Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
279  int iLit = Vec_IntEntry(pSwp->vProbes, ProbeId);
280  assert( iLit >= 0 );
281  return iLit;
282 }
283 
284 /**Function*************************************************************
285 
286  Synopsis [This procedure returns indexes of all currently defined valid probes.]
287 
288  Description []
289 
290  SideEffects []
291 
292  SeeAlso []
293 
294 ***********************************************************************/
295 Vec_Int_t * Gia_SweeperCollectValidProbeIds( Gia_Man_t * p )
296 {
297  Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
298  Vec_Int_t * vProbeIds = Vec_IntAlloc( 1000 );
299  int iLit, ProbeId;
300  Vec_IntForEachEntry( pSwp->vProbes, iLit, ProbeId )
301  {
302  if ( iLit < 0 ) continue;
303  Vec_IntPush( vProbeIds, ProbeId );
304  }
305  return vProbeIds;
306 }
307 
308 /**Function*************************************************************
309 
310  Synopsis []
311 
312  Description []
313 
314  SideEffects []
315 
316  SeeAlso []
317 
318 ***********************************************************************/
319 void Gia_SweeperCondPush( Gia_Man_t * p, int ProbeId )
320 {
321  Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
322  Vec_IntPush( pSwp->vCondProbes, ProbeId );
323 }
324 int Gia_SweeperCondPop( Gia_Man_t * p )
325 {
326  Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
327  return Vec_IntPop( pSwp->vCondProbes );
328 }
329 Vec_Int_t * Gia_SweeperCondVector( Gia_Man_t * p )
330 {
331  Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
332  return pSwp->vCondProbes;
333 }
334 
335 
336 /**Function*************************************************************
337 
338  Synopsis []
339 
340  Description []
341 
342  SideEffects []
343 
344  SeeAlso []
345 
346 ***********************************************************************/
347 static void Gia_ManExtract_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vObjIds )
348 {
349  if ( !Gia_ObjIsAnd(pObj) )
350  return;
351  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
352  return;
353  Gia_ObjSetTravIdCurrent(p, pObj);
354  Gia_ManExtract_rec( p, Gia_ObjFanin0(pObj), vObjIds );
355  Gia_ManExtract_rec( p, Gia_ObjFanin1(pObj), vObjIds );
356  Vec_IntPush( vObjIds, Gia_ObjId(p, pObj) );
357 }
358 Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vInNames, Vec_Ptr_t * vOutNames )
359 {
360  Vec_Int_t * vObjIds, * vValues;
361  Gia_Man_t * pNew, * pTemp;
362  Gia_Obj_t * pObj;
363  int i, ProbeId;
364  assert( vInNames == NULL || Gia_ManPiNum(p) == Vec_PtrSize(vInNames) );
365  assert( vOutNames == NULL || Vec_IntSize(vProbeIds) == Vec_PtrSize(vOutNames) );
366  // create new
367  Gia_ManIncrementTravId( p );
368  vObjIds = Vec_IntAlloc( 1000 );
369  Vec_IntForEachEntry( vProbeIds, ProbeId, i )
370  {
371  pObj = Gia_Lit2Obj( p, Gia_SweeperProbeLit(p, ProbeId) );
372  Gia_ManExtract_rec( p, Gia_Regular(pObj), vObjIds );
373  }
374  // create new manager
375  pNew = Gia_ManStart( 1 + Gia_ManPiNum(p) + Vec_IntSize(vObjIds) + Vec_IntSize(vProbeIds) + 100 );
376  pNew->pName = Abc_UtilStrsav( p->pName );
377  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
378  Gia_ManConst0(p)->Value = 0;
379  Gia_ManForEachPi( p, pObj, i )
380  pObj->Value = Gia_ManAppendCi(pNew);
381  // create internal nodes
382  Gia_ManHashStart( pNew );
383  vValues = Vec_IntAlloc( Vec_IntSize(vObjIds) );
384  Gia_ManForEachObjVec( vObjIds, p, pObj, i )
385  {
386  Vec_IntPush( vValues, pObj->Value );
387  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
388  }
389  Gia_ManHashStop( pNew );
390  // create outputs
391  Vec_IntForEachEntry( vProbeIds, ProbeId, i )
392  {
393  pObj = Gia_Lit2Obj( p, Gia_SweeperProbeLit(p, ProbeId) );
394  Gia_ManAppendCo( pNew, Gia_Regular(pObj)->Value ^ Gia_IsComplement(pObj) );
395  }
396  // return the values back
397  Gia_ManForEachPi( p, pObj, i )
398  pObj->Value = 0;
399  Gia_ManForEachObjVec( vObjIds, p, pObj, i )
400  pObj->Value = Vec_IntEntry( vValues, i );
401  Vec_IntFree( vObjIds );
402  Vec_IntFree( vValues );
403  // duplicate if needed
404  if ( Gia_ManHasDangling(pNew) )
405  {
406  pNew = Gia_ManCleanup( pTemp = pNew );
407  Gia_ManStop( pTemp );
408  }
409  // copy names if present
410  if ( vInNames )
411  pNew->vNamesIn = Vec_PtrDupStr( vInNames );
412  if ( vOutNames )
413  pNew->vNamesOut = Vec_PtrDupStr( vOutNames );
414  return pNew;
415 }
416 
417 /**Function*************************************************************
418 
419  Synopsis []
420 
421  Description []
422 
423  SideEffects []
424 
425  SeeAlso []
426 
427 ***********************************************************************/
428 void Gia_SweeperLogicDump( Gia_Man_t * p, Vec_Int_t * vProbeIds, int fDumpConds, char * pFileName )
429 {
430  Gia_Man_t * pGiaOuts = Gia_SweeperExtractUserLogic( p, vProbeIds, NULL, NULL );
431  Vec_Int_t * vProbeConds = Gia_SweeperCondVector( p );
432  printf( "Dumping logic cones" );
433  if ( fDumpConds && Vec_IntSize(vProbeConds) > 0 )
434  {
435  Gia_Man_t * pGiaCond = Gia_SweeperExtractUserLogic( p, vProbeConds, NULL, NULL );
436  Gia_ManDupAppendShare( pGiaOuts, pGiaCond );
437  pGiaOuts->nConstrs = Gia_ManPoNum(pGiaCond);
438  Gia_ManHashStop( pGiaOuts );
439  Gia_ManStop( pGiaCond );
440  printf( " and conditions" );
441  }
442  Gia_AigerWrite( pGiaOuts, pFileName, 0, 0 );
443  Gia_ManStop( pGiaOuts );
444  printf( " into file \"%s\".\n", pFileName );
445 }
446 
447 /**Function*************************************************************
448 
449  Synopsis [Sweeper cleanup.]
450 
451  Description [Returns new GIA with sweeper defined, which is the same
452  as the original sweeper, with all the dangling logic removed and SAT
453  solver restarted. The probe IDs are guaranteed to have the same logic
454  functions as in the original manager.]
455 
456  SideEffects [The input manager is deleted inside this procedure.]
457 
458  SeeAlso []
459 
460 ***********************************************************************/
461 Gia_Man_t * Gia_SweeperCleanup( Gia_Man_t * p, char * pCommLime )
462 {
463  Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
464  Vec_Int_t * vObjIds;
465  Gia_Man_t * pNew, * pTemp;
466  Gia_Obj_t * pObj;
467  int i, iLit, ProbeId;
468 
469  // collect all internal nodes pointed to by currently-used probes
470  Gia_ManIncrementTravId( p );
471  vObjIds = Vec_IntAlloc( 1000 );
472  Vec_IntForEachEntry( pSwp->vProbes, iLit, ProbeId )
473  {
474  if ( iLit < 0 ) continue;
475  pObj = Gia_Lit2Obj( p, iLit );
476  Gia_ManExtract_rec( p, Gia_Regular(pObj), vObjIds );
477  }
478  // create new manager
479  pNew = Gia_ManStart( 1 + Gia_ManPiNum(p) + Vec_IntSize(vObjIds) + 100 );
480  pNew->pName = Abc_UtilStrsav( p->pName );
481  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
482  Gia_ManConst0(p)->Value = 0;
483  Gia_ManForEachPi( p, pObj, i )
484  pObj->Value = Gia_ManAppendCi(pNew);
485  // create internal nodes
486  Gia_ManHashStart( pNew );
487  Gia_ManForEachObjVec( vObjIds, p, pObj, i )
488  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
489  Gia_ManHashStop( pNew );
490  // create outputs
491  Vec_IntForEachEntry( pSwp->vProbes, iLit, ProbeId )
492  {
493  if ( iLit < 0 ) continue;
494  pObj = Gia_Lit2Obj( p, iLit );
495  iLit = Gia_Regular(pObj)->Value ^ Gia_IsComplement(pObj);
496  Vec_IntWriteEntry( pSwp->vProbes, ProbeId, iLit );
497  }
498  Vec_IntFree( vObjIds );
499  // duplicate if needed
500  if ( Gia_ManHasDangling(pNew) )
501  {
502  pNew = Gia_ManCleanup( pTemp = pNew );
503  Gia_ManStop( pTemp );
504  }
505  // execute command line
506  if ( pCommLime )
507  {
508  // set pNew to be current GIA in ABC
509  Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew );
510  // execute command line pCommLine using Abc_CmdCommandExecute()
511  Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), pCommLime );
512  // get pNew to be current GIA in ABC
513  pNew = Abc_FrameGetGia( Abc_FrameGetGlobalFrame() );
514  }
515  // restart the SAT solver
516  Vec_IntClear( pSwp->vId2Lit );
517  sat_solver_delete( pSwp->pSat );
518  pSwp->pSat = sat_solver_new();
519  pSwp->nSatVars = 1;
520  sat_solver_setnvars( pSwp->pSat, 1000 );
521  Swp_ManSetObj2Lit( pSwp, 0, (iLit = Abc_Var2Lit(pSwp->nSatVars++, 0)) );
522  iLit = Abc_LitNot(iLit);
523  sat_solver_addclause( pSwp->pSat, &iLit, &iLit + 1 );
524  pSwp->timeStart = Abc_Clock();
525  // return the result
526  pNew->pData = p->pData; p->pData = NULL;
527  Gia_ManStop( p );
528  return pNew;
529 }
530 
531 
532 /**Function*************************************************************
533 
534  Synopsis [Addes clauses to the solver.]
535 
536  Description []
537 
538  SideEffects []
539 
540  SeeAlso []
541 
542 ***********************************************************************/
543 static void Gia_ManAddClausesMux( Swp_Man_t * p, Gia_Obj_t * pNode )
544 {
545  Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
546  int pLits[4], LitF, LitI, LitT, LitE, RetValue;
547  assert( !Gia_IsComplement( pNode ) );
548  assert( Gia_ObjIsMuxType( pNode ) );
549  // get nodes (I = if, T = then, E = else)
550  pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
551  // get the Litiable numbers
552  LitF = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNode) );
553  LitI = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNodeI) );
554  LitT = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNodeT) );
555  LitE = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNodeE) );
556 
557  // f = ITE(i, t, e)
558 
559  // i' + t' + f
560  // i' + t + f'
561  // i + e' + f
562  // i + e + f'
563 
564  // create four clauses
565  pLits[0] = Abc_LitNotCond(LitI, 1);
566  pLits[1] = Abc_LitNotCond(LitT, 1);
567  pLits[2] = Abc_LitNotCond(LitF, 0);
568  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
569  assert( RetValue );
570  pLits[0] = Abc_LitNotCond(LitI, 1);
571  pLits[1] = Abc_LitNotCond(LitT, 0);
572  pLits[2] = Abc_LitNotCond(LitF, 1);
573  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
574  assert( RetValue );
575  pLits[0] = Abc_LitNotCond(LitI, 0);
576  pLits[1] = Abc_LitNotCond(LitE, 1);
577  pLits[2] = Abc_LitNotCond(LitF, 0);
578  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
579  assert( RetValue );
580  pLits[0] = Abc_LitNotCond(LitI, 0);
581  pLits[1] = Abc_LitNotCond(LitE, 0);
582  pLits[2] = Abc_LitNotCond(LitF, 1);
583  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
584  assert( RetValue );
585 
586  // two additional clauses
587  // t' & e' -> f'
588  // t & e -> f
589 
590  // t + e + f'
591  // t' + e' + f
592 
593  if ( LitT == LitE )
594  {
595 // assert( fCompT == !fCompE );
596  return;
597  }
598 
599  pLits[0] = Abc_LitNotCond(LitT, 0);
600  pLits[1] = Abc_LitNotCond(LitE, 0);
601  pLits[2] = Abc_LitNotCond(LitF, 1);
602  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
603  assert( RetValue );
604  pLits[0] = Abc_LitNotCond(LitT, 1);
605  pLits[1] = Abc_LitNotCond(LitE, 1);
606  pLits[2] = Abc_LitNotCond(LitF, 0);
607  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
608  assert( RetValue );
609 }
610 
611 /**Function*************************************************************
612 
613  Synopsis [Addes clauses to the solver.]
614 
615  Description []
616 
617  SideEffects []
618 
619  SeeAlso []
620 
621 ***********************************************************************/
622 static void Gia_ManAddClausesSuper( Swp_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSuper )
623 {
624  int i, RetValue, Lit, LitNode, pLits[2];
625  assert( !Gia_IsComplement(pNode) );
626  assert( Gia_ObjIsAnd( pNode ) );
627  // suppose AND-gate is A & B = C
628  // add !A => !C or A + !C
629  // add !B => !C or B + !C
630  LitNode = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNode) );
631  Vec_IntForEachEntry( vSuper, Lit, i )
632  {
633  pLits[0] = Swp_ManLit2Lit( p, Lit );
634  pLits[1] = Abc_LitNot( LitNode );
635  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
636  assert( RetValue );
637  // update literals
638  Vec_IntWriteEntry( vSuper, i, Abc_LitNot(pLits[0]) );
639  }
640  // add A & B => C or !A + !B + C
641  Vec_IntPush( vSuper, LitNode );
642  RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vSuper), Vec_IntArray(vSuper) + Vec_IntSize(vSuper) );
643  assert( RetValue );
644  (void) RetValue;
645 }
646 
647 
648 /**Function*************************************************************
649 
650  Synopsis [Collects the supergate.]
651 
652  Description []
653 
654  SideEffects []
655 
656  SeeAlso []
657 
658 ***********************************************************************/
659 static void Gia_ManCollectSuper_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
660 {
661  // stop at complements, shared, PIs, and MUXes
662  if ( Gia_IsComplement(pObj) || pObj->fMark1 || Gia_ObjIsCi(pObj) || Gia_ObjIsMuxType(pObj) )
663  {
664  Vec_IntPushUnique( vSuper, Gia_Obj2Lit(p, pObj) );
665  return;
666  }
667  Gia_ManCollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper );
668  Gia_ManCollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper );
669 }
670 static void Gia_ManCollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
671 {
672  assert( !Gia_IsComplement(pObj) );
673  assert( Gia_ObjIsAnd(pObj) );
674  Vec_IntClear( vSuper );
675  Gia_ManCollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper );
676  Gia_ManCollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper );
677 }
678 
679 /**Function*************************************************************
680 
681  Synopsis [Updates the solver clause database.]
682 
683  Description []
684 
685  SideEffects []
686 
687  SeeAlso []
688 
689 ***********************************************************************/
690 static void Gia_ManObjAddToFrontier( Swp_Man_t * p, int Id, Vec_Int_t * vFront )
691 {
692  Gia_Obj_t * pObj;
693  if ( Id == 0 || Swp_ManObj2Lit(p, Id) )
694  return;
695  pObj = Gia_ManObj( p->pGia, Id );
696  Swp_ManSetObj2Lit( p, Id, Abc_Var2Lit(p->nSatVars++, pObj->fPhase) );
697  sat_solver_setnvars( p->pSat, p->nSatVars + 100 );
698  if ( Gia_ObjIsAnd(pObj) )
699  Vec_IntPush( vFront, Id );
700 }
701 static void Gia_ManCnfNodeAddToSolver( Swp_Man_t * p, int NodeId )
702 {
703  Gia_Obj_t * pNode;
704  int i, k, Id, Lit;
705  abctime clk;
706  // quit if CNF is ready
707  if ( NodeId == 0 || Swp_ManObj2Lit(p, NodeId) )
708  return;
709 clk = Abc_Clock();
710  // start the frontier
711  Vec_IntClear( p->vFront );
712  Gia_ManObjAddToFrontier( p, NodeId, p->vFront );
713  // explore nodes in the frontier
714  Gia_ManForEachObjVec( p->vFront, p->pGia, pNode, i )
715  {
716  // create the supergate
717  assert( Swp_ManObj2Lit(p, Gia_ObjId(p->pGia, pNode)) );
718  if ( Gia_ObjIsMuxType(pNode) )
719  {
720  Vec_IntClear( p->vFanins );
721  Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId0p( p->pGia, Gia_ObjFanin0(pNode) ) );
722  Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId0p( p->pGia, Gia_ObjFanin1(pNode) ) );
723  Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId1p( p->pGia, Gia_ObjFanin0(pNode) ) );
724  Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId1p( p->pGia, Gia_ObjFanin1(pNode) ) );
725  Vec_IntForEachEntry( p->vFanins, Id, k )
726  Gia_ManObjAddToFrontier( p, Id, p->vFront );
727  Gia_ManAddClausesMux( p, pNode );
728  }
729  else
730  {
731  Gia_ManCollectSuper( p->pGia, pNode, p->vFanins );
732  Vec_IntForEachEntry( p->vFanins, Lit, k )
733  Gia_ManObjAddToFrontier( p, Abc_Lit2Var(Lit), p->vFront );
734  Gia_ManAddClausesSuper( p, pNode, p->vFanins );
735  }
736  assert( Vec_IntSize(p->vFanins) > 1 );
737  }
738 p->timeCnf += Abc_Clock() - clk;
739 }
740 
741 
742 /**Function*************************************************************
743 
744  Synopsis []
745 
746  Description []
747 
748  SideEffects []
749 
750  SeeAlso []
751 
752 ***********************************************************************/
753 static Vec_Int_t * Gia_ManGetCex( Gia_Man_t * pGia, Vec_Int_t * vId2Lit, sat_solver * pSat, Vec_Int_t * vCex )
754 {
755  Gia_Obj_t * pObj;
756  int i, LitSat, Value;
757  Vec_IntClear( vCex );
758  Gia_ManForEachPi( pGia, pObj, i )
759  {
760  if ( Gia_ObjId(pGia, pObj) >= Vec_IntSize(vId2Lit) )
761  {
762  Vec_IntPush( vCex, 2 );
763  continue;
764  }
765  LitSat = Vec_IntEntry( vId2Lit, Gia_ObjId(pGia, pObj) );
766  if ( LitSat == 0 )
767  {
768  Vec_IntPush( vCex, 2 );
769  continue;
770  }
771  assert( LitSat > 0 );
772  Value = sat_solver_var_value(pSat, Abc_Lit2Var(LitSat)) ^ Abc_LitIsCompl(LitSat);
773  Vec_IntPush( vCex, Value );
774  }
775  return vCex;
776 }
777 
778 /**Function*************************************************************
779 
780  Synopsis [Runs equivalence test for probes.]
781 
782  Description []
783 
784  SideEffects []
785 
786  SeeAlso []
787 
788 ***********************************************************************/
789 int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 )
790 {
791  Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
792  int iLitOld, iLitNew, iLitAig, pLitsSat[2], RetValue, RetValue1, ProbeId, i;
793  abctime clk;
794  p->nSatCalls++;
795  assert( p->pSat != NULL );
796  p->vCexUser = NULL;
797 
798  // get the literals
799  iLitOld = Gia_SweeperProbeLit( pGia, Probe1 );
800  iLitNew = Gia_SweeperProbeLit( pGia, Probe2 );
801  // if the literals are identical, the probes are equivalent
802  if ( iLitOld == iLitNew )
803  return 1;
804  // if the literals are opposites, the probes are not equivalent
805  if ( Abc_LitRegular(iLitOld) == Abc_LitRegular(iLitNew) )
806  {
807  Vec_IntFill( p->vCexSwp, Gia_ManPiNum(pGia), 2 );
808  p->vCexUser = p->vCexSwp;
809  return 0;
810  }
811  // order the literals
812  if ( iLitOld < iLitNew )
813  ABC_SWAP( int, iLitOld, iLitNew );
814  assert( iLitOld > iLitNew );
815 
816  // create logic cones and the array of assumptions
817  Vec_IntClear( p->vCondAssump );
818  Vec_IntForEachEntry( p->vCondProbes, ProbeId, i )
819  {
820  iLitAig = Gia_SweeperProbeLit( pGia, ProbeId );
821  Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitAig) );
822  Vec_IntPush( p->vCondAssump, Abc_LitNot(Swp_ManLit2Lit(p, iLitAig)) );
823  }
824  Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitOld) );
825  Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitNew) );
826  sat_solver_compress( p->pSat );
827 
828  // set the SAT literals
829  pLitsSat[0] = Swp_ManLit2Lit( p, iLitOld );
830  pLitsSat[1] = Swp_ManLit2Lit( p, iLitNew );
831 
832  // solve under assumptions
833  // A = 1; B = 0 OR A = 1; B = 1
834  Vec_IntPush( p->vCondAssump, pLitsSat[0] );
835  Vec_IntPush( p->vCondAssump, Abc_LitNot(pLitsSat[1]) );
836 
837  // set runtime limit for this call
838  if ( p->nTimeOut )
839  sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
840 
841 clk = Abc_Clock();
842  RetValue1 = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondAssump), Vec_IntArray(p->vCondAssump) + Vec_IntSize(p->vCondAssump),
843  (ABC_INT64_T)p->nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
844  Vec_IntShrink( p->vCondAssump, Vec_IntSize(p->vCondAssump) - 2 );
845 p->timeSat += Abc_Clock() - clk;
846  if ( RetValue1 == l_False )
847  {
848  pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
849  RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
850  assert( RetValue );
851  pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
852 p->timeSatUnsat += Abc_Clock() - clk;
853  p->nSatCallsUnsat++;
854  }
855  else if ( RetValue1 == l_True )
856  {
857  p->vCexUser = Gia_ManGetCex( p->pGia, p->vId2Lit, p->pSat, p->vCexSwp );
858 p->timeSatSat += Abc_Clock() - clk;
859  p->nSatCallsSat++;
860  return 0;
861  }
862  else // if ( RetValue1 == l_Undef )
863  {
864 p->timeSatUndec += Abc_Clock() - clk;
865  p->nSatCallsUndec++;
866  return -1;
867  }
868 
869  // if the old node was constant 0, we already know the answer
870  if ( Gia_ManIsConstLit(iLitNew) )
871  {
872  p->nSatProofs++;
873  return 1;
874  }
875 
876  // solve under assumptions
877  // A = 0; B = 1 OR A = 0; B = 0
878  Vec_IntPush( p->vCondAssump, Abc_LitNot(pLitsSat[0]) );
879  Vec_IntPush( p->vCondAssump, pLitsSat[1] );
880 
881 clk = Abc_Clock();
882  RetValue1 = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondAssump), Vec_IntArray(p->vCondAssump) + Vec_IntSize(p->vCondAssump),
883  (ABC_INT64_T)p->nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
884  Vec_IntShrink( p->vCondAssump, Vec_IntSize(p->vCondAssump) - 2 );
885 p->timeSat += Abc_Clock() - clk;
886  if ( RetValue1 == l_False )
887  {
888  pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
889  RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
890  assert( RetValue );
891  pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
892 p->timeSatUnsat += Abc_Clock() - clk;
893  p->nSatCallsUnsat++;
894  }
895  else if ( RetValue1 == l_True )
896  {
897  p->vCexUser = Gia_ManGetCex( p->pGia, p->vId2Lit, p->pSat, p->vCexSwp );
898 p->timeSatSat += Abc_Clock() - clk;
899  p->nSatCallsSat++;
900  return 0;
901  }
902  else // if ( RetValue1 == l_Undef )
903  {
904 p->timeSatUndec += Abc_Clock() - clk;
905  p->nSatCallsUndec++;
906  return -1;
907  }
908  // return SAT proof
909  p->nSatProofs++;
910  return 1;
911 }
912 
913 /**Function*************************************************************
914 
915  Synopsis [Returns 1 if the set of conditions is UNSAT (0 if SAT; -1 if undecided).]
916 
917  Description []
918 
919  SideEffects []
920 
921  SeeAlso []
922 
923 ***********************************************************************/
924 int Gia_SweeperCondCheckUnsat( Gia_Man_t * pGia )
925 {
926  Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
927  int RetValue, ProbeId, iLitAig, i;
928  abctime clk;
929  assert( p->pSat != NULL );
930  p->nSatCalls++;
931  p->vCexUser = NULL;
932 
933  // create logic cones and the array of assumptions
934  Vec_IntClear( p->vCondAssump );
935  Vec_IntForEachEntry( p->vCondProbes, ProbeId, i )
936  {
937  iLitAig = Gia_SweeperProbeLit( pGia, ProbeId );
938  Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitAig) );
939  Vec_IntPush( p->vCondAssump, Abc_LitNot(Swp_ManLit2Lit(p, iLitAig)) );
940  }
941  sat_solver_compress( p->pSat );
942 
943  // set runtime limit for this call
944  if ( p->nTimeOut )
945  sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
946 
947 clk = Abc_Clock();
948  RetValue = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondAssump), Vec_IntArray(p->vCondAssump) + Vec_IntSize(p->vCondAssump),
949  (ABC_INT64_T)p->nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
950 p->timeSat += Abc_Clock() - clk;
951  if ( RetValue == l_False )
952  {
953  assert( Vec_IntSize(p->vCondProbes) > 0 );
954 p->timeSatUnsat += Abc_Clock() - clk;
955  p->nSatCallsUnsat++;
956  p->nSatProofs++;
957  return 1;
958  }
959  else if ( RetValue == l_True )
960  {
961  p->vCexUser = Gia_ManGetCex( p->pGia, p->vId2Lit, p->pSat, p->vCexSwp );
962 p->timeSatSat += Abc_Clock() - clk;
963  p->nSatCallsSat++;
964  return 0;
965  }
966  else // if ( RetValue1 == l_Undef )
967  {
968 p->timeSatUndec += Abc_Clock() - clk;
969  p->nSatCallsUndec++;
970  return -1;
971  }
972 }
973 
974 /**Function*************************************************************
975 
976  Synopsis [Performs grafting from another manager.]
977 
978  Description [Returns the array of resulting literals in the destination manager.]
979 
980  SideEffects []
981 
982  SeeAlso []
983 
984 ***********************************************************************/
985 Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * pSrc )
986 {
987  Vec_Int_t * vOutLits;
988  Gia_Obj_t * pObj;
989  int i;
990  assert( Gia_SweeperIsRunning(pDst) );
991  if ( vProbes )
992  assert( Vec_IntSize(vProbes) == Gia_ManPiNum(pSrc) );
993  else
994  assert( Gia_ManPiNum(pDst) == Gia_ManPiNum(pSrc) );
995  Gia_ManForEachPi( pSrc, pObj, i )
996  pObj->Value = vProbes ? Gia_SweeperProbeLit(pDst, Vec_IntEntry(vProbes, i)) : Gia_Obj2Lit(pDst,Gia_ManPi(pDst, i));
997  Gia_ManForEachAnd( pSrc, pObj, i )
998  pObj->Value = Gia_ManHashAnd( pDst, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
999  vOutLits = Vec_IntAlloc( Gia_ManPoNum(pSrc) );
1000  Gia_ManForEachPo( pSrc, pObj, i )
1001  Vec_IntPush( vOutLits, Gia_ObjFanin0Copy(pObj) );
1002  return vOutLits;
1003 }
1004 
1005 /**Function*************************************************************
1006 
1007  Synopsis [Performs conditional sweeping of the cone.]
1008 
1009  Description [Returns the result as a new GIA manager with as many inputs
1010  as the original manager and as many outputs as there are logic cones.]
1011 
1012  SideEffects []
1013 
1014  SeeAlso []
1015 
1016 ***********************************************************************/
1017 Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts, int nWords, int nConfs, int fVerify, int fVerbose )
1018 {
1019  Vec_Int_t * vProbeConds;
1020  Gia_Man_t * pGiaCond, * pGiaOuts, * pGiaRes;
1021  Ssc_Pars_t Pars, * pPars = &Pars;
1022  Ssc_ManSetDefaultParams( pPars );
1023  pPars->nWords = nWords;
1024  pPars->nBTLimit = nConfs;
1025  pPars->fVerify = fVerify;
1026  pPars->fVerbose = fVerbose;
1027  // sweeper is running
1028  assert( Gia_SweeperIsRunning(p) );
1029  // extract conditions and logic cones
1030  vProbeConds = Gia_SweeperCondVector( p );
1031  pGiaCond = Gia_SweeperExtractUserLogic( p, vProbeConds, NULL, NULL );
1032  pGiaOuts = Gia_SweeperExtractUserLogic( p, vProbeOuts, NULL, NULL );
1033  Gia_ManSetPhase( pGiaOuts );
1034  // if there is no conditions, define constant true constraint (constant 0 output)
1035  if ( Gia_ManPoNum(pGiaCond) == 0 )
1036  Gia_ManAppendCo( pGiaCond, Gia_ManConst0Lit() );
1037  // perform sweeping under constraints
1038  pGiaRes = Ssc_PerformSweeping( pGiaOuts, pGiaCond, pPars );
1039  Gia_ManStop( pGiaCond );
1040  Gia_ManStop( pGiaOuts );
1041  return pGiaRes;
1042 }
1043 
1044 /**Function*************************************************************
1045 
1046  Synopsis [Procedure to perform conditional fraig sweeping on separate logic cones.]
1047 
1048  Description [The procedure takes GIA with the sweeper defined. The sweeper
1049  is assumed to have some conditions currently pushed, which will be used
1050  as constraints for fraig sweeping. The second argument (vProbes) contains
1051  the array of probe IDs pointing to the user's logic cones to be SAT swept.
1052  Finally, the optional command line (pCommLine) is an ABC command line
1053  to be applied to the resulting GIA after SAT sweeping before it is
1054  grafted back into the original GIA manager. The return value is the status
1055  (success/failure) and the array of original probes possibly pointing to the
1056  new literals in the original GIA manager, corresponding to the user's
1057  logic cones after sweeping, synthesis and grafting.]
1058 
1059  SideEffects []
1060 
1061  SeeAlso []
1062 
1063 ***********************************************************************/
1064 int Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime, int nWords, int nConfs, int fVerify, int fVerbose )
1065 {
1066  Gia_Man_t * pNew;
1067  Vec_Int_t * vLits;
1068  int ProbeId, i;
1069  // sweeper is running
1070  assert( Gia_SweeperIsRunning(p) );
1071  // sweep the logic
1072  pNew = Gia_SweeperSweep( p, vProbeIds, nWords, nConfs, fVerify, fVerbose );
1073  if ( pNew == NULL )
1074  return 0;
1075  // execute command line
1076  if ( pCommLime )
1077  {
1078  // set pNew to be current GIA in ABC
1079  Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew );
1080  // execute command line pCommLine using Abc_CmdCommandExecute()
1081  Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), pCommLime );
1082  // get pNew to be current GIA in ABC
1083  pNew = Abc_FrameGetGia( Abc_FrameGetGlobalFrame() );
1084  }
1085  // return logic back into the main manager
1086  vLits = Gia_SweeperGraft( p, NULL, pNew );
1087  Gia_ManStop( pNew );
1088  // update the array of probes
1089  Vec_IntForEachEntry( vProbeIds, ProbeId, i )
1090  Gia_SweeperProbeUpdate( p, ProbeId, Vec_IntEntry(vLits, i) );
1091  Vec_IntFree( vLits );
1092  return 1;
1093 }
1094 
1095 /**Function*************************************************************
1096 
1097  Synopsis [Executes given command line for the logic defined by the probes.]
1098 
1099  Description [ ]
1100 
1101  SideEffects []
1102 
1103  SeeAlso []
1104 
1105 ***********************************************************************/
1106 int Gia_SweeperRun( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime, int fVerbose )
1107 {
1108  Gia_Man_t * pNew;
1109  Vec_Int_t * vLits;
1110  int ProbeId, i;
1111  // sweeper is running
1112  assert( Gia_SweeperIsRunning(p) );
1113  // sweep the logic
1114  pNew = Gia_SweeperExtractUserLogic( p, vProbeIds, NULL, NULL );
1115  // execute command line
1116  if ( pCommLime )
1117  {
1118  if ( fVerbose )
1119  printf( "GIA manager statistics before and after applying \"%s\":\n", pCommLime );
1120  if ( fVerbose )
1121  Gia_ManPrintStats( pNew, NULL );
1122  // set pNew to be current GIA in ABC
1123  Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew );
1124  // execute command line pCommLine using Abc_CmdCommandExecute()
1125  Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), pCommLime );
1126  // get pNew to be current GIA in ABC
1127  pNew = Abc_FrameGetGia( Abc_FrameGetGlobalFrame() );
1128  if ( fVerbose )
1129  Gia_ManPrintStats( pNew, NULL );
1130  }
1131  // return logic back into the main manager
1132  vLits = Gia_SweeperGraft( p, NULL, pNew );
1133  Gia_ManStop( pNew );
1134  // update the array of probes
1135  Vec_IntForEachEntry( vProbeIds, ProbeId, i )
1136  Gia_SweeperProbeUpdate( p, ProbeId, Vec_IntEntry(vLits, i) );
1137  Vec_IntFree( vLits );
1138  return 1;
1139 }
1140 
1141 /**Function*************************************************************
1142 
1143  Synopsis [Sweeper sweeper test.]
1144 
1145  Description []
1146 
1147  SideEffects []
1148 
1149  SeeAlso []
1150 
1151 ***********************************************************************/
1152 Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * pInit, int nWords, int nConfs, int fVerbose )
1153 {
1154  Gia_Man_t * p, * pGia;
1155  Gia_Obj_t * pObj;
1156  Vec_Int_t * vOuts;
1157  int i;
1158  // add one-hotness constraints
1159  p = Gia_ManDupOneHot( pInit );
1160  // create sweeper
1161  Gia_SweeperStart( p );
1162  // collect outputs and create conditions
1163  vOuts = Vec_IntAlloc( Gia_ManPoNum(p) );
1164  Gia_ManForEachPo( p, pObj, i )
1165  if ( i < Gia_ManPoNum(p) - p->nConstrs ) // this is the user's output
1166  Vec_IntPush( vOuts, Gia_SweeperProbeCreate( p, Gia_ObjFaninLit0p(p, pObj) ) );
1167  else // this is a constraint
1168  Gia_SweeperCondPush( p, Gia_SweeperProbeCreate( p, Gia_ObjFaninLit0p(p, pObj) ) );
1169  // perform the sweeping
1170  pGia = Gia_SweeperSweep( p, vOuts, nWords, nConfs, fVerbose, 0 );
1171 // pGia = Gia_ManDup( p );
1172  Vec_IntFree( vOuts );
1173  // sop the sweeper
1174  Gia_SweeperStop( p );
1175  Gia_ManStop( p );
1176  return pGia;
1177 }
1178 
1179 
1180 ////////////////////////////////////////////////////////////////////////
1181 /// END OF FILE ///
1182 ////////////////////////////////////////////////////////////////////////
1183 
1184 ABC_NAMESPACE_IMPL_END
1185 
sat_solver_set_runtime_limit
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
Gia_SweeperStart
Gia_Man_t * Gia_SweeperStart(Gia_Man_t *pGia)
Definition: giaSweeper.c:145
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Swp_ManStop
static void Swp_ManStop(Gia_Man_t *pGia)
Definition: giaSweeper.c:131
Gia_ObjChild0
static Gia_Obj_t * Gia_ObjChild0(Gia_Obj_t *pObj)
Definition: gia.h:457
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Gia_SweeperMemUsage
double Gia_SweeperMemUsage(Gia_Man_t *pGia)
Definition: giaSweeper.c:168
Swp_Man_t_::vFanins
Vec_Int_t * vFanins
Definition: giaSweeper.c:69
Gia_ManCollectSuper
static void Gia_ManCollectSuper(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vSuper)
Definition: giaSweeper.c:670
Gia_SweeperCollectValidProbeIds
Vec_Int_t * Gia_SweeperCollectValidProbeIds(Gia_Man_t *p)
Definition: giaSweeper.c:295
Swp_Man_t_::vProbes
Vec_Int_t * vProbes
Definition: giaSweeper.c:62
Swp_Man_t_::nConfMax
int nConfMax
Definition: giaSweeper.c:60
Gia_SweeperCondVector
Vec_Int_t * Gia_SweeperCondVector(Gia_Man_t *p)
Definition: giaSweeper.c:329
Swp_ManStart
static Swp_Man_t * Swp_ManStart(Gia_Man_t *pGia)
FUNCTION DEFINITIONS ///.
Definition: giaSweeper.c:107
Ssc_ManSetDefaultParams
void Ssc_ManSetDefaultParams(Ssc_Pars_t *p)
MACRO DEFINITIONS ///.
Definition: sscCore.c:46
Gia_SweeperCondPush
void Gia_SweeperCondPush(Gia_Man_t *p, int ProbeId)
Definition: giaSweeper.c:319
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManDupOneHot
Gia_Man_t * Gia_ManDupOneHot(Gia_Man_t *p)
Definition: giaDup.c:2785
Gia_Man_t_::pHTable
int * pHTable
Definition: gia.h:110
Gia_ManPrintStats
void Gia_ManPrintStats(Gia_Man_t *p, Gps_Par_t *pPars)
Definition: giaMan.c:389
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Gia_ManAppendCo
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
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
Swp_Man_t_::nSatCallsUndec
int nSatCallsUndec
Definition: giaSweeper.c:77
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)
Gia_Regular
static Gia_Obj_t * Gia_Regular(Gia_Obj_t *p)
Definition: gia.h:377
Gia_ObjIsTravIdCurrent
static int Gia_ObjIsTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:533
Gia_ManIsConstLit
static int Gia_ManIsConstLit(int iLit)
Definition: gia.h:375
Swp_Man_t_::vCondAssump
Vec_Int_t * vCondAssump
Definition: giaSweeper.c:64
Abc_Lit2LitL
static int Abc_Lit2LitL(int *pMap, int Lit)
Definition: abc_global.h:270
Gia_ObjFaninLit0p
static int Gia_ObjFaninLit0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:469
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
sat_solver_compress
static void sat_solver_compress(sat_solver *s)
Definition: satSolver.h:217
Gia_SweeperSetRuntimeLimit
void Gia_SweeperSetRuntimeLimit(Gia_Man_t *p, int nSeconds)
Definition: giaSweeper.c:225
Gia_SweeperExtractUserLogic
Gia_Man_t * Gia_SweeperExtractUserLogic(Gia_Man_t *p, Vec_Int_t *vProbeIds, Vec_Ptr_t *vInNames, Vec_Ptr_t *vOutNames)
Definition: giaSweeper.c:358
Ssc_Pars_t
typedefABC_NAMESPACE_HEADER_START struct Ssc_Pars_t_ Ssc_Pars_t
INCLUDES ///.
Definition: ssc.h:43
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Gia_SweeperProbeUpdate
int Gia_SweeperProbeUpdate(Gia_Man_t *p, int ProbeId, int iLitNew)
Definition: giaSweeper.c:267
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Gia_ObjFaninId1p
static int Gia_ObjFaninId1p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:464
Gia_ManAddClausesMux
static void Gia_ManAddClausesMux(Swp_Man_t *p, Gia_Obj_t *pNode)
Definition: giaSweeper.c:543
Vec_IntSetEntry
static void Vec_IntSetEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:418
l_True
#define l_True
Definition: SolverTypes.h:84
Gia_SweeperProbeCreate
int Gia_SweeperProbeCreate(Gia_Man_t *p, int iLit)
Definition: giaSweeper.c:249
Vec_IntGetEntry
static int Vec_IntGetEntry(Vec_Int_t *p, int i)
Definition: bblif.c:401
Gia_Obj_t_::fMark1
unsigned fMark1
Definition: gia.h:84
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Gia_SweeperFraigTest
Gia_Man_t * Gia_SweeperFraigTest(Gia_Man_t *pInit, int nWords, int nConfs, int fVerbose)
Definition: giaSweeper.c:1152
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
sat_solver_memory
double sat_solver_memory(sat_solver *s)
Definition: satSolver.c:1236
Swp_Man_t_::pSat
sat_solver * pSat
Definition: giaSweeper.c:66
nWords
int nWords
Definition: abcNpn.c:127
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Gia_SweeperGraft
Vec_Int_t * Gia_SweeperGraft(Gia_Man_t *pDst, Vec_Int_t *vProbes, Gia_Man_t *pSrc)
Definition: giaSweeper.c:985
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Gia_Obj_t_
Definition: gia.h:75
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition: abc_global.h:218
Gia_SweeperSetConflictLimit
void Gia_SweeperSetConflictLimit(Gia_Man_t *p, int nConfMax)
Definition: giaSweeper.c:220
Swp_Man_t_::timeSatUndec
abctime timeSatUndec
Definition: giaSweeper.c:85
Gia_ManHasDangling
int Gia_ManHasDangling(Gia_Man_t *p)
Definition: giaUtil.c:1155
Swp_Man_t_::timeTotal
abctime timeTotal
Definition: giaSweeper.c:80
Gia_SweeperSweep
Gia_Man_t * Gia_SweeperSweep(Gia_Man_t *p, Vec_Int_t *vProbeOuts, int nWords, int nConfs, int fVerify, int fVerbose)
Definition: giaSweeper.c:1017
Swp_ManObj2Lit
static int Swp_ManObj2Lit(Swp_Man_t *p, int Id)
Definition: giaSweeper.c:88
Gia_Man_t_::fSweeper
int fSweeper
Definition: gia.h:113
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition: abc_global.h:223
Gia_ObjChild1
static Gia_Obj_t * Gia_ObjChild1(Gia_Obj_t *pObj)
Definition: gia.h:458
Gia_ManConst0Lit
static int Gia_ManConst0Lit()
Definition: gia.h:371
Swp_Man_t_::vCexSwp
Vec_Int_t * vCexSwp
Definition: giaSweeper.c:70
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition: gia.h:74
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Gia_SweeperProbeDelete
int Gia_SweeperProbeDelete(Gia_Man_t *p, int ProbeId)
Definition: giaSweeper.c:258
Swp_Man_t_::nSatProofs
int nSatProofs
Definition: giaSweeper.c:78
Swp_Man_t_::vFront
Vec_Int_t * vFront
Definition: giaSweeper.c:68
Gia_SweeperPrintStats
void Gia_SweeperPrintStats(Gia_Man_t *pGia)
Definition: giaSweeper.c:181
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Swp_Man_t_::nSatCallsUnsat
int nSatCallsUnsat
Definition: giaSweeper.c:76
Gia_SweeperLogicDump
void Gia_SweeperLogicDump(Gia_Man_t *p, Vec_Int_t *vProbeIds, int fDumpConds, char *pFileName)
Definition: giaSweeper.c:428
Gia_ManPi
static Gia_Obj_t * Gia_ManPi(Gia_Man_t *p, int v)
Definition: gia.h:405
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_Man_t_::nConstrs
int nConstrs
Definition: gia.h:117
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Swp_Man_t_::timeCnf
abctime timeCnf
Definition: giaSweeper.c:81
Swp_ManLit2Lit
static int Swp_ManLit2Lit(Swp_Man_t *p, int Lit)
Definition: giaSweeper.c:89
Swp_Man_t_::nSatCallsSat
int nSatCallsSat
Definition: giaSweeper.c:75
Swp_Man_t_::nTimeOut
int nTimeOut
Definition: giaSweeper.c:61
Gia_ObjFanin1Copy
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
Gia_SweeperCleanup
Gia_Man_t * Gia_SweeperCleanup(Gia_Man_t *p, char *pCommLime)
Definition: giaSweeper.c:461
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Gia_ObjSetTravIdCurrent
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
Gia_Man_t_::pData
void * pData
Definition: gia.h:169
Ssc_PerformSweeping
Gia_Man_t * Ssc_PerformSweeping(Gia_Man_t *pAig, Gia_Man_t *pCare, Ssc_Pars_t *pPars)
Definition: sscCore.c:413
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
Swp_Man_t_::vCondProbes
Vec_Int_t * vCondProbes
Definition: giaSweeper.c:63
Abc_FrameGetGlobalFrame
void * Abc_FrameGetGlobalFrame()
Definition: mainFrame.c:593
Gia_ManHashStart
void Gia_ManHashStart(Gia_Man_t *p)
Definition: giaHash.c:117
Gia_Man_t_::pSpec
char * pSpec
Definition: gia.h:98
Vec_IntPop
static int Vec_IntPop(Vec_Int_t *p)
Definition: extraZddTrunc.c:110
Swp_Man_t_::timeSatUnsat
abctime timeSatUnsat
Definition: giaSweeper.c:84
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Swp_Man_t_::pGia
Gia_Man_t * pGia
Definition: giaSweeper.c:59
Gia_ManExtract_rec
static void Gia_ManExtract_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vObjIds)
Definition: giaSweeper.c:347
Swp_Man_t_::timeStart
abctime timeStart
Definition: giaSweeper.c:79
Swp_Man_t_::timeSatSat
abctime timeSatSat
Definition: giaSweeper.c:83
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Gia_SweeperStop
void Gia_SweeperStop(Gia_Man_t *pGia)
Definition: giaSweeper.c:157
Vec_IntCap
static int Vec_IntCap(Vec_Int_t *p)
Definition: vecInt.h:368
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact)
Definition: giaAiger.c:1024
Gia_Man_t_::vNamesOut
Vec_Ptr_t * vNamesOut
Definition: gia.h:156
Gia_ObjFanin0Copy
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
Gia_ManDupAppendShare
void Gia_ManDupAppendShare(Gia_Man_t *p, Gia_Man_t *pTwo)
Definition: giaDup.c:765
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Gia_ManCollectSuper_rec
static void Gia_ManCollectSuper_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vSuper)
Definition: giaSweeper.c:659
Gia_ManAddClausesSuper
static void Gia_ManAddClausesSuper(Swp_Man_t *p, Gia_Obj_t *pNode, Vec_Int_t *vSuper)
Definition: giaSweeper.c:622
Gia_ObjIsMuxType
int Gia_ObjIsMuxType(Gia_Obj_t *pNode)
Definition: giaUtil.c:885
Swp_Man_t_::timeSat
abctime timeSat
Definition: giaSweeper.c:82
Abc_LitNot
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
Gia_Obj_t_::fPhase
unsigned fPhase
Definition: gia.h:85
Gia_ManObjAddToFrontier
static void Gia_ManObjAddToFrontier(Swp_Man_t *p, int Id, Vec_Int_t *vFront)
Definition: giaSweeper.c:690
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Gia_IsComplement
static int Gia_IsComplement(Gia_Obj_t *p)
Definition: gia.h:380
Swp_Man_t_::vId2Lit
Vec_Int_t * vId2Lit
Definition: giaSweeper.c:67
Gia_SweeperIsRunning
int Gia_SweeperIsRunning(Gia_Man_t *pGia)
Definition: giaSweeper.c:164
Vec_IntShrink
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
Gia_SweeperFraig
int Gia_SweeperFraig(Gia_Man_t *p, Vec_Int_t *vProbeIds, char *pCommLime, int nWords, int nConfs, int fVerify, int fVerbose)
Definition: giaSweeper.c:1064
Gia_SweeperCondPop
int Gia_SweeperCondPop(Gia_Man_t *p)
Definition: giaSweeper.c:324
Swp_Man_t_
Definition: giaSweeper.c:57
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_ObjRecognizeMux
Gia_Obj_t * Gia_ObjRecognizeMux(Gia_Obj_t *pNode, Gia_Obj_t **ppNodeT, Gia_Obj_t **ppNodeE)
Definition: giaUtil.c:959
Gia_Man_t_
Definition: gia.h:95
Swp_Man_t_::vCexUser
Vec_Int_t * vCexUser
Definition: giaSweeper.c:71
ABC_PRMP
#define ABC_PRMP(a, f, F)
Definition: abc_global.h:227
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Swp_Man_t
typedefABC_NAMESPACE_IMPL_START struct Swp_Man_t_ Swp_Man_t
DECLARATIONS ///.
Definition: giaSweeper.c:56
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
l_False
#define l_False
Definition: SolverTypes.h:85
Gia_ObjFaninId0p
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Abc_FrameUpdateGia
void Abc_FrameUpdateGia(Abc_Frame_t *pAbc, Gia_Man_t *pNew)
Definition: abc.c:616
Gia_SweeperGetCex
Vec_Int_t * Gia_SweeperGetCex(Gia_Man_t *p)
Definition: giaSweeper.c:230
sat_solver_t
Definition: satSolver.h:91
Gia_SweeperCheckEquiv
int Gia_SweeperCheckEquiv(Gia_Man_t *pGia, int Probe1, int Probe2)
Definition: giaSweeper.c:789
Gia_ManCnfNodeAddToSolver
static void Gia_ManCnfNodeAddToSolver(Swp_Man_t *p, int NodeId)
Definition: giaSweeper.c:701
Abc_LitRegular
static int Abc_LitRegular(int Lit)
Definition: abc_global.h:268
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManSetPhase
void Gia_ManSetPhase(Gia_Man_t *p)
Definition: giaUtil.c:379
Swp_ManSetObj2Lit
static void Swp_ManSetObj2Lit(Swp_Man_t *p, int Id, int Lit)
Definition: giaSweeper.c:90
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Gia_Lit2Obj
static Gia_Obj_t * Gia_Lit2Obj(Gia_Man_t *p, int iLit)
Definition: gia.h:434
Gia_Man_t_::vNamesIn
Vec_Ptr_t * vNamesIn
Definition: gia.h:155
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
Gia_SweeperCondCheckUnsat
int Gia_SweeperCondCheckUnsat(Gia_Man_t *pGia)
Definition: giaSweeper.c:924
Sat_SolverPrintStats
void Sat_SolverPrintStats(FILE *pFile, sat_solver *p)
Definition: satUtil.c:188
Gia_SweeperProbeLit
int Gia_SweeperProbeLit(Gia_Man_t *p, int ProbeId)
Definition: giaSweeper.c:276
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_IntPushUnique
static int Vec_IntPushUnique(Vec_Int_t *p, int Entry)
Definition: vecInt.h:832
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Abc_FrameGetGia
Gia_Man_t * Abc_FrameGetGia(Abc_Frame_t *pAbc)
Definition: abc.c:656
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Swp_Man_t_::nSatVars
int nSatVars
Definition: giaSweeper.c:72
Vec_PtrDupStr
static Vec_Ptr_t * Vec_PtrDupStr(Vec_Ptr_t *pVec)
Definition: vecPtr.h:179
Gia_ManGetCex
static Vec_Int_t * Gia_ManGetCex(Gia_Man_t *pGia, Vec_Int_t *vId2Lit, sat_solver *pSat, Vec_Int_t *vCex)
Definition: giaSweeper.c:753
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Gia_Obj2Lit
static int Gia_Obj2Lit(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:433
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
Gia_SweeperRun
int Gia_SweeperRun(Gia_Man_t *p, Vec_Int_t *vProbeIds, char *pCommLime, int fVerbose)
Definition: giaSweeper.c:1106
Swp_Man_t_::nSatCalls
int nSatCalls
Definition: giaSweeper.c:74