1 /**CFile****************************************************************
2
3 FileName [abcFunc.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Network and node package.]
8
9 Synopsis [Experimental procedures.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: abcFunc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "acb.h"
22 #include "aig/miniaig/ndr.h"
23 #include "sat/cnf/cnf.h"
24 #include "sat/bsat/satStore.h"
25 #include "sat/satoko/satoko.h"
26 #include "map/mio/mio.h"
27 #include "misc/util/utilTruth.h"
28 #include "aig/gia/giaAig.h"
29
30 ABC_NAMESPACE_IMPL_START
31
32 ////////////////////////////////////////////////////////////////////////
33 /// DECLARATIONS ///
34 ////////////////////////////////////////////////////////////////////////
35
36 #define ACB_LAST_NAME_ID 14
37
38 typedef enum {
39 ACB_NONE = 0, // 0: unused
40 ACB_MODULE, // 1: "module"
41 ACB_ENDMODULE, // 2: "endmodule"
42 ACB_INPUT, // 3: "input"
43 ACB_OUTPUT, // 4: "output"
44 ACB_WIRE, // 5: "wire"
45 ACB_BUF, // 6: "buf"
46 ACB_NOT, // 7: "not"
47 ACB_AND, // 8: "and"
48 ACB_NAND, // 9: "nand"
49 ACB_OR, // 10: "or"
50 ACB_NOR, // 11: "nor"
51 ACB_XOR, // 12: "xor"
52 ACB_XNOR, // 13: "xnor"
53 ACB_UNUSED // 14: unused
54 } Acb_KeyWords_t;
55
Acb_Num2Name(int i)56 static inline char * Acb_Num2Name( int i )
57 {
58 if ( i == 1 ) return "module";
59 if ( i == 2 ) return "endmodule";
60 if ( i == 3 ) return "input";
61 if ( i == 4 ) return "output";
62 if ( i == 5 ) return "wire";
63 if ( i == 6 ) return "buf";
64 if ( i == 7 ) return "not";
65 if ( i == 8 ) return "and";
66 if ( i == 9 ) return "nand";
67 if ( i == 10 ) return "or";
68 if ( i == 11 ) return "nor";
69 if ( i == 12 ) return "xor";
70 if ( i == 13 ) return "xnor";
71 return NULL;
72 }
73
Acb_Type2Oper(int i)74 static inline int Acb_Type2Oper( int i )
75 {
76 if ( i == 6 ) return ABC_OPER_BIT_BUF;
77 if ( i == 7 ) return ABC_OPER_BIT_INV;
78 if ( i == 8 ) return ABC_OPER_BIT_AND;
79 if ( i == 9 ) return ABC_OPER_BIT_NAND;
80 if ( i == 10 ) return ABC_OPER_BIT_OR;
81 if ( i == 11 ) return ABC_OPER_BIT_NOR;
82 if ( i == 12 ) return ABC_OPER_BIT_XOR;
83 if ( i == 13 ) return ABC_OPER_BIT_NXOR;
84 assert( 0 );
85 return -1;
86 }
87
Acb_Oper2Name(int i)88 static inline char * Acb_Oper2Name( int i )
89 {
90 if ( i == ABC_OPER_CONST_F ) return "const0";
91 if ( i == ABC_OPER_CONST_T ) return "const1";
92 if ( i == ABC_OPER_BIT_BUF ) return "buf";
93 if ( i == ABC_OPER_BIT_INV ) return "not";
94 if ( i == ABC_OPER_BIT_AND ) return "and";
95 if ( i == ABC_OPER_BIT_NAND ) return "nand";
96 if ( i == ABC_OPER_BIT_OR ) return "or";
97 if ( i == ABC_OPER_BIT_NOR ) return "nor";
98 if ( i == ABC_OPER_BIT_XOR ) return "xor";
99 if ( i == ABC_OPER_BIT_NXOR ) return "xnor";
100 assert( 0 );
101 return NULL;
102 }
103
104 ////////////////////////////////////////////////////////////////////////
105 /// FUNCTION DEFINITIONS ///
106 ////////////////////////////////////////////////////////////////////////
107
108 /**Function*************************************************************
109
110 Synopsis [Installs the required standard cell library.]
111
112 Description []
113
114 SideEffects []
115
116 SeeAlso []
117
118 ***********************************************************************/
119 char * pLibStr[25] = {
120 "GATE buf 1 O=a; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
121 "GATE inv 1 O=!a; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
122 "GATE and2 1 O=a*b; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
123 "GATE and3 1 O=a*b*c; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
124 "GATE and4 1 O=a*b*c*d; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
125 "GATE or2 1 O=a+b; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
126 "GATE or3 1 O=a+b+c; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
127 "GATE or4 1 O=a+b+c+d; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
128 "GATE nand2 1 O=!(a*b); PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
129 "GATE nand3 1 O=!(a*b*c); PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
130 "GATE nand4 1 O=!(a*b*c*d); PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
131 "GATE nor2 1 O=!(a+b); PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
132 "GATE nor3 1 O=!(a+b+c); PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
133 "GATE nor4 1 O=!(a+b+c+d); PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
134 "GATE xor 1 O=!a*b+a*!b; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
135 "GATE xnor 1 O=a*b+!a*!b; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
136 "GATE zero 0 O=CONST0;\n"
137 "GATE one 0 O=CONST1;\n"
138 };
Acb_IntallLibrary()139 void Acb_IntallLibrary()
140 {
141 extern Mio_Library_t * Mio_LibraryReadBuffer( char * pBuffer, int fExtendedFormat, st__table * tExcludeGate, int fVerbose );
142 Mio_Library_t * pLib;
143 int i;
144 // create library string
145 Vec_Str_t * vLibStr = Vec_StrAlloc( 1000 );
146 for ( i = 0; pLibStr[i]; i++ )
147 Vec_StrAppend( vLibStr, pLibStr[i] );
148 Vec_StrPush( vLibStr, '\0' );
149 // create library
150 pLib = Mio_LibraryReadBuffer( Vec_StrArray(vLibStr), 0, NULL, 0 );
151 Mio_LibrarySetName( pLib, Abc_UtilStrsav("iccad17.genlib") );
152 Mio_UpdateGenlib( pLib );
153 Vec_StrFree( vLibStr );
154 }
155
156 /**Function*************************************************************
157
158 Synopsis [Parse Verilog file into an intermediate representation.]
159
160 Description []
161
162 SideEffects []
163
164 SeeAlso []
165
166 ***********************************************************************/
Acb_VerilogStartNames()167 Abc_Nam_t * Acb_VerilogStartNames()
168 {
169 Abc_Nam_t * pNames = Abc_NamStart( 100, 16 );
170 int i, NameId, fFound;
171 for ( i = 1; i < ACB_UNUSED; i++ )
172 {
173 NameId = Abc_NamStrFindOrAdd( pNames, Acb_Num2Name(i), &fFound );
174 assert( i == NameId && !fFound );
175 }
176 return pNames;
177 }
Acb_VerilogRemoveComments(char * pBuffer)178 void Acb_VerilogRemoveComments ( char * pBuffer )
179 {
180 char * pTemp;
181 for ( pTemp = pBuffer; *pTemp; pTemp++ )
182 if ( pTemp[0] == '/' && pTemp[1] == '/' )
183 while ( *pTemp && *pTemp != '\n' )
184 *pTemp++ = ' ';
185 }
Acb_VerilogSimpleLex(char * pFileName,Abc_Nam_t * pNames)186 Vec_Int_t * Acb_VerilogSimpleLex( char * pFileName, Abc_Nam_t * pNames )
187 {
188 Vec_Int_t * vBuffer = Vec_IntAlloc( 1000 );
189 char * pBuffer = Extra_FileReadContents( pFileName );
190 char * pToken, * pStart, * pLimit = pBuffer + strlen(pBuffer);
191 if ( pBuffer == NULL )
192 return NULL;
193 Acb_VerilogRemoveComments( pBuffer );
194 pToken = strtok( pBuffer, " \n\r\t(),;=" );
195 while ( pToken )
196 {
197 int iToken = Abc_NamStrFindOrAdd( pNames, pToken, NULL );
198 if ( !strcmp(pToken, "assign") )
199 Vec_IntPush( vBuffer, ACB_BUF );
200 else
201 Vec_IntPush( vBuffer, iToken );
202 if ( iToken >= ACB_BUF && iToken < ACB_UNUSED )
203 {
204 for ( pStart = pToken; pStart < pLimit && *pStart != '\n'; pStart++ )
205 if ( *pStart == '(' )
206 break;
207 if ( *pStart == '(' )
208 {
209 pToken = strtok( pStart, " \n\r\t(),;=" );
210 continue;
211 }
212 }
213 pToken = strtok( NULL, " \n\r\t(),;=" );
214 }
215 ABC_FREE( pBuffer );
216 return vBuffer;
217 }
Acb_WireIsTarget(int Token,Abc_Nam_t * pNames)218 int Acb_WireIsTarget( int Token, Abc_Nam_t * pNames )
219 {
220 char * pStr = Abc_NamStr(pNames, Token);
221 return pStr[0] == 't' && pStr[1] == '_';
222 }
Acb_VerilogSimpleParse(Vec_Int_t * vBuffer,Abc_Nam_t * pNames)223 void * Acb_VerilogSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames )
224 {
225 Ndr_Data_t * pDesign = NULL;
226 Vec_Int_t * vInputs = Vec_IntAlloc(100);
227 Vec_Int_t * vOutputs = Vec_IntAlloc(100);
228 Vec_Int_t * vWires = Vec_IntAlloc(100);
229 Vec_Int_t * vTypes = Vec_IntAlloc(100);
230 Vec_Int_t * vFanins = Vec_IntAlloc(100);
231 Vec_Int_t * vCur = NULL;
232 int i, ModuleID, Token, Size, Count = 0;
233 assert( Vec_IntEntry(vBuffer, 0) == ACB_MODULE );
234 Vec_IntForEachEntryStart( vBuffer, Token, i, 2 )
235 {
236 if ( vCur == NULL && Token >= ACB_UNUSED )
237 continue;
238 if ( Token == ACB_ENDMODULE )
239 break;
240 if ( Token == ACB_INPUT )
241 vCur = vInputs;
242 else if ( Token == ACB_OUTPUT )
243 vCur = vOutputs;
244 else if ( Token == ACB_WIRE )
245 vCur = vWires;
246 else if ( Token >= ACB_BUF && Token <= ACB_XNOR )
247 {
248 //char * pToken = Abc_NamStr(pNames, Vec_IntEntry(vBuffer, i+1));
249 Vec_IntPush( vTypes, Token );
250 Vec_IntPush( vTypes, Vec_IntSize(vFanins) );
251 vCur = vFanins;
252 //if ( pToken[1] == 'z' && pToken[2] == '_' && pToken[3] == 'g' && pToken[4] == '_' )
253 // i++;
254 }
255 else
256 Vec_IntPush( vCur, Token );
257 }
258 Vec_IntPush( vTypes, -1 );
259 Vec_IntPush( vTypes, Vec_IntSize(vFanins) );
260 // create design
261 pDesign = Ndr_Create( Vec_IntEntry(vBuffer, 1) );
262 ModuleID = Ndr_AddModule( pDesign, Vec_IntEntry(vBuffer, 1) );
263 // create inputs
264 Ndr_DataResize( pDesign, Vec_IntSize(vInputs) );
265 Vec_IntForEachEntry( vInputs, Token, i )
266 Ndr_DataPush( pDesign, NDR_INPUT, Token );
267 Ndr_DataAddTo( pDesign, ModuleID-256, Vec_IntSize(vInputs) );
268 Ndr_DataAddTo( pDesign, 0, Vec_IntSize(vInputs) );
269 // create outputs
270 Ndr_DataResize( pDesign, Vec_IntSize(vOutputs) );
271 Vec_IntForEachEntry( vOutputs, Token, i )
272 Ndr_DataPush( pDesign, NDR_OUTPUT, Token );
273 Ndr_DataAddTo( pDesign, ModuleID-256, Vec_IntSize(vOutputs) );
274 Ndr_DataAddTo( pDesign, 0, Vec_IntSize(vOutputs) );
275 // create targets
276 Ndr_DataResize( pDesign, Vec_IntSize(vWires) );
277 Vec_IntForEachEntry( vWires, Token, i )
278 if ( Acb_WireIsTarget(Token, pNames) )
279 Ndr_DataPush( pDesign, NDR_TARGET, Token ), Count++;
280 Ndr_DataAddTo( pDesign, ModuleID-256, Count );
281 Ndr_DataAddTo( pDesign, 0, Count );
282 // create nodes
283 Vec_IntForEachEntry( vInputs, Token, i )
284 Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CI, 0, 0, 0, 0, 0, NULL, 1, &Token, NULL ); // no fanins
285 if ( (Token = Abc_NamStrFind(pNames, "1\'b0")) )
286 Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CONST_F, 0, 0, 0, 0, 0, NULL, 1, &Token, NULL ); // no fanins
287 if ( (Token = Abc_NamStrFind(pNames, "1\'b1")) )
288 Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CONST_T, 0, 0, 0, 0, 0, NULL, 1, &Token, NULL ); // no fanins
289 Vec_IntForEachEntryDouble( vTypes, Token, Size, i )
290 if ( Token > 0 )
291 {
292 int Output = Vec_IntEntry(vFanins, Size);
293 int nFanins = Vec_IntEntry(vTypes, i+3) - Size - 1;
294 int * pFanins = Vec_IntEntryP(vFanins, Size+1);
295 Ndr_AddObject( pDesign, ModuleID, Acb_Type2Oper(Token), 0, 0, 0, 0, nFanins, pFanins, 1, &Output, NULL ); // many fanins
296 }
297 Vec_IntForEachEntry( vOutputs, Token, i )
298 Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CO, 0, 0, 0, 0, 1, &Token, 1, &Token, NULL ); // one fanin
299 // cleanup
300 Vec_IntFree( vInputs );
301 Vec_IntFree( vOutputs );
302 Vec_IntFree( vWires );
303 Vec_IntFree( vTypes );
304 Vec_IntFree( vFanins );
305 return pDesign;
306 }
307
308 /**Function*************************************************************
309
310 Synopsis [Read weights of nodes from the weight file.]
311
312 Description []
313
314 SideEffects []
315
316 SeeAlso []
317
318 ***********************************************************************/
Acb_ReadWeightMap(char * pFileName,Abc_Nam_t * pNames)319 Vec_Int_t * Acb_ReadWeightMap( char * pFileName, Abc_Nam_t * pNames )
320 {
321 Vec_Int_t * vWeights = Vec_IntStartFull( Abc_NamObjNumMax(pNames) );
322 char * pBuffer = Extra_FileReadContents( pFileName );
323 char * pToken, * pNum;
324 if ( pBuffer == NULL )
325 return NULL;
326 pToken = strtok( pBuffer, " \n\r()," );
327 pNum = strtok( NULL, " \n\r()," );
328 while ( pToken )
329 {
330 int NameId = Abc_NamStrFind(pNames, pToken);
331 int Number = atoi(pNum);
332 if ( NameId <= 0 )
333 {
334 printf( "Cannot find name \"%s\" among node names of this network.\n", pToken );
335 continue;
336 }
337 Vec_IntWriteEntry( vWeights, NameId, Number );
338 pToken = strtok( NULL, " \n\r(),;" );
339 pNum = strtok( NULL, " \n\r(),;" );
340 }
341 ABC_FREE( pBuffer );
342 return vWeights;
343 }
344
345 /**Function*************************************************************
346
347 Synopsis [Create network from the intermediate representation.]
348
349 Description []
350
351 SideEffects []
352
353 SeeAlso []
354
355 ***********************************************************************/
Acb_VerilogSimpleRead(char * pFileName,char * pFileNameW)356 Acb_Ntk_t * Acb_VerilogSimpleRead( char * pFileName, char * pFileNameW )
357 {
358 extern Acb_Ntk_t * Acb_NtkFromNdr( char * pFileName, void * pModule, Abc_Nam_t * pNames, Vec_Int_t * vWeights, int nNameIdMax );
359 Acb_Ntk_t * pNtk;
360 Abc_Nam_t * pNames = Acb_VerilogStartNames();
361 Vec_Int_t * vBuffer = Acb_VerilogSimpleLex( pFileName, pNames );
362 void * pModule = vBuffer ? Acb_VerilogSimpleParse( vBuffer, pNames ) : NULL;
363 Vec_Int_t * vWeights = pFileNameW ? Acb_ReadWeightMap( pFileNameW, pNames ) : NULL;
364 if ( pFileName && pModule == NULL )
365 {
366 printf( "Cannot read input file \"%s\".\n", pFileName );
367 return NULL;
368 }
369 if ( pFileNameW && vWeights == NULL )
370 {
371 printf( "Cannot read weight file \"%s\".\n", pFileNameW );
372 return NULL;
373 }
374 // Ndr_ModuleWriteVerilog( "iccad17/unit1/test.v", pModule, pNameStrs );
375 pNtk = Acb_NtkFromNdr( pFileName, pModule, pNames, vWeights, Abc_NamObjNumMax(pNames) );
376 Ndr_Delete( pModule );
377 Vec_IntFree( vBuffer );
378 Vec_IntFreeP( &vWeights );
379 Abc_NamDeref( pNames );
380 return pNtk;
381 }
382
383 /**Function*************************************************************
384
385 Synopsis [Write Verilog for sanity checking.]
386
387 Description []
388
389 SideEffects []
390
391 SeeAlso []
392
393 ***********************************************************************/
Acb_VerilogSimpleWrite(Acb_Ntk_t * p,char * pFileName)394 void Acb_VerilogSimpleWrite( Acb_Ntk_t * p, char * pFileName )
395 {
396 int i, iObj, fFirst = 1;
397 FILE * pFile = fopen( pFileName, "wb" );
398 if ( pFile == NULL ) { printf( "Cannot open file \"%s\" for writing.\n", pFileName ); return; }
399
400 fprintf( pFile, "\nmodule %s (\n ", Acb_NtkName(p) );
401
402 Acb_NtkForEachPi( p, iObj, i )
403 fprintf( pFile, "%s, ", Acb_ObjNameStr(p, iObj) );
404 fprintf( pFile, "\n " );
405
406 Acb_NtkForEachPo( p, iObj, i )
407 fprintf( pFile, "%s%s", fFirst ? "":", ", Acb_ObjNameStr(p, iObj) ), fFirst = 0;
408 fprintf( pFile, "\n);\n\n" );
409
410 Acb_NtkForEachPi( p, iObj, i )
411 fprintf( pFile, " input %s;\n", Acb_ObjNameStr(p, iObj) );
412 fprintf( pFile, "\n" );
413
414 Acb_NtkForEachPo( p, iObj, i )
415 fprintf( pFile, " output %s;\n", Acb_ObjNameStr(p, iObj) );
416 fprintf( pFile, "\n" );
417
418 Acb_NtkForEachNode( p, iObj )
419 if ( Acb_ObjFaninNum(p, iObj) > 0 )
420 fprintf( pFile, " wire %s;\n", Acb_ObjNameStr(p, iObj) );
421 fprintf( pFile, "\n" );
422
423 Acb_NtkForEachNode( p, iObj )
424 if ( Acb_ObjFaninNum(p, iObj) > 0 )
425 {
426 int * pFanin, iFanin, k, start = ftell(pFile)+55;
427 fprintf( pFile, " %s (", Acb_Oper2Name( Acb_ObjType(p, iObj) ) );
428 fprintf( pFile, " %s", Acb_ObjNameStr(p, iObj) );
429 Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, k )
430 //if ( iFanin == 0 ) fprintf( pFile, ", <zero>" ); else
431 fprintf( pFile, ", %s", Acb_ObjNameStr(p, iFanin) );
432 fprintf( pFile, " );" );
433 if ( Acb_NtkHasObjWeights(p) && Acb_ObjWeight(p, iObj) > 0 )
434 fprintf( pFile, " %*s // weight = %d", (int)(start-ftell(pFile)), "", Acb_ObjWeight(p, iObj) );
435 fprintf( pFile, "\n" );
436 }
437 else // constant nodes
438 {
439 assert( Acb_ObjType(p, iObj) == ABC_OPER_CONST_F || Acb_ObjType(p, iObj) == ABC_OPER_CONST_T );
440 fprintf( pFile, " %s (", Acb_Oper2Name( ABC_OPER_BIT_BUF ) );
441 fprintf( pFile, " 1\'b%d", Acb_ObjType(p, iObj) == ABC_OPER_CONST_T );
442 fprintf( pFile, " );\n" );
443 }
444
445 fprintf( pFile, "\nendmodule\n\n" );
446 fclose( pFile );
447 }
448
449
450
451
452
453
454
455 /**Function*************************************************************
456
457 Synopsis [Compute roots (PO nodes in the TFO of the targets in F).]
458
459 Description []
460
461 SideEffects []
462
463 SeeAlso []
464
465 ***********************************************************************/
Acb_NtkFindRoots_rec(Acb_Ntk_t * p,int iObj,Vec_Bit_t * vBlock)466 int Acb_NtkFindRoots_rec( Acb_Ntk_t * p, int iObj, Vec_Bit_t * vBlock )
467 {
468 int * pFanin, iFanin, i, Res = 0;
469 if ( Acb_ObjIsTravIdPrev(p, iObj) )
470 return 1;
471 if ( Acb_ObjSetTravIdCur(p, iObj) )
472 return 0;
473 assert( !Acb_ObjIsCi(p, iObj) );
474 Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, i )
475 Res |= Acb_NtkFindRoots_rec( p, iFanin, vBlock );
476 if ( Res ) Acb_ObjSetTravIdPrev( p, iObj );
477 if ( Res ) Vec_BitWriteEntry( vBlock, iObj, 1 );
478 return Res;
479 }
Acb_NtkFindRoots(Acb_Ntk_t * p,Vec_Int_t * vTargets,Vec_Bit_t ** pvBlock)480 Vec_Int_t * Acb_NtkFindRoots( Acb_Ntk_t * p, Vec_Int_t * vTargets, Vec_Bit_t ** pvBlock )
481 {
482 int i, iObj;
483 Vec_Int_t * vRoots = Vec_IntAlloc( 1000 );
484 Vec_Bit_t * vBlock = Vec_BitStart( Acb_NtkObjNum(p) );
485 *pvBlock = vBlock;
486 // mark targets
487 Acb_NtkIncTravId( p );
488 assert( Vec_IntSize(vTargets) > 0 );
489 Vec_IntForEachEntry( vTargets, iObj, i )
490 {
491 Acb_ObjSetTravIdCur( p, iObj );
492 Vec_BitWriteEntry( vBlock, iObj, 1 );
493 }
494 // mark inputs
495 Acb_NtkIncTravId( p );
496 Acb_NtkForEachCi( p, iObj, i )
497 Acb_ObjSetTravIdCur( p, iObj );
498 // collect outputs reachable from targets
499 Acb_NtkForEachCoDriver( p, iObj, i )
500 if ( Acb_NtkFindRoots_rec(p, iObj, vBlock) )
501 Vec_IntPush( vRoots, i );
502 //Vec_IntPrint( vRoots );
503 return vRoots;
504 }
505
506 /**Function*************************************************************
507
508 Synopsis [Compute support in the TFI of the roots.]
509
510 Description []
511
512 SideEffects []
513
514 SeeAlso []
515
516 ***********************************************************************/
Acb_NtkFindSupp_rec(Acb_Ntk_t * p,int iObj,Vec_Int_t * vSupp)517 void Acb_NtkFindSupp_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vSupp )
518 {
519 int * pFanin, iFanin, i;
520 if ( Acb_ObjSetTravIdCur(p, iObj) )
521 return;
522 if ( Acb_ObjIsCi(p, iObj) )
523 Vec_IntPush( vSupp, Acb_ObjCioId(p, iObj) );
524 else
525 Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, i )
526 Acb_NtkFindSupp_rec( p, iFanin, vSupp );
527 }
Acb_NtkFindSupp(Acb_Ntk_t * p,Vec_Int_t * vRoots)528 Vec_Int_t * Acb_NtkFindSupp( Acb_Ntk_t * p, Vec_Int_t * vRoots )
529 {
530 int i, iObj;
531 Vec_Int_t * vSupp = Vec_IntAlloc( 1000 );
532 Acb_NtkIncTravId( p );
533 Acb_NtkForEachCoDriverVec( vRoots, p, iObj, i )
534 Acb_NtkFindSupp_rec( p, iObj, vSupp );
535 Vec_IntSort( vSupp, 0 );
536 //Vec_IntPrint( vSupp );
537 return vSupp;
538 }
539
540 /**Function*************************************************************
541
542 Synopsis [Collect divisors whose support is completely contained in vSupp.]
543
544 Description []
545
546 SideEffects []
547
548 SeeAlso []
549
550 ***********************************************************************/
Acb_NtkFindDivs_rec(Acb_Ntk_t * p,int iObj)551 int Acb_NtkFindDivs_rec( Acb_Ntk_t * p, int iObj )
552 {
553 int * pFanin, iFanin, i, Res = 1;
554 if ( Acb_ObjIsTravIdPrev(p, iObj) )
555 return 1;
556 if ( Acb_ObjSetTravIdCur(p, iObj) )
557 return 0;
558 if ( Acb_ObjIsCi(p, iObj) )
559 return 0;
560 Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, i )
561 Res &= Acb_NtkFindDivs_rec( p, iFanin );
562 if ( Res ) Acb_ObjSetTravIdPrev( p, iObj );
563 return Res;
564 }
Acb_NtkFindDivsCis(Acb_Ntk_t * p,Vec_Int_t * vSupp)565 Vec_Int_t * Acb_NtkFindDivsCis( Acb_Ntk_t * p, Vec_Int_t * vSupp )
566 {
567 int i, iObj;
568 Vec_Int_t * vDivs = Vec_IntAlloc( Vec_IntSize(vSupp) );
569 Acb_NtkForEachCiVec( vSupp, p, iObj, i )
570 {
571 assert( Acb_ObjWeight(p, iObj) > 0 );
572 Vec_IntPush( vDivs, iObj );
573 }
574 printf( "Divisors are %d support variables (CIs in the TFO of the targets).\n", Vec_IntSize(vSupp) );
575 return vDivs;
576 }
Acb_NtkFindDivs(Acb_Ntk_t * p,Vec_Int_t * vSupp,Vec_Bit_t * vBlock,int fVerbose)577 Vec_Int_t * Acb_NtkFindDivs( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Bit_t * vBlock, int fVerbose )
578 {
579 int fPrintWeights = 0;
580 int nDivLimit = 3000;
581 int i, iObj;
582 Vec_Int_t * vDivs = Vec_IntAlloc( 1000 );
583 // mark inputs
584 Acb_NtkIncTravId( p );
585 Acb_NtkForEachCiVec( vSupp, p, iObj, i )
586 {
587 Acb_ObjSetTravIdCur( p, iObj );
588 if ( Acb_ObjWeight(p, iObj) > 0 )
589 Vec_IntPush( vDivs, iObj );
590 }
591 // collect nodes whose support is contained in vSupp
592 Acb_NtkIncTravId( p );
593 Acb_NtkForEachNode( p, iObj )
594 if ( !Vec_BitEntry(vBlock, iObj) && Acb_ObjWeight(p, iObj) > 0 && Acb_NtkFindDivs_rec(p, iObj) )
595 Vec_IntPush( vDivs, iObj );
596 // sort divisors by cost (first cheap ones; later expensive ones)
597 Vec_IntSelectSortCost( Vec_IntArray(vDivs), Vec_IntSize(vDivs), &p->vObjWeight );
598 //Vec_IntPrint( vDivs );
599 nDivLimit = Abc_MinInt( Vec_IntSize(vDivs), nDivLimit );
600 if ( fPrintWeights )
601 {
602 // Vec_IntForEachEntryStop( vDivs, iObj, i, nDivLimit )
603 // printf( "%d:%d (w=%d) ", i, iObj, Vec_IntEntry(&p->vObjWeight, iObj) );
604 // printf( "\n" );
605
606 printf( " : " );
607 Vec_IntForEachEntryStop( vDivs, iObj, i, nDivLimit )
608 printf( "%d", (Vec_IntEntry(&p->vObjWeight, iObj) / 100) % 10 );
609 printf( "\n" );
610 printf( " : " );
611 Vec_IntForEachEntryStop( vDivs, iObj, i, nDivLimit )
612 printf( "%d", (Vec_IntEntry(&p->vObjWeight, iObj) / 10) % 10 );
613 printf( "\n" );
614 printf( " : " );
615 Vec_IntForEachEntryStop( vDivs, iObj, i, nDivLimit )
616 printf( "%d", (Vec_IntEntry(&p->vObjWeight, iObj) / 1) % 10 );
617 printf( "\n" );
618 }
619 if ( fVerbose )
620 printf( "Reducing divisor set from %d to ", Vec_IntSize(vDivs) );
621 Vec_IntShrink( vDivs, nDivLimit );
622 if ( fVerbose )
623 printf( "%d.\n", Vec_IntSize(vDivs) );
624 return vDivs;
625 }
626
627 /**Function*************************************************************
628
629 Synopsis [Compute support and internal nodes in the TFI of the roots.]
630
631 Description []
632
633 SideEffects []
634
635 SeeAlso []
636
637 ***********************************************************************/
Acb_NtkFindNodes_rec(Acb_Ntk_t * p,int iObj,Vec_Int_t * vNodes)638 void Acb_NtkFindNodes_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vNodes )
639 {
640 int * pFanin, iFanin, i;
641 if ( Acb_ObjSetTravIdCur(p, iObj) )
642 return;
643 if ( Acb_ObjIsCi(p, iObj) )
644 return;
645 Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, i )
646 Acb_NtkFindNodes_rec( p, iFanin, vNodes );
647 assert( !Acb_ObjIsCo(p, iObj) );
648 Vec_IntPush( vNodes, iObj );
649 }
Acb_NtkFindNodes(Acb_Ntk_t * p,Vec_Int_t * vRoots,Vec_Int_t * vDivs)650 Vec_Int_t * Acb_NtkFindNodes( Acb_Ntk_t * p, Vec_Int_t * vRoots, Vec_Int_t * vDivs )
651 {
652 int i, iObj;
653 Vec_Int_t * vNodes = Vec_IntAlloc( 1000 );
654 Acb_NtkIncTravId( p );
655 Acb_NtkForEachCoDriverVec( vRoots, p, iObj, i )
656 Acb_NtkFindNodes_rec( p, iObj, vNodes );
657 if ( vDivs )
658 Vec_IntForEachEntry( vDivs, iObj, i )
659 Acb_NtkFindNodes_rec( p, iObj, vNodes );
660 return vNodes;
661 }
662
663 /**Function*************************************************************
664
665 Synopsis [Derive AIG for one network.]
666
667 Description []
668
669 SideEffects []
670
671 SeeAlso []
672
673 ***********************************************************************/
Acb_ObjToGia(Gia_Man_t * pNew,Acb_Ntk_t * p,int iObj,Vec_Int_t * vTemp)674 int Acb_ObjToGia( Gia_Man_t * pNew, Acb_Ntk_t * p, int iObj, Vec_Int_t * vTemp )
675 {
676 //char * pName = Abc_NamStr( p->pDesign->pStrs, Acb_ObjName(p, iObj) );
677 int * pFanin, iFanin, k, Type, Res;
678 assert( !Acb_ObjIsCio(p, iObj) );
679 Vec_IntClear( vTemp );
680 Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, k )
681 {
682 assert( Acb_ObjCopy(p, iFanin) >= 0 );
683 Vec_IntPush( vTemp, Acb_ObjCopy(p, iFanin) );
684 }
685 Type = Acb_ObjType( p, iObj );
686 if ( Type == ABC_OPER_CONST_F )
687 return 0;
688 if ( Type == ABC_OPER_CONST_T )
689 return 1;
690 if ( Type == ABC_OPER_BIT_BUF )
691 return Vec_IntEntry(vTemp, 0);
692 if ( Type == ABC_OPER_BIT_INV )
693 return Abc_LitNot( Vec_IntEntry(vTemp, 0) );
694 if ( Type == ABC_OPER_BIT_AND || Type == ABC_OPER_BIT_NAND )
695 {
696 Res = 1;
697 Vec_IntForEachEntry( vTemp, iFanin, k )
698 Res = Gia_ManHashAnd( pNew, Res, iFanin );
699 return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NAND );
700 }
701 if ( Type == ABC_OPER_BIT_OR || Type == ABC_OPER_BIT_NOR )
702 {
703 Res = 0;
704 Vec_IntForEachEntry( vTemp, iFanin, k )
705 Res = Gia_ManHashOr( pNew, Res, iFanin );
706 return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NOR );
707 }
708 if ( Type == ABC_OPER_BIT_XOR || Type == ABC_OPER_BIT_NXOR )
709 {
710 Res = 0;
711 Vec_IntForEachEntry( vTemp, iFanin, k )
712 Res = Gia_ManHashXor( pNew, Res, iFanin );
713 return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NXOR );
714 }
715 assert( 0 );
716 return -1;
717 }
Acb_NtkToGia(Acb_Ntk_t * p,Vec_Int_t * vSupp,Vec_Int_t * vNodes,Vec_Int_t * vRoots,Vec_Int_t * vDivs,Vec_Int_t * vTargets)718 Gia_Man_t * Acb_NtkToGia( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Int_t * vNodes, Vec_Int_t * vRoots, Vec_Int_t * vDivs, Vec_Int_t * vTargets )
719 {
720 Gia_Man_t * pNew, * pOne;
721 Vec_Int_t * vFanins;
722 int i, iObj;
723 pNew = Gia_ManStart( 2 * Acb_NtkObjNum(p) + 1000 );
724 pNew->pName = Abc_UtilStrsav(Acb_NtkName(p));
725 Gia_ManHashAlloc( pNew );
726 Acb_NtkCleanObjCopies( p );
727 // create primary inputs
728 Acb_NtkForEachCiVec( vSupp, p, iObj, i )
729 Acb_ObjSetCopy( p, iObj, Gia_ManAppendCi(pNew) );
730 // add targets as primary inputs
731 if ( vTargets )
732 Vec_IntForEachEntry( vTargets, iObj, i )
733 Acb_ObjSetCopy( p, iObj, Gia_ManAppendCi(pNew) );
734 // bit-blast internal nodes
735 vFanins = Vec_IntAlloc( 4 );
736 Vec_IntForEachEntry( vNodes, iObj, i )
737 if ( Acb_ObjCopy(p, iObj) == -1 ) // skip targets assigned above
738 Acb_ObjSetCopy( p, iObj, Acb_ObjToGia(pNew, p, iObj, vFanins) );
739 Vec_IntFree( vFanins );
740 // create primary outputs
741 Acb_NtkForEachCoDriverVec( vRoots, p, iObj, i )
742 Gia_ManAppendCo( pNew, Acb_ObjCopy(p, iObj) );
743 // add divisor as primary outputs (if the divisors are not primary inputs)
744 if ( vDivs && Vec_IntSize(vDivs) > Vec_IntSize(vSupp) )
745 Vec_IntForEachEntry( vDivs, iObj, i )
746 Gia_ManAppendCo( pNew, Acb_ObjCopy(p, iObj) );
747 Gia_ManHashStop( pNew );
748 pNew = Gia_ManCleanup( pOne = pNew );
749 Gia_ManStop( pOne );
750 return pNew;
751 }
752
753 /**Function*************************************************************
754
755 Synopsis [Derive miter of two AIGs.]
756
757 Description []
758
759 SideEffects []
760
761 SeeAlso []
762
763 ***********************************************************************/
Acb_CreateMiter(Gia_Man_t * pF,Gia_Man_t * pG)764 Gia_Man_t * Acb_CreateMiter( Gia_Man_t * pF, Gia_Man_t * pG )
765 {
766 Gia_Man_t * pNew, * pOne;
767 Gia_Obj_t * pObj;
768 int i, iMiter = 0, iXor;
769 Gia_ManFillValue( pF );
770 Gia_ManFillValue( pG );
771 pNew = Gia_ManStart( Gia_ManObjNum(pF) + Gia_ManObjNum(pF) + 1000 );
772 Gia_ManHashAlloc( pNew );
773 Gia_ManConst0(pF)->Value = 0;
774 Gia_ManConst0(pG)->Value = 0;
775 Gia_ManForEachCi( pF, pObj, i )
776 pObj->Value = Gia_ManAppendCi( pNew );
777 Gia_ManForEachCi( pG, pObj, i )
778 pObj->Value = Gia_ManCi(pF, i)->Value;
779 Gia_ManForEachAnd( pF, pObj, i )
780 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
781 Gia_ManForEachAnd( pG, pObj, i )
782 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
783 Gia_ManForEachCo( pG, pObj, i )
784 {
785 iXor = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(pF, i)) );
786 iMiter = Gia_ManHashOr( pNew, iMiter, iXor );
787 }
788 Gia_ManAppendCo( pNew, iMiter );
789 Gia_ManForEachCo( pF, pObj, i )
790 if ( i >= Gia_ManCoNum(pG) )
791 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
792 Gia_ManHashStop( pNew );
793 pNew = Gia_ManCleanup( pOne = pNew );
794 Gia_ManStop( pOne );
795 return pNew;
796 }
797
798 /**Function*************************************************************
799
800 Synopsis []
801
802 Description []
803
804 SideEffects []
805
806 SeeAlso []
807
808 ***********************************************************************/
809 #define NWORDS 64
810
Vec_IntPermute(Vec_Int_t * p)811 void Vec_IntPermute( Vec_Int_t * p )
812 {
813 int i, nSize = Vec_IntSize( p );
814 int * pArray = Vec_IntArray( p );
815 srand( time(NULL) );
816 for ( i = 0; i < nSize; i++ )
817 {
818 int j = rand()%nSize;
819 ABC_SWAP( int, pArray[i], pArray[j] );
820 }
821 }
822
Acb_PrintPatterns(Vec_Wrd_t * vPats,int nPats,Vec_Int_t * vWeights)823 void Acb_PrintPatterns( Vec_Wrd_t * vPats, int nPats, Vec_Int_t * vWeights )
824 {
825 int i, k, Entry, nDivs = Vec_IntSize(vWeights);
826 printf( " : " );
827 Vec_IntForEachEntry( vWeights, Entry, i )
828 printf( "%d", (Entry / 100) % 10 );
829 printf( "\n" );
830 printf( " : " );
831 Vec_IntForEachEntry( vWeights, Entry, i )
832 printf( "%d", (Entry / 10) % 10 );
833 printf( "\n" );
834 printf( " : " );
835 Vec_IntForEachEntry( vWeights, Entry, i )
836 printf( "%d", (Entry / 1) % 10 );
837 printf( "\n" );
838 printf( "\n" );
839
840 printf( " : " );
841 for ( i = 0; i < nDivs; i++ )
842 printf( "%d", (i / 100) % 10 );
843 printf( "\n" );
844 printf( " : " );
845 for ( i = 0; i < nDivs; i++ )
846 printf( "%d", (i / 10) % 10 );
847 printf( "\n" );
848 printf( " : " );
849 for ( i = 0; i < nDivs; i++ )
850 printf( "%d", i % 10 );
851 printf( "\n" );
852 printf( "\n" );
853
854 for ( k = 0; k < nPats; k++ )
855 {
856 printf( "%3d : ", k );
857 for ( i = 0; i < nDivs; i++ )
858 printf( "%c", Abc_TtGetBit(Vec_WrdEntryP(vPats, NWORDS*i), k) ? '*' : '|' );
859 printf( "\n" );
860 }
861 printf( "\n" );
862 }
863
Acb_DeriveWeights(Vec_Int_t * vDivs,Acb_Ntk_t * pNtkF)864 Vec_Int_t * Acb_DeriveWeights( Vec_Int_t * vDivs, Acb_Ntk_t * pNtkF )
865 {
866 int i, iDiv;
867 Vec_Int_t * vWeights = Vec_IntAlloc( Vec_IntSize(vDivs) );
868 Vec_IntForEachEntry( vDivs, iDiv, i )
869 Vec_IntPush( vWeights, Vec_IntEntry(&pNtkF->vObjWeight, iDiv) );
870 return vWeights;
871 }
Acb_ComputeSuppCost(Vec_Int_t * vSupp,Vec_Int_t * vWeights,int iFirstDiv)872 int Acb_ComputeSuppCost( Vec_Int_t * vSupp, Vec_Int_t * vWeights, int iFirstDiv )
873 {
874 int i, Entry, Cost = 0;
875 Vec_IntForEachEntry( vSupp, Entry, i )
876 Cost += Vec_IntEntry( vWeights, Abc_Lit2Var(Entry) - iFirstDiv );
877 return Cost;
878 }
Acb_FindSupportStart(sat_solver * pSat,int iFirstDiv,Vec_Int_t * vWeights,Vec_Wrd_t ** pvPats,int * piPats)879 Vec_Int_t * Acb_FindSupportStart( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeights, Vec_Wrd_t ** pvPats, int * piPats )
880 {
881 int i, status, nDivs = Vec_IntSize(vWeights);
882 Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
883 Vec_Wrd_t * vPats = Vec_WrdStart( NWORDS * nDivs );
884 int iPat = 0;
885 while ( 1 )
886 {
887 int fFound = 0;
888 // try one run
889 status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 );
890 if ( status == l_False )
891 break;
892 assert( status == l_True );
893 // collect pattern
894 for ( i = 0; i < nDivs; i++ )
895 {
896 if ( sat_solver_var_value(pSat, iFirstDiv+i) == 0 )
897 continue;
898 Abc_TtSetBit( Vec_WrdEntryP(vPats, NWORDS*i), iPat );
899 if ( fFound )
900 continue;
901 // process new divisor
902 Vec_IntPush( vSupp, Abc_Var2Lit(iFirstDiv+i, 1) );
903 //printf( "Selecting divisor %d with weight %d\n", i, Vec_IntEntry(vWeights, i) );
904 fFound = 1;
905 }
906 if ( fFound == 0 )
907 {
908 Vec_WrdFree( vPats );
909 Vec_IntFree( vSupp );
910 return NULL;
911 }
912 assert( fFound );
913 iPat++;
914 }
915 *piPats = iPat;
916 *pvPats = vPats;
917 Vec_IntSort( vSupp, 0 );
918 return vSupp;
919 }
Acb_FindArgMaxUnderMask(Vec_Wrd_t * vPats,word Mask[NWORDS],Vec_Int_t * vWeights,int nPats)920 int Acb_FindArgMaxUnderMask( Vec_Wrd_t * vPats, word Mask[NWORDS], Vec_Int_t * vWeights, int nPats )
921 {
922 int nDivs = Vec_WrdSize(vPats)/NWORDS;
923 int nWords = Abc_Bit6WordNum(nPats);
924 int i, iBest = -1;
925 int Cost, CostBest = -1;
926 for ( i = 0; i < nDivs; i++ )
927 {
928 word * pPat = Vec_WrdEntryP(vPats, NWORDS*i);
929 Cost = Abc_TtCountOnesVecMask(Mask, pPat, nWords, 0);
930 if ( CostBest < Cost )
931 // if ( CostBest == -1 || (float)CostBest/Cost < 0.6*(float)Vec_IntEntry(vWeights, iBest)/Vec_IntEntry(vWeights, i) )
932 // if ( CostBest == -1 || (float)CostBest/Cost < 0.67*(float)Vec_IntEntry(vWeights, iBest)/Vec_IntEntry(vWeights, i) )
933 {
934 CostBest = Cost;
935 iBest = i;
936 }
937 }
938 return iBest;
939 }
Acb_FindArgMaxUnderMask2(Vec_Wrd_t * vPats,word Mask[NWORDS],Vec_Int_t * vWeights,int nPats)940 int Acb_FindArgMaxUnderMask2( Vec_Wrd_t * vPats, word Mask[NWORDS], Vec_Int_t * vWeights, int nPats )
941 {
942 int nDivs = Vec_WrdSize(vPats)/NWORDS;
943 int i, b, iBest = -1;
944 int Cost, CostBest = -1;
945 // count how many times each of them appears
946 Vec_Int_t * vCounts = Vec_IntStart(nPats);
947 for ( i = 0; i < nDivs; i++ )
948 {
949 word * pPat = Vec_WrdEntryP(vPats, NWORDS*i);
950 for ( b = 0; b < nPats; b++ )
951 if ( Abc_TtGetBit(pPat, b) )
952 Vec_IntAddToEntry( vCounts, b, 1 );
953 }
954 for ( i = 0; i < nDivs; i++ )
955 {
956 word * pPat = Vec_WrdEntryP(vPats, NWORDS*i);
957 // Cost = Abc_TtCountOnesVecMask(Mask, pPat, NWORDS, 0);
958 Cost = 0;
959 for ( b = 0; b < nPats; b++ )
960 if ( Abc_TtGetBit(pPat, b) && Abc_TtGetBit(Mask, b) )
961 Cost += 1000000/Vec_IntEntry(vCounts, b);
962 if ( CostBest < Cost )
963 {
964 CostBest = Cost;
965 iBest = i;
966 }
967 }
968 Vec_IntFree( vCounts );
969 return iBest;
970 }
971
Acb_FindSupportNext(sat_solver * pSat,int iFirstDiv,Vec_Int_t * vWeights,Vec_Wrd_t * vPats,int * pnPats)972 Vec_Int_t * Acb_FindSupportNext( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeights, Vec_Wrd_t * vPats, int * pnPats )
973 {
974 int i, status, nDivs = Vec_IntSize(vWeights);
975 Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
976 word * pMask, Mask[NWORDS]; Abc_TtConst( Mask, NWORDS, 1 );
977 while ( 1 )
978 {
979 int iDivBest = Acb_FindArgMaxUnderMask( vPats, Mask, vWeights, *pnPats );
980 Vec_IntPush( vSupp, Abc_Var2Lit(iFirstDiv+iDivBest, 1) );
981 //printf( "Selecting divisor %d with weight %d\n", iDivBest, Vec_IntEntry(vWeights, iDivBest) );
982 // Mask &= ~Vec_WrdEntry( vPats, iDivBest );
983 pMask = Vec_WrdEntryP( vPats, NWORDS*iDivBest );
984 Abc_TtAndSharp( Mask, Mask, pMask, NWORDS, 1 );
985
986 // try one run
987 status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 );
988 if ( status == l_False )
989 break;
990 assert( status == l_True );
991 // collect pattern
992 for ( i = 0; i < nDivs; i++ )
993 {
994 if ( sat_solver_var_value(pSat, iFirstDiv+i) == 0 )
995 continue;
996 Abc_TtSetBit( Vec_WrdEntryP(vPats, NWORDS*i), *pnPats );
997 }
998 (*pnPats)++;
999 if ( *pnPats == NWORDS*64 )
1000 {
1001 Vec_IntFreeP( &vSupp );
1002 return NULL;
1003 }
1004 assert( *pnPats < NWORDS*64 );
1005 //Acb_PrintPatterns( vPats, *pnPats, vWeights );
1006 //i = i;
1007 }
1008 Vec_IntSort( vSupp, 0 );
1009 return vSupp;
1010 }
Acb_FindSupportMinOne(sat_solver * pSat,int iFirstDiv,Vec_Wrd_t * vPats,int * pnPats,Vec_Int_t * vSupp,int iVar)1011 Vec_Int_t * Acb_FindSupportMinOne( sat_solver * pSat, int iFirstDiv, Vec_Wrd_t * vPats, int * pnPats, Vec_Int_t * vSupp, int iVar )
1012 {
1013 int i, iLit, status;
1014 int nDivs = Vec_WrdSize(vPats)/NWORDS;
1015 Vec_Int_t * vLits = Vec_IntAlloc( Vec_IntSize(vSupp) );
1016 Vec_IntForEachEntry( vSupp, iLit, i )
1017 if ( i != iVar )
1018 Vec_IntPush( vLits, iLit );
1019 // try one run
1020 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), 0, 0, 0, 0 );
1021 if ( status == l_False )
1022 return vLits;
1023 Vec_IntFree( vLits );
1024 assert( status == l_True );
1025 // collect pattern
1026 for ( i = 0; i < nDivs; i++ )
1027 {
1028 if ( sat_solver_var_value(pSat, iFirstDiv+i) == 0 )
1029 continue;
1030 Abc_TtSetBit( Vec_WrdEntryP(vPats, NWORDS*i), *pnPats );
1031 }
1032 (*pnPats)++;
1033 if ( *pnPats == NWORDS*64 )
1034 return NULL;
1035 return vSupp;
1036 }
Acb_FindSupportMin(sat_solver * pSat,int iFirstDiv,Vec_Wrd_t * vPats,int * pnPats,Vec_Int_t * vSuppStart)1037 Vec_Int_t * Acb_FindSupportMin( sat_solver * pSat, int iFirstDiv, Vec_Wrd_t * vPats, int * pnPats, Vec_Int_t * vSuppStart )
1038 {
1039 Vec_Int_t * vTemp, * vSupp = Vec_IntDup( vSuppStart ); int i;
1040 for ( i = Vec_IntSize(vSupp)-1; i >= 0; i-- )
1041 {
1042 vSupp = Acb_FindSupportMinOne( pSat, iFirstDiv, vPats, pnPats, vTemp = vSupp, i );
1043 if ( vTemp != vSupp )
1044 Vec_IntFree( vTemp );
1045 if ( vSupp == NULL )
1046 return NULL;
1047 }
1048 return vSupp;
1049 }
Acb_FindReplace(sat_solver * pSat,int iFirstDiv,Vec_Int_t * vWeights,Vec_Wrd_t * vPats,int nPats,Vec_Int_t * vSupp)1050 void Acb_FindReplace( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeights, Vec_Wrd_t * vPats, int nPats, Vec_Int_t * vSupp )
1051 {
1052 int i, k, iLit, iLit2, status, nWords = Abc_Bit6WordNum(nPats);
1053 word Covered[NWORDS], Both[NWORDS], Mask[NWORDS], * pMask;
1054 assert( nWords <= NWORDS );
1055 // prepare constant pattern
1056 Abc_TtConst( Mask, nWords, 0 );
1057 for ( i = 0; i < nPats; i++ )
1058 Abc_TtSetBit( Mask, i );
1059 // try to replace each by a cheaper one
1060 Vec_IntForEachEntry( vSupp, iLit, i )
1061 {
1062 int iDiv = Abc_Lit2Var(iLit) - iFirstDiv;
1063 // collect covered except by this one
1064 Abc_TtConst( Covered, nWords, 0 );
1065 Vec_IntForEachEntry( vSupp, iLit2, k )
1066 {
1067 if ( iLit2 == iLit )
1068 continue;
1069 pMask = Vec_WrdEntryP( vPats, NWORDS*(Abc_Lit2Var(iLit2) - iFirstDiv) );
1070 Abc_TtOr( Covered, Covered, pMask, nWords );
1071 }
1072 // consider any cheaper ones that this one
1073 for ( k = 0; k < iDiv; k++ )
1074 {
1075 if ( Vec_IntEntry(vWeights, k) == Vec_IntEntry(vWeights, iDiv) )
1076 continue;
1077 assert( Vec_IntEntry(vWeights, k) < Vec_IntEntry(vWeights, iDiv) );
1078 pMask = Vec_WrdEntryP( vPats, NWORDS*k );
1079 // check if it covers the remaining ones
1080 Abc_TtOr( Both, Covered, pMask, nWords );
1081 if ( !Abc_TtEqual(Both, Mask, nWords) )
1082 continue;
1083 // try this one
1084 Vec_IntWriteEntry( vSupp, i, Abc_Var2Lit(iFirstDiv+k, 1) );
1085 status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 );
1086 if ( status == l_False ) // success
1087 {
1088 //printf( "Replacing %d(%d) by %d(%d) with const difference %d.\n",
1089 // iDiv, Vec_IntEntry(vWeights, iDiv), k, Vec_IntEntry(vWeights, k),
1090 // Vec_IntEntry(vWeights, iDiv) - Vec_IntEntry(vWeights, k) );
1091 break;
1092 }
1093 Vec_IntWriteEntry( vSupp, i, iLit );
1094 }
1095 }
1096 }
1097
Acb_FindSupport(sat_solver * pSat,int iFirstDiv,Vec_Int_t * vWeights,Vec_Int_t * vSuppStart,int TimeOut)1098 Vec_Int_t * Acb_FindSupport( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeights, Vec_Int_t * vSuppStart, int TimeOut )
1099 {
1100 abctime clkLimit = TimeOut * CLOCKS_PER_SEC + Abc_Clock();
1101 Vec_Wrd_t * vPats = NULL;
1102 int nPats = 0;
1103 Vec_Int_t * vSuppBest, * vSupp;//, * vTemp;
1104 int CostBest, Cost;
1105 int Iter;
1106
1107 // find initial best
1108 CostBest = Acb_ComputeSuppCost( vSuppStart, vWeights, iFirstDiv );
1109 vSuppBest = Vec_IntDup( vSuppStart );
1110 printf( "Starting cost = %d.\n", CostBest );
1111
1112 // iteratively find the one with the most ones in the uncovered rows
1113 for ( Iter = 0; Iter < 200; Iter++ )
1114 {
1115 if ( Abc_Clock() > clkLimit )
1116 {
1117 Vec_IntFree( vSuppBest );
1118 Vec_WrdFree( vPats );
1119 return NULL;
1120 }
1121 if ( Iter == 0 )
1122 vSupp = Acb_FindSupportStart( pSat, iFirstDiv, vWeights, &vPats, &nPats );
1123 else
1124 vSupp = Acb_FindSupportNext( pSat, iFirstDiv, vWeights, vPats, &nPats );
1125 if ( vSupp == NULL )
1126 {
1127 Vec_IntFree( vSuppBest );
1128 return NULL;
1129 }
1130 //vSupp = Acb_FindSupportMin( pSat, iFirstDiv, vPats, &nPats, vTemp = vSupp );
1131 //Vec_IntFree( vTemp );
1132 if ( vSupp == NULL )
1133 break;
1134 Cost = Acb_ComputeSuppCost( vSupp, vWeights, iFirstDiv );
1135 //Acb_PrintPatterns( vPats, nPats, vWeights );
1136 if ( CostBest > Cost )
1137 {
1138 CostBest = Cost;
1139 ABC_SWAP( Vec_Int_t *, vSuppBest, vSupp );
1140 printf( "Iter %4d: Next cost = %d. ", Iter, Cost );
1141 printf( "Updating best solution.\n" );
1142 }
1143 Vec_IntFree( vSupp );
1144 }
1145 Acb_FindReplace( pSat, iFirstDiv, vWeights, vPats, nPats, vSuppBest );
1146
1147 //printf( "Number of patterns = %d.\n", nPats );
1148 Vec_WrdFree( vPats );
1149 return vSuppBest;
1150 }
1151
1152 /**Function*************************************************************
1153
1154 Synopsis [Compute the best support of the targets.]
1155
1156 Description []
1157
1158 SideEffects []
1159
1160 SeeAlso []
1161
1162 ***********************************************************************/
Acb_DerivePatchSupport(Cnf_Dat_t * pCnf,int iTar,int nTargets,int nCoDivs,Vec_Int_t * vDivs,Acb_Ntk_t * pNtkF,Vec_Int_t * vSuppOld,int TimeOut)1163 Vec_Int_t * Acb_DerivePatchSupport( Cnf_Dat_t * pCnf, int iTar, int nTargets, int nCoDivs, Vec_Int_t * vDivs, Acb_Ntk_t * pNtkF, Vec_Int_t * vSuppOld, int TimeOut )
1164 {
1165 Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
1166 int i, Lit;
1167 int iCoVarBeg = 1;
1168 int iCiVarBeg = pCnf->nVars - nTargets;
1169 sat_solver * pSat = sat_solver_new();
1170 sat_solver_setnvars( pSat, 2 * pCnf->nVars + nCoDivs );
1171 // add clauses
1172 for ( i = 0; i < pCnf->nClauses; i++ )
1173 if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
1174 return NULL;
1175 // add output clause
1176 Lit = Abc_Var2Lit( iCoVarBeg, 0 );
1177 if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
1178 return NULL;
1179 // add clauses
1180 pCnf->pMan = NULL;
1181 Cnf_DataLift( pCnf, pCnf->nVars );
1182 for ( i = 0; i < pCnf->nClauses; i++ )
1183 if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
1184 return NULL;
1185 Cnf_DataLift( pCnf, -pCnf->nVars );
1186 // add output clause
1187 Lit = Abc_Var2Lit( iCoVarBeg+pCnf->nVars, 0 );
1188 if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
1189 return NULL;
1190 // create XORs for targets
1191 // add negative literal
1192 Lit = Abc_Var2Lit( iCiVarBeg + iTar, 1 );
1193 if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
1194 return NULL;
1195 // add positive literal
1196 Lit = Abc_Var2Lit( iCiVarBeg+pCnf->nVars + iTar, 0 );
1197 if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
1198 return NULL;
1199 // create XORs for divisors
1200 if ( nCoDivs > 0 )
1201 {
1202 abctime clk = Abc_Clock();
1203 int fUseMinAssump = 1;
1204 int iLit, nSuppNew, status;
1205 int iDivVar = 2 * pCnf->nVars;
1206 int pLits[2];
1207 int j = 0, iDivOld;
1208 Vec_IntClear( vSupp );
1209 if ( vSuppOld )
1210 {
1211 // start with predefined support
1212 Vec_IntForEachEntry( vSuppOld, iDivOld, j )
1213 {
1214 int iVar0 = iCoVarBeg+1+iDivOld;
1215 int iVar1 = iCoVarBeg+1+iDivOld+pCnf->nVars;
1216 //printf( "Selecting predefined divisor %d with weight %d\n",
1217 // iDivOld, Vec_IntEntry(&pNtkF->vObjWeight, Vec_IntEntry(vDivs, iDivOld)) );
1218 // add equality clauses
1219 pLits[0] = Abc_Var2Lit( iVar0, 0 );
1220 pLits[1] = Abc_Var2Lit( iVar1, 1 );
1221 if ( !sat_solver_addclause( pSat, pLits, pLits+2 ) )
1222 {
1223 printf( "Unsat is detected earlier.\n" );
1224 status = l_False;
1225 break;
1226 }
1227 pLits[0] = Abc_Var2Lit( iVar0, 1 );
1228 pLits[1] = Abc_Var2Lit( iVar1, 0 );
1229 if ( !sat_solver_addclause( pSat, pLits, pLits+2 ) )
1230 {
1231 printf( "Unsat is detected earlier.\n" );
1232 status = l_False;
1233 break;
1234 }
1235 }
1236 }
1237 if ( vSuppOld == NULL || j == Vec_IntSize(vSuppOld) )
1238 {
1239 for ( i = 0; i < nCoDivs; i++ )
1240 {
1241 sat_solver_add_xor( pSat, iDivVar+i, iCoVarBeg+1+i, iCoVarBeg+1+i+pCnf->nVars, 0 );
1242 Vec_IntPush( vSupp, Abc_Var2Lit(iDivVar+i, 1) );
1243 }
1244 // try one run
1245 if ( TimeOut ) sat_solver_set_runtime_limit( pSat, TimeOut * CLOCKS_PER_SEC + Abc_Clock() );
1246 status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 );
1247 if ( TimeOut ) sat_solver_set_runtime_limit( pSat, 0 );
1248 if ( status == l_True )
1249 {
1250 printf( "ECO does not exist.\n" );
1251 sat_solver_delete( pSat );
1252 Vec_IntFree( vSupp );
1253 return NULL;
1254 }
1255 if ( status == l_Undef )
1256 {
1257 printf( "Support computation timed out after %d sec.\n", TimeOut );
1258 sat_solver_delete( pSat );
1259 Vec_IntFree( vSupp );
1260 return NULL;
1261 }
1262 assert( status == l_False );
1263 printf( "Proved that the problem has a solution. " );
1264 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1265 // find minimum subset
1266 if ( fUseMinAssump )
1267 {
1268 int fUseSuppMin = 1;
1269 // solve in a standard way
1270 abctime clk = Abc_Clock();
1271 nSuppNew = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 );
1272 Vec_IntShrink( vSupp, nSuppNew );
1273 Vec_IntSort( vSupp, 0 );
1274 printf( "Found one feasible set of %d divisors. ", Vec_IntSize(vSupp) );
1275 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1276
1277 // perform minimization
1278 if ( fUseSuppMin && Vec_IntSize(vSupp) > 0 )
1279 {
1280 abctime clk = Abc_Clock();
1281 Vec_Int_t * vSupp2 = Vec_IntDup( vSupp );
1282 Vec_Int_t * vTemp, * vWeights = Acb_DeriveWeights( vDivs, pNtkF );
1283 vSupp = Acb_FindSupport( pSat, iDivVar, vWeights, vTemp = vSupp, TimeOut );
1284 Vec_IntFree( vWeights );
1285 Vec_IntFree( vTemp );
1286 if ( vSupp == NULL )
1287 {
1288 printf( "Support minimization did not succeed. " );
1289 //sat_solver_delete( pSat );
1290 vSupp = vSupp2;
1291 }
1292 else
1293 {
1294 Vec_IntFree( vSupp2 );
1295 printf( "Minimized support to %d supp vars. ", Vec_IntSize(vSupp) );
1296 }
1297 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1298 }
1299 }
1300 else
1301 {
1302 int * pFinal, nFinal = sat_solver_final( pSat, &pFinal );
1303 printf( "AnalyzeFinal returned %d (out of %d).\n", nFinal, Vec_IntSize(vSupp) );
1304 Vec_IntClear( vSupp );
1305 for ( i = 0; i < nFinal; i++ )
1306 Vec_IntPush( vSupp, Abc_LitNot(pFinal[i]) );
1307 // try one run
1308 status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 );
1309 assert( status == l_False );
1310 // try again
1311 nFinal = sat_solver_final( pSat, &pFinal );
1312 printf( "AnalyzeFinal returned %d (out of %d).\n", nFinal, Vec_IntSize(vSupp) );
1313 }
1314 // remap them into numbers
1315 Vec_IntForEachEntry( vSupp, iLit, i )
1316 Vec_IntWriteEntry( vSupp, i, Abc_Lit2Var(iLit)-iDivVar );
1317 Vec_IntSort( vSupp, 0 );
1318 }
1319 }
1320 sat_solver_delete( pSat );
1321 if ( vSupp ) Vec_IntSort( vSupp, 0 );
1322 return vSupp;
1323 }
1324
satoko_add_xor(satoko_t * pSat,int iVarA,int iVarB,int iVarC,int fCompl)1325 static inline int satoko_add_xor( satoko_t * pSat, int iVarA, int iVarB, int iVarC, int fCompl )
1326 {
1327 int Lits[3];
1328 int Cid;
1329 assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
1330
1331 Lits[0] = toLitCond( iVarA, !fCompl );
1332 Lits[1] = toLitCond( iVarB, 1 );
1333 Lits[2] = toLitCond( iVarC, 1 );
1334 Cid = satoko_add_clause( pSat, Lits, 3 );
1335 assert( Cid );
1336
1337 Lits[0] = toLitCond( iVarA, !fCompl );
1338 Lits[1] = toLitCond( iVarB, 0 );
1339 Lits[2] = toLitCond( iVarC, 0 );
1340 Cid = satoko_add_clause( pSat, Lits, 3 );
1341 assert( Cid );
1342
1343 Lits[0] = toLitCond( iVarA, fCompl );
1344 Lits[1] = toLitCond( iVarB, 1 );
1345 Lits[2] = toLitCond( iVarC, 0 );
1346 Cid = satoko_add_clause( pSat, Lits, 3 );
1347 assert( Cid );
1348
1349 Lits[0] = toLitCond( iVarA, fCompl );
1350 Lits[1] = toLitCond( iVarB, 0 );
1351 Lits[2] = toLitCond( iVarC, 1 );
1352 Cid = satoko_add_clause( pSat, Lits, 3 );
1353 assert( Cid );
1354 return 4;
1355 }
Acb_DerivePatchSupportS(Cnf_Dat_t * pCnf,int nCiTars,int nCoDivs,Vec_Int_t * vDivs,Acb_Ntk_t * pNtkF,Vec_Int_t * vSuppOld,int TimeOut)1356 Vec_Int_t * Acb_DerivePatchSupportS( Cnf_Dat_t * pCnf, int nCiTars, int nCoDivs, Vec_Int_t * vDivs, Acb_Ntk_t * pNtkF, Vec_Int_t * vSuppOld, int TimeOut )
1357 {
1358 Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
1359 int i, Lit;
1360 int iCoVarBeg = 1;
1361 int iCiVarBeg = pCnf->nVars - nCiTars;
1362 satoko_t * pSat = satoko_create();
1363 satoko_setnvars( pSat, 2 * pCnf->nVars + nCiTars + nCoDivs );
1364 satoko_options(pSat)->no_simplify = 1;
1365 // add clauses
1366 for ( i = 0; i < pCnf->nClauses; i++ )
1367 if ( !satoko_add_clause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
1368 return NULL;
1369 // add output clause
1370 Lit = Abc_Var2Lit( iCoVarBeg, 0 );
1371 if ( !satoko_add_clause( pSat, &Lit, 1 ) )
1372 return NULL;
1373 // add clauses
1374 pCnf->pMan = NULL;
1375 Cnf_DataLift( pCnf, pCnf->nVars );
1376 for ( i = 0; i < pCnf->nClauses; i++ )
1377 if ( !satoko_add_clause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
1378 return NULL;
1379 Cnf_DataLift( pCnf, -pCnf->nVars );
1380 // add output clause
1381 Lit = Abc_Var2Lit( iCoVarBeg+pCnf->nVars, 0 );
1382 if ( !satoko_add_clause( pSat, &Lit, 1 ) )
1383 return NULL;
1384 // create XORs for targets
1385 if ( nCiTars > 0 )
1386 {
1387 /*
1388 int iXorVar = 2 * pCnf->nVars;
1389 int Lit;
1390 Vec_IntClear( vSupp );
1391 for ( i = 0; i < nCiTars; i++ )
1392 {
1393 satoko_add_xor( pSat, iXorVar+i, iCiVarBeg+i, iCiVarBeg+i+pCnf->nVars, 0 );
1394 Vec_IntPush( vSupp, Abc_Var2Lit(iXorVar+i, 0) );
1395 }
1396 if ( !satoko_add_clause( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp) ) )
1397 return NULL;
1398 */
1399 // add negative literal
1400 Lit = Abc_Var2Lit( iCiVarBeg, 1 );
1401 if ( !satoko_add_clause( pSat, &Lit, 1 ) )
1402 return NULL;
1403 // add positive literal
1404 Lit = Abc_Var2Lit( iCiVarBeg+pCnf->nVars, 0 );
1405 if ( !satoko_add_clause( pSat, &Lit, 1 ) )
1406 return NULL;
1407 }
1408 // create XORs for divisors
1409 if ( nCoDivs > 0 )
1410 {
1411 abctime clk = Abc_Clock();
1412 int fUseMinAssump = 1;
1413 int iLit, status, nSuppNew;
1414 int iDivVar = 2 * pCnf->nVars + nCiTars;
1415 Vec_IntClear( vSupp );
1416 for ( i = 0; i < nCoDivs; i++ )
1417 {
1418 satoko_add_xor( pSat, iDivVar+i, iCoVarBeg+1+i, iCoVarBeg+1+i+pCnf->nVars, 0 );
1419 Vec_IntPush( vSupp, Abc_Var2Lit(iDivVar+i, 1) );
1420 /*
1421 pLits[0] = Abc_Var2Lit(iCoVarBeg+1+i, 1);
1422 pLits[1] = Abc_Var2Lit(iCoVarBeg+1+i+pCnf->nVars, 0);
1423 pLits[2] = Abc_Var2Lit(iDivVar+i, 1);
1424 if ( !satoko_add_clause( pSat, pLits, 3 ) )
1425 assert( 0 );
1426
1427 pLits[0] = Abc_Var2Lit(iCoVarBeg+1+i, 0);
1428 pLits[1] = Abc_Var2Lit(iCoVarBeg+1+i+pCnf->nVars, 1);
1429 pLits[2] = Abc_Var2Lit(iDivVar+i, 1);
1430 if ( !satoko_add_clause( pSat, pLits, 3 ) )
1431 assert( 0 );
1432
1433 Vec_IntPush( vSupp, Abc_Var2Lit(iDivVar+i, 0) );
1434 */
1435 }
1436
1437 // try one run
1438 status = satoko_solve_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp) );
1439 if ( status != l_False )
1440 {
1441 printf( "Demonstrated that the problem has NO solution. " );
1442 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1443 satoko_destroy( pSat );
1444 Vec_IntFree( vSupp );
1445 return NULL;
1446 }
1447 assert( status == l_False );
1448 printf( "Proved that the problem has a solution. " );
1449 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1450
1451 // find minimum subset
1452 if ( fUseMinAssump )
1453 {
1454 abctime clk = Abc_Clock();
1455 nSuppNew = satoko_minimize_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 );
1456 Vec_IntShrink( vSupp, nSuppNew );
1457 printf( "Solved the problem with %d supp vars. ", Vec_IntSize(vSupp) );
1458 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1459 }
1460 else
1461 {
1462 int * pFinal, nFinal = satoko_final_conflict( pSat, &pFinal );
1463 printf( "AnalyzeFinal returned %d (out of %d).\n", nFinal, Vec_IntSize(vSupp) );
1464 Vec_IntClear( vSupp );
1465 for ( i = 0; i < nFinal; i++ )
1466 Vec_IntPush( vSupp, Abc_LitNot(pFinal[i]) );
1467 // try one run
1468 status = satoko_solve_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp) );
1469 assert( status == l_False );
1470 // try again
1471 nFinal = satoko_final_conflict( pSat, &pFinal );
1472 printf( "AnalyzeFinal returned %d (out of %d).\n", nFinal, Vec_IntSize(vSupp) );
1473 }
1474
1475 // remap them into numbers
1476 Vec_IntForEachEntry( vSupp, iLit, i )
1477 Vec_IntWriteEntry( vSupp, i, Abc_Lit2Var(iLit)-iDivVar );
1478 Vec_IntSort( vSupp, 0 );
1479 //Vec_IntPrint( vSupp );
1480 }
1481 satoko_destroy( pSat );
1482 Vec_IntSort( vSupp, 0 );
1483 return vSupp;
1484 }
1485
1486
1487 /**Function*************************************************************
1488
1489 Synopsis [Compute functions of the targets.]
1490
1491 Description []
1492
1493 SideEffects []
1494
1495 SeeAlso []
1496
1497 ***********************************************************************/
Acb_EnumerateSatAssigns(sat_solver * pSat,int PivotVar,int FreeVar,Vec_Int_t * vDivVars,Vec_Int_t * vTempLits,Vec_Str_t * vTempSop)1498 char * Acb_EnumerateSatAssigns( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vTempLits, Vec_Str_t * vTempSop )
1499 {
1500 int fCreatePrime = 1;
1501 int status, i, iMint, iVar, iLit, nFinal, * pFinal, pLits[2];
1502 Vec_Int_t * vTemp, * vLits;
1503 assert( FreeVar < sat_solver_nvars(pSat) );
1504 pLits[0] = Abc_Var2Lit( PivotVar, 1 ); // F = 1
1505 pLits[1] = Abc_Var2Lit( FreeVar, 0 ); // iNewLit
1506 Vec_StrClear( vTempSop );
1507 Vec_StrGrow( vTempSop, 8 * (Vec_IntSize(vDivVars) + 3) + 1 );
1508 // check constant 0
1509 status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 );
1510 if ( status == l_False )
1511 {
1512 Vec_StrPush( vTempSop, ' ' );
1513 Vec_StrPush( vTempSop, '0' );
1514 Vec_StrPush( vTempSop, '\n' );
1515 Vec_StrPush( vTempSop, '\0' );
1516 return Vec_StrReleaseArray(vTempSop);
1517 }
1518 // check constant 1
1519 pLits[0] = Abc_LitNot(pLits[0]);
1520 status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 );
1521 pLits[0] = Abc_LitNot(pLits[0]);
1522 if ( status == l_False || Vec_IntSize(vDivVars) == 0 )
1523 {
1524 Vec_StrPush( vTempSop, ' ' );
1525 Vec_StrPush( vTempSop, '1' );
1526 Vec_StrPush( vTempSop, '\n' );
1527 Vec_StrPush( vTempSop, '\0' );
1528 return Vec_StrReleaseArray(vTempSop);
1529 }
1530 //Vec_IntPrint( vDivVars );
1531 vTemp = Vec_IntAlloc( 100 );
1532 vLits = Vec_IntAlloc( 100 );
1533 for ( iMint = 0; ; iMint++ )
1534 {
1535 if ( iMint == 1000 )
1536 {
1537 //if ( Vec_IntSize(vDivVars) == 0 )
1538 {
1539 printf( "Assuming constant 0 function.\n" );
1540 Vec_StrClear( vTempSop );
1541 Vec_StrPush( vTempSop, ' ' );
1542 Vec_StrPush( vTempSop, '0' );
1543 Vec_StrPush( vTempSop, '\n' );
1544 Vec_StrPush( vTempSop, '\0' );
1545 return Vec_StrReleaseArray(vTempSop);
1546 }
1547
1548 printf( "Reached the limit on the number of cubes (1000).\n" );
1549 Vec_IntFree( vTemp );
1550 Vec_IntFree( vLits );
1551 return NULL;
1552 }
1553 //int Offset = Vec_StrSize(vTempSop);
1554 // find onset minterm
1555 status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 );
1556 if ( status == l_False )
1557 {
1558 printf( "Finished enumerating %d cubes.\n", iMint );
1559 Vec_IntFree( vTemp );
1560 Vec_IntFree( vLits );
1561 Vec_StrPush( vTempSop, '\0' );
1562 return Vec_StrReleaseArray(vTempSop);
1563 }
1564 assert( status == l_True );
1565 // collect divisor literals
1566 Vec_IntClear( vTempLits );
1567 Vec_IntPush( vTempLits, Abc_LitNot(pLits[0]) ); // F = 0
1568 //printf( "%8d %3d ", 0, 0 );
1569 // Vec_IntForEachEntry( vDivVars, iVar, i )
1570 Vec_IntForEachEntryReverse( vDivVars, iVar, i )
1571 {
1572 Vec_IntPush( vTempLits, sat_solver_var_literal(pSat, iVar) );
1573 //printf( "%c", '0' + sat_solver_var_value(pSat, iVar) );
1574 }
1575 //printf( "\n" );
1576 // create new cube
1577 for ( i = 0; i < Vec_IntSize(vDivVars); i++ )
1578 Vec_StrPush( vTempSop, '-' );
1579 if ( fCreatePrime )
1580 {
1581 // expand against offset
1582 status = sat_solver_push(pSat, Vec_IntEntry(vTempLits, 0));
1583 assert( status == 1 );
1584 nFinal = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vTempLits)+1, Vec_IntSize(vTempLits)-1, 0 );
1585 Vec_IntShrink( vTempLits, nFinal+1 );
1586 sat_solver_pop(pSat);
1587 // compute cube and add clause
1588 Vec_IntWriteEntry( vTempLits, 0, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
1589 Vec_IntForEachEntryStart( vTempLits, iLit, i, 1 )
1590 {
1591 Vec_IntWriteEntry( vTempLits, i, Abc_LitNot(iLit) );
1592 iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(iLit) ); assert( iVar >= 0 );
1593 //uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
1594 Vec_StrWriteEntry( vTempSop, Vec_StrSize(vTempSop) - Vec_IntSize(vDivVars) + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) );
1595 }
1596 }
1597 else
1598 {
1599 // expand against offset
1600 status = sat_solver_solve( pSat, Vec_IntArray(vTempLits), Vec_IntLimit(vTempLits), 0, 0, 0, 0 );
1601 if ( status != l_False )
1602 printf( "Selected onset minterm number %d belongs to the offset (this is a bug).\n", iMint );
1603 assert( status == l_False );
1604
1605 // compute cube and add clause
1606 nFinal = sat_solver_final( pSat, &pFinal );
1607 Vec_IntSelectSort( pFinal, nFinal );
1608 /*
1609 // pretend that this is final
1610 veci_resize(&pSat->conf_final,0);
1611 Vec_IntForEachEntry( vTempLits, iLit, i )
1612 veci_push(&pSat->conf_final, lit_neg(iLit));
1613 pFinal = pSat->conf_final.ptr;
1614 nFinal = Vec_IntSize(vTempLits);
1615 */
1616 ////////////////////////////////////////////////////////
1617 // create new cube
1618 Vec_IntClear( vTemp );
1619 Vec_IntPush( vTemp, Abc_LitNot(pLits[0]) ); // F = 0
1620 for ( i = 0; i < nFinal; i++ )
1621 {
1622 if ( pFinal[i] == pLits[0] )
1623 continue;
1624 Vec_IntPush( vTemp, Abc_LitNot(pFinal[i]) );
1625 }
1626
1627 //Vec_IntPrint( vTemp );
1628 // try removing each one starting with the last one
1629 //printf( "Started with %d lits ", nFinal-1 );
1630 for ( i = nFinal - 1; i > 0; i-- )
1631 {
1632 int iLit = Vec_IntEntry( vTemp, i );
1633 Vec_IntDrop( vTemp, i );
1634 // try SAT
1635 status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), 0, 0, 0, 0 );
1636 if ( status == l_False )
1637 {
1638 // printf( "U" );
1639 continue;
1640 }
1641 //if ( status == l_True )
1642 // printf( "S" );
1643 //else if ( status == l_Undef )
1644 // printf( "T" );
1645 Vec_IntInsert( vTemp, i, iLit );
1646 }
1647 //printf( " Ended up with %d lits\n", Vec_IntSize(vTemp)-1 );
1648 //Vec_IntPrint( vTemp );
1649
1650 Vec_IntForEachEntry( vTemp, iLit, i )
1651 pFinal[i] = Abc_LitNot(iLit);
1652 nFinal = Vec_IntSize(vTemp);
1653 ////////////////////////////////////////////////////////
1654
1655
1656 Vec_IntClear( vTempLits );
1657 Vec_IntPush( vTempLits, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
1658 for ( i = 0; i < nFinal; i++ )
1659 {
1660 if ( pFinal[i] == pLits[0] )
1661 continue;
1662 Vec_IntPush( vTempLits, pFinal[i] );
1663 iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
1664 //uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
1665 Vec_StrWriteEntry( vTempSop, Vec_StrSize(vTempSop) - Vec_IntSize(vDivVars) + iVar, (char)('0' + Abc_LitIsCompl(pFinal[i])) );
1666 }
1667 }
1668 //printf( "%6d : %8d %3d ", iMint, (int)pSat->stats.conflicts, Vec_IntSize(vTempLits)-1 );
1669
1670 Vec_StrAppend( vTempSop, " 1\n" );
1671 status = sat_solver_addclause( pSat, Vec_IntArray(vTempLits), Vec_IntLimit(vTempLits) );
1672 assert( status );
1673
1674 //Vec_StrPush( vTempSop, '\0' );
1675 //printf( "%s", Vec_StrEntryP(vTempSop, Offset) );
1676 //Vec_StrPop( vTempSop );
1677 }
1678 assert( 0 );
1679 return NULL;
1680 }
Acb_DeriveOnePatchFunction(Cnf_Dat_t * pCnf,int iTar,int nTargets,int nCoDivs,Vec_Int_t * vUsed,int fCisOnly)1681 char * Acb_DeriveOnePatchFunction( Cnf_Dat_t * pCnf, int iTar, int nTargets, int nCoDivs, Vec_Int_t * vUsed, int fCisOnly )
1682 {
1683 char * pSop = NULL;
1684 Vec_Int_t * vTempLits = Vec_IntAlloc( Vec_IntSize(vUsed)+1 );
1685 Vec_Str_t * vTempSop = Vec_StrAlloc(0);
1686 int i, Lit;
1687 int iCiVarBeg = pCnf->nVars - nTargets - Vec_IntSize(vUsed);
1688 int iCoVarBeg = 1, Index;
1689 sat_solver * pSat = sat_solver_new();
1690 sat_solver_setnvars( pSat, pCnf->nVars + 1 );
1691 // add clauses
1692 for ( i = 0; i < pCnf->nClauses; i++ )
1693 if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
1694 return NULL;
1695 // add output clause
1696 Lit = Abc_Var2Lit( iCoVarBeg, 0 );
1697 if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
1698 return NULL;
1699 // remap vUsed to be in terms of divisor variables
1700 if ( fCisOnly )
1701 {
1702 Vec_IntForEachEntry( vUsed, Index, i )
1703 Vec_IntWriteEntry( vUsed, i, iCiVarBeg + Index );
1704 }
1705 else
1706 {
1707 Vec_IntForEachEntry( vUsed, Index, i )
1708 Vec_IntWriteEntry( vUsed, i, iCoVarBeg + 1 + Index );
1709 }
1710 // enumerate assignments for each target in terms of used divisors
1711 pSop = Acb_EnumerateSatAssigns( pSat, pCnf->nVars - nTargets + iTar, pCnf->nVars, vUsed, vTempLits, vTempSop );
1712 Vec_IntFree( vTempLits );
1713 Vec_StrFree( vTempSop );
1714 sat_solver_delete( pSat );
1715 if ( pSop == NULL )
1716 return NULL;
1717 //printf( "Function %d:\n%s", i, pSop );
1718 // remap vUsed to be in terms of original divisors
1719 if ( fCisOnly )
1720 {
1721 Vec_IntForEachEntry( vUsed, Index, i )
1722 Vec_IntWriteEntry( vUsed, i, Index - iCiVarBeg );
1723 }
1724 else
1725 {
1726 Vec_IntForEachEntry( vUsed, Index, i )
1727 Vec_IntWriteEntry( vUsed, i, Index - (iCoVarBeg + 1) );
1728 }
1729 return pSop;
1730 }
Acb_CheckMiter(Cnf_Dat_t * pCnf)1731 int Acb_CheckMiter( Cnf_Dat_t * pCnf )
1732 {
1733 int iCoVarBeg = 1, i, Lit, status;
1734 sat_solver * pSat = sat_solver_new();
1735 sat_solver_setnvars( pSat, pCnf->nVars );
1736 // add clauses
1737 for ( i = 0; i < pCnf->nClauses; i++ )
1738 if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
1739 return 1;
1740 // add output clause
1741 Lit = Abc_Var2Lit( iCoVarBeg, 0 );
1742 if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
1743 return 1;
1744 status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
1745 sat_solver_delete( pSat );
1746 return status == l_False;
1747 }
1748
1749
1750 /**Function*************************************************************
1751
1752 Synopsis [Update miter by substituting the last target by a given function.]
1753
1754 Description []
1755
1756 SideEffects []
1757
1758 SeeAlso []
1759
1760 ***********************************************************************/
Acb_CollectIntNodes_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vNodes)1761 void Acb_CollectIntNodes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
1762 {
1763 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
1764 return;
1765 Gia_ObjSetTravIdCurrent(p, pObj);
1766 assert( Gia_ObjIsAnd(pObj) );
1767 Acb_CollectIntNodes_rec( p, Gia_ObjFanin0(pObj), vNodes );
1768 Acb_CollectIntNodes_rec( p, Gia_ObjFanin1(pObj), vNodes );
1769 Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
1770 }
Acb_CollectIntNodes(Gia_Man_t * p,Vec_Int_t * vNodes0,Vec_Int_t * vNodes1)1771 void Acb_CollectIntNodes( Gia_Man_t * p, Vec_Int_t * vNodes0, Vec_Int_t * vNodes1 )
1772 {
1773 Gia_Obj_t * pObj; int i;
1774 Vec_IntClear( vNodes0 );
1775 Vec_IntClear( vNodes1 );
1776 Gia_ManIncrementTravId( p );
1777 Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
1778 Gia_ManForEachCi( p, pObj, i )
1779 Gia_ObjSetTravIdCurrent( p, pObj );
1780 Gia_ManForEachCo( p, pObj, i )
1781 if ( i > 0 )
1782 Acb_CollectIntNodes_rec( p, Gia_ObjFanin0(pObj), vNodes1 );
1783 Gia_ManForEachCo( p, pObj, i )
1784 if ( i == 0 )
1785 Acb_CollectIntNodes_rec( p, Gia_ObjFanin0(pObj), vNodes0 );
1786 }
Acb_UpdateMiter(Gia_Man_t * pM,Gia_Man_t * pOne,int iTar,int nTargets,Vec_Int_t * vUsed,int fCisOnly)1787 Gia_Man_t * Acb_UpdateMiter( Gia_Man_t * pM, Gia_Man_t * pOne, int iTar, int nTargets, Vec_Int_t * vUsed, int fCisOnly )
1788 {
1789 Gia_Man_t * pRes, * pTemp;
1790 Gia_Obj_t * pObj; int i;
1791 Vec_Int_t * vNodes0 = Vec_IntAlloc( Gia_ManAndNum(pM) );
1792 Vec_Int_t * vNodes1 = Vec_IntAlloc( Gia_ManAndNum(pM) );
1793 Acb_CollectIntNodes( pM, vNodes0, vNodes1 );
1794 Gia_ManFillValue( pM );
1795 Gia_ManFillValue( pOne );
1796 // create new
1797 pRes = Gia_ManStart( Gia_ManObjNum(pM) + Gia_ManObjNum(pOne) );
1798 Gia_ManHashAlloc( pRes );
1799 Gia_ManConst0(pM)->Value = 0;
1800 Gia_ManConst0(pOne)->Value = 0;
1801 // copy first part of the miter
1802 Gia_ManForEachCi( pM, pObj, i )
1803 // if ( i < Gia_ManCiNum(pM) - 1 )
1804 pObj->Value = Gia_ManAppendCi( pRes );
1805 Gia_ManForEachObjVec( vNodes1, pM, pObj, i )
1806 pObj->Value = Gia_ManHashAnd( pRes, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1807 Gia_ManForEachCo( pM, pObj, i )
1808 if ( i > 0 )
1809 pObj->Value = Gia_ObjFanin0Copy(pObj);
1810 // transfer to New
1811 //assert( Gia_ManCiNum(pOne) <= Vec_IntSize(vUsed) );
1812 assert( Gia_ManCoNum(pOne) == 1 );
1813 if ( fCisOnly )
1814 {
1815 Gia_ManForEachCi( pOne, pObj, i )
1816 if ( i < Vec_IntSize(vUsed) )
1817 pObj->Value = Gia_ManCi(pM, Vec_IntEntry(vUsed, i))->Value;
1818 }
1819 else
1820 {
1821 Gia_ManForEachCi( pOne, pObj, i )
1822 pObj->Value = Gia_ManCo(pM, 1+Vec_IntEntry(vUsed, i))->Value;
1823 }
1824 Gia_ManForEachAnd( pOne, pObj, i )
1825 pObj->Value = Gia_ManHashAnd( pRes, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1826 // transfer to miter
1827 pObj = Gia_ManCi( pM, Gia_ManCiNum(pM) - nTargets + iTar );
1828 pObj->Value = Gia_ObjFanin0Copy( Gia_ManCo(pOne, 0) );
1829 Gia_ManForEachObjVec( vNodes0, pM, pObj, i )
1830 pObj->Value = Gia_ManHashAnd( pRes, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1831 Gia_ManForEachCo( pM, pObj, i )
1832 Gia_ManAppendCo( pRes, Gia_ObjFanin0Copy(pObj) );
1833 // cleanup
1834 Vec_IntFree( vNodes0 );
1835 Vec_IntFree( vNodes1 );
1836 Gia_ManHashStop( pRes );
1837 pRes = Gia_ManCleanup( pTemp = pRes );
1838 Gia_ManStop( pTemp );
1839 assert( Gia_ManCiNum(pRes) == Gia_ManCiNum(pM) );
1840 assert( Gia_ManCoNum(pRes) == Gia_ManCoNum(pM) );
1841 return pRes;
1842 }
1843
1844 /**Function*************************************************************
1845
1846 Synopsis [Generate strings representing instance and the patch.]
1847
1848 Description []
1849
1850 SideEffects []
1851
1852 SeeAlso []
1853
1854 ***********************************************************************/
Acb_GenerateInstance(Acb_Ntk_t * p,Vec_Int_t * vDivs,Vec_Int_t * vUsed,Vec_Int_t * vTars)1855 Vec_Str_t * Acb_GenerateInstance( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUsed, Vec_Int_t * vTars )
1856 {
1857 int i, iObj;
1858 Vec_Str_t * vStr = Vec_StrAlloc( 100 );
1859 Vec_StrAppend( vStr, " patch p0 (" );
1860 Vec_IntForEachEntry( vTars, iObj, i )
1861 Vec_StrPrintF( vStr, "%s .%s(%s)", i ? ",":"", Acb_ObjNameStr(p, iObj), Acb_ObjNameStr(p, iObj) );
1862 Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i )
1863 Vec_StrPrintF( vStr, ", .%s(%s)", Acb_ObjNameStr(p, iObj), Acb_ObjNameStr(p, iObj) );
1864 Vec_StrAppend( vStr, " );\n\n" );
1865 Vec_StrPush( vStr, '\0' );
1866 return vStr;
1867 }
Acb_GenerateSignalNames(Acb_Ntk_t * p,Vec_Int_t * vDivs,Vec_Int_t * vUsed,int nNodes,Vec_Int_t * vTars,Vec_Wec_t * vGates)1868 Vec_Ptr_t * Acb_GenerateSignalNames( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUsed, int nNodes, Vec_Int_t * vTars, Vec_Wec_t * vGates )
1869 {
1870 Vec_Ptr_t * vRes = Vec_PtrStart( Vec_IntSize(vUsed) + nNodes );
1871 Vec_Str_t * vStr = Vec_StrAlloc(1000); int i, iObj, nWires = 1;
1872 // create input names
1873 Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i )
1874 Vec_PtrWriteEntry( vRes, i, Abc_UtilStrsav(Acb_ObjNameStr(p, iObj)) );
1875 // create names for nodes driving outputs
1876 assert( Vec_WecSize(vGates) == Vec_IntSize(vUsed) + nNodes + Vec_IntSize(vTars) );
1877 Vec_IntForEachEntry( vTars, iObj, i )
1878 {
1879 Vec_Int_t * vGate = Vec_WecEntry( vGates, Vec_IntSize(vUsed) + nNodes + i );
1880 assert( Vec_IntEntry(vGate, 0) == ABC_OPER_BIT_BUF );
1881 Vec_PtrWriteEntry( vRes, Vec_IntEntry(vGate, 1), Abc_UtilStrsav(Acb_ObjNameStr(p, iObj)) );
1882 }
1883 for ( i = Vec_IntSize(vUsed); i < Vec_IntSize(vUsed) + nNodes; i++ )
1884 if ( Vec_PtrEntry(vRes, i) == NULL )
1885 {
1886 Vec_StrPrintF( vStr, "ww%d", nWires++ );
1887 Vec_StrPush( vStr, '\0' );
1888 Vec_PtrWriteEntry( vRes, i, Vec_StrReleaseArray(vStr) );
1889 }
1890 Vec_StrFree( vStr );
1891 return vRes;
1892 }
Acb_GeneratePatch(Acb_Ntk_t * p,Vec_Int_t * vDivs,Vec_Int_t * vUsed,Vec_Ptr_t * vSops,Vec_Ptr_t * vGias,Vec_Int_t * vTars)1893 Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUsed, Vec_Ptr_t * vSops, Vec_Ptr_t * vGias, Vec_Int_t * vTars )
1894 {
1895 extern Vec_Wec_t * Abc_SopSynthesize( Vec_Ptr_t * vSops );
1896 extern Vec_Wec_t * Abc_GiaSynthesize( Vec_Ptr_t * vGias, Gia_Man_t * pMulti );
1897 Vec_Wec_t * vGates = vGias ? Abc_GiaSynthesize(vGias, NULL) : Abc_SopSynthesize(vSops); Vec_Int_t * vGate;
1898 int nOuts = vGias ? Vec_PtrSize(vGias) : Vec_PtrSize(vSops);
1899 int i, k, iObj, nWires = Vec_WecSize(vGates) - Vec_IntSize(vUsed) - nOuts, fFirst = 1;
1900 Vec_Ptr_t * vNames = Acb_GenerateSignalNames( p, vDivs, vUsed, nWires, vTars, vGates );
1901
1902 Vec_Str_t * vStr = Vec_StrAlloc( 100 );
1903 Vec_StrAppend( vStr, "module patch (" );
1904
1905 assert( Vec_IntSize(vTars) == nOuts );
1906 Vec_IntForEachEntry( vTars, iObj, i )
1907 Vec_StrPrintF( vStr, "%s %s", i ? ",":"", Acb_ObjNameStr(p, iObj) );
1908 Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i )
1909 Vec_StrPrintF( vStr, ", %s", Acb_ObjNameStr(p, iObj) );
1910 Vec_StrAppend( vStr, " );\n\n" );
1911
1912 Vec_StrAppend( vStr, " output" );
1913 Vec_IntForEachEntry( vTars, iObj, i )
1914 Vec_StrPrintF( vStr, "%s %s", i ? ",":"", Acb_ObjNameStr(p, iObj) );
1915 Vec_StrAppend( vStr, ";\n" );
1916
1917 Vec_StrAppend( vStr, " input" );
1918 Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i )
1919 Vec_StrPrintF( vStr, "%s %s", i ? ",":"", Acb_ObjNameStr(p, iObj) );
1920 Vec_StrAppend( vStr, ";\n" );
1921
1922 if ( nWires > nOuts )
1923 {
1924 Vec_StrAppend( vStr, " wire" );
1925 for ( i = 0; i < nWires; i++ )
1926 {
1927 char * pName = (char *)Vec_PtrEntry( vNames, Vec_IntSize(vUsed)+i );
1928 if ( !strncmp(pName, "ww", 2) )
1929 Vec_StrPrintF( vStr, "%s %s", fFirst ? "":",", pName ), fFirst = 0;
1930 }
1931 Vec_StrAppend( vStr, ";\n\n" );
1932 }
1933
1934 // create internal nodes
1935 Vec_WecForEachLevelStartStop( vGates, vGate, i, Vec_IntSize(vUsed), Vec_IntSize(vUsed)+nWires )
1936 {
1937 if ( Vec_IntSize(vGate) > 2 )
1938 {
1939 Vec_StrPrintF( vStr, " %s (", Acb_Oper2Name(Vec_IntEntry(vGate, 0)) );
1940 Vec_IntForEachEntryStart( vGate, iObj, k, 1 )
1941 Vec_StrPrintF( vStr, "%s %s", k > 1 ? ",":"", (char *)Vec_PtrEntry(vNames, iObj) );
1942 Vec_StrAppend( vStr, " );\n" );
1943 }
1944 else
1945 {
1946 assert( Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_F || Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T );
1947 Vec_StrPrintF( vStr, " %s (", Acb_Oper2Name( ABC_OPER_BIT_BUF ) );
1948 Vec_StrPrintF( vStr, " %s, ", (char *)Vec_PtrEntry(vNames, Vec_IntEntry(vGate, 1)) );
1949 Vec_StrPrintF( vStr, " 1\'b%d", Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T );
1950 Vec_StrPrintF( vStr, " );\n" );
1951 }
1952 }
1953 Vec_StrAppend( vStr, "\nendmodule\n\n" );
1954 Vec_StrPush( vStr, '\0' );
1955 Vec_PtrFreeFree( vNames );
1956 Vec_WecFree( vGates );
1957
1958 printf( "Synthesized patch with %d inputs, %d outputs and %d gates.\n", Vec_IntSize(vUsed), nOuts, nWires );
1959 return vStr;
1960 }
1961
1962 /**Function*************************************************************
1963
1964 Synopsis [Patch generation.]
1965
1966 Description []
1967
1968 SideEffects []
1969
1970 SeeAlso []
1971
1972 ***********************************************************************/
Acb_GenerateInstance2(Vec_Ptr_t * vIns,Vec_Ptr_t * vOuts)1973 Vec_Str_t * Acb_GenerateInstance2( Vec_Ptr_t * vIns, Vec_Ptr_t * vOuts )
1974 {
1975 char * pName; int i;
1976 Vec_Str_t * vStr = Vec_StrAlloc( 100 );
1977 Vec_StrAppend( vStr, " patch p0 (" );
1978 Vec_PtrForEachEntry( char *, vOuts, pName, i )
1979 Vec_StrPrintF( vStr, "%s .%s(t%d_%s)", i ? ",":"", pName, i, pName );
1980 Vec_PtrForEachEntry( char *, vIns, pName, i )
1981 Vec_StrPrintF( vStr, ", .%s(%s)", pName, pName );
1982 Vec_StrAppend( vStr, " );\n\n" );
1983 Vec_StrPush( vStr, '\0' );
1984 return vStr;
1985 }
Acb_GenerateSignalNames2(Vec_Wec_t * vGates,Vec_Ptr_t * vIns,Vec_Ptr_t * vOuts)1986 Vec_Ptr_t * Acb_GenerateSignalNames2( Vec_Wec_t * vGates, Vec_Ptr_t * vIns, Vec_Ptr_t * vOuts )
1987 {
1988 int nIns = Vec_PtrSize(vIns), nOuts = Vec_PtrSize(vOuts);
1989 int nNodes = Vec_WecSize(vGates) - nIns - nOuts;
1990 Vec_Ptr_t * vRes = Vec_PtrStart( Vec_WecSize(vGates) ); char * pName;
1991 Vec_Str_t * vStr = Vec_StrAlloc(1000); int i, nWires = 1;
1992 // create input names
1993 Vec_PtrForEachEntry( char *, vIns, pName, i )
1994 Vec_PtrWriteEntry( vRes, i, Abc_UtilStrsav(pName) );
1995 // create names for nodes driving outputs
1996 Vec_PtrForEachEntry( char *, vOuts, pName, i )
1997 {
1998 Vec_Int_t * vGate = Vec_WecEntry( vGates, nIns + nNodes + i );
1999 assert( Vec_IntEntry(vGate, 0) == ABC_OPER_BIT_BUF );
2000 Vec_PtrWriteEntry( vRes, Vec_IntEntry(vGate, 1), Abc_UtilStrsav(pName) );
2001 }
2002 for ( i = nIns; i < nIns + nNodes; i++ )
2003 if ( Vec_PtrEntry(vRes, i) == NULL )
2004 {
2005 Vec_StrPrintF( vStr, "ww%d", nWires++ );
2006 Vec_StrPush( vStr, '\0' );
2007 Vec_PtrWriteEntry( vRes, i, Vec_StrReleaseArray(vStr) );
2008 }
2009 Vec_StrFree( vStr );
2010 return vRes;
2011 }
Acb_GeneratePatch2(Gia_Man_t * pGia,Vec_Ptr_t * vIns,Vec_Ptr_t * vOuts)2012 Vec_Str_t * Acb_GeneratePatch2( Gia_Man_t * pGia, Vec_Ptr_t * vIns, Vec_Ptr_t * vOuts )
2013 {
2014 extern Vec_Wec_t * Abc_GiaSynthesize( Vec_Ptr_t * vGias, Gia_Man_t * pMulti );
2015 Vec_Wec_t * vGates = Abc_GiaSynthesize( NULL, pGia ); Vec_Int_t * vGate;
2016 int nIns = Vec_PtrSize(vIns), nOuts = Vec_PtrSize(vOuts); char * pName;
2017 int i, k, iObj, nWires = Vec_WecSize(vGates) - nIns - nOuts, fFirst = 1;
2018 Vec_Ptr_t * vNames = Acb_GenerateSignalNames2( vGates, vIns, vOuts );
2019
2020 Vec_Str_t * vStr = Vec_StrAlloc( 100 );
2021 Vec_StrAppend( vStr, "module patch (" );
2022
2023 Vec_PtrForEachEntry( char *, vOuts, pName, i )
2024 Vec_StrPrintF( vStr, "%s %s", i ? ",":"", pName );
2025 Vec_PtrForEachEntry( char *, vIns, pName, i )
2026 Vec_StrPrintF( vStr, ", %s", pName );
2027 Vec_StrAppend( vStr, " );\n\n" );
2028
2029 Vec_StrAppend( vStr, " output" );
2030 Vec_PtrForEachEntry( char *, vOuts, pName, i )
2031 Vec_StrPrintF( vStr, "%s %s", i ? ",":"", pName );
2032 Vec_StrAppend( vStr, ";\n" );
2033
2034 Vec_StrAppend( vStr, " input" );
2035 Vec_PtrForEachEntry( char *, vIns, pName, i )
2036 Vec_StrPrintF( vStr, "%s %s", i ? ",":"", pName );
2037 Vec_StrAppend( vStr, ";\n" );
2038
2039 if ( nWires > nOuts )
2040 {
2041 Vec_StrAppend( vStr, " wire" );
2042 for ( i = 0; i < nWires; i++ )
2043 {
2044 char * pName = (char *)Vec_PtrEntry( vNames, nIns+i );
2045 if ( !strncmp(pName, "ww", 2) )
2046 Vec_StrPrintF( vStr, "%s %s", fFirst ? "":",", pName ), fFirst = 0;
2047 }
2048 Vec_StrAppend( vStr, ";\n\n" );
2049 }
2050
2051 // create internal nodes
2052 Vec_WecForEachLevelStartStop( vGates, vGate, i, nIns, nIns+nWires )
2053 {
2054 if ( Vec_IntSize(vGate) > 2 )
2055 {
2056 Vec_StrPrintF( vStr, " %s (", Acb_Oper2Name(Vec_IntEntry(vGate, 0)) );
2057 Vec_IntForEachEntryStart( vGate, iObj, k, 1 )
2058 Vec_StrPrintF( vStr, "%s %s", k > 1 ? ",":"", (char *)Vec_PtrEntry(vNames, iObj) );
2059 Vec_StrAppend( vStr, " );\n" );
2060 }
2061 else
2062 {
2063 assert( Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_F || Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T );
2064 Vec_StrPrintF( vStr, " %s (", Acb_Oper2Name( ABC_OPER_BIT_BUF ) );
2065 Vec_StrPrintF( vStr, " %s, ", (char *)Vec_PtrEntry(vNames, Vec_IntEntry(vGate, 1)) );
2066 Vec_StrPrintF( vStr, " 1\'b%d", Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T );
2067 Vec_StrPrintF( vStr, " );\n" );
2068 }
2069 }
2070 Vec_StrAppend( vStr, "\nendmodule\n\n" );
2071 Vec_StrPush( vStr, '\0' );
2072 Vec_PtrFreeFree( vNames );
2073 Vec_WecFree( vGates );
2074
2075 printf( "Synthesized patch with %d inputs, %d outputs and %d gates.\n", nIns, nOuts, nWires );
2076 return vStr;
2077 }
Acb_GenerateFile2(Gia_Man_t * pGia,Vec_Ptr_t * vIns,Vec_Ptr_t * vOuts,char * pFileName,char * pFileNameOut)2078 void Acb_GenerateFile2( Gia_Man_t * pGia, Vec_Ptr_t * vIns, Vec_Ptr_t * vOuts, char * pFileName, char * pFileNameOut )
2079 {
2080 extern void Acb_GenerateFilePatch( Vec_Str_t * p, char * pFileNamePatch );
2081 extern void Acb_GenerateFileOut( Vec_Str_t * vPatchLine, char * pFileNameF, char * pFileNameOut, Vec_Str_t * vPatch );
2082 extern void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames, int fNumber );
2083 Vec_Str_t * vInst = Acb_GenerateInstance2( vIns, vOuts );
2084 Vec_Str_t * vPatch = Acb_GeneratePatch2( pGia, vIns, vOuts );
2085 //printf( "%s", Vec_StrArray(vPatch) );
2086 //Gia_AigerWrite( pGia, "test.aig", 0, 0, 0 );
2087 // generate output files
2088 Acb_GenerateFilePatch( vPatch, "patch.v" );
2089 printf( "Finished dumping patch file \"%s\".\n", "patch.v" );
2090 Acb_NtkInsert( pFileName, "temp.v", vOuts, 0 );
2091 printf( "Finished dumping intermediate file \"%s\".\n", "temp.v" );
2092 Acb_GenerateFileOut( vInst, "temp.v", pFileNameOut, vPatch );
2093 printf( "Finished dumping the resulting file \"%s\".\n", pFileNameOut );
2094 Vec_StrFree( vInst );
2095 Vec_StrFree( vPatch );
2096 }
2097
2098 /**Function*************************************************************
2099
2100 Synopsis [Produce output files.]
2101
2102 Description []
2103
2104 SideEffects []
2105
2106 SeeAlso []
2107
2108 ***********************************************************************/
Acb_GenerateFilePatch(Vec_Str_t * p,char * pFileNamePatch)2109 void Acb_GenerateFilePatch( Vec_Str_t * p, char * pFileNamePatch )
2110 {
2111 FILE * pFile = fopen( pFileNamePatch, "wb" );
2112 if ( !pFile )
2113 return;
2114 fprintf( pFile, "%s", Vec_StrArray(p) );
2115 fclose( pFile );
2116 }
Acb_GenerateFileOut(Vec_Str_t * vPatchLine,char * pFileNameF,char * pFileNameOut,Vec_Str_t * vPatch)2117 void Acb_GenerateFileOut( Vec_Str_t * vPatchLine, char * pFileNameF, char * pFileNameOut, Vec_Str_t * vPatch )
2118 {
2119 FILE * pFileOut;
2120 char * pBuffer = Extra_FileReadContents( pFileNameF );
2121 if ( pBuffer == NULL )
2122 return;
2123 pFileOut = fopen( pFileNameOut, "wb" );
2124 if ( pFileOut )
2125 {
2126 char * pTemp = strstr( pBuffer, "endmodule" );
2127 int nFirst = pTemp-pBuffer, nSecond = strlen(pBuffer) - nFirst;
2128 int Value = fwrite( pBuffer, nFirst, 1, pFileOut );
2129 fprintf( pFileOut, "\n%s", Vec_StrArray(vPatchLine) );
2130 Value = fwrite( pBuffer+nFirst, nSecond, 1, pFileOut );
2131 if ( vPatch )
2132 fprintf( pFileOut, "\n%s\n", Vec_StrArray(vPatch) );
2133 }
2134 ABC_FREE( pBuffer );
2135 fclose( pFileOut );
2136 }
2137
2138 /**Function*************************************************************
2139
2140 Synopsis [Print parameters of the patch.]
2141
2142 Description []
2143
2144 SideEffects []
2145
2146 SeeAlso []
2147
2148 ***********************************************************************/
Acb_PrintPatch(Acb_Ntk_t * pNtkF,Vec_Int_t * vDivs,Vec_Int_t * vUsed,abctime clk)2149 void Acb_PrintPatch( Acb_Ntk_t * pNtkF, Vec_Int_t * vDivs, Vec_Int_t * vUsed, abctime clk )
2150 {
2151 int i, iObj, Weight = 0;
2152 printf( "Patch has %d inputs: ", Vec_IntSize(vUsed) );
2153 Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i )
2154 {
2155 printf( "%d=%s(w=%d) ", Vec_IntEntry(vUsed, i), Acb_ObjNameStr(pNtkF, iObj), Acb_ObjWeight(pNtkF, iObj) );
2156 Weight += Acb_ObjWeight(pNtkF, iObj);
2157 }
2158 printf( "\nTotal weight = %d ", Weight );
2159 Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clk );
2160 printf( "\n" );
2161 }
2162
2163 /**Function*************************************************************
2164
2165 Synopsis [Quantifies targets 0 up to iTar (out of nTars).]
2166
2167 Description []
2168
2169 SideEffects []
2170
2171 SeeAlso []
2172
2173 ***********************************************************************/
Acb_NtkEcoSynthesize(Gia_Man_t * p)2174 Gia_Man_t * Acb_NtkEcoSynthesize( Gia_Man_t * p )
2175 {
2176 int Iter, fVerbose = 0;
2177 Gia_Man_t * pNew = Gia_ManDup( p );
2178
2179 if ( fVerbose ) printf( "M_quo: " );
2180 if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
2181
2182 pNew = Gia_ManAreaBalance( p = pNew, 0, 0, 0, 0 );
2183 Gia_ManStop( p );
2184
2185 if ( fVerbose ) printf( "M_bal: " );
2186 if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
2187
2188 for ( Iter = 0; Iter < 2; Iter++ )
2189 {
2190 pNew = Gia_ManCompress2( p = pNew, 1, 0 );
2191 Gia_ManStop( p );
2192
2193 if ( fVerbose ) printf( "M_dc2: " );
2194 if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
2195 }
2196
2197 pNew = Gia_ManAigSyn2( p = pNew, 0, 1, 0, 100, 0, 0, 0 );
2198 Gia_ManStop( p );
2199
2200 if ( fVerbose ) printf( "M_sn2: " );
2201 if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
2202
2203 for ( Iter = 0; Iter < 2; Iter++ )
2204 {
2205 pNew = Gia_ManCompress2( p = pNew, 1, 0 );
2206 Gia_ManStop( p );
2207
2208 if ( fVerbose ) printf( "M_dc2: " );
2209 if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
2210 }
2211 return pNew;
2212 }
Acb_NtkDeriveMiterCnf(Gia_Man_t * p,int iTar,int nTars,int fVerbose)2213 Cnf_Dat_t * Acb_NtkDeriveMiterCnf( Gia_Man_t * p, int iTar, int nTars, int fVerbose )
2214 {
2215 Gia_Man_t * pCof = Gia_ManDup( p );
2216 Cnf_Dat_t * pCnf; int v;
2217 for ( v = 0; v < iTar; v++ )
2218 {
2219 Gia_Man_t * pTemp;
2220 pCof = Gia_ManDupUniv( p = pCof, Gia_ManCiNum(pCof) - nTars + v );
2221 //pCof = Acb_NtkEcoSynthesize( pTemp = pCof );
2222 //pCof = Gia_ManCompress2( pTemp = pCof, 1, 0 );
2223 pCof = Gia_ManAigSyn2( pTemp = pCof, 0, 1, 0, 100, 0, 0, 0 );
2224 Gia_ManStop( pTemp );
2225 if ( Gia_ManAndNum(pCof) > 10000 )
2226 {
2227 printf( "Quantifying target %3d ", v );
2228 Gia_ManPrintStats( pCof, NULL );
2229 }
2230 assert( Gia_ManCiNum(pCof) == Gia_ManCiNum(p) );
2231 Gia_ManStop( p );
2232 }
2233 if ( fVerbose ) printf( "M_quo: " );
2234 if ( fVerbose ) Gia_ManPrintStats( pCof, NULL );
2235 //pCof = Acb_NtkEcoSynthesize( p = pCof );
2236 //Gia_ManStop( p );
2237 if ( fVerbose ) printf( "M_syn: " );
2238 if ( fVerbose ) Gia_ManPrintStats( pCof, NULL );
2239 if ( 0 && iTar < nTars )
2240 {
2241 Gia_Man_t * pCof0 = Gia_ManDupCofactorVar( pCof, Gia_ManCiNum(pCof) - nTars + iTar, 0 );
2242 Gia_Man_t * pCof1 = Gia_ManDupCofactorVar( pCof, Gia_ManCiNum(pCof) - nTars + iTar, 1 );
2243 pCof0 = Acb_NtkEcoSynthesize( p = pCof0 );
2244 Gia_ManStop( p );
2245 pCof1 = Acb_NtkEcoSynthesize( p = pCof1 );
2246 Gia_ManStop( p );
2247 Gia_AigerWrite( pCof0, "eco_qbf0.aig", 0, 0, 0 );
2248 Gia_AigerWrite( pCof1, "eco_qbf1.aig", 0, 0, 0 );
2249 Gia_ManStop( pCof0 );
2250 Gia_ManStop( pCof1 );
2251 printf( "Dumped cof0 into file \"%s\".\n", "eco_qbf0.aig" );
2252 printf( "Dumped cof1 into file \"%s\".\n", "eco_qbf1.aig" );
2253 }
2254 // Gia_AigerWrite( pCof, "eco_qbf.aig", 0, 0, 0 );
2255 // printf( "Dumped the result of quantification into file \"%s\".\n", "eco_qbf.aig" );
2256 pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCof, 8, 0, 0, 0, 0 );
2257 Gia_ManStop( pCof );
2258 return pCnf;
2259 }
Gia_ManInterOneInt(Gia_Man_t * pCof1,Gia_Man_t * pCof0,int Depth)2260 Gia_Man_t * Gia_ManInterOneInt( Gia_Man_t * pCof1, Gia_Man_t * pCof0, int Depth )
2261 {
2262 extern Gia_Man_t * Gia_ManInterOne( Gia_Man_t * pNtkOn, Gia_Man_t * pNtkOff, int fVerbose );
2263 extern Gia_Man_t * Abc_GiaSynthesizeInter( Gia_Man_t * p );
2264 Gia_Man_t * pGia[2] = { pCof0, pCof1 };
2265 Gia_Man_t * pCof[2][2] = {{0}}, * pTemp;
2266 Gia_Man_t * pInter[2], * pFinal;
2267 Gia_Obj_t * pObj;
2268 int i, n, m, Count, CountBest = 0, iVarBest = -1;
2269 // find PIs with the highest fanout
2270 Vec_Int_t * vFanCount;
2271 if ( Gia_ManAndNum(pCof1) == 0 || Gia_ManAndNum(pCof0) == 0 )
2272 return Gia_ManDup(pCof1);
2273 vFanCount = Vec_IntStart( Gia_ManCiNum(pCof0) );
2274 for ( n = 0; n < 2; n++ )
2275 {
2276 Gia_ManForEachAnd( pGia[n], pObj, i )
2277 {
2278 if ( Gia_ObjIsCi(Gia_ObjFanin0(pObj)) )
2279 Vec_IntAddToEntry( vFanCount, Gia_ObjCioId(Gia_ObjFanin0(pObj)), 1 );
2280 if ( Gia_ObjIsCi(Gia_ObjFanin1(pObj)) )
2281 Vec_IntAddToEntry( vFanCount, Gia_ObjCioId(Gia_ObjFanin1(pObj)), 1 );
2282 }
2283 }
2284 Vec_IntForEachEntry( vFanCount, Count, i )
2285 if ( CountBest < Count )
2286 {
2287 CountBest = Count;
2288 iVarBest = i;
2289 }
2290 Vec_IntFree( vFanCount );
2291 // Gia_Man_t * Gia_ManDupCofactorVar( Gia_Man_t * p, int iVar, int Value )
2292 for ( n = 0; n < 2; n++ )
2293 for ( m = 0; m < 2; m++ )
2294 {
2295 pCof[n][m] = Gia_ManDupCofactorVar( pGia[n], iVarBest, m );
2296 pCof[n][m] = Acb_NtkEcoSynthesize( pTemp = pCof[n][m] );
2297 Gia_ManStop( pTemp );
2298 printf( "%*sCof%d%d : ", 8-Depth, "", n, m );
2299 Gia_ManPrintStats( pCof[n][m], NULL );
2300 }
2301 for ( m = 0; m < 2; m++ )
2302 {
2303 if ( Gia_ManAndNum(pCof[1][m]) == 0 || Gia_ManAndNum(pCof[0][m]) == 0 )
2304 pInter[m] = Gia_ManDup( pCof[1][m] );
2305 else if ( Depth == 1 )
2306 pInter[m] = Gia_ManInterOne( pCof[1][m], pCof[0][m], 1 );
2307 else
2308 pInter[m] = Gia_ManInterOneInt( pCof[1][m], pCof[0][m], Depth-1 );
2309 printf( "%*sInter%d : ", 8-Depth, "", m );
2310 Gia_ManPrintStats( pInter[m], NULL );
2311 pInter[m] = Abc_GiaSynthesizeInter( pTemp = pInter[m] );
2312 Gia_ManStop( pTemp );
2313 printf( "%*sInter%d : ", 8-Depth, "", m );
2314 Gia_ManPrintStats( pInter[m], NULL );
2315 }
2316 for ( n = 0; n < 2; n++ )
2317 for ( m = 0; m < 2; m++ )
2318 Gia_ManStop( pCof[n][m] );
2319 pFinal = Gia_ManDupMux( iVarBest, pInter[1], pInter[0] );
2320 for ( m = 0; m < 2; m++ )
2321 Gia_ManStop( pInter[m] );
2322 return pFinal;
2323 }
Acb_NtkDeriveMiterCnfInter2(Gia_Man_t * p,int iTar,int nTars)2324 Gia_Man_t * Acb_NtkDeriveMiterCnfInter2( Gia_Man_t * p, int iTar, int nTars )
2325 {
2326 // extern Gia_Man_t * Gia_ManInterOne( Gia_Man_t * pNtkOn, Gia_Man_t * pNtkOff, int fVerbose );
2327 extern Gia_Man_t * Abc_GiaSynthesizeInter( Gia_Man_t * p );
2328 Gia_Man_t * pInter, * pCof0, * pCof1, * pCof = Gia_ManDup( p ); int v;
2329 for ( v = 0; v < iTar; v++ )
2330 {
2331 pCof = Gia_ManDupUniv( p = pCof, Gia_ManCiNum(pCof) - nTars + v );
2332 assert( Gia_ManCiNum(pCof) == Gia_ManCiNum(p) );
2333 Gia_ManStop( p );
2334
2335 pCof = Acb_NtkEcoSynthesize( p = pCof );
2336 Gia_ManStop( p );
2337 }
2338 pCof0 = Gia_ManDupCofactorVar( pCof, Gia_ManCiNum(pCof) - nTars + iTar, 1 );
2339 pCof1 = Gia_ManDupCofactorVar( pCof, Gia_ManCiNum(pCof) - nTars + iTar, 0 );
2340 Gia_ManStop( pCof );
2341 pCof0 = Acb_NtkEcoSynthesize( p = pCof0 );
2342 Gia_ManStop( p );
2343 pCof1 = Acb_NtkEcoSynthesize( p = pCof1 );
2344 Gia_ManStop( p );
2345
2346 printf( "Cof0 : " );
2347 Gia_ManPrintStats( pCof0, NULL );
2348 printf( "Cof1 : " );
2349 Gia_ManPrintStats( pCof1, NULL );
2350
2351 if ( Gia_ManAndNum(pCof1) == 0 || Gia_ManAndNum(pCof0) == 0 )
2352 pInter = Gia_ManDup(pCof1);
2353 else
2354 pInter = Gia_ManInterOneInt( pCof1, pCof0, 7 );
2355 Gia_ManStop( pCof0 );
2356 Gia_ManStop( pCof1 );
2357 pInter = Abc_GiaSynthesizeInter( p = pInter );
2358 Gia_ManStop( p );
2359 //Gia_ManPrintStats( pInter, NULL );
2360 pInter = Gia_ManDupRemovePis( p = pInter, nTars );
2361 Gia_ManStop( p );
2362 //Gia_ManPrintStats( pInter, NULL );
2363 return pInter;
2364 }
Acb_NtkDeriveMiterCnfInter(Gia_Man_t * p,int iTar,int nTars)2365 Gia_Man_t * Acb_NtkDeriveMiterCnfInter( Gia_Man_t * p, int iTar, int nTars )
2366 {
2367 Gia_Man_t * pCof1, * pCof = Gia_ManDup( p ); int v;
2368 for ( v = 0; v < iTar; v++ )
2369 {
2370 pCof = Gia_ManDupUniv( p = pCof, Gia_ManCiNum(pCof) - nTars + v );
2371 assert( Gia_ManCiNum(pCof) == Gia_ManCiNum(p) );
2372 Gia_ManStop( p );
2373
2374 pCof = Acb_NtkEcoSynthesize( p = pCof );
2375 Gia_ManStop( p );
2376 }
2377 pCof1 = Gia_ManDupCofactorVar( pCof, Gia_ManCiNum(pCof) - nTars + iTar, 0 );
2378 Gia_ManStop( pCof );
2379
2380 pCof1 = Acb_NtkEcoSynthesize( p = pCof1 );
2381 Gia_ManStop( p );
2382
2383 pCof1 = Gia_ManDupRemovePis( p = pCof1, nTars );
2384 Gia_ManStop( p );
2385 return pCof1;
2386 }
2387
2388 /**Function*************************************************************
2389
2390 Synopsis [Transform patch functions to have common support.]
2391
2392 Description []
2393
2394 SideEffects []
2395
2396 SeeAlso []
2397
2398 ***********************************************************************/
Acb_RemapOneFunction(char * pStr,Vec_Int_t * vSupp,Vec_Int_t * vMap,int nVars)2399 char * Acb_RemapOneFunction( char * pStr, Vec_Int_t * vSupp, Vec_Int_t * vMap, int nVars )
2400 {
2401 Vec_Str_t * vTempSop = Vec_StrAlloc( 100 );
2402 char * pToken = strtok( pStr, "\n" ); int i;
2403 while ( pToken != NULL )
2404 {
2405 for ( i = 0; i < nVars; i++ )
2406 Vec_StrPush( vTempSop, '-' );
2407 for ( i = 0; pToken[i] != ' '; i++ )
2408 if ( pToken[i] != '-' )
2409 {
2410 int iVar = Vec_IntEntry( vMap, Vec_IntEntry(vSupp, i) );
2411 assert( iVar >= 0 && iVar < nVars );
2412 Vec_StrWriteEntry( vTempSop, Vec_StrSize(vTempSop) - nVars + iVar, pToken[i] );
2413 }
2414 Vec_StrPrintF( vTempSop, " %d\n", pToken[i+1] - '0' );
2415 pToken = strtok( NULL, "\n" );
2416 }
2417 Vec_StrPush( vTempSop, '\0' );
2418 pToken = Vec_StrReleaseArray(vTempSop);
2419 Vec_StrFree( vTempSop );
2420 return pToken;
2421 }
Acb_TransformPatchFunctions(Vec_Ptr_t * vSops,Vec_Wec_t * vSupps,Vec_Int_t ** pvUsed,int nDivs)2422 Vec_Ptr_t * Acb_TransformPatchFunctions( Vec_Ptr_t * vSops, Vec_Wec_t * vSupps, Vec_Int_t ** pvUsed, int nDivs )
2423 {
2424 Vec_Ptr_t * vFuncs = Vec_PtrAlloc( Vec_PtrSize(vSops) );
2425 Vec_Int_t * vUsed = Vec_IntAlloc( 100 );
2426 Vec_Int_t * vMap = Vec_IntStartFull( nDivs );
2427 Vec_Int_t * vPres = Vec_IntStart( nDivs );
2428 Vec_Int_t * vLevel;
2429 int i, k, iVar;
2430 // check what divisors are used
2431 Vec_WecForEachLevel( vSupps, vLevel, i )
2432 {
2433 char * pSop = (char *)Vec_PtrEntry( vSops, i );
2434 char * pStrCopy = Abc_UtilStrsav( pSop );
2435 char * pToken = strtok( pStrCopy, "\n" );
2436 while ( pToken != NULL )
2437 {
2438 for ( k = 0; pToken[k] != ' '; k++ )
2439 if ( pToken[k] != '-' )
2440 Vec_IntWriteEntry( vPres, Vec_IntEntry(vLevel, k), 1 );
2441 pToken = strtok( NULL, "\n" );
2442 }
2443 ABC_FREE( pStrCopy );
2444 }
2445 // create common order
2446 Vec_WecForEachLevel( vSupps, vLevel, i )
2447 Vec_IntForEachEntry( vLevel, iVar, k )
2448 {
2449 if ( !Vec_IntEntry(vPres, iVar) )
2450 continue;
2451 if ( Vec_IntEntry(vMap, iVar) >= 0 )
2452 continue;
2453 Vec_IntWriteEntry( vMap, iVar, Vec_IntSize(vUsed) );
2454 Vec_IntPush( vUsed, iVar );
2455 }
2456 printf( "The number of used variables %d (out of %d).\n", Vec_IntSum(vPres), Vec_IntSize(vPres) );
2457 // remap SOPs
2458 Vec_WecForEachLevel( vSupps, vLevel, i )
2459 {
2460 char * pSop = (char *)Vec_PtrEntry( vSops, i );
2461 pSop = Acb_RemapOneFunction( pSop, vLevel, vMap, Vec_IntSize(vUsed) );
2462 //printf( "Function %d\n%s", i, pSop );
2463 Vec_PtrPush( vFuncs, pSop );
2464 }
2465 Vec_IntFree( vPres );
2466 Vec_IntFree( vMap );
2467 *pvUsed = vUsed;
2468 return vFuncs;
2469 }
2470
2471 /**Function*************************************************************
2472
2473 Synopsis [Performs ECO for two networks.]
2474
2475 Description []
2476
2477 SideEffects []
2478
2479 SeeAlso []
2480
2481 ***********************************************************************/
Acb_NtkEcoPerform(Acb_Ntk_t * pNtkF,Acb_Ntk_t * pNtkG,char * pFileName[4],int fCisOnly,int fCheck,int fVerbose)2482 int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4], int fCisOnly, int fCheck, int fVerbose )
2483 {
2484 extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp );
2485
2486 abctime clk = Abc_Clock();
2487 int nTargets = Vec_IntSize(&pNtkF->vTargets);
2488 int TimeOut = fCisOnly ? 0 : 60; // 60 seconds
2489 int RetValue = 1;
2490
2491 // compute various sets of nodes
2492 Vec_Bit_t * vBlock;
2493 Vec_Int_t * vRoots = Acb_NtkFindRoots( pNtkF, &pNtkF->vTargets, &vBlock );
2494 Vec_Int_t * vSuppF = Acb_NtkFindSupp( pNtkF, vRoots );
2495 Vec_Int_t * vSuppG = Acb_NtkFindSupp( pNtkG, vRoots );
2496 Vec_Int_t * vSupp = Vec_IntTwoMerge( vSuppF, vSuppG );
2497 Vec_Int_t * vDivs = fCisOnly ? Acb_NtkFindDivsCis( pNtkF, vSupp ) : Acb_NtkFindDivs( pNtkF, vSupp, vBlock, fVerbose );
2498 Vec_Int_t * vNodesF = Acb_NtkFindNodes( pNtkF, vRoots, vDivs );
2499 Vec_Int_t * vNodesG = Acb_NtkFindNodes( pNtkG, vRoots, NULL );
2500
2501 // create AIGs
2502 Gia_Man_t * pGiaF = Acb_NtkToGia( pNtkF, vSupp, vNodesF, vRoots, vDivs, &pNtkF->vTargets );
2503 Gia_Man_t * pGiaG = Acb_NtkToGia( pNtkG, vSupp, vNodesG, vRoots, NULL, NULL );
2504 Gia_Man_t * pGiaM = Acb_CreateMiter( pGiaF, pGiaG );
2505
2506 Cnf_Dat_t * pCnf;
2507 Gia_Man_t * pTemp, * pOne;
2508 Vec_Ptr_t * vSops = Vec_PtrAlloc( nTargets );
2509 Vec_Wec_t * vSupps = Vec_WecAlloc( nTargets );
2510 Vec_Int_t * vSuppOld = Vec_IntAlloc( 100 );
2511
2512 Vec_Int_t * vUsed = NULL;
2513 Vec_Ptr_t * vFuncs = NULL;
2514 Vec_Ptr_t * vGias = fCisOnly ? Vec_PtrAlloc(nTargets) : NULL;
2515 Vec_Str_t * vInst = NULL, * vPatch = NULL;
2516
2517 char * pSop = NULL;
2518 int i, Res;
2519
2520 if ( fVerbose )
2521 {
2522 printf( "The number of targets = %d.\n", nTargets );
2523
2524 printf( "NtkF: " );
2525 Gia_ManPrintStats( pGiaF, NULL );
2526 printf( "NtkG: " );
2527 Gia_ManPrintStats( pGiaG, NULL );
2528 printf( "Miter: " );
2529 Gia_ManPrintStats( pGiaM, NULL );
2530 }
2531
2532 // check that the problem has a solution
2533 if ( fCheck )//fCisOnly )
2534 {
2535 int Lit, status;
2536 sat_solver * pSat;
2537 pCnf = Acb_NtkDeriveMiterCnf( pGiaM, nTargets, nTargets, fVerbose );
2538 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
2539 Cnf_DataFree( pCnf );
2540 // add output clause
2541 Lit = Abc_Var2Lit( 1, 0 );
2542 status = sat_solver_addclause( pSat, &Lit, &Lit+1 );
2543 status = status == 0 ? l_False : sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
2544 sat_solver_delete( pSat );
2545 printf( "The ECO problem has %s solution. ", status == l_False ? "a" : "NO" );
2546 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2547 if ( status != l_False )
2548 {
2549 RetValue = 0;
2550 goto cleanup;
2551 }
2552 }
2553
2554 for ( i = nTargets-1; i >= 0; i-- )
2555 {
2556 Vec_Int_t * vSupp = NULL;
2557 printf( "\nConsidering target %d (out of %d)...\n", i, nTargets );
2558 // compute support of this target
2559 if ( fCisOnly )
2560 {
2561 vSupp = Vec_IntStartNatural( Vec_IntSize(vDivs) );
2562 printf( "Target %d has support with %d variables.\n", i, Vec_IntSize(vSupp) );
2563
2564 pOne = Acb_NtkDeriveMiterCnfInter( pGiaM, i, nTargets );
2565 printf( "Tar%02d: ", i );
2566 Gia_ManPrintStats( pOne, NULL );
2567
2568 // update miter
2569 pGiaM = Acb_UpdateMiter( pTemp = pGiaM, pOne, i, nTargets, vSupp, fCisOnly );
2570 Gia_ManStop( pTemp );
2571
2572 // add to functions
2573 Vec_PtrPush( vGias, pOne );
2574 }
2575 else
2576 {
2577 pCnf = Acb_NtkDeriveMiterCnf( pGiaM, i, nTargets, fVerbose );
2578 // vSupp = Acb_DerivePatchSupportS( pCnf, i, nTargets, Vec_IntSize(vDivs), vDivs, pNtkF, NULL, TimeOut );
2579 vSupp = Acb_DerivePatchSupport( pCnf, i, nTargets, Vec_IntSize(vDivs), vDivs, pNtkF, vSuppOld, TimeOut );
2580 if ( vSupp == NULL )
2581 {
2582 Cnf_DataFree( pCnf );
2583 RetValue = 0;
2584 goto cleanup;
2585 }
2586 Vec_IntAppend( vSuppOld, vSupp );
2587 Vec_IntClear( vSupp );
2588 Vec_IntAppend( vSupp, vSuppOld );
2589 //Vec_IntClear( vSuppOld );
2590
2591 // derive function of this target
2592 pSop = Acb_DeriveOnePatchFunction( pCnf, i, nTargets, Vec_IntSize(vDivs), vSupp, fCisOnly );
2593 Cnf_DataFree( pCnf );
2594 if ( pSop == NULL )
2595 {
2596 RetValue = 0;
2597 goto cleanup;
2598 }
2599
2600 // add new function to the miter
2601 pOne = Abc_SopSynthesizeOne( pSop, 1 );
2602 printf( "Tar%02d: ", i );
2603 Gia_ManPrintStats( pOne, NULL );
2604
2605 // update miter
2606 pGiaM = Acb_UpdateMiter( pTemp = pGiaM, pOne, i, nTargets, vSupp, fCisOnly );
2607 Gia_ManStop( pTemp );
2608 Gia_ManStop( pOne );
2609
2610 // add to functions
2611 Vec_PtrPush( vSops, pSop );
2612 }
2613 // add to supports
2614 Vec_IntAppend( Vec_WecPushLevel(vSupps), vSupp );
2615 Vec_IntFree( vSupp );
2616 }
2617
2618 // make sure the function is UNSAT
2619 printf( "\n" );
2620 if ( !fCisOnly )
2621 {
2622 abctime clk = Abc_Clock();
2623 pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGiaM, 8, 0, 0, 0, 0 );
2624 Res = Acb_CheckMiter( pCnf );
2625 Cnf_DataFree( pCnf );
2626 if ( Res == 1 )
2627 printf( "The ECO solution was verified successfully. " );
2628 else
2629 printf( "The ECO solution verification FAILED. " );
2630 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2631 }
2632
2633 // derive new patch functions
2634 if ( fCisOnly )
2635 {
2636 vUsed = Vec_IntStartNatural( Vec_IntSize(vDivs) );
2637 Vec_PtrReverseOrder( vGias );
2638 }
2639 else
2640 {
2641 vFuncs = Acb_TransformPatchFunctions( vSops, vSupps, &vUsed, Vec_IntSize(vDivs) );
2642 Vec_PtrReverseOrder( vFuncs );
2643 }
2644
2645 // generate instance and patch
2646 vInst = Acb_GenerateInstance( pNtkF, vDivs, vUsed, &pNtkF->vTargets );
2647 vPatch = Acb_GeneratePatch( pNtkF, vDivs, vUsed, vFuncs, vGias, &pNtkF->vTargets );
2648
2649 // print the results
2650 //printf( "%s", Vec_StrArray(vPatch) );
2651 Acb_PrintPatch( pNtkF, vDivs, vUsed, clk );
2652
2653 // generate output files
2654 if ( pFileName[3] == NULL ) Acb_GenerateFilePatch( vPatch, "patch.v" );
2655 Acb_GenerateFileOut( vInst, pFileName[0], pFileName[3] ? pFileName[3] : "out.v", vPatch );
2656 printf( "Finished dumping resulting file \"%s\".\n\n", pFileName[3] ? pFileName[3] : "out.v" );
2657 //Gia_AigerWrite( pGiaG, "test.aig", 0, 0, 0 );
2658 cleanup:
2659 // cleanup
2660 if ( vGias )
2661 {
2662 Gia_Man_t * pTemp; int i;
2663 Vec_PtrForEachEntry( Gia_Man_t *, vGias, pTemp, i )
2664 Gia_ManStop( pTemp );
2665 Vec_PtrFree( vGias );
2666 }
2667 Vec_StrFreeP( &vPatch );
2668 Vec_StrFreeP( &vInst );
2669
2670 Vec_PtrFreeFree( vSops );
2671 Vec_WecFree( vSupps );
2672 Vec_IntFree( vSuppOld );
2673 Vec_IntFreeP( &vUsed );
2674 if ( vFuncs ) Vec_PtrFreeFree( vFuncs );
2675
2676 Gia_ManStop( pGiaF );
2677 Gia_ManStop( pGiaG );
2678 Gia_ManStop( pGiaM );
2679
2680 Vec_IntFreeP( &vSuppF );
2681 Vec_IntFreeP( &vSuppG );
2682 Vec_IntFreeP( &vSupp );
2683 Vec_IntFreeP( &vNodesF );
2684 Vec_IntFreeP( &vNodesG );
2685 Vec_IntFreeP( &vRoots );
2686 Vec_IntFreeP( &vDivs );
2687 Vec_BitFreeP( &vBlock );
2688 return RetValue;
2689 }
2690
2691 /**Function*************************************************************
2692
2693 Synopsis [Read/write test.]
2694
2695 Description []
2696
2697 SideEffects []
2698
2699 SeeAlso []
2700
2701 ***********************************************************************/
Acb_NtkTestRun2(char * pFileNames[3],int fVerbose)2702 void Acb_NtkTestRun2( char * pFileNames[3], int fVerbose )
2703 {
2704 char * pFileNameOut = Extra_FileNameGenericAppend( pFileNames[0], "_w.v" );
2705 Acb_Ntk_t * pNtk = Acb_VerilogSimpleRead( pFileNames[0], pFileNames[2] );
2706 Acb_VerilogSimpleWrite( pNtk, pFileNameOut );
2707 Acb_ManFree( pNtk->pDesign );
2708 Acb_IntallLibrary();
2709 }
2710
2711
2712 /**Function*************************************************************
2713
2714 Synopsis [Top level procedure.]
2715
2716 Description []
2717
2718 SideEffects []
2719
2720 SeeAlso []
2721
2722 ***********************************************************************/
Acb_NtkRunEco(char * pFileNames[4],int fCheck,int fVerbose)2723 void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose )
2724 {
2725 Acb_Ntk_t * pNtkF = Acb_VerilogSimpleRead( pFileNames[0], pFileNames[2] );
2726 Acb_Ntk_t * pNtkG = Acb_VerilogSimpleRead( pFileNames[1], NULL );
2727 if ( !pNtkF || !pNtkG )
2728 return;
2729 //int * pArray = Vec_IntArray( &pNtkF->vTargets );
2730 //ABC_SWAP( int, pArray[7], pArray[4] );
2731 //Vec_IntReverseOrder( &pNtkF->vTargets );
2732 //Vec_IntPermute( &pNtkF->vTargets );
2733 //Vec_IntPrint( &pNtkF->vTargets );
2734
2735 assert( Acb_NtkCiNum(pNtkF) == Acb_NtkCiNum(pNtkG) );
2736 assert( Acb_NtkCoNum(pNtkF) == Acb_NtkCoNum(pNtkG) );
2737
2738 Acb_IntallLibrary();
2739
2740 if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 0, fCheck, fVerbose ) )
2741 {
2742 printf( "General computation timed out. Trying inputs only.\n\n" );
2743 if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 1, fCheck, fVerbose ) )
2744 printf( "Input-only computation also timed out.\n\n" );
2745 }
2746
2747 Acb_ManFree( pNtkF->pDesign );
2748 Acb_ManFree( pNtkG->pDesign );
2749 }
2750
2751 ////////////////////////////////////////////////////////////////////////
2752 /// END OF FILE ///
2753 ////////////////////////////////////////////////////////////////////////
2754
2755
2756 ABC_NAMESPACE_IMPL_END
2757
2758