1 /**CFile****************************************************************
2
3 FileName [giaSupp.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis [Support minimization for AIGs.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: giaSupp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "gia.h"
22 #include "sat/satoko/satoko.h"
23
24 #ifdef ABC_USE_CUDD
25 #include "bdd/extrab/extraBdd.h"
26 #endif
27
28 ABC_NAMESPACE_IMPL_START
29
30 ////////////////////////////////////////////////////////////////////////
31 /// DECLARATIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 #ifdef ABC_USE_CUDD
35
36 struct Gia_ManMin_t_
37 {
38 // problem formulation
39 Gia_Man_t * pGia;
40 int iLits[2];
41 // structural information
42 Vec_Int_t * vCis[2];
43 Vec_Int_t * vObjs[2];
44 Vec_Int_t * vCleared;
45 // intermediate functions
46 DdManager * dd;
47 Vec_Ptr_t * vFuncs;
48 Vec_Int_t * vSupp;
49 };
50
51 ////////////////////////////////////////////////////////////////////////
52 /// FUNCTION DEFINITIONS ///
53 ////////////////////////////////////////////////////////////////////////
54
55 /**Function*************************************************************
56
57 Synopsis [Create/delete the data representation manager.]
58
59 Description []
60
61 SideEffects []
62
63 SeeAlso []
64
65 ***********************************************************************/
Gia_ManSuppStart(Gia_Man_t * pGia)66 Gia_ManMin_t * Gia_ManSuppStart( Gia_Man_t * pGia )
67 {
68 Gia_ManMin_t * p;
69 p = ABC_CALLOC( Gia_ManMin_t, 1 );
70 p->pGia = pGia;
71 p->vCis[0] = Vec_IntAlloc( 512 );
72 p->vCis[1] = Vec_IntAlloc( 512 );
73 p->vObjs[0] = Vec_IntAlloc( 512 );
74 p->vObjs[1] = Vec_IntAlloc( 512 );
75 p->vCleared = Vec_IntAlloc( 512 );
76 p->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
77 // Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
78 Cudd_AutodynDisable( p->dd );
79 p->vFuncs = Vec_PtrAlloc( 10000 );
80 p->vSupp = Vec_IntAlloc( 10000 );
81 return p;
82 }
Gia_ManSuppStop(Gia_ManMin_t * p)83 void Gia_ManSuppStop( Gia_ManMin_t * p )
84 {
85 Vec_IntFreeP( &p->vCis[0] );
86 Vec_IntFreeP( &p->vCis[1] );
87 Vec_IntFreeP( &p->vObjs[0] );
88 Vec_IntFreeP( &p->vObjs[1] );
89 Vec_IntFreeP( &p->vCleared );
90 Vec_PtrFreeP( &p->vFuncs );
91 Vec_IntFreeP( &p->vSupp );
92 printf( "Refs = %d. \n", Cudd_CheckZeroRef( p->dd ) );
93 Cudd_Quit( p->dd );
94 ABC_FREE( p );
95 }
96
97 /**Function*************************************************************
98
99 Synopsis [Compute variables, which are not in the support.]
100
101 Description []
102
103 SideEffects []
104
105 SeeAlso []
106
107 ***********************************************************************/
Gia_ManFindRemoved(Gia_ManMin_t * p)108 int Gia_ManFindRemoved( Gia_ManMin_t * p )
109 {
110 extern void ddSupportStep2( DdNode * f, int * support );
111 extern void ddClearFlag2( DdNode * f );
112
113 //int fVerbose = 1;
114 int nBddLimit = 100000;
115 int nPart0 = Vec_IntSize(p->vCis[0]);
116 int n, i, iObj, nVars = 0;
117 DdNode * bFunc0, * bFunc1, * bFunc;
118 Vec_PtrFillExtra( p->vFuncs, Gia_ManObjNum(p->pGia), NULL );
119 // assign variables
120 for ( n = 0; n < 2; n++ )
121 Vec_IntForEachEntry( p->vCis[n], iObj, i )
122 Vec_PtrWriteEntry( p->vFuncs, iObj, Cudd_bddIthVar(p->dd, nVars++) );
123 // create nodes
124 for ( n = 0; n < 2; n++ )
125 Vec_IntForEachEntry( p->vObjs[n], iObj, i )
126 {
127 Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
128 bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(p->vFuncs, Gia_ObjFaninId0(pObj, iObj)), Gia_ObjFaninC0(pObj) );
129 bFunc1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(p->vFuncs, Gia_ObjFaninId1(pObj, iObj)), Gia_ObjFaninC1(pObj) );
130 bFunc = Cudd_bddAndLimit( p->dd, bFunc0, bFunc1, nBddLimit );
131 assert( bFunc != NULL );
132 Cudd_Ref( bFunc );
133 Vec_PtrWriteEntry( p->vFuncs, iObj, bFunc );
134 }
135 // create new node
136 bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(p->vFuncs, Abc_Lit2Var(p->iLits[0])), Abc_LitIsCompl(p->iLits[0]) );
137 bFunc1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(p->vFuncs, Abc_Lit2Var(p->iLits[1])), Abc_LitIsCompl(p->iLits[1]) );
138 bFunc = Cudd_bddAndLimit( p->dd, bFunc0, bFunc1, nBddLimit );
139 assert( bFunc != NULL );
140 Cudd_Ref( bFunc );
141 //if ( fVerbose ) Extra_bddPrint( p->dd, bFunc ), printf( "\n" );
142 // collect support
143 Vec_IntFill( p->vSupp, nVars, 0 );
144 ddSupportStep2( Cudd_Regular(bFunc), Vec_IntArray(p->vSupp) );
145 ddClearFlag2( Cudd_Regular(bFunc) );
146 // find variables not present in the support
147 Vec_IntClear( p->vCleared );
148 for ( i = 0; i < nVars; i++ )
149 if ( Vec_IntEntry(p->vSupp, i) == 0 )
150 Vec_IntPush( p->vCleared, i < nPart0 ? Vec_IntEntry(p->vCis[0], i) : Vec_IntEntry(p->vCis[1], i-nPart0) );
151 //printf( "%d(%d)%d ", Cudd_SupportSize(p->dd, bFunc), Vec_IntSize(p->vCleared), Cudd_DagSize(bFunc) );
152 // deref results
153 Cudd_RecursiveDeref( p->dd, bFunc );
154 for ( n = 0; n < 2; n++ )
155 Vec_IntForEachEntry( p->vObjs[n], iObj, i )
156 Cudd_RecursiveDeref( p->dd, (DdNode *)Vec_PtrEntry(p->vFuncs, iObj) );
157 //Vec_IntPrint( p->vCleared );
158 return Vec_IntSize(p->vCleared);
159 }
160
161 /**Function*************************************************************
162
163 Synopsis [Compute variables, which are not in the support.]
164
165 Description []
166
167 SideEffects []
168
169 SeeAlso []
170
171 ***********************************************************************/
Gia_ManRebuildOne(Gia_ManMin_t * p,int n)172 int Gia_ManRebuildOne( Gia_ManMin_t * p, int n )
173 {
174 int i, iObj, iGiaLitNew = -1;
175 Vec_Int_t * vTempIns = p->vCis[n];
176 Vec_Int_t * vTempNds = p->vObjs[n];
177 Vec_Int_t * vCopies = &p->pGia->vCopies;
178 Vec_IntFillExtra( vCopies, Gia_ManObjNum(p->pGia), -1 );
179 assert( p->iLits[n] >= 2 );
180 // process inputs
181 Vec_IntForEachEntry( vTempIns, iObj, i )
182 Vec_IntWriteEntry( vCopies, iObj, Abc_Var2Lit(iObj, 0) );
183 // process constants
184 assert( Vec_IntSize(p->vCleared) > 0 );
185 Vec_IntForEachEntry( p->vCleared, iObj, i )
186 Vec_IntWriteEntry( vCopies, iObj, 0 );
187 if ( Vec_IntSize(vTempNds) == 0 )
188 iGiaLitNew = Vec_IntEntry( vCopies, Abc_Lit2Var(p->iLits[n]) );
189 else
190 {
191 Vec_IntForEachEntry( vTempNds, iObj, i )
192 {
193 Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
194 int iGiaLit0 = Vec_IntEntry( vCopies, Gia_ObjFaninId0p(p->pGia, pObj) );
195 int iGiaLit1 = Vec_IntEntry( vCopies, Gia_ObjFaninId1p(p->pGia, pObj) );
196 iGiaLit0 = Abc_LitNotCond( iGiaLit0, Gia_ObjFaninC0(pObj) );
197 iGiaLit1 = Abc_LitNotCond( iGiaLit1, Gia_ObjFaninC1(pObj) );
198 iGiaLitNew = Gia_ManHashAnd( p->pGia, iGiaLit0, iGiaLit1 );
199 Vec_IntWriteEntry( vCopies, iObj, iGiaLitNew );
200 }
201 assert( Abc_Lit2Var(p->iLits[n]) == iObj );
202 }
203 return Abc_LitNotCond( iGiaLitNew, Abc_LitIsCompl(p->iLits[n]) );
204 }
205
206 /**Function*************************************************************
207
208 Synopsis [Collect nodes.]
209
210 Description []
211
212 SideEffects []
213
214 SeeAlso []
215
216 ***********************************************************************/
Gia_ManGatherSupp_rec(Gia_Man_t * p,int iObj,Vec_Int_t * vCis,Vec_Int_t * vObjs)217 static inline int Gia_ManGatherSupp_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vCis, Vec_Int_t * vObjs )
218 {
219 int Val0, Val1;
220 Gia_Obj_t * pObj;
221 if ( Gia_ObjIsTravIdPreviousId(p, iObj) )
222 return 1;
223 if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
224 return 0;
225 Gia_ObjSetTravIdCurrentId(p, iObj);
226 pObj = Gia_ManObj( p, iObj );
227 if ( Gia_ObjIsCi(pObj) )
228 {
229 Vec_IntPush( vCis, iObj );
230 return 0;
231 }
232 assert( Gia_ObjIsAnd(pObj) );
233 Val0 = Gia_ManGatherSupp_rec( p, Gia_ObjFaninId0(pObj, iObj), vCis, vObjs );
234 Val1 = Gia_ManGatherSupp_rec( p, Gia_ObjFaninId1(pObj, iObj), vCis, vObjs );
235 Vec_IntPush( vObjs, iObj );
236 return Val0 || Val1;
237 }
Gia_ManGatherSupp(Gia_ManMin_t * p)238 int Gia_ManGatherSupp( Gia_ManMin_t * p )
239 {
240 int n, Overlap = 0;
241 Gia_ManIncrementTravId( p->pGia );
242 for ( n = 0; n < 2; n++ )
243 {
244 Vec_IntClear( p->vCis[n] );
245 Vec_IntClear( p->vObjs[n] );
246 Gia_ManIncrementTravId( p->pGia );
247 Overlap = Gia_ManGatherSupp_rec( p->pGia, Abc_Lit2Var(p->iLits[n]), p->vCis[n], p->vObjs[n] );
248 assert( n || !Overlap );
249 }
250 return Overlap;
251 }
252
253 /**Function*************************************************************
254
255 Synopsis [Takes a literal and returns a support-minized literal.]
256
257 Description []
258
259 SideEffects []
260
261 SeeAlso []
262
263 ***********************************************************************/
Gia_ManSupportAnd(Gia_ManMin_t * p,int iLit0,int iLit1)264 int Gia_ManSupportAnd( Gia_ManMin_t * p, int iLit0, int iLit1 )
265 {
266 int iLitNew0, iLitNew1;
267 p->iLits[0] = iLit0;
268 p->iLits[1] = iLit1;
269 if ( iLit0 < 2 || iLit1 < 2 || !Gia_ManGatherSupp(p) || !Gia_ManFindRemoved(p) )
270 return Gia_ManHashAnd( p->pGia, iLit0, iLit1 );
271 iLitNew0 = Gia_ManRebuildOne( p, 0 );
272 iLitNew1 = Gia_ManRebuildOne( p, 1 );
273 return Gia_ManHashAnd( p->pGia, iLitNew0, iLitNew1 );
274 }
275
276
277 #else
278
279 Gia_ManMin_t * Gia_ManSuppStart( Gia_Man_t * pGia ) { return NULL; }
280 int Gia_ManSupportAnd( Gia_ManMin_t * p, int iLit0, int iLit1 ) { return 0; }
281 void Gia_ManSuppStop( Gia_ManMin_t * p ) {}
282
283 #endif
284
285
286 /**Function*************************************************************
287
288 Synopsis [Testbench.]
289
290 Description []
291
292 SideEffects []
293
294 SeeAlso []
295
296 ***********************************************************************/
Gia_ManSupportAndTest(Gia_Man_t * pGia)297 Gia_Man_t * Gia_ManSupportAndTest( Gia_Man_t * pGia )
298 {
299 Gia_ManMin_t * pMan;
300 Gia_Man_t * pNew, * pTemp;
301 Gia_Obj_t * pObj;
302 int i;
303 Gia_ManFillValue( pGia );
304 pNew = Gia_ManStart( Gia_ManObjNum(pGia) );
305 pNew->pName = Abc_UtilStrsav( pGia->pName );
306 pNew->pSpec = Abc_UtilStrsav( pGia->pSpec );
307 Gia_ManHashAlloc( pNew );
308 Gia_ManConst0(pGia)->Value = 0;
309 pMan = Gia_ManSuppStart( pNew );
310 Gia_ManForEachObj1( pGia, pObj, i )
311 {
312 if ( Gia_ObjIsAnd(pObj) )
313 {
314 // pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
315 pObj->Value = Gia_ManSupportAnd( pMan, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
316 }
317 else if ( Gia_ObjIsCi(pObj) )
318 pObj->Value = Gia_ManAppendCi( pNew );
319 else if ( Gia_ObjIsCo(pObj) )
320 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
321 else assert( 0 );
322
323 if ( i % 10000 == 0 )
324 printf( "%d\n", i );
325 }
326 Gia_ManSuppStop( pMan );
327 Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia) );
328 pNew = Gia_ManCleanup( pTemp = pNew );
329 Gia_ManStop( pTemp );
330 return pNew;
331 }
332
333
334
335
336 struct Gia_Man2Min_t_
337 {
338 // problem formulation
339 Gia_Man_t * pGia;
340 int iLits[2];
341 // structural information
342 Vec_Int_t * vCis[2];
343 Vec_Int_t * vObjs[2];
344 // SAT solving
345 satoko_t * pSat; // SAT solver
346 Vec_Wrd_t * vSims; // simulation
347 Vec_Ptr_t * vFrontier; // CNF construction
348 Vec_Ptr_t * vFanins; // CNF construction
349 Vec_Int_t * vSatVars; // nodes
350 int nCisOld; // previous number of CIs
351 int iPattern; // the next pattern to write
352 int nSatSat;
353 int nSatUnsat;
354 int nCalls;
355 int nSims;
356 int nSupps;
357 };
358
Gia_Min2ObjSatId(Gia_Man_t * p,Gia_Obj_t * pObj)359 static inline int Gia_Min2ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjCopyArray(p, Gia_ObjId(p, pObj)); }
Gia_Min2ObjSetSatId(Gia_Man_t * p,Gia_Obj_t * pObj,int Num)360 static inline int Gia_Min2ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num ) { assert(Gia_Min2ObjSatId(p, pObj) == -1); Gia_ObjSetCopyArray(p, Gia_ObjId(p, pObj), Num); return Num; }
Gia_Min2ObjCleanSatId(Gia_Man_t * p,Gia_Obj_t * pObj)361 static inline void Gia_Min2ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(Gia_Min2ObjSatId(p, pObj) != -1); Gia_ObjSetCopyArray(p, Gia_ObjId(p, pObj), -1); }
362
363
364 /**Function*************************************************************
365
366 Synopsis [Create/delete the data representation manager.]
367
368 Description []
369
370 SideEffects []
371
372 SeeAlso []
373
374 ***********************************************************************/
Gia_Man2SuppStart(Gia_Man_t * pGia)375 Gia_Man2Min_t * Gia_Man2SuppStart( Gia_Man_t * pGia )
376 {
377 Gia_Man2Min_t * p;
378 p = ABC_CALLOC( Gia_Man2Min_t, 1 );
379 p->pGia = pGia;
380 p->vCis[0] = Vec_IntAlloc( 512 );
381 p->vCis[1] = Vec_IntAlloc( 512 );
382 p->vObjs[0] = Vec_IntAlloc( 512 );
383 p->vObjs[1] = Vec_IntAlloc( 512 );
384 // SAT solving
385 p->pSat = satoko_create();
386 p->vSims = Vec_WrdAlloc( 1000 );
387 p->vFrontier = Vec_PtrAlloc( 1000 );
388 p->vFanins = Vec_PtrAlloc( 100 );
389 p->vSatVars = Vec_IntAlloc( 100 );
390 p->iPattern = 1;
391 satoko_options(p->pSat)->learnt_ratio = 0; // prevent garbage collection
392 return p;
393 }
Gia_Man2SuppStop(Gia_Man2Min_t * p)394 void Gia_Man2SuppStop( Gia_Man2Min_t * p )
395 {
396 // printf( "Total calls = %8d. Supps = %6d. Sims = %6d. SAT = %6d. UNSAT = %6d.\n",
397 // p->nCalls, p->nSupps, p->nSims, p->nSatSat, p->nSatUnsat );
398 Vec_IntFreeP( &p->vCis[0] );
399 Vec_IntFreeP( &p->vCis[1] );
400 Vec_IntFreeP( &p->vObjs[0] );
401 Vec_IntFreeP( &p->vObjs[1] );
402 Gia_ManCleanMark01( p->pGia );
403 satoko_destroy( p->pSat );
404 Vec_WrdFreeP( &p->vSims );
405 Vec_PtrFreeP( &p->vFrontier );
406 Vec_PtrFreeP( &p->vFanins );
407 Vec_IntFreeP( &p->vSatVars );
408 ABC_FREE( p );
409 }
410
411 /**Function*************************************************************
412
413 Synopsis [Adds clauses to the solver.]
414
415 Description []
416
417 SideEffects []
418
419 SeeAlso []
420
421 ***********************************************************************/
Gia_Min2AddClausesMux(Gia_Man_t * p,Gia_Obj_t * pNode,satoko_t * pSat)422 void Gia_Min2AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, satoko_t * pSat )
423 {
424 int fPolarFlip = 0;
425 Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
426 int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
427
428 assert( !Gia_IsComplement( pNode ) );
429 assert( pNode->fMark0 );
430 // get nodes (I = if, T = then, E = else)
431 pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
432 // get the variable numbers
433 VarF = Gia_Min2ObjSatId(p, pNode);
434 VarI = Gia_Min2ObjSatId(p, pNodeI);
435 VarT = Gia_Min2ObjSatId(p, Gia_Regular(pNodeT));
436 VarE = Gia_Min2ObjSatId(p, Gia_Regular(pNodeE));
437 // get the complementation flags
438 fCompT = Gia_IsComplement(pNodeT);
439 fCompE = Gia_IsComplement(pNodeE);
440
441 // f = ITE(i, t, e)
442
443 // i' + t' + f
444 // i' + t + f'
445 // i + e' + f
446 // i + e + f'
447
448 // create four clauses
449 pLits[0] = Abc_Var2Lit(VarI, 1);
450 pLits[1] = Abc_Var2Lit(VarT, 1^fCompT);
451 pLits[2] = Abc_Var2Lit(VarF, 0);
452 if ( fPolarFlip )
453 {
454 if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
455 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
456 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
457 }
458 RetValue = satoko_add_clause( pSat, pLits, 3 );
459 assert( RetValue );
460 pLits[0] = Abc_Var2Lit(VarI, 1);
461 pLits[1] = Abc_Var2Lit(VarT, 0^fCompT);
462 pLits[2] = Abc_Var2Lit(VarF, 1);
463 if ( fPolarFlip )
464 {
465 if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
466 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
467 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
468 }
469 RetValue = satoko_add_clause( pSat, pLits, 3 );
470 assert( RetValue );
471 pLits[0] = Abc_Var2Lit(VarI, 0);
472 pLits[1] = Abc_Var2Lit(VarE, 1^fCompE);
473 pLits[2] = Abc_Var2Lit(VarF, 0);
474 if ( fPolarFlip )
475 {
476 if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
477 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
478 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
479 }
480 RetValue = satoko_add_clause( pSat, pLits, 3 );
481 assert( RetValue );
482 pLits[0] = Abc_Var2Lit(VarI, 0);
483 pLits[1] = Abc_Var2Lit(VarE, 0^fCompE);
484 pLits[2] = Abc_Var2Lit(VarF, 1);
485 if ( fPolarFlip )
486 {
487 if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
488 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
489 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
490 }
491 RetValue = satoko_add_clause( pSat, pLits, 3 );
492 assert( RetValue );
493
494 // two additional clauses
495 // t' & e' -> f'
496 // t & e -> f
497
498 // t + e + f'
499 // t' + e' + f
500
501 if ( VarT == VarE )
502 {
503 // assert( fCompT == !fCompE );
504 return;
505 }
506
507 pLits[0] = Abc_Var2Lit(VarT, 0^fCompT);
508 pLits[1] = Abc_Var2Lit(VarE, 0^fCompE);
509 pLits[2] = Abc_Var2Lit(VarF, 1);
510 if ( fPolarFlip )
511 {
512 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
513 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
514 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
515 }
516 RetValue = satoko_add_clause( pSat, pLits, 3 );
517 assert( RetValue );
518 pLits[0] = Abc_Var2Lit(VarT, 1^fCompT);
519 pLits[1] = Abc_Var2Lit(VarE, 1^fCompE);
520 pLits[2] = Abc_Var2Lit(VarF, 0);
521 if ( fPolarFlip )
522 {
523 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
524 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
525 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
526 }
527 RetValue = satoko_add_clause( pSat, pLits, 3 );
528 assert( RetValue );
529 }
Gia_Min2AddClausesSuper(Gia_Man_t * p,Gia_Obj_t * pNode,Vec_Ptr_t * vSuper,satoko_t * pSat)530 void Gia_Min2AddClausesSuper( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper, satoko_t * pSat )
531 {
532 int fPolarFlip = 0;
533 Gia_Obj_t * pFanin;
534 int * pLits, nLits, RetValue, i;
535 assert( !Gia_IsComplement(pNode) );
536 assert( Gia_ObjIsAnd( pNode ) );
537 // create storage for literals
538 nLits = Vec_PtrSize(vSuper) + 1;
539 pLits = ABC_ALLOC( int, nLits );
540 // suppose AND-gate is A & B = C
541 // add !A => !C or A + !C
542 Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
543 {
544 pLits[0] = Abc_Var2Lit(Gia_Min2ObjSatId(p, Gia_Regular(pFanin)), Gia_IsComplement(pFanin));
545 pLits[1] = Abc_Var2Lit(Gia_Min2ObjSatId(p, pNode), 1);
546 if ( fPolarFlip )
547 {
548 if ( Gia_Regular(pFanin)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
549 if ( pNode->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
550 }
551 RetValue = satoko_add_clause( pSat, pLits, 2 );
552 assert( RetValue );
553 }
554 // add A & B => C or !A + !B + C
555 Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
556 {
557 pLits[i] = Abc_Var2Lit(Gia_Min2ObjSatId(p, Gia_Regular(pFanin)), !Gia_IsComplement(pFanin));
558 if ( fPolarFlip )
559 {
560 if ( Gia_Regular(pFanin)->fPhase ) pLits[i] = Abc_LitNot( pLits[i] );
561 }
562 }
563 pLits[nLits-1] = Abc_Var2Lit(Gia_Min2ObjSatId(p, pNode), 0);
564 if ( fPolarFlip )
565 {
566 if ( pNode->fPhase ) pLits[nLits-1] = Abc_LitNot( pLits[nLits-1] );
567 }
568 RetValue = satoko_add_clause( pSat, pLits, nLits );
569 assert( RetValue );
570 ABC_FREE( pLits );
571 }
572
573 /**Function*************************************************************
574
575 Synopsis [Adds clauses and returns CNF variable of the node.]
576
577 Description []
578
579 SideEffects []
580
581 SeeAlso []
582
583 ***********************************************************************/
Gia_Min2CollectSuper_rec(Gia_Obj_t * pObj,Vec_Ptr_t * vSuper,int fFirst,int fUseMuxes)584 void Gia_Min2CollectSuper_rec( Gia_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
585 {
586 // if the new node is complemented or a PI, another gate begins
587 if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) ||
588 (!fFirst && Gia_ObjValue(pObj) > 1) ||
589 (fUseMuxes && pObj->fMark0) )
590 {
591 Vec_PtrPushUnique( vSuper, pObj );
592 return;
593 }
594 // go through the branches
595 Gia_Min2CollectSuper_rec( Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes );
596 Gia_Min2CollectSuper_rec( Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes );
597 }
Gia_Min2CollectSuper(Gia_Obj_t * pObj,int fUseMuxes,Vec_Ptr_t * vSuper)598 void Gia_Min2CollectSuper( Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
599 {
600 assert( !Gia_IsComplement(pObj) );
601 assert( !Gia_ObjIsCi(pObj) );
602 Vec_PtrClear( vSuper );
603 Gia_Min2CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
604 }
Gia_Min2ObjAddToFrontier(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Ptr_t * vFrontier,satoko_t * pSat,Vec_Int_t * vSatVars)605 void Gia_Min2ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier, satoko_t * pSat, Vec_Int_t * vSatVars )
606 {
607 assert( !Gia_IsComplement(pObj) );
608 assert( !Gia_ObjIsConst0(pObj) );
609 if ( Gia_Min2ObjSatId(p, pObj) >= 0 )
610 return;
611 assert( Gia_Min2ObjSatId(p, pObj) == -1 );
612 Vec_IntPush( vSatVars, Gia_ObjId(p, pObj) );
613 Gia_Min2ObjSetSatId( p, pObj, satoko_add_variable(pSat, 0) );
614 if ( Gia_ObjIsAnd(pObj) )
615 Vec_PtrPush( vFrontier, pObj );
616 }
Gia_Min2ObjGetCnfVar(Gia_Man2Min_t * p,int iObj)617 int Gia_Min2ObjGetCnfVar( Gia_Man2Min_t * p, int iObj )
618 {
619 Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
620 Gia_Obj_t * pNode, * pFanin;
621 int i, k, fUseMuxes = 1;
622 if ( Gia_Min2ObjSatId(p->pGia, pObj) >= 0 )
623 return Gia_Min2ObjSatId(p->pGia, pObj);
624 if ( Gia_ObjIsCi(pObj) )
625 {
626 Vec_IntPush( p->vSatVars, iObj );
627 return Gia_Min2ObjSetSatId( p->pGia, pObj, satoko_add_variable(p->pSat, 0) );
628 }
629 assert( Gia_ObjIsAnd(pObj) );
630 // start the frontier
631 Vec_PtrClear( p->vFrontier );
632 Gia_Min2ObjAddToFrontier( p->pGia, pObj, p->vFrontier, p->pSat, p->vSatVars );
633 // explore nodes in the frontier
634 Vec_PtrForEachEntry( Gia_Obj_t *, p->vFrontier, pNode, i )
635 {
636 assert( Gia_Min2ObjSatId(p->pGia,pNode) >= 0 );
637 if ( fUseMuxes && pNode->fMark0 )
638 {
639 Vec_PtrClear( p->vFanins );
640 Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin0(pNode) ) );
641 Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin1(pNode) ) );
642 Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin0(pNode) ) );
643 Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin1(pNode) ) );
644 Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k )
645 Gia_Min2ObjAddToFrontier( p->pGia, Gia_Regular(pFanin), p->vFrontier, p->pSat, p->vSatVars );
646 Gia_Min2AddClausesMux( p->pGia, pNode, p->pSat );
647 }
648 else
649 {
650 Gia_Min2CollectSuper( pNode, fUseMuxes, p->vFanins );
651 Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k )
652 Gia_Min2ObjAddToFrontier( p->pGia, Gia_Regular(pFanin), p->vFrontier, p->pSat, p->vSatVars );
653 Gia_Min2AddClausesSuper( p->pGia, pNode, p->vFanins, p->pSat );
654 }
655 assert( Vec_PtrSize(p->vFanins) > 1 );
656 }
657 return Gia_Min2ObjSatId(p->pGia,pObj);
658 }
659
660 /**Function*************************************************************
661
662 Synopsis [Returns 0 if the node is not a constant.]
663
664 Description []
665
666 SideEffects []
667
668 SeeAlso []
669
670 ***********************************************************************/
Gia_Min2ManSimulate(Gia_Man2Min_t * p)671 int Gia_Min2ManSimulate( Gia_Man2Min_t * p )
672 {
673 word Sim0, Sim1; int n, i, iObj;
674 p->nSims++;
675 // add random values to new CIs
676 Vec_WrdFillExtra( p->vSims, Gia_ManObjNum(p->pGia), 0 );
677 for ( i = p->nCisOld; i < Gia_ManCiNum(p->pGia); i++ )
678 Vec_WrdWriteEntry( p->vSims, Gia_ManCiIdToId(p->pGia, i), Gia_ManRandomW( 0 ) << 1 );
679 p->nCisOld = Gia_ManCiNum(p->pGia);
680 // simulate internal nodes
681 for ( n = 0; n < 2; n++ )
682 Vec_IntForEachEntry( p->vObjs[n], iObj, i )
683 {
684 Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
685 Sim0 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId0p(p->pGia, pObj) );
686 Sim1 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId1p(p->pGia, pObj) );
687 Sim0 = Gia_ObjFaninC0(pObj) ? ~Sim0 : Sim0;
688 Sim1 = Gia_ObjFaninC1(pObj) ? ~Sim1 : Sim1;
689 Vec_WrdWriteEntry( p->vSims, iObj, Sim0 & Sim1 );
690 }
691 Sim0 = Vec_WrdEntry( p->vSims, Abc_Lit2Var(p->iLits[0]) );
692 Sim1 = Vec_WrdEntry( p->vSims, Abc_Lit2Var(p->iLits[1]) );
693 Sim0 = Abc_LitIsCompl(p->iLits[0]) ? ~Sim0 : Sim0;
694 Sim1 = Abc_LitIsCompl(p->iLits[1]) ? ~Sim1 : Sim1;
695 // assert( (Sim0 & Sim1) != ~0 );
696 return (Sim0 & Sim1) == 0;
697 }
698
699 /**Function*************************************************************
700
701 Synopsis [Internal simulation APIs.]
702
703 Description []
704
705 SideEffects []
706
707 SeeAlso []
708
709 ***********************************************************************/
Gia_Min2SimSetInputBit(Gia_Man2Min_t * p,int iObj,int Bit,int iPattern)710 static inline void Gia_Min2SimSetInputBit( Gia_Man2Min_t * p, int iObj, int Bit, int iPattern )
711 {
712 word * pSim = Vec_WrdEntryP( p->vSims, iObj );
713 assert( iPattern > 0 && iPattern < 64 );
714 if ( Abc_InfoHasBit( (unsigned*)pSim, iPattern ) != Bit )
715 Abc_InfoXorBit( (unsigned*)pSim, iPattern );
716 }
Gia_Min2ManSolve(Gia_Man2Min_t * p)717 int Gia_Min2ManSolve( Gia_Man2Min_t * p )
718 {
719 int iObj0 = Abc_Lit2Var(p->iLits[0]);
720 int iObj1 = Abc_Lit2Var(p->iLits[1]);
721 int n, i, status, iVar0, iVar1, iTemp;
722 assert( iObj0 > 0 && iObj1 > 0 );
723 // Vec_IntForEachEntry( &p->pGia->vCopies, iTemp, i )
724 // assert( iTemp == -1 );
725 Vec_IntFillExtra( &p->pGia->vCopies, Gia_ManObjNum(p->pGia), -1 );
726 Vec_IntClear( p->vSatVars );
727 assert( satoko_varnum(p->pSat) == 0 );
728 iVar0 = Gia_Min2ObjGetCnfVar( p, iObj0 );
729 iVar1 = Gia_Min2ObjGetCnfVar( p, iObj1 );
730 satoko_assump_push( p->pSat, Abc_Var2Lit(iVar0, Abc_LitIsCompl(p->iLits[0])) );
731 satoko_assump_push( p->pSat, Abc_Var2Lit(iVar1, Abc_LitIsCompl(p->iLits[1])) );
732 status = satoko_solve( p->pSat );
733 satoko_assump_pop( p->pSat );
734 satoko_assump_pop( p->pSat );
735 if ( status == SATOKO_SAT )
736 {
737 //printf( "Disproved %d %d\n", p->iLits[0], p->iLits[1] );
738 assert( Gia_Min2ManSimulate(p) == 1 );
739 for ( n = 0; n < 2; n++ )
740 Vec_IntForEachEntry( p->vCis[n], iTemp, i )
741 Gia_Min2SimSetInputBit( p, iTemp, satoko_var_polarity(p->pSat, Gia_Min2ObjSatId(p->pGia, Gia_ManObj(p->pGia, iTemp))) == SATOKO_LIT_TRUE, p->iPattern );
742 //assert( Gia_Min2ManSimulate(p) == 0 );
743 p->iPattern = p->iPattern == 63 ? 1 : p->iPattern + 1;
744 p->nSatSat++;
745 }
746 //printf( "supp %d node %d vars %d\n",
747 // Vec_IntSize(p->vCis[0]) + Vec_IntSize(p->vCis[1]),
748 // Vec_IntSize(p->vObjs[0]) + Vec_IntSize(p->vObjs[1]),
749 // Vec_IntSize(p->vSatVars) );
750 satoko_rollback( p->pSat );
751 Vec_IntForEachEntry( p->vSatVars, iTemp, i )
752 Gia_Min2ObjCleanSatId( p->pGia, Gia_ManObj(p->pGia, iTemp) );
753 return status == SATOKO_UNSAT;
754 }
755
756 /**Function*************************************************************
757
758 Synopsis [Collect nodes.]
759
760 Description []
761
762 SideEffects []
763
764 SeeAlso []
765
766 ***********************************************************************/
Gia_Min2ManGatherSupp_rec(Gia_Man_t * p,int iObj,Vec_Int_t * vCis,Vec_Int_t * vObjs)767 static inline int Gia_Min2ManGatherSupp_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vCis, Vec_Int_t * vObjs )
768 {
769 int Val0, Val1;
770 Gia_Obj_t * pObj;
771 if ( Gia_ObjIsTravIdPreviousId(p, iObj) )
772 return 1;
773 if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
774 return 0;
775 Gia_ObjSetTravIdCurrentId(p, iObj);
776 pObj = Gia_ManObj( p, iObj );
777 if ( Gia_ObjIsCi(pObj) )
778 {
779 Vec_IntPush( vCis, iObj );
780 return 0;
781 }
782 assert( Gia_ObjIsAnd(pObj) );
783 Val0 = Gia_Min2ManGatherSupp_rec( p, Gia_ObjFaninId0(pObj, iObj), vCis, vObjs );
784 Val1 = Gia_Min2ManGatherSupp_rec( p, Gia_ObjFaninId1(pObj, iObj), vCis, vObjs );
785 Vec_IntPush( vObjs, iObj );
786 return Val0 || Val1;
787 }
Gia_Min2ManGatherSupp(Gia_Man2Min_t * p)788 int Gia_Min2ManGatherSupp( Gia_Man2Min_t * p )
789 {
790 int n, Overlap = 0;
791 p->nSupps++;
792 Gia_ManIncrementTravId( p->pGia );
793 for ( n = 0; n < 2; n++ )
794 {
795 Vec_IntClear( p->vCis[n] );
796 Vec_IntClear( p->vObjs[n] );
797 Gia_ManIncrementTravId( p->pGia );
798 Overlap = Gia_Min2ManGatherSupp_rec( p->pGia, Abc_Lit2Var(p->iLits[n]), p->vCis[n], p->vObjs[n] );
799 assert( n || !Overlap );
800 }
801 return Overlap;
802 }
803
804 /**Function*************************************************************
805
806 Synopsis [Takes a literal and returns a support-minized literal.]
807
808 Description []
809
810 SideEffects []
811
812 SeeAlso []
813
814 ***********************************************************************/
Gia_Man2SupportAnd(Gia_Man2Min_t * p,int iLit0,int iLit1)815 int Gia_Man2SupportAnd( Gia_Man2Min_t * p, int iLit0, int iLit1 )
816 {
817 p->nCalls++;
818 //return Gia_ManHashAnd( p->pGia, iLit0, iLit1 );
819 p->iLits[0] = iLit0;
820 p->iLits[1] = iLit1;
821 if ( iLit0 < 2 || iLit1 < 2 || Abc_Lit2Var(iLit0) == Abc_Lit2Var(iLit1) || Gia_ManHashLookupInt(p->pGia, iLit0, iLit1) ||
822 !Gia_Min2ManGatherSupp(p) || !Gia_Min2ManSimulate(p) || !Gia_Min2ManSolve(p) )
823 return Gia_ManHashAnd( p->pGia, iLit0, iLit1 );
824 //printf( "%d %d\n", iLit0, iLit1 );
825 p->nSatUnsat++;
826 return 0;
827 }
828
829 /**Function*************************************************************
830
831 Synopsis [Testbench.]
832
833 Description []
834
835 SideEffects []
836
837 SeeAlso []
838
839 ***********************************************************************/
Gia_Man2SupportAndTest(Gia_Man_t * pGia)840 Gia_Man_t * Gia_Man2SupportAndTest( Gia_Man_t * pGia )
841 {
842 Gia_Man2Min_t * pMan;
843 Gia_Man_t * pNew, * pTemp;
844 Gia_Obj_t * pObj;
845 int i;
846 Gia_ManRandomW( 1 );
847 Gia_ManFillValue( pGia );
848 pNew = Gia_ManStart( Gia_ManObjNum(pGia) );
849 pNew->pName = Abc_UtilStrsav( pGia->pName );
850 pNew->pSpec = Abc_UtilStrsav( pGia->pSpec );
851 Gia_ManHashAlloc( pNew );
852 Gia_ManConst0(pGia)->Value = 0;
853 pMan = Gia_Man2SuppStart( pNew );
854 Gia_ManForEachObj1( pGia, pObj, i )
855 {
856 if ( Gia_ObjIsAnd(pObj) )
857 {
858 // pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
859 pObj->Value = Gia_Man2SupportAnd( pMan, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
860 }
861 else if ( Gia_ObjIsCi(pObj) )
862 pObj->Value = Gia_ManAppendCi( pNew );
863 else if ( Gia_ObjIsCo(pObj) )
864 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
865 else assert( 0 );
866
867 //if ( i % 10000 == 0 )
868 // printf( "%d\n", i );
869 }
870 Gia_Man2SuppStop( pMan );
871 Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia) );
872 pNew = Gia_ManCleanup( pTemp = pNew );
873 Gia_ManStop( pTemp );
874 return pNew;
875 }
876
877
878
879
880 ////////////////////////////////////////////////////////////////////////
881 /// END OF FILE ///
882 ////////////////////////////////////////////////////////////////////////
883
884
885 ABC_NAMESPACE_IMPL_END
886
887