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
Swp_ManObj2Lit(Swp_Man_t * p,int Id)88 static inline int Swp_ManObj2Lit( Swp_Man_t * p, int Id ) { return Vec_IntGetEntry( p->vId2Lit, Id ); }
Swp_ManLit2Lit(Swp_Man_t * p,int Lit)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 ); }
Swp_ManSetObj2Lit(Swp_Man_t * p,int Id,int 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 ***********************************************************************/
Swp_ManStart(Gia_Man_t * pGia)107 static inline Swp_Man_t * Swp_ManStart( Gia_Man_t * pGia )
108 {
109 Swp_Man_t * p;
110 int Lit;
111 assert( Vec_IntSize(&pGia->vHTable) );
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 }
Swp_ManStop(Gia_Man_t * pGia)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 }
Gia_SweeperStart(Gia_Man_t * pGia)145 Gia_Man_t * Gia_SweeperStart( Gia_Man_t * pGia )
146 {
147 if ( pGia == NULL )
148 pGia = Gia_ManStart( 10000 );
149 if ( Vec_IntSize(&pGia->vHTable) == 0 )
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 }
Gia_SweeperStop(Gia_Man_t * pGia)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 }
Gia_SweeperIsRunning(Gia_Man_t * pGia)164 int Gia_SweeperIsRunning( Gia_Man_t * pGia )
165 {
166 return (pGia->pData != NULL);
167 }
Gia_SweeperMemUsage(Gia_Man_t * pGia)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 }
Gia_SweeperPrintStats(Gia_Man_t * pGia)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 ***********************************************************************/
Gia_SweeperSetConflictLimit(Gia_Man_t * p,int nConfMax)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 }
Gia_SweeperSetRuntimeLimit(Gia_Man_t * p,int nSeconds)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 }
Gia_SweeperGetCex(Gia_Man_t * p)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
Gia_SweeperProbeCreate(Gia_Man_t * p,int iLit)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
Gia_SweeperProbeDelete(Gia_Man_t * p,int ProbeId)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
Gia_SweeperProbeUpdate(Gia_Man_t * p,int ProbeId,int iLitNew)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
Gia_SweeperProbeLit(Gia_Man_t * p,int ProbeId)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 ***********************************************************************/
Gia_SweeperCollectValidProbeIds(Gia_Man_t * p)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 ***********************************************************************/
Gia_SweeperCondPush(Gia_Man_t * p,int ProbeId)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 }
Gia_SweeperCondPop(Gia_Man_t * p)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 }
Gia_SweeperCondVector(Gia_Man_t * p)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 ***********************************************************************/
Gia_ManExtract_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vObjIds)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 }
Gia_SweeperExtractUserLogic(Gia_Man_t * p,Vec_Int_t * vProbeIds,Vec_Ptr_t * vInNames,Vec_Ptr_t * vOutNames)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 ***********************************************************************/
Gia_SweeperLogicDump(Gia_Man_t * p,Vec_Int_t * vProbeIds,int fDumpConds,char * pFileName)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, 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 ***********************************************************************/
Gia_SweeperCleanup(Gia_Man_t * p,char * pCommLime)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 ***********************************************************************/
Gia_ManAddClausesMux(Swp_Man_t * p,Gia_Obj_t * pNode)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 ***********************************************************************/
Gia_ManAddClausesSuper(Swp_Man_t * p,Gia_Obj_t * pNode,Vec_Int_t * vSuper)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 ***********************************************************************/
Gia_ManCollectSuper_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vSuper)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 }
Gia_ManCollectSuper(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vSuper)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 ***********************************************************************/
Gia_ManObjAddToFrontier(Swp_Man_t * p,int Id,Vec_Int_t * vFront)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 }
Gia_ManCnfNodeAddToSolver(Swp_Man_t * p,int NodeId)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 ***********************************************************************/
Gia_ManGetCex(Gia_Man_t * pGia,Vec_Int_t * vId2Lit,sat_solver * pSat,Vec_Int_t * vCex)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 ***********************************************************************/
Gia_SweeperCheckEquiv(Gia_Man_t * pGia,int Probe1,int Probe2)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 ***********************************************************************/
Gia_SweeperCondCheckUnsat(Gia_Man_t * pGia)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 ***********************************************************************/
Gia_SweeperGraft(Gia_Man_t * pDst,Vec_Int_t * vProbes,Gia_Man_t * pSrc)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 ***********************************************************************/
Gia_SweeperSweep(Gia_Man_t * p,Vec_Int_t * vProbeOuts,int nWords,int nConfs,int fVerify,int fVerbose)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 ***********************************************************************/
Gia_SweeperFraig(Gia_Man_t * p,Vec_Int_t * vProbeIds,char * pCommLime,int nWords,int nConfs,int fVerify,int fVerbose)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 ***********************************************************************/
Gia_SweeperRun(Gia_Man_t * p,Vec_Int_t * vProbeIds,char * pCommLime,int fVerbose)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 ***********************************************************************/
Gia_SweeperFraigTest(Gia_Man_t * pInit,int nWords,int nConfs,int fVerbose)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
1186