ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
acbFunc.c
Go to the documentation of this file.
1
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#include "base/main/main.h"
30#include "base/cmd/cmd.h"
31
32ABC_NAMESPACE_IMPL_START
33
37
38typedef 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_MUX, // 14: "_HMUX"
54 ACB_DC, // 15: "_DC"
55 ACB_UNUSED // 14: unused
56} Acb_KeyWords_t;
57
58static inline char * Acb_Num2Name( int i )
59{
60 if ( i == 1 ) return "module";
61 if ( i == 2 ) return "endmodule";
62 if ( i == 3 ) return "input";
63 if ( i == 4 ) return "output";
64 if ( i == 5 ) return "wire";
65 if ( i == 6 ) return "buf";
66 if ( i == 7 ) return "not";
67 if ( i == 8 ) return "and";
68 if ( i == 9 ) return "nand";
69 if ( i == 10 ) return "or";
70 if ( i == 11 ) return "nor";
71 if ( i == 12 ) return "xor";
72 if ( i == 13 ) return "xnor";
73 if ( i == 14 ) return "_HMUX";
74 if ( i == 15 ) return "_DC";
75 return NULL;
76}
77
78static inline int Acb_Type2Oper( int i )
79{
80 if ( i == 6 ) return ABC_OPER_BIT_BUF;
81 if ( i == 7 ) return ABC_OPER_BIT_INV;
82 if ( i == 8 ) return ABC_OPER_BIT_AND;
83 if ( i == 9 ) return ABC_OPER_BIT_NAND;
84 if ( i == 10 ) return ABC_OPER_BIT_OR;
85 if ( i == 11 ) return ABC_OPER_BIT_NOR;
86 if ( i == 12 ) return ABC_OPER_BIT_XOR;
87 if ( i == 13 ) return ABC_OPER_BIT_NXOR;
88 if ( i == 14 ) return ABC_OPER_BIT_MUX;
89 if ( i == 15 ) return ABC_OPER_TRI;
90 assert( 0 );
91 return -1;
92}
93
94static inline char * Acb_Oper2Name( int i )
95{
96 if ( i == ABC_OPER_CONST_F ) return "const0";
97 if ( i == ABC_OPER_CONST_T ) return "const1";
98 if ( i == ABC_OPER_CONST_X ) return "constX";
99 if ( i == ABC_OPER_BIT_BUF ) return "buf";
100 if ( i == ABC_OPER_BIT_INV ) return "not";
101 if ( i == ABC_OPER_BIT_AND ) return "and";
102 if ( i == ABC_OPER_BIT_NAND ) return "nand";
103 if ( i == ABC_OPER_BIT_OR ) return "or";
104 if ( i == ABC_OPER_BIT_NOR ) return "nor";
105 if ( i == ABC_OPER_BIT_XOR ) return "xor";
106 if ( i == ABC_OPER_BIT_NXOR ) return "xnor";
107 if ( i == ABC_OPER_BIT_MUX ) return "mux";
108 if ( i == ABC_OPER_TRI ) return "_DC";
109 assert( 0 );
110 return NULL;
111}
112
116
128char * pLibStr[25] = {
129 "GATE buf 1 O=a; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
130 "GATE inv 1 O=!a; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
131 "GATE and2 1 O=a*b; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
132 "GATE and3 1 O=a*b*c; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
133 "GATE and4 1 O=a*b*c*d; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
134 "GATE or2 1 O=a+b; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
135 "GATE or3 1 O=a+b+c; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
136 "GATE or4 1 O=a+b+c+d; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
137 "GATE nand2 1 O=!(a*b); PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
138 "GATE nand3 1 O=!(a*b*c); PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
139 "GATE nand4 1 O=!(a*b*c*d); PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
140 "GATE nor2 1 O=!(a+b); PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
141 "GATE nor3 1 O=!(a+b+c); PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
142 "GATE nor4 1 O=!(a+b+c+d); PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
143 "GATE xor 1 O=!a*b+a*!b; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
144 "GATE xnor 1 O=a*b+!a*!b; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
145 "GATE zero 0 O=CONST0;\n"
146 "GATE one 0 O=CONST1;\n"
147};
148char * pLibStr2[25] = {
149 "GATE buf 1 O=a; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
150 "GATE inv 1 O=!a; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
151 "GATE and2 1 O=a*b; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
152 "GATE or2 1 O=a+b; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
153 "GATE nand2 1 O=!(a*b); PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
154 "GATE nor2 1 O=!(a+b); PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
155 "GATE xor 1 O=!a*b+a*!b; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
156 "GATE xnor 1 O=a*b+!a*!b; PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
157 "GATE zero 0 O=CONST0;\n"
158 "GATE one 0 O=CONST1;\n"
159};
160void Acb_IntallLibrary( int f2Ins )
161{
162 extern Mio_Library_t * Mio_LibraryReadBuffer( char * pBuffer, int fExtendedFormat, st__table * tExcludeGate, int nFaninLimit, int fVerbose );
163 Mio_Library_t * pLib;
164 int i;
165 // create library string
166 Vec_Str_t * vLibStr = Vec_StrAlloc( 1000 );
167 char ** ppLibStr = f2Ins ? pLibStr2 : pLibStr;
168 for ( i = 0; ppLibStr[i]; i++ )
169 Vec_StrAppend( vLibStr, ppLibStr[i] );
170 Vec_StrPush( vLibStr, '\0' );
171 // create library
172 pLib = Mio_LibraryReadBuffer( Vec_StrArray(vLibStr), 0, NULL, 0, 0 );
173 Mio_LibrarySetName( pLib, Abc_UtilStrsav("iccad17.genlib") );
174 Mio_UpdateGenlib( pLib );
175 Vec_StrFree( vLibStr );
176}
177
189Abc_Nam_t * Acb_VerilogStartNames()
190{
191 Abc_Nam_t * pNames = Abc_NamStart( 100, 16 );
192 int i, NameId, fFound;
193 for ( i = 1; i < ACB_UNUSED; i++ )
194 {
195 NameId = Abc_NamStrFindOrAdd( pNames, Acb_Num2Name(i), &fFound );
196 assert( i == NameId && !fFound );
197 }
198 return pNames;
199}
200void Acb_VerilogRemoveComments ( char * pBuffer )
201{
202 char * pTemp;
203 for ( pTemp = pBuffer; *pTemp; pTemp++ )
204 if ( pTemp[0] == '/' && pTemp[1] == '/' )
205 while ( *pTemp && *pTemp != '\n' )
206 *pTemp++ = ' ';
207}
208Vec_Int_t * Acb_VerilogSimpleLex( char * pFileName, Abc_Nam_t * pNames )
209{
210 Vec_Int_t * vBuffer = Vec_IntAlloc( 1000 );
211 char * pBuffer = Extra_FileReadContents( pFileName );
212 char * pToken, * pStart, * pLimit = pBuffer + strlen(pBuffer);
213 int i, iToken, RLeft = -1, RRight = -1;
214 if ( pBuffer == NULL )
215 return NULL;
216 Acb_VerilogRemoveComments( pBuffer );
217 pToken = strtok( pBuffer, " \n\r\t(),;=" );
218 while ( pToken )
219 {
220 if ( 0 )
221 {
222 if ( !strcmp(pToken, "assign") )
223 {
224 int fBuffer = 0;
225 int nToks = 0, pToks[4];
226 while ( 1 )
227 {
228 pToken = strtok( NULL, " \n\r\t(),=~&" );
229 if ( pToken[0] == ';' )
230 break;
231 if ( pToken[strlen(pToken)-1] == ';' )
232 {
233 pToken[strlen(pToken)-1] = 0;
234 assert( nToks < 3 );
235 pToks[nToks++] = Abc_NamStrFindOrAdd( pNames, pToken, NULL );
236 fBuffer = 1;
237 break;
238 }
239 else
240 {
241 assert( nToks < 3 );
242 pToks[nToks++] = Abc_NamStrFindOrAdd( pNames, pToken, NULL );
243 }
244 }
245 assert( nToks == 2 || nToks == 3 );
246 Vec_IntPush( vBuffer, fBuffer ? ACB_AND : ACB_NAND );
247 Vec_IntPush( vBuffer, pToks[0] );
248 Vec_IntPush( vBuffer, pToks[1] );
249 Vec_IntPush( vBuffer, nToks == 3 ? pToks[2] : pToks[1] );
250 pToken = strtok( NULL, " \n\r\t(),;=" );
251 continue;
252 }
253 }
254
255 if ( pToken[0] == '[' )
256 {
257 assert( RLeft == -1 );
258 RLeft = atoi(pToken+1);
259 RRight = atoi(strstr(pToken,":")+1);
260 pToken = strtok( NULL, " \n\r\t(),;=" );
261 continue;
262 }
263 if ( pToken[0] == '\\' )
264 pToken++;
265 if ( !strcmp(pToken, "assign") )
266 iToken = ACB_BUF;
267 else
268 iToken = Abc_NamStrFindOrAdd( pNames, pToken, NULL );
269 if ( iToken < ACB_UNUSED )
270 RLeft = RRight = -1;
271 else if ( RLeft != -1 )
272 {
273 char Buffer[1000];
274 assert( strlen(pToken) < 990 );
275 for ( i = RRight; i <= RLeft; i++ )
276 {
277 sprintf( Buffer, "%s[%d]", pToken, i );
278 iToken = Abc_NamStrFindOrAdd( pNames, Buffer, NULL );
279 Vec_IntPush( vBuffer, iToken );
280 }
281 pToken = strtok( NULL, " \n\r\t(),;=" );
282 continue;
283 }
284 Vec_IntPush( vBuffer, iToken );
285 if ( iToken >= ACB_BUF && iToken < ACB_UNUSED )
286 {
287 for ( pStart = pToken; pStart < pLimit && *pStart != '\n'; pStart++ )
288 if ( *pStart == '(' )
289 break;
290 if ( *pStart == '(' )
291 {
292 pToken = strtok( pStart, " \n\r\t(),;=" );
293 continue;
294 }
295 }
296 pToken = strtok( NULL, " \n\r\t(),;=" );
297 }
298 ABC_FREE( pBuffer );
299 return vBuffer;
300}
301int Acb_WireIsTarget( int Token, Abc_Nam_t * pNames )
302{
303 char * pStr = Abc_NamStr(pNames, Token);
304 return pStr[0] == 't' && pStr[1] == '_';
305}
306void * Acb_VerilogSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames )
307{
308 Ndr_Data_t * pDesign = NULL;
309 Vec_Int_t * vInputs = Vec_IntAlloc(100);
310 Vec_Int_t * vOutputs = Vec_IntAlloc(100);
311 Vec_Int_t * vWires = Vec_IntAlloc(100);
312 Vec_Int_t * vTypes = Vec_IntAlloc(100);
313 Vec_Int_t * vFanins = Vec_IntAlloc(100);
314 Vec_Int_t * vCur = NULL;
315 int i, ModuleID, Token, Size, Count = 0;
316 assert( Vec_IntEntry(vBuffer, 0) == ACB_MODULE );
317 Vec_IntForEachEntryStart( vBuffer, Token, i, 2 )
318 {
319 if ( vCur == NULL && Token >= ACB_UNUSED )
320 continue;
321 if ( Token == ACB_ENDMODULE )
322 break;
323 if ( Token == ACB_INPUT )
324 vCur = vInputs;
325 else if ( Token == ACB_OUTPUT )
326 vCur = vOutputs;
327 else if ( Token == ACB_WIRE )
328 vCur = vWires;
329 else if ( Token >= ACB_BUF && Token < ACB_UNUSED )
330 {
331 Vec_IntPush( vTypes, Token );
332 Vec_IntPush( vTypes, Vec_IntSize(vFanins) );
333 vCur = vFanins;
334 }
335 else
336 Vec_IntPush( vCur, Token );
337 }
338 Vec_IntPush( vTypes, -1 );
339 Vec_IntPush( vTypes, Vec_IntSize(vFanins) );
340 // create design
341 pDesign = (Ndr_Data_t *)Ndr_Create( Vec_IntEntry(vBuffer, 1) );
342 ModuleID = Ndr_AddModule( pDesign, Vec_IntEntry(vBuffer, 1) );
343 // create inputs
344 Ndr_DataResize( pDesign, Vec_IntSize(vInputs) );
345 Vec_IntForEachEntry( vInputs, Token, i )
346 Ndr_DataPush( pDesign, NDR_INPUT, Token );
347 Ndr_DataAddTo( pDesign, ModuleID-256, Vec_IntSize(vInputs) );
348 Ndr_DataAddTo( pDesign, 0, Vec_IntSize(vInputs) );
349 // create outputs
350 Ndr_DataResize( pDesign, Vec_IntSize(vOutputs) );
351 Vec_IntForEachEntry( vOutputs, Token, i )
352 Ndr_DataPush( pDesign, NDR_OUTPUT, Token );
353 Ndr_DataAddTo( pDesign, ModuleID-256, Vec_IntSize(vOutputs) );
354 Ndr_DataAddTo( pDesign, 0, Vec_IntSize(vOutputs) );
355 // create targets
356 Ndr_DataResize( pDesign, Vec_IntSize(vWires) );
357 Vec_IntForEachEntry( vWires, Token, i )
358 if ( Acb_WireIsTarget(Token, pNames) )
359 Ndr_DataPush( pDesign, NDR_TARGET, Token ), Count++;
360 Ndr_DataAddTo( pDesign, ModuleID-256, Count );
361 Ndr_DataAddTo( pDesign, 0, Count );
362 // create nodes
363 Vec_IntForEachEntry( vInputs, Token, i )
364 Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CI, 0, 0, 0, 0, 0, NULL, 1, &Token, NULL ); // no fanins
365 if ( (Token = Abc_NamStrFind(pNames, "1\'b0")) )
366 Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CONST_F, 0, 0, 0, 0, 0, NULL, 1, &Token, NULL ); // no fanins
367 if ( (Token = Abc_NamStrFind(pNames, "1\'b1")) )
368 Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CONST_T, 0, 0, 0, 0, 0, NULL, 1, &Token, NULL ); // no fanins
369 if ( (Token = Abc_NamStrFind(pNames, "1\'bx")) )
370 Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CONST_X, 0, 0, 0, 0, 0, NULL, 1, &Token, NULL ); // no fanins
371 Vec_IntForEachEntryDouble( vTypes, Token, Size, i )
372 if ( Token > 0 )
373 {
374 int Output = Vec_IntEntry(vFanins, Size);
375 int nFanins = Vec_IntEntry(vTypes, i+3) - Size - 1;
376 int * pFanins = Vec_IntEntryP(vFanins, Size+1);
377 Ndr_AddObject( pDesign, ModuleID, Acb_Type2Oper(Token), 0, 0, 0, 0, nFanins, pFanins, 1, &Output, NULL ); // many fanins
378 }
379 Vec_IntForEachEntry( vOutputs, Token, i )
380 Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CO, 0, 0, 0, 0, 1, &Token, 1, &Token, NULL ); // one fanin
381 // cleanup
382 Vec_IntFree( vInputs );
383 Vec_IntFree( vOutputs );
384 Vec_IntFree( vWires );
385 Vec_IntFree( vTypes );
386 Vec_IntFree( vFanins );
387 return pDesign;
388}
389
401int Gia_FileSimpleParse_rec( Gia_Man_t * pNew, int Token, Vec_Int_t * vMapType, Vec_Int_t * vTypes, Vec_Int_t * vFanins, Vec_Int_t * vMap )
402{
403 int nFanins, * pFanins, pLits[16];
404 int i, Type, Size, Place = Vec_IntEntry( vMapType, Token );
405 int iLit = Vec_IntEntry( vMap, Token );
406 if ( iLit >= 0 )
407 return iLit;
408 Place = Vec_IntEntry( vMapType, Token );
409 assert( Place >= 0 );
410 Type = Vec_IntEntry( vTypes, Place );
411 Size = Vec_IntEntry( vTypes, Place+1 );
412 nFanins = Vec_IntEntry(vTypes, Place+3) - Size - 1;
413 pFanins = Vec_IntEntryP(vFanins, Size+1);
414 assert( nFanins > 0 && nFanins < 16 );
415 for ( i = 0; i < nFanins; i++ )
416 Gia_FileSimpleParse_rec( pNew, pFanins[i], vMapType, vTypes, vFanins, vMap );
417 for ( i = 0; i < nFanins; i++ )
418 pLits[i] = Vec_IntEntry( vMap, pFanins[i] );
419 if ( nFanins == 1 )
420 {
421 assert( Type == ACB_BUF || Type == ACB_NOT );
422 iLit = Abc_LitNotCond( pLits[0], Type == ACB_NOT );
423 iLit = Gia_ManAppendAnd2( pNew, iLit, iLit );
424 }
425 else
426 {
427 iLit = pLits[0];
428 if ( Type == ACB_AND || Type == ACB_NAND )
429 for ( i = 1; i < nFanins; i++ )
430 iLit = Gia_ManAppendAnd2( pNew, iLit, pLits[i] );
431 else if ( Type == ACB_OR || Type == ACB_NOR )
432 for ( i = 1; i < nFanins; i++ )
433 iLit = Gia_ManAppendOr2( pNew, iLit, pLits[i] );
434 else if ( Type == ACB_XOR || Type == ACB_XNOR )
435 for ( i = 1; i < nFanins; i++ )
436 iLit = Gia_ManAppendXor2( pNew, iLit, pLits[i] );
437 else assert( 0 );
438 iLit = Abc_LitNotCond( iLit, (Type == ACB_NAND || Type == ACB_NOR || Type == ACB_XNOR) );
439 }
440 Vec_IntWriteEntry( vMap, Token, iLit );
441 return iLit;
442}
443Gia_Man_t * Gia_FileSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames, int fNames, char * pFileW )
444{
445 Gia_Man_t * pNew = NULL;
446 Vec_Int_t * vInputs = Vec_IntAlloc(100);
447 Vec_Int_t * vOutputs = Vec_IntAlloc(100);
448 Vec_Int_t * vWires = Vec_IntAlloc(100);
449 Vec_Int_t * vTypes = Vec_IntAlloc(100);
450 Vec_Int_t * vFanins = Vec_IntAlloc(100);
451 Vec_Int_t * vCur = NULL;
452 Vec_Int_t * vMap = Vec_IntStartFull( Abc_NamObjNumMax(pNames) );
453 Vec_Int_t * vMapType = Vec_IntStartFull( Abc_NamObjNumMax(pNames) );
454 int i, iLit, Token, Size;
455 char Buffer[1000];
456 assert( Vec_IntEntry(vBuffer, 0) == ACB_MODULE );
457 Vec_IntForEachEntryStart( vBuffer, Token, i, 2 )
458 {
459 if ( vCur == NULL && Token >= ACB_UNUSED )
460 continue;
461 if ( Token == ACB_ENDMODULE )
462 break;
463 if ( Token == ACB_INPUT )
464 vCur = vInputs;
465 else if ( Token == ACB_OUTPUT )
466 vCur = vOutputs;
467 else if ( Token == ACB_WIRE )
468 vCur = vWires;
469 else if ( Token >= ACB_BUF && Token < ACB_UNUSED )
470 {
471 Vec_IntPush( vTypes, Token );
472 Vec_IntPush( vTypes, Vec_IntSize(vFanins) );
473 vCur = vFanins;
474 }
475 else if ( pFileW && vCur == vWires && Abc_NamStr(pNames, Token)[0] == 't' )
476 Vec_IntPush( vInputs, Token );
477 else
478 Vec_IntPush( vCur, Token );
479 }
480 Vec_IntPush( vTypes, -1 );
481 Vec_IntPush( vTypes, Vec_IntSize(vFanins) );
482 // map types
483 Vec_IntForEachEntryDouble( vTypes, Token, Size, i )
484 if ( Token > 0 )
485 Vec_IntWriteEntry( vMapType, Vec_IntEntry(vFanins, Size), i );
486 // create design
487 pNew = Gia_ManStart( 10000 );
488 pNew->pName = Abc_UtilStrsav( Abc_NamStr(pNames, Vec_IntEntry(vBuffer, 1)) );
489 pNew->fGiaSimple = 1;
490 if ( (Token = Abc_NamStrFind(pNames, "1\'b0")) )
491 Vec_IntWriteEntry( vMap, Token, 0 );
492 if ( (Token = Abc_NamStrFind(pNames, "1\'b1")) )
493 Vec_IntWriteEntry( vMap, Token, 1 );
494 if ( (Token = Abc_NamStrFind(pNames, "1\'bx")) )
495 Vec_IntWriteEntry( vMap, Token, 0 );
496 if ( (Token = Abc_NamStrFind(pNames, "1\'bz")) )
497 Vec_IntWriteEntry( vMap, Token, 0 );
498 Vec_IntForEachEntry( vInputs, Token, i )
499 Gia_ManAppendCi(pNew);
500 Vec_IntForEachEntry( vInputs, Token, i )
501 Vec_IntWriteEntry( vMap, Token, Gia_ManAppendAnd2(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, i)) );
502 Vec_IntForEachEntry( vOutputs, Token, i )
503 Gia_FileSimpleParse_rec( pNew, Token, vMapType, vTypes, vFanins, vMap );
504 Vec_IntForEachEntry( vOutputs, Token, i )
505 Gia_ManAppendCo( pNew, Vec_IntEntry(vMap, Token) );
506 // create names
507 if ( fNames )
508 {
509 pNew->vPolars = Vec_BitStart( Gia_ManObjNum(pNew) );
510 pNew->vNamesNode = Vec_PtrStart( Gia_ManObjNum(pNew) );
511 Vec_IntForEachEntry( vMap, iLit, Token )
512 {
513 if ( iLit == -1 || !Gia_ObjIsAnd(Gia_ManObj(pNew, Abc_Lit2Var(iLit))) )
514 continue;
515 sprintf( Buffer, "%c_%s", Abc_LitIsCompl(iLit) ? 'c' : 'd', Abc_NamStr(pNames, Token) );
516 assert( Vec_PtrEntry(pNew->vNamesNode, Abc_Lit2Var(iLit)) == NULL );
517 Vec_PtrWriteEntry( pNew->vNamesNode, Abc_Lit2Var(iLit), Abc_UtilStrsav(Buffer) );
518 Vec_BitWriteEntry( pNew->vPolars, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit) );
519 }
520 }
521 else
522 {
523 Gia_Man_t * pTemp;
524 pNew = Gia_ManDupDfsRehash( pTemp = pNew );
525 Gia_ManStop( pTemp );
526 }
527 pNew->vNamesIn = Vec_PtrAlloc( Vec_IntSize(vInputs) );
528 Vec_IntForEachEntry( vInputs, Token, i )
529 Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Abc_NamStr(pNames, Token)) );
530 pNew->vNamesOut = Vec_PtrAlloc( Vec_IntSize(vOutputs) );
531 Vec_IntForEachEntry( vOutputs, Token, i )
532 Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Abc_NamStr(pNames, Token)) );
533 if ( pFileW && fNames )
534 {
535 extern Vec_Int_t * Acb_ReadWeightMap( char * pFileName, Abc_Nam_t * pNames );
536 Vec_Int_t * vT2W = Acb_ReadWeightMap( pFileW, pNames );
537 assert( pNew->vWeights == NULL );
538 pNew->vWeights = Vec_IntStartFull( Gia_ManObjNum(pNew) );
539 Vec_IntForEachEntry( vMap, iLit, Token )
540 if ( iLit != -1 && Vec_IntEntry(vT2W, Token) != -1 )
541 Vec_IntWriteEntry( pNew->vWeights, Abc_Lit2Var(iLit), Vec_IntEntry(vT2W, Token) );
542 Vec_IntFree( vT2W );
543 }
544 // cleanup
545 Vec_IntFree( vInputs );
546 Vec_IntFree( vOutputs );
547 Vec_IntFree( vWires );
548 Vec_IntFree( vTypes );
549 Vec_IntFree( vFanins );
550 Vec_IntFree( vMap );
551 Vec_IntFree( vMapType );
552 return pNew;
553}
554Gia_Man_t * Gia_FileSimpleRead( char * pFileName, int fNames, char * pFileW )
555{
556 Abc_Nam_t * pNames = Acb_VerilogStartNames();
557 Vec_Int_t * vBuffer = Acb_VerilogSimpleLex( pFileName, pNames );
558 Gia_Man_t * pNew = vBuffer ? Gia_FileSimpleParse( vBuffer, pNames, fNames, pFileW ) : NULL;
559 assert( pNew->pSpec == NULL );
560 pNew->pSpec = Abc_UtilStrsav( pFileName );
561 Abc_NamDeref( pNames );
562 Vec_IntFree( vBuffer );
563 return pNew;
564}
565
577Vec_Int_t * Acb_ReadWeightMap( char * pFileName, Abc_Nam_t * pNames )
578{
579 Vec_Int_t * vWeights = Vec_IntStartFull( Abc_NamObjNumMax(pNames) );
580 char * pBuffer = Extra_FileReadContents( pFileName );
581 char * pToken, * pNum;
582 if ( pBuffer == NULL )
583 return NULL;
584 pToken = strtok( pBuffer, " \n\r()," );
585 pNum = strtok( NULL, " \n\r()," );
586 while ( pToken )
587 {
588 int NameId = Abc_NamStrFind(pNames, pToken);
589 int Number = atoi(pNum);
590 if ( NameId <= 0 )
591 {
592 printf( "Cannot find name \"%s\" among node names of this network.\n", pToken );
593 continue;
594 }
595 Vec_IntWriteEntry( vWeights, NameId, Number );
596 pToken = strtok( NULL, " \n\r(),;" );
597 pNum = strtok( NULL, " \n\r(),;" );
598 }
599 ABC_FREE( pBuffer );
600 return vWeights;
601}
602
614char ** Acb_PrepareNames( Abc_Nam_t * p )
615{
616 char ** ppRes = ABC_CALLOC( char *, Abc_NamObjNumMax(p) );
617 int i;
618 for ( i = 0; i < Abc_NamObjNumMax(p); i++ )
619 ppRes[i] = Abc_NamStr( p, i );
620 return ppRes;
621}
622Acb_Ntk_t * Acb_VerilogSimpleRead( char * pFileName, char * pFileNameW )
623{
624 extern Acb_Ntk_t * Acb_NtkFromNdr( char * pFileName, void * pModule, Abc_Nam_t * pNames, Vec_Int_t * vWeights, int nNameIdMax );
625 Acb_Ntk_t * pNtk;
626 Abc_Nam_t * pNames = Acb_VerilogStartNames();
627 Vec_Int_t * vBuffer = Acb_VerilogSimpleLex( pFileName, pNames );
628 void * pModule = vBuffer ? Acb_VerilogSimpleParse( vBuffer, pNames ) : NULL;
629 Vec_Int_t * vWeights = pFileNameW ? Acb_ReadWeightMap( pFileNameW, pNames ) : NULL;
630 if ( pFileName && pModule == NULL )
631 {
632 printf( "Cannot read input file \"%s\".\n", pFileName );
633 return NULL;
634 }
635 if ( pFileNameW && vWeights == NULL )
636 {
637 printf( "Cannot read weight file \"%s\".\n", pFileNameW );
638 return NULL;
639 }
640 if ( 0 )
641 {
642 char ** ppNames = Acb_PrepareNames(pNames);
643 Ndr_WriteVerilog( Extra_FileNameGenericAppend(pFileName, "_ndr.v"), pModule, ppNames, 1 );
644 ABC_FREE( ppNames );
645 }
646 pNtk = Acb_NtkFromNdr( pFileName, pModule, pNames, vWeights, Abc_NamObjNumMax(pNames) );
647 Ndr_Delete( pModule );
648 Vec_IntFree( vBuffer );
649 Vec_IntFreeP( &vWeights );
650 Abc_NamDeref( pNames );
651 return pNtk;
652}
653void Acb_VerilogSimpleReadTest( char * pFileName )
654{
655 Acb_Ntk_t * p = Acb_VerilogSimpleRead( pFileName, NULL );
656 Acb_NtkFree( p );
657}
658
670void Acb_VerilogSimpleWrite( Acb_Ntk_t * p, char * pFileName )
671{
672 int i, iObj, fFirst = 1;
673 FILE * pFile = fopen( pFileName, "wb" );
674 if ( pFile == NULL ) { printf( "Cannot open file \"%s\" for writing.\n", pFileName ); return; }
675
676 fprintf( pFile, "\nmodule %s (\n ", Acb_NtkName(p) );
677
678 Acb_NtkForEachPi( p, iObj, i )
679 fprintf( pFile, "%s, ", Acb_ObjNameStr(p, iObj) );
680 fprintf( pFile, "\n " );
681
682 Acb_NtkForEachPo( p, iObj, i )
683 fprintf( pFile, "%s%s", fFirst ? "":", ", Acb_ObjNameStr(p, iObj) ), fFirst = 0;
684 fprintf( pFile, "\n);\n\n" );
685
686 Acb_NtkForEachPi( p, iObj, i )
687 fprintf( pFile, " input %s;\n", Acb_ObjNameStr(p, iObj) );
688 fprintf( pFile, "\n" );
689
690 Acb_NtkForEachPo( p, iObj, i )
691 fprintf( pFile, " output %s;\n", Acb_ObjNameStr(p, iObj) );
692 fprintf( pFile, "\n" );
693
694 Acb_NtkForEachNode( p, iObj )
695 if ( Acb_ObjFaninNum(p, iObj) > 0 )
696 fprintf( pFile, " wire %s;\n", Acb_ObjNameStr(p, iObj) );
697 fprintf( pFile, "\n" );
698
699 Acb_NtkForEachNode( p, iObj )
700 if ( Acb_ObjFaninNum(p, iObj) > 0 )
701 {
702 int * pFanin, iFanin, k, start = ftell(pFile)+55;
703 fprintf( pFile, " %s (", Acb_Oper2Name( Acb_ObjType(p, iObj) ) );
704 fprintf( pFile, " %s", Acb_ObjNameStr(p, iObj) );
705 Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, k )
706 //if ( iFanin == 0 ) fprintf( pFile, ", <zero>" ); else
707 fprintf( pFile, ", %s", Acb_ObjNameStr(p, iFanin) );
708 fprintf( pFile, " );" );
709 if ( Acb_NtkHasObjWeights(p) && Acb_ObjWeight(p, iObj) > 0 )
710 fprintf( pFile, " %*s // weight = %d", (int)(start-ftell(pFile)), "", Acb_ObjWeight(p, iObj) );
711 fprintf( pFile, "\n" );
712 }
713 else // constant nodes
714 {
715 assert( Acb_ObjType(p, iObj) == ABC_OPER_CONST_F || Acb_ObjType(p, iObj) == ABC_OPER_CONST_T );
716 fprintf( pFile, " %s (", Acb_Oper2Name( ABC_OPER_BIT_BUF ) );
717 if ( Acb_ObjType(p, iObj) == ABC_OPER_CONST_X )
718 fprintf( pFile, " 1\'bx" );
719 else
720 fprintf( pFile, " 1\'b%d", Acb_ObjType(p, iObj) == ABC_OPER_CONST_T );
721 fprintf( pFile, " );\n" );
722 }
723
724 fprintf( pFile, "\nendmodule\n\n" );
725 fclose( pFile );
726}
727
728
729
730
731
732
733
745int Acb_NtkFindRoots_rec( Acb_Ntk_t * p, int iObj, Vec_Bit_t * vBlock )
746{
747 int * pFanin, iFanin, i, Res = 0;
748 if ( Acb_ObjIsTravIdPrev(p, iObj) )
749 return 1;
750 if ( Acb_ObjSetTravIdCur(p, iObj) )
751 return 0;
752 assert( !Acb_ObjIsCi(p, iObj) );
753 Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, i )
754 Res |= Acb_NtkFindRoots_rec( p, iFanin, vBlock );
755 if ( Res ) Acb_ObjSetTravIdPrev( p, iObj );
756 if ( Res ) Vec_BitWriteEntry( vBlock, iObj, 1 );
757 return Res;
758}
759Vec_Int_t * Acb_NtkFindRoots( Acb_Ntk_t * p, Vec_Int_t * vTargets, Vec_Bit_t ** pvBlock )
760{
761 int i, iObj;
762 Vec_Int_t * vRoots = Vec_IntAlloc( 1000 );
763 Vec_Bit_t * vBlock = Vec_BitStart( Acb_NtkObjNum(p) );
764 *pvBlock = vBlock;
765 // mark targets
766 Acb_NtkIncTravId( p );
767 assert( Vec_IntSize(vTargets) > 0 );
768 Vec_IntForEachEntry( vTargets, iObj, i )
769 {
770 Acb_ObjSetTravIdCur( p, iObj );
771 Vec_BitWriteEntry( vBlock, iObj, 1 );
772 }
773 // mark inputs
774 Acb_NtkIncTravId( p );
775 Acb_NtkForEachCi( p, iObj, i )
776 Acb_ObjSetTravIdCur( p, iObj );
777 // visit internal nodes
778 Acb_NtkForEachNode( p, iObj )
779 Acb_NtkFindRoots_rec(p, iObj, vBlock);
780 // collect outputs reachable from targets
781 Acb_NtkForEachCoDriver( p, iObj, i )
782 if ( Acb_NtkFindRoots_rec(p, iObj, vBlock) )
783 Vec_IntPush( vRoots, i );
784 //Vec_IntPrint( vRoots );
785 return vRoots;
786}
787
799void Acb_NtkFindSupp_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vSupp )
800{
801 int * pFanin, iFanin, i;
802 if ( Acb_ObjSetTravIdCur(p, iObj) )
803 return;
804 if ( Acb_ObjIsCi(p, iObj) )
805 Vec_IntPush( vSupp, Acb_ObjCioId(p, iObj) );
806 else
807 Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, i )
808 Acb_NtkFindSupp_rec( p, iFanin, vSupp );
809}
810Vec_Int_t * Acb_NtkFindSupp( Acb_Ntk_t * p, Vec_Int_t * vRoots )
811{
812 int i, iObj;
813 Vec_Int_t * vSupp = Vec_IntAlloc( 1000 );
814 Acb_NtkIncTravId( p );
815 Acb_NtkForEachCoDriverVec( vRoots, p, iObj, i )
816 Acb_NtkFindSupp_rec( p, iObj, vSupp );
817 Vec_IntSort( vSupp, 0 );
818 //Vec_IntPrint( vSupp );
819 return vSupp;
820}
821
833int Acb_NtkFindDivs_rec( Acb_Ntk_t * p, int iObj )
834{
835 int * pFanin, iFanin, i, Res = 1;
836 if ( Acb_ObjIsTravIdPrev(p, iObj) )
837 return 1;
838 if ( Acb_ObjSetTravIdCur(p, iObj) )
839 return 0;
840 if ( Acb_ObjIsCi(p, iObj) )
841 return 0;
842 Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, i )
843 Res &= Acb_NtkFindDivs_rec( p, iFanin );
844 if ( Res ) Acb_ObjSetTravIdPrev( p, iObj );
845 return Res;
846}
847Vec_Int_t * Acb_NtkFindDivsCis( Acb_Ntk_t * p, Vec_Int_t * vSupp )
848{
849 int i, iObj;
850 Vec_Int_t * vDivs = Vec_IntAlloc( Vec_IntSize(vSupp) );
851 Acb_NtkForEachCiVec( vSupp, p, iObj, i )
852 {
853 assert( Acb_ObjWeight(p, iObj) > 0 );
854 Vec_IntPush( vDivs, iObj );
855 }
856 printf( "Divisors are %d support variables (CIs in the TFO of the targets).\n", Vec_IntSize(vSupp) );
857 return vDivs;
858}
859Vec_Int_t * Acb_NtkFindDivs( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Bit_t * vBlock, int fUnitW, int fVerbose )
860{
861 int fPrintWeights = 0;
862 int nDivLimit = 5000;
863 int i, iObj;
864 Vec_Int_t * vDivs = Vec_IntAlloc( 1000 );
865 if ( fUnitW )
866 {
867 Acb_NtkForEachNode( p, iObj )
868 if ( Acb_ObjWeight(p, iObj) > 0 )
869 Vec_IntWriteEntry( &p->vObjWeight, iObj, 1 );
870 }
871 // mark inputs
872 Acb_NtkIncTravId( p );
873 Acb_NtkForEachCiVec( vSupp, p, iObj, i )
874 {
875 Acb_ObjSetTravIdCur( p, iObj );
876 if ( Acb_ObjWeight(p, iObj) > 0 )
877 Vec_IntPush( vDivs, iObj );
878 }
879 // collect nodes whose support is contained in vSupp
880 Acb_NtkIncTravId( p );
881 Acb_NtkForEachNode( p, iObj )
882 if ( !Vec_BitEntry(vBlock, iObj) && Acb_ObjWeight(p, iObj) > 0 && Acb_NtkFindDivs_rec(p, iObj) )
883 Vec_IntPush( vDivs, iObj );
884 // sort divisors by cost (first cheap ones; later expensive ones)
885 Vec_IntSelectSortCost( Vec_IntArray(vDivs), Vec_IntSize(vDivs), &p->vObjWeight );
886 //Vec_IntPrint( vDivs );
887 nDivLimit = Abc_MinInt( Vec_IntSize(vDivs), nDivLimit );
888 if ( fPrintWeights )
889 {
890// Vec_IntForEachEntryStop( vDivs, iObj, i, nDivLimit )
891// printf( "%d:%d (w=%d) ", i, iObj, Vec_IntEntry(&p->vObjWeight, iObj) );
892// printf( "\n" );
893
894 printf( " : " );
895 Vec_IntForEachEntryStop( vDivs, iObj, i, nDivLimit )
896 printf( "%d", (Vec_IntEntry(&p->vObjWeight, iObj) / 100) % 10 );
897 printf( "\n" );
898 printf( " : " );
899 Vec_IntForEachEntryStop( vDivs, iObj, i, nDivLimit )
900 printf( "%d", (Vec_IntEntry(&p->vObjWeight, iObj) / 10) % 10 );
901 printf( "\n" );
902 printf( " : " );
903 Vec_IntForEachEntryStop( vDivs, iObj, i, nDivLimit )
904 printf( "%d", (Vec_IntEntry(&p->vObjWeight, iObj) / 1) % 10 );
905 printf( "\n" );
906 }
907 if ( fVerbose )
908 printf( "Reducing divisor set from %d to ", Vec_IntSize(vDivs) );
909 Vec_IntShrink( vDivs, nDivLimit );
910 if ( fVerbose )
911 printf( "%d.\n", Vec_IntSize(vDivs) );
912 return vDivs;
913}
914
926void Acb_NtkFindNodes_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vNodes )
927{
928 int * pFanin, iFanin, i;
929 if ( Acb_ObjSetTravIdCur(p, iObj) )
930 return;
931 if ( Acb_ObjIsCi(p, iObj) )
932 return;
933 Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, i )
934 Acb_NtkFindNodes_rec( p, iFanin, vNodes );
935 assert( !Acb_ObjIsCo(p, iObj) );
936 Vec_IntPush( vNodes, iObj );
937}
938Vec_Int_t * Acb_NtkFindNodes( Acb_Ntk_t * p, Vec_Int_t * vRoots, Vec_Int_t * vDivs )
939{
940 int i, iObj;
941 Vec_Int_t * vNodes = Vec_IntAlloc( 1000 );
942 Acb_NtkIncTravId( p );
943 Acb_NtkForEachCoDriverVec( vRoots, p, iObj, i )
944 Acb_NtkFindNodes_rec( p, iObj, vNodes );
945 if ( vDivs )
946 Vec_IntForEachEntry( vDivs, iObj, i )
947 Acb_NtkFindNodes_rec( p, iObj, vNodes );
948 return vNodes;
949}
950
962int Acb_ObjToGia( Gia_Man_t * pNew, Acb_Ntk_t * p, int iObj, Vec_Int_t * vTemp )
963{
964 //char * pName = Abc_NamStr( p->pDesign->pStrs, Acb_ObjName(p, iObj) );
965 int * pFanin, iFanin, k, Type, Res;
966 assert( !Acb_ObjIsCio(p, iObj) );
967 Vec_IntClear( vTemp );
968 Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, k )
969 {
970 assert( Acb_ObjCopy(p, iFanin) >= 0 );
971 Vec_IntPush( vTemp, Acb_ObjCopy(p, iFanin) );
972 }
973 Type = Acb_ObjType( p, iObj );
974 if ( Type == ABC_OPER_CONST_F )
975 return 0;
976 if ( Type == ABC_OPER_CONST_T )
977 return 1;
978 if ( Type == ABC_OPER_BIT_BUF )
979 return Vec_IntEntry(vTemp, 0);
980 if ( Type == ABC_OPER_BIT_INV )
981 return Abc_LitNot( Vec_IntEntry(vTemp, 0) );
982 if ( Type == ABC_OPER_BIT_AND || Type == ABC_OPER_BIT_NAND )
983 {
984 Res = 1;
985 Vec_IntForEachEntry( vTemp, iFanin, k )
986 Res = Gia_ManHashAnd( pNew, Res, iFanin );
987 return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NAND );
988 }
989 if ( Type == ABC_OPER_BIT_OR || Type == ABC_OPER_BIT_NOR )
990 {
991 Res = 0;
992 Vec_IntForEachEntry( vTemp, iFanin, k )
993 Res = Gia_ManHashOr( pNew, Res, iFanin );
994 return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NOR );
995 }
996 if ( Type == ABC_OPER_BIT_XOR || Type == ABC_OPER_BIT_NXOR )
997 {
998 Res = 0;
999 Vec_IntForEachEntry( vTemp, iFanin, k )
1000 Res = Gia_ManHashXor( pNew, Res, iFanin );
1001 return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NXOR );
1002 }
1003 assert( 0 );
1004 return -1;
1005}
1006Gia_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 )
1007{
1008 Gia_Man_t * pNew, * pOne;
1009 Vec_Int_t * vFanins;
1010 int i, iObj;
1011 pNew = Gia_ManStart( 2 * Acb_NtkObjNum(p) + 1000 );
1012 pNew->pName = Abc_UtilStrsav(Acb_NtkName(p));
1013 Gia_ManHashAlloc( pNew );
1014 Acb_NtkCleanObjCopies( p );
1015 // create primary inputs
1016 Acb_NtkForEachCiVec( vSupp, p, iObj, i )
1017 Acb_ObjSetCopy( p, iObj, Gia_ManAppendCi(pNew) );
1018 // add targets as primary inputs
1019 if ( vTargets )
1020 Vec_IntForEachEntry( vTargets, iObj, i )
1021 Acb_ObjSetCopy( p, iObj, Gia_ManAppendCi(pNew) );
1022 // bit-blast internal nodes
1023 vFanins = Vec_IntAlloc( 4 );
1024 Vec_IntForEachEntry( vNodes, iObj, i )
1025 if ( Acb_ObjCopy(p, iObj) == -1 ) // skip targets assigned above
1026 Acb_ObjSetCopy( p, iObj, Acb_ObjToGia(pNew, p, iObj, vFanins) );
1027 Vec_IntFree( vFanins );
1028 // create primary outputs
1029 Acb_NtkForEachCoDriverVec( vRoots, p, iObj, i )
1030 Gia_ManAppendCo( pNew, Acb_ObjCopy(p, iObj) );
1031 // add divisor as primary outputs (if the divisors are not primary inputs)
1032 if ( vDivs )//&& Vec_IntSize(vDivs) > Vec_IntSize(vSupp) )
1033 Vec_IntForEachEntry( vDivs, iObj, i )
1034 Gia_ManAppendCo( pNew, Acb_ObjCopy(p, iObj) );
1035 Gia_ManHashStop( pNew );
1036 pNew = Gia_ManCleanup( pOne = pNew );
1037 Gia_ManStop( pOne );
1038 return pNew;
1039}
1040int Acb_NtkSaveNames( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Int_t * vNodes, Vec_Int_t * vRoots, Vec_Int_t * vDivs, Vec_Int_t * vTargets, Gia_Man_t * pNew )
1041{
1042 int i, iObj;
1043 assert( pNew->vNamesIn == NULL );
1044
1045 pNew->vNamesIn = Vec_PtrAlloc( Gia_ManCiNum(pNew) );
1046 Acb_NtkForEachCiVec( vSupp, p, iObj, i )
1047 Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Acb_ObjNameStr(p, iObj)) );
1048 if ( vTargets )
1049 Vec_IntForEachEntry( vTargets, iObj, i )
1050 Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Acb_ObjNameStr(p, iObj)) );
1051
1052 pNew->vNamesOut = Vec_PtrAlloc( Gia_ManCoNum(pNew) );
1053 Acb_NtkForEachCoDriverVec( vRoots, p, iObj, i )
1054 Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Acb_ObjNameStr(p, iObj)) );
1055 if ( vDivs )
1056 Vec_IntForEachEntry( vDivs, iObj, i )
1057 {
1058 char Buffer[100];
1059 assert( strlen(Acb_ObjNameStr(p, iObj)) < 90 );
1060 sprintf( Buffer, "%s_%d", Acb_ObjNameStr(p, iObj), Acb_ObjWeight(p, iObj) );
1061 Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
1062 }
1063 return 1;
1064}
1065
1077Gia_Man_t * Acb_CreateMiter( Gia_Man_t * pF, Gia_Man_t * pG )
1078{
1079 Gia_Man_t * pNew, * pOne;
1080 Gia_Obj_t * pObj;
1081 int i, iMiter = 0, iXor;
1082 Gia_ManFillValue( pF );
1083 Gia_ManFillValue( pG );
1084 pNew = Gia_ManStart( Gia_ManObjNum(pF) + Gia_ManObjNum(pF) + 1000 );
1085 Gia_ManHashAlloc( pNew );
1086 Gia_ManConst0(pF)->Value = 0;
1087 Gia_ManConst0(pG)->Value = 0;
1088 Gia_ManForEachCi( pF, pObj, i )
1089 pObj->Value = Gia_ManAppendCi( pNew );
1090 Gia_ManForEachCi( pG, pObj, i )
1091 pObj->Value = Gia_ManCi(pF, i)->Value;
1092 Gia_ManForEachAnd( pF, pObj, i )
1093 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1094 Gia_ManForEachAnd( pG, pObj, i )
1095 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1096 Gia_ManForEachCo( pG, pObj, i )
1097 {
1098 iXor = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(pF, i)) );
1099 iMiter = Gia_ManHashOr( pNew, iMiter, iXor );
1100 }
1101 Gia_ManAppendCo( pNew, iMiter );
1102 Gia_ManForEachCo( pF, pObj, i )
1103 if ( i >= Gia_ManCoNum(pG) )
1104 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1105 Gia_ManHashStop( pNew );
1106 pNew = Gia_ManCleanup( pOne = pNew );
1107 Gia_ManStop( pOne );
1108 return pNew;
1109}
1110
1122#define NWORDS 256
1123
1124void Vec_IntPermute( Vec_Int_t * p )
1125{
1126 int i, nSize = Vec_IntSize( p );
1127 int * pArray = Vec_IntArray( p );
1128 srand( time(NULL) );
1129 for ( i = 0; i < nSize; i++ )
1130 {
1131 int j = rand()%nSize;
1132 ABC_SWAP( int, pArray[i], pArray[j] );
1133 }
1134}
1135
1136void Vec_IntPermute2( Vec_Int_t * p )
1137{
1138 int i, nSize = Vec_IntSize( p );
1139 int * pArray = Vec_IntArray( p );
1140 srand( time(NULL) );
1141 for ( i = 0; i < nSize-1; i++ )
1142 {
1143 if ( rand() % 3 == 0 )
1144 {
1145 printf( "Permuting %d and %d\n", i, i+1 );
1146 ABC_SWAP( int, pArray[i], pArray[i+1] );
1147 }
1148 }
1149}
1150
1151void Acb_PrintPatterns( Vec_Wrd_t * vPats, int nPats, Vec_Int_t * vWeights )
1152{
1153 int i, k, Entry, nDivs = Vec_IntSize(vWeights);
1154 printf( " : " );
1155 Vec_IntForEachEntry( vWeights, Entry, i )
1156 printf( "%d", (Entry / 100) % 10 );
1157 printf( "\n" );
1158 printf( " : " );
1159 Vec_IntForEachEntry( vWeights, Entry, i )
1160 printf( "%d", (Entry / 10) % 10 );
1161 printf( "\n" );
1162 printf( " : " );
1163 Vec_IntForEachEntry( vWeights, Entry, i )
1164 printf( "%d", (Entry / 1) % 10 );
1165 printf( "\n" );
1166 printf( "\n" );
1167
1168 printf( " : " );
1169 for ( i = 0; i < nDivs; i++ )
1170 printf( "%d", (i / 100) % 10 );
1171 printf( "\n" );
1172 printf( " : " );
1173 for ( i = 0; i < nDivs; i++ )
1174 printf( "%d", (i / 10) % 10 );
1175 printf( "\n" );
1176 printf( " : " );
1177 for ( i = 0; i < nDivs; i++ )
1178 printf( "%d", i % 10 );
1179 printf( "\n" );
1180 printf( "\n" );
1181
1182 for ( k = 0; k < nPats; k++ )
1183 {
1184 printf( "%3d : ", k );
1185 for ( i = 0; i < nDivs; i++ )
1186 printf( "%c", Abc_TtGetBit(Vec_WrdEntryP(vPats, NWORDS*i), k) ? '*' : '|' );
1187 printf( "\n" );
1188 }
1189 printf( "\n" );
1190}
1191
1192Vec_Int_t * Acb_DeriveWeights( Vec_Int_t * vDivs, Acb_Ntk_t * pNtkF )
1193{
1194 int i, iDiv;
1195 Vec_Int_t * vWeights = Vec_IntAlloc( Vec_IntSize(vDivs) );
1196 Vec_IntForEachEntry( vDivs, iDiv, i )
1197 Vec_IntPush( vWeights, Vec_IntEntry(&pNtkF->vObjWeight, iDiv) );
1198 return vWeights;
1199}
1200int Acb_ComputeSuppCost( Vec_Int_t * vSupp, Vec_Int_t * vWeights, int iFirstDiv )
1201{
1202 int i, Entry, Cost = 0;
1203 Vec_IntForEachEntry( vSupp, Entry, i )
1204 Cost += Vec_IntEntry( vWeights, Abc_Lit2Var(Entry) - iFirstDiv );
1205 return Cost;
1206}
1207Vec_Int_t * Acb_FindSupportStart( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeights, Vec_Wrd_t ** pvPats, int * piPats )
1208{
1209 int i, status, nDivs = Vec_IntSize(vWeights);
1210 Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
1211 Vec_Wrd_t * vPats = Vec_WrdStart( NWORDS * nDivs );
1212 int iPat = 0;
1213 while ( 1 )
1214 {
1215 int fFound = 0;
1216 // try one run
1217 status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 );
1218 if ( status == l_False )
1219 break;
1220 assert( status == l_True );
1221 // collect pattern
1222 for ( i = 0; i < nDivs; i++ )
1223 {
1224 if ( sat_solver_var_value(pSat, iFirstDiv+i) == 0 )
1225 continue;
1226 Abc_TtSetBit( Vec_WrdEntryP(vPats, NWORDS*i), iPat );
1227 if ( fFound )
1228 continue;
1229 // process new divisor
1230 Vec_IntPush( vSupp, Abc_Var2Lit(iFirstDiv+i, 1) );
1231 //printf( "Selecting divisor %d with weight %d\n", i, Vec_IntEntry(vWeights, i) );
1232 fFound = 1;
1233 }
1234 if ( fFound == 0 )
1235 break;
1236/*
1237 if ( fFound == 0 )
1238 {
1239 printf( "For some reason, cannot find a divisor.\n" );
1240 Vec_WrdFree( vPats );
1241 Vec_IntFree( vSupp );
1242 return NULL;
1243 }
1244*/
1245 assert( fFound );
1246 iPat++;
1247 }
1248 *piPats = iPat;
1249 *pvPats = vPats;
1250 Vec_IntSort( vSupp, 0 );
1251 return vSupp;
1252}
1253int Acb_FindArgMaxUnderMask( Vec_Wrd_t * vPats, word Mask[NWORDS], Vec_Int_t * vWeights, int nPats )
1254{
1255 int nDivs = Vec_WrdSize(vPats)/NWORDS;
1256 int nWords = Abc_Bit6WordNum(nPats);
1257 int i, iBest = -1;
1258 int Cost, CostBest = -1;
1259 for ( i = 0; i < nDivs; i++ )
1260 {
1261 word * pPat = Vec_WrdEntryP(vPats, NWORDS*i);
1262 Cost = Abc_TtCountOnesVecMask(Mask, pPat, nWords, 0);
1263 if ( CostBest < Cost )
1264// if ( CostBest == -1 || (float)CostBest/Cost < 0.6*(float)Vec_IntEntry(vWeights, iBest)/Vec_IntEntry(vWeights, i) )
1265// if ( CostBest == -1 || (float)CostBest/Cost < 0.67*(float)Vec_IntEntry(vWeights, iBest)/Vec_IntEntry(vWeights, i) )
1266 {
1267 CostBest = Cost;
1268 iBest = i;
1269 }
1270 }
1271 return iBest;
1272}
1273int Acb_FindArgMaxUnderMask2( Vec_Wrd_t * vPats, word Mask[NWORDS], Vec_Int_t * vWeights, int nPats )
1274{
1275 int nDivs = Vec_WrdSize(vPats)/NWORDS;
1276 int i, b, iBest = -1;
1277 int Cost, CostBest = -1;
1278 // count how many times each of them appears
1279 Vec_Int_t * vCounts = Vec_IntStart(nPats);
1280 for ( i = 0; i < nDivs; i++ )
1281 {
1282 word * pPat = Vec_WrdEntryP(vPats, NWORDS*i);
1283 for ( b = 0; b < nPats; b++ )
1284 if ( Abc_TtGetBit(pPat, b) )
1285 Vec_IntAddToEntry( vCounts, b, 1 );
1286 }
1287 for ( i = 0; i < nDivs; i++ )
1288 {
1289 word * pPat = Vec_WrdEntryP(vPats, NWORDS*i);
1290// Cost = Abc_TtCountOnesVecMask(Mask, pPat, NWORDS, 0);
1291 Cost = 0;
1292 for ( b = 0; b < nPats; b++ )
1293 if ( Abc_TtGetBit(pPat, b) && Abc_TtGetBit(Mask, b) )
1294 Cost += 1000000/Vec_IntEntry(vCounts, b);
1295 if ( CostBest < Cost )
1296 {
1297 CostBest = Cost;
1298 iBest = i;
1299 }
1300 }
1301 Vec_IntFree( vCounts );
1302 return iBest;
1303}
1304
1305Vec_Int_t * Acb_FindSupportNext( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeights, Vec_Wrd_t * vPats, int * pnPats )
1306{
1307 int i, status, nDivs = Vec_IntSize(vWeights);
1308 Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
1309 word * pMask, Mask[NWORDS]; Abc_TtConst( Mask, NWORDS, 1 );
1310 while ( 1 )
1311 {
1312 int iDivBest = Acb_FindArgMaxUnderMask( vPats, Mask, vWeights, *pnPats );
1313 Vec_IntPush( vSupp, Abc_Var2Lit(iFirstDiv+iDivBest, 1) );
1314 //printf( "Selecting divisor %d with weight %d\n", iDivBest, Vec_IntEntry(vWeights, iDivBest) );
1315// Mask &= ~Vec_WrdEntry( vPats, iDivBest );
1316 pMask = Vec_WrdEntryP( vPats, NWORDS*iDivBest );
1317 Abc_TtAndSharp( Mask, Mask, pMask, NWORDS, 1 );
1318
1319 // try one run
1320 status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 );
1321 if ( status == l_False )
1322 break;
1323 assert( status == l_True );
1324 // collect pattern
1325 for ( i = 0; i < nDivs; i++ )
1326 {
1327 if ( sat_solver_var_value(pSat, iFirstDiv+i) == 0 )
1328 continue;
1329 Abc_TtSetBit( Vec_WrdEntryP(vPats, NWORDS*i), *pnPats );
1330 }
1331 (*pnPats)++;
1332 if ( *pnPats == NWORDS*64 )
1333 {
1334 printf( "Exceeded %d words.\n", NWORDS );
1335 Vec_IntFreeP( &vSupp );
1336 return NULL;
1337 }
1338 assert( *pnPats < NWORDS*64 );
1339 //Acb_PrintPatterns( vPats, *pnPats, vWeights );
1340 //i = i;
1341 }
1342 Vec_IntSort( vSupp, 0 );
1343 return vSupp;
1344}
1345Vec_Int_t * Acb_FindSupportMinOne( sat_solver * pSat, int iFirstDiv, Vec_Wrd_t * vPats, int * pnPats, Vec_Int_t * vSupp, int iVar )
1346{
1347 int i, iLit, status;
1348 int nDivs = Vec_WrdSize(vPats)/NWORDS;
1349 Vec_Int_t * vLits = Vec_IntAlloc( Vec_IntSize(vSupp) );
1350 Vec_IntForEachEntry( vSupp, iLit, i )
1351 if ( i != iVar )
1352 Vec_IntPush( vLits, iLit );
1353 // try one run
1354 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), 0, 0, 0, 0 );
1355 if ( status == l_False )
1356 return vLits;
1357 Vec_IntFree( vLits );
1358 assert( status == l_True );
1359 // collect pattern
1360 for ( i = 0; i < nDivs; i++ )
1361 {
1362 if ( sat_solver_var_value(pSat, iFirstDiv+i) == 0 )
1363 continue;
1364 Abc_TtSetBit( Vec_WrdEntryP(vPats, NWORDS*i), *pnPats );
1365 }
1366 (*pnPats)++;
1367 if ( *pnPats == NWORDS*64 )
1368 return NULL;
1369 return vSupp;
1370}
1371Vec_Int_t * Acb_FindSupportMin( sat_solver * pSat, int iFirstDiv, Vec_Wrd_t * vPats, int * pnPats, Vec_Int_t * vSuppStart )
1372{
1373 Vec_Int_t * vTemp, * vSupp = Vec_IntDup( vSuppStart ); int i;
1374 for ( i = Vec_IntSize(vSupp)-1; i >= 0; i-- )
1375 {
1376 vSupp = Acb_FindSupportMinOne( pSat, iFirstDiv, vPats, pnPats, vTemp = vSupp, i );
1377 if ( vTemp != vSupp )
1378 Vec_IntFree( vTemp );
1379 if ( vSupp == NULL )
1380 return NULL;
1381 }
1382 return vSupp;
1383}
1384void Acb_FindReplace( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeights, Vec_Wrd_t * vPats, int nPats, Vec_Int_t * vSupp )
1385{
1386 int i, k, iLit, iLit2, status, nWords = Abc_Bit6WordNum(nPats);
1387 word Covered[NWORDS], Both[NWORDS], Mask[NWORDS], * pMask;
1388 assert( nWords <= NWORDS );
1389 // prepare constant pattern
1390 Abc_TtConst( Mask, nWords, 0 );
1391 for ( i = 0; i < nPats; i++ )
1392 Abc_TtSetBit( Mask, i );
1393 // try to replace each by a cheaper one
1394 Vec_IntForEachEntry( vSupp, iLit, i )
1395 {
1396 int iDiv = Abc_Lit2Var(iLit) - iFirstDiv;
1397 // collect covered except by this one
1398 Abc_TtConst( Covered, nWords, 0 );
1399 Vec_IntForEachEntry( vSupp, iLit2, k )
1400 {
1401 if ( iLit2 == iLit )
1402 continue;
1403 pMask = Vec_WrdEntryP( vPats, NWORDS*(Abc_Lit2Var(iLit2) - iFirstDiv) );
1404 Abc_TtOr( Covered, Covered, pMask, nWords );
1405 }
1406 // consider any cheaper ones that this one
1407 for ( k = 0; k < iDiv; k++ )
1408 {
1409 if ( Vec_IntEntry(vWeights, k) == Vec_IntEntry(vWeights, iDiv) )
1410 continue;
1411 assert( Vec_IntEntry(vWeights, k) < Vec_IntEntry(vWeights, iDiv) );
1412 pMask = Vec_WrdEntryP( vPats, NWORDS*k );
1413 // check if it covers the remaining ones
1414 Abc_TtOr( Both, Covered, pMask, nWords );
1415 if ( !Abc_TtEqual(Both, Mask, nWords) )
1416 continue;
1417 // try this one
1418 Vec_IntWriteEntry( vSupp, i, Abc_Var2Lit(iFirstDiv+k, 1) );
1419 status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 );
1420 if ( status == l_False ) // success
1421 {
1422 //printf( "Replacing %d(%d) by %d(%d) with const difference %d.\n",
1423 // iDiv, Vec_IntEntry(vWeights, iDiv), k, Vec_IntEntry(vWeights, k),
1424 // Vec_IntEntry(vWeights, iDiv) - Vec_IntEntry(vWeights, k) );
1425 break;
1426 }
1427 Vec_IntWriteEntry( vSupp, i, iLit );
1428 }
1429 }
1430}
1431
1432Vec_Int_t * Acb_FindSupport( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeights, Vec_Int_t * vSuppStart, int TimeOut )
1433{
1434 abctime clkLimit = TimeOut * CLOCKS_PER_SEC + Abc_Clock();
1435 Vec_Wrd_t * vPats = NULL;
1436 int nPats = 0;
1437 Vec_Int_t * vSuppBest, * vSupp, * vTemp;
1438 int CostBest, Cost;
1439 int Iter;
1440
1441 // find initial best
1442 CostBest = Acb_ComputeSuppCost( vSuppStart, vWeights, iFirstDiv );
1443 vSuppBest = Vec_IntDup( vSuppStart );
1444 printf( "Starting cost = %d.\n", CostBest );
1445
1446 // iteratively find the one with the most ones in the uncovered rows
1447 for ( Iter = 0; Iter < 500; Iter++ )
1448 {
1449 if ( Abc_Clock() > clkLimit )
1450 {
1451 printf( "Timeout after %d sec.\n", TimeOut );
1452 break;
1453 }
1454 if ( Iter == 0 )
1455 vSupp = Acb_FindSupportStart( pSat, iFirstDiv, vWeights, &vPats, &nPats );
1456 else
1457 vSupp = Acb_FindSupportNext( pSat, iFirstDiv, vWeights, vPats, &nPats );
1458 if ( vSupp == NULL )
1459 break;
1460 vSupp = Acb_FindSupportMin( pSat, iFirstDiv, vPats, &nPats, vTemp = vSupp );
1461 Vec_IntFree( vTemp );
1462 if ( vSupp == NULL )
1463 break;
1464 Cost = Acb_ComputeSuppCost( vSupp, vWeights, iFirstDiv );
1465 //Acb_PrintPatterns( vPats, nPats, vWeights );
1466 if ( CostBest > Cost )
1467 {
1468 CostBest = Cost;
1469 ABC_SWAP( Vec_Int_t *, vSuppBest, vSupp );
1470 printf( "Iter %4d: Next cost = %5d. ", Iter, Cost );
1471 printf( "Updating best solution.\n" );
1472 }
1473 Vec_IntFree( vSupp );
1474 }
1475 if ( vPats )
1476 Acb_FindReplace( pSat, iFirstDiv, vWeights, vPats, nPats, vSuppBest );
1477 //printf( "Number of patterns = %d.\n", nPats );
1478 Vec_WrdFreeP( &vPats );
1479 return vSuppBest;
1480}
1481
1493Vec_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 )
1494{
1495 Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
1496 int i, Lit;
1497 int iCoVarBeg = 1;
1498 int iCiVarBeg = pCnf->nVars - nTargets;
1499 sat_solver * pSat = sat_solver_new();
1500 sat_solver_setnvars( pSat, 2 * pCnf->nVars + nCoDivs );
1501 // add clauses
1502 for ( i = 0; i < pCnf->nClauses; i++ )
1503 if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
1504 return NULL;
1505 // add output clause
1506 Lit = Abc_Var2Lit( iCoVarBeg, 0 );
1507 if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
1508 return NULL;
1509 // add clauses
1510 pCnf->pMan = NULL;
1511 Cnf_DataLift( pCnf, pCnf->nVars );
1512 for ( i = 0; i < pCnf->nClauses; i++ )
1513 if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
1514 return NULL;
1515 Cnf_DataLift( pCnf, -pCnf->nVars );
1516 // add output clause
1517 Lit = Abc_Var2Lit( iCoVarBeg+pCnf->nVars, 0 );
1518 if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
1519 return NULL;
1520 // create XORs for targets
1521 // add negative literal
1522 Lit = Abc_Var2Lit( iCiVarBeg + iTar, 1 );
1523 if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
1524 return NULL;
1525 // add positive literal
1526 Lit = Abc_Var2Lit( iCiVarBeg+pCnf->nVars + iTar, 0 );
1527 if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
1528 return NULL;
1529 // create XORs for divisors
1530 if ( nCoDivs > 0 )
1531 {
1532 abctime clk = Abc_Clock();
1533 int fUseMinAssump = 1;
1534 int iLit, nSuppNew, status;
1535 int iDivVar = 2 * pCnf->nVars;
1536 int pLits[2];
1537 int j = 0, iDivOld;
1538 Vec_IntClear( vSupp );
1539 if ( vSuppOld )
1540 {
1541 // start with predefined support
1542 Vec_IntForEachEntry( vSuppOld, iDivOld, j )
1543 {
1544 int iVar0 = iCoVarBeg+1+iDivOld;
1545 int iVar1 = iCoVarBeg+1+iDivOld+pCnf->nVars;
1546 //printf( "Selecting predefined divisor %d with weight %d\n",
1547 // iDivOld, Vec_IntEntry(&pNtkF->vObjWeight, Vec_IntEntry(vDivs, iDivOld)) );
1548 // add equality clauses
1549 pLits[0] = Abc_Var2Lit( iVar0, 0 );
1550 pLits[1] = Abc_Var2Lit( iVar1, 1 );
1551 if ( !sat_solver_addclause( pSat, pLits, pLits+2 ) )
1552 {
1553 printf( "Unsat is detected earlier.\n" );
1554 status = l_False;
1555 break;
1556 }
1557 pLits[0] = Abc_Var2Lit( iVar0, 1 );
1558 pLits[1] = Abc_Var2Lit( iVar1, 0 );
1559 if ( !sat_solver_addclause( pSat, pLits, pLits+2 ) )
1560 {
1561 printf( "Unsat is detected earlier.\n" );
1562 status = l_False;
1563 break;
1564 }
1565 }
1566 }
1567 if ( vSuppOld == NULL || j == Vec_IntSize(vSuppOld) )
1568 {
1569 for ( i = 0; i < nCoDivs; i++ )
1570 {
1571 sat_solver_add_xor( pSat, iDivVar+i, iCoVarBeg+1+i, iCoVarBeg+1+i+pCnf->nVars, 0 );
1572 Vec_IntPush( vSupp, Abc_Var2Lit(iDivVar+i, 1) );
1573 }
1574 // try one run
1575 if ( TimeOut ) sat_solver_set_runtime_limit( pSat, TimeOut * CLOCKS_PER_SEC + Abc_Clock() );
1576 status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 );
1577 if ( TimeOut ) sat_solver_set_runtime_limit( pSat, 0 );
1578 if ( status == l_True )
1579 {
1580 printf( "ECO does not exist.\n" );
1581 sat_solver_delete( pSat );
1582 Vec_IntFree( vSupp );
1583 return NULL;
1584 }
1585 if ( status == l_Undef )
1586 {
1587 printf( "Support computation timed out after %d sec.\n", TimeOut );
1588 sat_solver_delete( pSat );
1589 Vec_IntFree( vSupp );
1590 return NULL;
1591 }
1592 assert( status == l_False );
1593 printf( "Proved that the problem has a solution. " );
1594 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1595 // find minimum subset
1596 if ( fUseMinAssump )
1597 {
1598 int fUseSuppMin = 1;
1599 // solve in a standard way
1600 abctime clk = Abc_Clock();
1601 nSuppNew = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 );
1602 Vec_IntShrink( vSupp, nSuppNew );
1603 Vec_IntSort( vSupp, 0 );
1604 printf( "Found one feasible set of %d divisors. ", Vec_IntSize(vSupp) );
1605 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1606
1607 // perform minimization
1608 if ( fUseSuppMin && Vec_IntSize(vSupp) > 0 )
1609 {
1610 abctime clk = Abc_Clock();
1611 Vec_Int_t * vSupp2 = Vec_IntDup( vSupp );
1612 Vec_Int_t * vTemp, * vWeights = Acb_DeriveWeights( vDivs, pNtkF );
1613 vSupp = Acb_FindSupport( pSat, iDivVar, vWeights, vTemp = vSupp, TimeOut );
1614 Vec_IntFree( vWeights );
1615 Vec_IntFree( vTemp );
1616 if ( vSupp == NULL )
1617 {
1618 printf( "Support minimization did not succeed. " );
1619 //sat_solver_delete( pSat );
1620 vSupp = vSupp2;
1621 }
1622 else
1623 {
1624 Vec_IntFree( vSupp2 );
1625 printf( "Minimized support to %d supp vars. ", Vec_IntSize(vSupp) );
1626 }
1627 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1628 }
1629 }
1630 else
1631 {
1632 int * pFinal, nFinal = sat_solver_final( pSat, &pFinal );
1633 printf( "AnalyzeFinal returned %d (out of %d).\n", nFinal, Vec_IntSize(vSupp) );
1634 Vec_IntClear( vSupp );
1635 for ( i = 0; i < nFinal; i++ )
1636 Vec_IntPush( vSupp, Abc_LitNot(pFinal[i]) );
1637 // try one run
1638 status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 );
1639 assert( status == l_False );
1640 // try again
1641 nFinal = sat_solver_final( pSat, &pFinal );
1642 printf( "AnalyzeFinal returned %d (out of %d).\n", nFinal, Vec_IntSize(vSupp) );
1643 }
1644 // remap them into numbers
1645 Vec_IntForEachEntry( vSupp, iLit, i )
1646 Vec_IntWriteEntry( vSupp, i, Abc_Lit2Var(iLit)-iDivVar );
1647 Vec_IntSort( vSupp, 0 );
1648 }
1649 }
1650 sat_solver_delete( pSat );
1651 if ( vSupp ) Vec_IntSort( vSupp, 0 );
1652 return vSupp;
1653}
1654
1655static inline int satoko_add_xor( satoko_t * pSat, int iVarA, int iVarB, int iVarC, int fCompl )
1656{
1657 int Lits[3];
1658 int Cid;
1659 assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
1660
1661 Lits[0] = toLitCond( iVarA, !fCompl );
1662 Lits[1] = toLitCond( iVarB, 1 );
1663 Lits[2] = toLitCond( iVarC, 1 );
1664 Cid = satoko_add_clause( pSat, Lits, 3 );
1665 assert( Cid );
1666
1667 Lits[0] = toLitCond( iVarA, !fCompl );
1668 Lits[1] = toLitCond( iVarB, 0 );
1669 Lits[2] = toLitCond( iVarC, 0 );
1670 Cid = satoko_add_clause( pSat, Lits, 3 );
1671 assert( Cid );
1672
1673 Lits[0] = toLitCond( iVarA, fCompl );
1674 Lits[1] = toLitCond( iVarB, 1 );
1675 Lits[2] = toLitCond( iVarC, 0 );
1676 Cid = satoko_add_clause( pSat, Lits, 3 );
1677 assert( Cid );
1678
1679 Lits[0] = toLitCond( iVarA, fCompl );
1680 Lits[1] = toLitCond( iVarB, 0 );
1681 Lits[2] = toLitCond( iVarC, 1 );
1682 Cid = satoko_add_clause( pSat, Lits, 3 );
1683 assert( Cid );
1684 return 4;
1685}
1686Vec_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 )
1687{
1688 Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
1689 int i, Lit;
1690 int iCoVarBeg = 1;
1691 int iCiVarBeg = pCnf->nVars - nCiTars;
1692 satoko_t * pSat = satoko_create();
1693 satoko_setnvars( pSat, 2 * pCnf->nVars + nCiTars + nCoDivs );
1694 satoko_options(pSat)->no_simplify = 1;
1695 // add clauses
1696 for ( i = 0; i < pCnf->nClauses; i++ )
1697 if ( !satoko_add_clause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
1698 return NULL;
1699 // add output clause
1700 Lit = Abc_Var2Lit( iCoVarBeg, 0 );
1701 if ( !satoko_add_clause( pSat, &Lit, 1 ) )
1702 return NULL;
1703 // add clauses
1704 pCnf->pMan = NULL;
1705 Cnf_DataLift( pCnf, pCnf->nVars );
1706 for ( i = 0; i < pCnf->nClauses; i++ )
1707 if ( !satoko_add_clause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
1708 return NULL;
1709 Cnf_DataLift( pCnf, -pCnf->nVars );
1710 // add output clause
1711 Lit = Abc_Var2Lit( iCoVarBeg+pCnf->nVars, 0 );
1712 if ( !satoko_add_clause( pSat, &Lit, 1 ) )
1713 return NULL;
1714 // create XORs for targets
1715 if ( nCiTars > 0 )
1716 {
1717/*
1718 int iXorVar = 2 * pCnf->nVars;
1719 int Lit;
1720 Vec_IntClear( vSupp );
1721 for ( i = 0; i < nCiTars; i++ )
1722 {
1723 satoko_add_xor( pSat, iXorVar+i, iCiVarBeg+i, iCiVarBeg+i+pCnf->nVars, 0 );
1724 Vec_IntPush( vSupp, Abc_Var2Lit(iXorVar+i, 0) );
1725 }
1726 if ( !satoko_add_clause( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp) ) )
1727 return NULL;
1728*/
1729 // add negative literal
1730 Lit = Abc_Var2Lit( iCiVarBeg, 1 );
1731 if ( !satoko_add_clause( pSat, &Lit, 1 ) )
1732 return NULL;
1733 // add positive literal
1734 Lit = Abc_Var2Lit( iCiVarBeg+pCnf->nVars, 0 );
1735 if ( !satoko_add_clause( pSat, &Lit, 1 ) )
1736 return NULL;
1737 }
1738 // create XORs for divisors
1739 if ( nCoDivs > 0 )
1740 {
1741 abctime clk = Abc_Clock();
1742 int fUseMinAssump = 1;
1743 int iLit, status, nSuppNew;
1744 int iDivVar = 2 * pCnf->nVars + nCiTars;
1745 Vec_IntClear( vSupp );
1746 for ( i = 0; i < nCoDivs; i++ )
1747 {
1748 satoko_add_xor( pSat, iDivVar+i, iCoVarBeg+1+i, iCoVarBeg+1+i+pCnf->nVars, 0 );
1749 Vec_IntPush( vSupp, Abc_Var2Lit(iDivVar+i, 1) );
1750/*
1751 pLits[0] = Abc_Var2Lit(iCoVarBeg+1+i, 1);
1752 pLits[1] = Abc_Var2Lit(iCoVarBeg+1+i+pCnf->nVars, 0);
1753 pLits[2] = Abc_Var2Lit(iDivVar+i, 1);
1754 if ( !satoko_add_clause( pSat, pLits, 3 ) )
1755 assert( 0 );
1756
1757 pLits[0] = Abc_Var2Lit(iCoVarBeg+1+i, 0);
1758 pLits[1] = Abc_Var2Lit(iCoVarBeg+1+i+pCnf->nVars, 1);
1759 pLits[2] = Abc_Var2Lit(iDivVar+i, 1);
1760 if ( !satoko_add_clause( pSat, pLits, 3 ) )
1761 assert( 0 );
1762
1763 Vec_IntPush( vSupp, Abc_Var2Lit(iDivVar+i, 0) );
1764*/
1765 }
1766
1767 // try one run
1768 status = satoko_solve_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp) );
1769 if ( status != l_False )
1770 {
1771 printf( "Demonstrated that the problem has NO solution. " );
1772 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1773 satoko_destroy( pSat );
1774 Vec_IntFree( vSupp );
1775 return NULL;
1776 }
1777 assert( status == l_False );
1778 printf( "Proved that the problem has a solution. " );
1779 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1780
1781 // find minimum subset
1782 if ( fUseMinAssump )
1783 {
1784 abctime clk = Abc_Clock();
1785 nSuppNew = satoko_minimize_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 );
1786 Vec_IntShrink( vSupp, nSuppNew );
1787 printf( "Solved the problem with %d supp vars. ", Vec_IntSize(vSupp) );
1788 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1789 }
1790 else
1791 {
1792 int * pFinal, nFinal = satoko_final_conflict( pSat, &pFinal );
1793 printf( "AnalyzeFinal returned %d (out of %d).\n", nFinal, Vec_IntSize(vSupp) );
1794 Vec_IntClear( vSupp );
1795 for ( i = 0; i < nFinal; i++ )
1796 Vec_IntPush( vSupp, Abc_LitNot(pFinal[i]) );
1797 // try one run
1798 status = satoko_solve_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp) );
1799 assert( status == l_False );
1800 // try again
1801 nFinal = satoko_final_conflict( pSat, &pFinal );
1802 printf( "AnalyzeFinal returned %d (out of %d).\n", nFinal, Vec_IntSize(vSupp) );
1803 }
1804
1805 // remap them into numbers
1806 Vec_IntForEachEntry( vSupp, iLit, i )
1807 Vec_IntWriteEntry( vSupp, i, Abc_Lit2Var(iLit)-iDivVar );
1808 Vec_IntSort( vSupp, 0 );
1809 //Vec_IntPrint( vSupp );
1810 }
1811 satoko_destroy( pSat );
1812 Vec_IntSort( vSupp, 0 );
1813 return vSupp;
1814}
1815
1816
1828char * Acb_EnumerateSatAssigns( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vTempLits, Vec_Str_t * vTempSop )
1829{
1830 int fCreatePrime = 1;
1831 int status, i, iMint, iVar, iLit, nFinal, * pFinal, pLits[2];
1832 Vec_Int_t * vTemp, * vLits;
1833 assert( FreeVar < sat_solver_nvars(pSat) );
1834 pLits[0] = Abc_Var2Lit( PivotVar, 1 ); // F = 1
1835 pLits[1] = Abc_Var2Lit( FreeVar, 0 ); // iNewLit
1836 Vec_StrClear( vTempSop );
1837 Vec_StrGrow( vTempSop, 8 * (Vec_IntSize(vDivVars) + 3) + 1 );
1838 // check constant 0
1839 status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 );
1840 if ( status == l_False )
1841 {
1842 Vec_StrPush( vTempSop, ' ' );
1843 Vec_StrPush( vTempSop, '0' );
1844 Vec_StrPush( vTempSop, '\n' );
1845 Vec_StrPush( vTempSop, '\0' );
1846 return Vec_StrReleaseArray(vTempSop);
1847 }
1848 // check constant 1
1849 pLits[0] = Abc_LitNot(pLits[0]);
1850 status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 );
1851 pLits[0] = Abc_LitNot(pLits[0]);
1852 if ( status == l_False || Vec_IntSize(vDivVars) == 0 )
1853 {
1854 Vec_StrPush( vTempSop, ' ' );
1855 Vec_StrPush( vTempSop, '1' );
1856 Vec_StrPush( vTempSop, '\n' );
1857 Vec_StrPush( vTempSop, '\0' );
1858 return Vec_StrReleaseArray(vTempSop);
1859 }
1860 //Vec_IntPrint( vDivVars );
1861 vTemp = Vec_IntAlloc( 100 );
1862 vLits = Vec_IntAlloc( 100 );
1863 for ( iMint = 0; ; iMint++ )
1864 {
1865 if ( iMint == 1000 )
1866 {
1867 if ( Vec_IntSize(vDivVars) == 0 )
1868 {
1869 printf( "Assuming constant 0 function.\n" );
1870 Vec_StrClear( vTempSop );
1871 Vec_StrPush( vTempSop, ' ' );
1872 Vec_StrPush( vTempSop, '0' );
1873 Vec_StrPush( vTempSop, '\n' );
1874 Vec_StrPush( vTempSop, '\0' );
1875 return Vec_StrReleaseArray(vTempSop);
1876 }
1877
1878 printf( "Reached the limit on the number of cubes (1000).\n" );
1879 Vec_IntFree( vTemp );
1880 Vec_IntFree( vLits );
1881 return NULL;
1882 }
1883 //int Offset = Vec_StrSize(vTempSop);
1884 // find onset minterm
1885 status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 );
1886 if ( status == l_False )
1887 {
1888 printf( "Finished enumerating %d cubes.\n", iMint );
1889 Vec_IntFree( vTemp );
1890 Vec_IntFree( vLits );
1891 Vec_StrPush( vTempSop, '\0' );
1892 return Vec_StrReleaseArray(vTempSop);
1893 }
1894 assert( status == l_True );
1895 // collect divisor literals
1896 Vec_IntClear( vTempLits );
1897 Vec_IntPush( vTempLits, Abc_LitNot(pLits[0]) ); // F = 0
1898 //printf( "%8d %3d ", 0, 0 );
1899// Vec_IntForEachEntry( vDivVars, iVar, i )
1900 Vec_IntForEachEntryReverse( vDivVars, iVar, i )
1901 {
1902 Vec_IntPush( vTempLits, sat_solver_var_literal(pSat, iVar) );
1903 //printf( "%c", '0' + sat_solver_var_value(pSat, iVar) );
1904 }
1905 //printf( "\n" );
1906 // create new cube
1907 for ( i = 0; i < Vec_IntSize(vDivVars); i++ )
1908 Vec_StrPush( vTempSop, '-' );
1909 if ( fCreatePrime )
1910 {
1911 // expand against offset
1912 status = sat_solver_push(pSat, Vec_IntEntry(vTempLits, 0));
1913 assert( status == 1 );
1914 nFinal = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vTempLits)+1, Vec_IntSize(vTempLits)-1, 0 );
1915 Vec_IntShrink( vTempLits, nFinal+1 );
1916 sat_solver_pop(pSat);
1917 // compute cube and add clause
1918 Vec_IntWriteEntry( vTempLits, 0, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
1919 Vec_IntForEachEntryStart( vTempLits, iLit, i, 1 )
1920 {
1921 Vec_IntWriteEntry( vTempLits, i, Abc_LitNot(iLit) );
1922 iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(iLit) ); assert( iVar >= 0 );
1923 //uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
1924 Vec_StrWriteEntry( vTempSop, Vec_StrSize(vTempSop) - Vec_IntSize(vDivVars) + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) );
1925 }
1926 }
1927 else
1928 {
1929 // expand against offset
1930 status = sat_solver_solve( pSat, Vec_IntArray(vTempLits), Vec_IntLimit(vTempLits), 0, 0, 0, 0 );
1931 if ( status != l_False )
1932 printf( "Selected onset minterm number %d belongs to the offset (this is a bug).\n", iMint );
1933 assert( status == l_False );
1934
1935 // compute cube and add clause
1936 nFinal = sat_solver_final( pSat, &pFinal );
1937 Vec_IntSelectSort( pFinal, nFinal );
1938/*
1939 // pretend that this is final
1940 veci_resize(&pSat->conf_final,0);
1941 Vec_IntForEachEntry( vTempLits, iLit, i )
1942 veci_push(&pSat->conf_final, lit_neg(iLit));
1943 pFinal = pSat->conf_final.ptr;
1944 nFinal = Vec_IntSize(vTempLits);
1945*/
1947 // create new cube
1948 Vec_IntClear( vTemp );
1949 Vec_IntPush( vTemp, Abc_LitNot(pLits[0]) ); // F = 0
1950 for ( i = 0; i < nFinal; i++ )
1951 {
1952 if ( pFinal[i] == pLits[0] )
1953 continue;
1954 Vec_IntPush( vTemp, Abc_LitNot(pFinal[i]) );
1955 }
1956
1957 //Vec_IntPrint( vTemp );
1958 // try removing each one starting with the last one
1959 //printf( "Started with %d lits ", nFinal-1 );
1960 for ( i = nFinal - 1; i > 0; i-- )
1961 {
1962 int iLit = Vec_IntEntry( vTemp, i );
1963 Vec_IntDrop( vTemp, i );
1964 // try SAT
1965 status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), 0, 0, 0, 0 );
1966 if ( status == l_False )
1967 {
1968 // printf( "U" );
1969 continue;
1970 }
1971 //if ( status == l_True )
1972 // printf( "S" );
1973 //else if ( status == l_Undef )
1974 // printf( "T" );
1975 Vec_IntInsert( vTemp, i, iLit );
1976 }
1977 //printf( " Ended up with %d lits\n", Vec_IntSize(vTemp)-1 );
1978 //Vec_IntPrint( vTemp );
1979
1980 Vec_IntForEachEntry( vTemp, iLit, i )
1981 pFinal[i] = Abc_LitNot(iLit);
1982 nFinal = Vec_IntSize(vTemp);
1984
1985
1986 Vec_IntClear( vTempLits );
1987 Vec_IntPush( vTempLits, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
1988 for ( i = 0; i < nFinal; i++ )
1989 {
1990 if ( pFinal[i] == pLits[0] )
1991 continue;
1992 Vec_IntPush( vTempLits, pFinal[i] );
1993 iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
1994 //uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
1995 Vec_StrWriteEntry( vTempSop, Vec_StrSize(vTempSop) - Vec_IntSize(vDivVars) + iVar, (char)('0' + Abc_LitIsCompl(pFinal[i])) );
1996 }
1997 }
1998 //printf( "%6d : %8d %3d ", iMint, (int)pSat->stats.conflicts, Vec_IntSize(vTempLits)-1 );
1999
2000 Vec_StrAppend( vTempSop, " 1\n" );
2001 status = sat_solver_addclause( pSat, Vec_IntArray(vTempLits), Vec_IntLimit(vTempLits) );
2002 assert( status );
2003
2004 //Vec_StrPush( vTempSop, '\0' );
2005 //printf( "%s", Vec_StrEntryP(vTempSop, Offset) );
2006 //Vec_StrPop( vTempSop );
2007 }
2008 assert( 0 );
2009 return NULL;
2010}
2011char * Acb_DeriveOnePatchFunction( Cnf_Dat_t * pCnf, int iTar, int nTargets, int nCoDivs, Vec_Int_t * vUsed, int fCisOnly )
2012{
2013 char * pSop = NULL;
2014 Vec_Int_t * vTempLits = Vec_IntAlloc( Vec_IntSize(vUsed)+1 );
2015 Vec_Str_t * vTempSop = Vec_StrAlloc(0);
2016 int i, Lit;
2017 int iCiVarBeg = pCnf->nVars - nTargets - Vec_IntSize(vUsed);
2018 int iCoVarBeg = 1, Index;
2019 sat_solver * pSat = sat_solver_new();
2020 sat_solver_setnvars( pSat, pCnf->nVars + 1 );
2021 // add clauses
2022 for ( i = 0; i < pCnf->nClauses; i++ )
2023 if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
2024 return NULL;
2025 // add output clause
2026 Lit = Abc_Var2Lit( iCoVarBeg, 0 );
2027 if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
2028 return NULL;
2029 // remap vUsed to be in terms of divisor variables
2030 if ( fCisOnly )
2031 {
2032 Vec_IntForEachEntry( vUsed, Index, i )
2033 Vec_IntWriteEntry( vUsed, i, iCiVarBeg + Index );
2034 }
2035 else
2036 {
2037 Vec_IntForEachEntry( vUsed, Index, i )
2038 Vec_IntWriteEntry( vUsed, i, iCoVarBeg + 1 + Index );
2039 }
2040 // enumerate assignments for each target in terms of used divisors
2041 pSop = Acb_EnumerateSatAssigns( pSat, pCnf->nVars - nTargets + iTar, pCnf->nVars, vUsed, vTempLits, vTempSop );
2042 Vec_IntFree( vTempLits );
2043 Vec_StrFree( vTempSop );
2044 sat_solver_delete( pSat );
2045 if ( pSop == NULL )
2046 return NULL;
2047 //printf( "Function %d:\n%s", i, pSop );
2048 // remap vUsed to be in terms of original divisors
2049 if ( fCisOnly )
2050 {
2051 Vec_IntForEachEntry( vUsed, Index, i )
2052 Vec_IntWriteEntry( vUsed, i, Index - iCiVarBeg );
2053 }
2054 else
2055 {
2056 Vec_IntForEachEntry( vUsed, Index, i )
2057 Vec_IntWriteEntry( vUsed, i, Index - (iCoVarBeg + 1) );
2058 }
2059 return pSop;
2060}
2061int Acb_CheckMiter( Cnf_Dat_t * pCnf )
2062{
2063 int iCoVarBeg = 1, i, Lit, status;
2064 sat_solver * pSat = sat_solver_new();
2065 sat_solver_setnvars( pSat, pCnf->nVars );
2066 // add clauses
2067 for ( i = 0; i < pCnf->nClauses; i++ )
2068 if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
2069 return 1;
2070 // add output clause
2071 Lit = Abc_Var2Lit( iCoVarBeg, 0 );
2072 if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
2073 return 1;
2074 status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
2075 sat_solver_delete( pSat );
2076 return status == l_False;
2077}
2078
2079
2091void Acb_CollectIntNodes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
2092{
2093 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
2094 return;
2095 Gia_ObjSetTravIdCurrent(p, pObj);
2096 assert( Gia_ObjIsAnd(pObj) );
2097 Acb_CollectIntNodes_rec( p, Gia_ObjFanin0(pObj), vNodes );
2098 Acb_CollectIntNodes_rec( p, Gia_ObjFanin1(pObj), vNodes );
2099 Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
2100}
2101void Acb_CollectIntNodes( Gia_Man_t * p, Vec_Int_t * vNodes0, Vec_Int_t * vNodes1 )
2102{
2103 Gia_Obj_t * pObj; int i;
2104 Vec_IntClear( vNodes0 );
2105 Vec_IntClear( vNodes1 );
2106 Gia_ManIncrementTravId( p );
2107 Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
2108 Gia_ManForEachCi( p, pObj, i )
2109 Gia_ObjSetTravIdCurrent( p, pObj );
2110 Gia_ManForEachCo( p, pObj, i )
2111 if ( i > 0 )
2112 Acb_CollectIntNodes_rec( p, Gia_ObjFanin0(pObj), vNodes1 );
2113 Gia_ManForEachCo( p, pObj, i )
2114 if ( i == 0 )
2115 Acb_CollectIntNodes_rec( p, Gia_ObjFanin0(pObj), vNodes0 );
2116}
2117Gia_Man_t * Acb_UpdateMiter( Gia_Man_t * pM, Gia_Man_t * pOne, int iTar, int nTargets, Vec_Int_t * vUsed, int fCisOnly )
2118{
2119 Gia_Man_t * pRes, * pTemp;
2120 Gia_Obj_t * pObj; int i;
2121 Vec_Int_t * vNodes0 = Vec_IntAlloc( Gia_ManAndNum(pM) );
2122 Vec_Int_t * vNodes1 = Vec_IntAlloc( Gia_ManAndNum(pM) );
2123 Acb_CollectIntNodes( pM, vNodes0, vNodes1 );
2124 Gia_ManFillValue( pM );
2125 Gia_ManFillValue( pOne );
2126 // create new
2127 pRes = Gia_ManStart( Gia_ManObjNum(pM) + Gia_ManObjNum(pOne) );
2128 Gia_ManHashAlloc( pRes );
2129 Gia_ManConst0(pM)->Value = 0;
2130 Gia_ManConst0(pOne)->Value = 0;
2131 // copy first part of the miter
2132 Gia_ManForEachCi( pM, pObj, i )
2133// if ( i < Gia_ManCiNum(pM) - 1 )
2134 pObj->Value = Gia_ManAppendCi( pRes );
2135 Gia_ManForEachObjVec( vNodes1, pM, pObj, i )
2136 pObj->Value = Gia_ManHashAnd( pRes, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2137 Gia_ManForEachCo( pM, pObj, i )
2138 if ( i > 0 )
2139 pObj->Value = Gia_ObjFanin0Copy(pObj);
2140 // transfer to New
2141 //assert( Gia_ManCiNum(pOne) <= Vec_IntSize(vUsed) );
2142 assert( Gia_ManCoNum(pOne) == 1 );
2143 if ( fCisOnly )
2144 {
2145 Gia_ManForEachCi( pOne, pObj, i )
2146 if ( i < Vec_IntSize(vUsed) )
2147 pObj->Value = Gia_ManCi(pM, Vec_IntEntry(vUsed, i))->Value;
2148 }
2149 else
2150 {
2151 Gia_ManForEachCi( pOne, pObj, i )
2152 pObj->Value = Gia_ManCo(pM, 1+Vec_IntEntry(vUsed, i))->Value;
2153 }
2154 Gia_ManForEachAnd( pOne, pObj, i )
2155 pObj->Value = Gia_ManHashAnd( pRes, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2156 // transfer to miter
2157 pObj = Gia_ManCi( pM, Gia_ManCiNum(pM) - nTargets + iTar );
2158 pObj->Value = Gia_ObjFanin0Copy( Gia_ManCo(pOne, 0) );
2159 Gia_ManForEachObjVec( vNodes0, pM, pObj, i )
2160 pObj->Value = Gia_ManHashAnd( pRes, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2161 Gia_ManForEachCo( pM, pObj, i )
2162 Gia_ManAppendCo( pRes, Gia_ObjFanin0Copy(pObj) );
2163 // cleanup
2164 Vec_IntFree( vNodes0 );
2165 Vec_IntFree( vNodes1 );
2166 Gia_ManHashStop( pRes );
2167 pRes = Gia_ManCleanup( pTemp = pRes );
2168 Gia_ManStop( pTemp );
2169 assert( Gia_ManCiNum(pRes) == Gia_ManCiNum(pM) );
2170 assert( Gia_ManCoNum(pRes) == Gia_ManCoNum(pM) );
2171 return pRes;
2172}
2173
2185Vec_Str_t * Acb_GenerateInstance( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUsed, Vec_Int_t * vTars )
2186{
2187 int i, iObj;
2188 Vec_Str_t * vStr = Vec_StrAlloc( 100 );
2189 Vec_StrAppend( vStr, " patch p0 (" );
2190 Vec_IntForEachEntry( vTars, iObj, i )
2191 Vec_StrPrintF( vStr, "%s .%s(%s)", i ? ",":"", Acb_ObjNameStr(p, iObj), Acb_ObjNameStr(p, iObj) );
2192 Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i )
2193 Vec_StrPrintF( vStr, ", .%s(%s)", Acb_ObjNameStr(p, iObj), Acb_ObjNameStr(p, iObj) );
2194 Vec_StrAppend( vStr, " );\n\n" );
2195 Vec_StrPush( vStr, '\0' );
2196 return vStr;
2197}
2198Vec_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 )
2199{
2200 Vec_Ptr_t * vRes = Vec_PtrStart( Vec_IntSize(vUsed) + nNodes );
2201 Vec_Str_t * vStr = Vec_StrAlloc(1000); int i, iObj, nWires = 1;
2202 // create input names
2203 Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i )
2204 Vec_PtrWriteEntry( vRes, i, Abc_UtilStrsav(Acb_ObjNameStr(p, iObj)) );
2205 // create names for nodes driving outputs
2206 assert( Vec_WecSize(vGates) == Vec_IntSize(vUsed) + nNodes + Vec_IntSize(vTars) );
2207 Vec_IntForEachEntry( vTars, iObj, i )
2208 {
2209 Vec_Int_t * vGate = Vec_WecEntry( vGates, Vec_IntSize(vUsed) + nNodes + i );
2210 assert( Vec_IntEntry(vGate, 0) == ABC_OPER_BIT_BUF );
2211 Vec_PtrWriteEntry( vRes, Vec_IntEntry(vGate, 1), Abc_UtilStrsav(Acb_ObjNameStr(p, iObj)) );
2212 }
2213 for ( i = Vec_IntSize(vUsed); i < Vec_IntSize(vUsed) + nNodes; i++ )
2214 if ( Vec_PtrEntry(vRes, i) == NULL )
2215 {
2216 Vec_StrPrintF( vStr, "ww%d", nWires++ );
2217 Vec_StrPush( vStr, '\0' );
2218 Vec_PtrWriteEntry( vRes, i, Vec_StrReleaseArray(vStr) );
2219 }
2220 Vec_StrFree( vStr );
2221 return vRes;
2222}
2223Vec_Int_t * Acb_GetUsedDivs( Vec_Int_t * vDivs, Vec_Int_t * vUsed )
2224{
2225 int i, iObj;
2226 Vec_Int_t * vRes = Vec_IntAlloc( Vec_IntSize(vUsed) );
2227 Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i )
2228 Vec_IntPush( vRes, iObj );
2229 return vRes;
2230}
2231Vec_Ptr_t * Acb_SignalNames( Acb_Ntk_t * p, Vec_Int_t * vObjs )
2232{
2233 Vec_Ptr_t * vNames = Vec_PtrAlloc( Vec_IntSize(vObjs) );
2234 int i, iObj;
2235 Vec_IntForEachEntry( vObjs, iObj, i )
2236 Vec_PtrPush( vNames, Acb_ObjNameStr(p, iObj) );
2237 return vNames;
2238}
2239Vec_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 )
2240{
2241 extern int Acb_NtkCollectMfsGates( char * pFileName, Vec_Ptr_t * vNamesRefed, Vec_Ptr_t * vNamesDerefed, int nGates1[5] );
2242 extern Vec_Wec_t * Abc_SopSynthesize( Vec_Ptr_t * vSops );
2243 extern Vec_Wec_t * Abc_GiaSynthesize( Vec_Ptr_t * vGias, Gia_Man_t * pMulti );
2244 Vec_Wec_t * vGates = vGias ? Abc_GiaSynthesize(vGias, NULL) : Abc_SopSynthesize(vSops); Vec_Int_t * vGate;
2245 int nOuts = vGias ? Vec_PtrSize(vGias) : Vec_PtrSize(vSops);
2246 int i, k, iObj, nWires = Vec_WecSize(vGates) - Vec_IntSize(vUsed) - nOuts, fFirst = 1;
2247 int nGates1[5] = {0}, nGates0[5] = {0};
2248 Vec_Ptr_t * vNames = Acb_GenerateSignalNames( p, vDivs, vUsed, nWires, vTars, vGates );
2249 Vec_Str_t * vStr = Vec_StrAlloc( 100 );
2250 Vec_Int_t * vSup = Acb_GetUsedDivs( vDivs, vUsed );
2251 Vec_Ptr_t * vSpN = Acb_SignalNames( p, vSup );
2252 Vec_Int_t * vTfi = Acb_ObjCollectTfiVec( p, vSup );
2253 Vec_Int_t * vTfo = Acb_ObjCollectTfoVec( p, vTars );
2254 int nPiCount = Acb_NtkCountPiBuffers( p, vSup );
2255 int nPoCount = Acb_NtkCountPoDrivers( p, vTars );
2256 int nMffc = Abc_FrameReadSpecName() ? Acb_NtkCollectMfsGates( Abc_FrameReadSpecName(), vSpN, Abc_FrameReadSignalNames(), nGates1 ) : 0;
2257 Vec_PtrFree( vSpN );
2258 Vec_IntFree( vSup );
2259 Vec_WecForEachLevelStartStop( vGates, vGate, i, Vec_IntSize(vUsed), Vec_IntSize(vUsed)+nWires )
2260 {
2261 if ( Vec_IntSize(vGate) > 2 )
2262 {
2263 char * pName = Acb_Oper2Name(Vec_IntEntry(vGate, 0));
2264 if ( !strcmp(pName, "buf") )
2265 nGates0[2]++;
2266 else if ( !strcmp(pName, "not") )
2267 nGates0[3]++;
2268 else
2269 nGates0[4] += Vec_IntSize(vGate) - 3;
2270 }
2271 else
2272 nGates0[Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T]++;
2273 }
2274
2275 Vec_StrPrintF( vStr, "// Patch : in = %d out = %d : pi_in = %d po_out = %d : tfi = %d tfo = %d\n", Vec_IntSize(vUsed), nOuts, nPiCount, nPoCount, Vec_IntSize(vTfi), Vec_IntSize(vTfo) );
2276 Vec_StrPrintF( vStr, "// Added : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n", nWires, nGates0[0], nGates0[1], nGates0[2], nGates0[3], nGates0[4] );
2277 if ( Abc_FrameReadSpecName() )
2278 Vec_StrPrintF( vStr, "// Removed : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n", nMffc, nGates1[0], nGates1[1], nGates1[2], nGates1[3], nGates1[4] );
2279 if ( Abc_FrameReadSpecName() )
2280 Vec_StrPrintF( vStr, "// TOTAL : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n", nWires-nMffc, nGates0[0]-nGates1[0], nGates0[1]-nGates1[1], nGates0[2]-nGates1[2], nGates0[3]-nGates1[3], nGates0[4]-nGates1[4] );
2281 Vec_StrPrintF( vStr, "\n" );
2282
2283 Vec_StrAppend( vStr, "module patch (" );
2284
2285 assert( Vec_IntSize(vTars) == nOuts );
2286 Vec_IntForEachEntry( vTars, iObj, i )
2287 Vec_StrPrintF( vStr, "%s %s", i ? ",":"", Acb_ObjNameStr(p, iObj) );
2288 Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i )
2289 Vec_StrPrintF( vStr, ", %s", Acb_ObjNameStr(p, iObj) );
2290 Vec_StrAppend( vStr, " );\n\n" );
2291
2292 Vec_StrAppend( vStr, " output" );
2293 Vec_IntForEachEntry( vTars, iObj, i )
2294 Vec_StrPrintF( vStr, "%s %s", i ? ",":"", Acb_ObjNameStr(p, iObj) );
2295 Vec_StrAppend( vStr, ";\n" );
2296
2297 Vec_StrAppend( vStr, " input" );
2298 Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i )
2299 Vec_StrPrintF( vStr, "%s %s", i ? ",":"", Acb_ObjNameStr(p, iObj) );
2300 Vec_StrAppend( vStr, ";\n" );
2301
2302 if ( nWires > nOuts )
2303 {
2304 Vec_StrAppend( vStr, " wire" );
2305 for ( i = 0; i < nWires; i++ )
2306 {
2307 char * pName = (char *)Vec_PtrEntry( vNames, Vec_IntSize(vUsed)+i );
2308 if ( !strncmp(pName, "ww", 2) )
2309 Vec_StrPrintF( vStr, "%s %s", fFirst ? "":",", pName ), fFirst = 0;
2310 }
2311 Vec_StrAppend( vStr, ";\n\n" );
2312 }
2313
2314 // create internal nodes
2315 Vec_WecForEachLevelStartStop( vGates, vGate, i, Vec_IntSize(vUsed), Vec_IntSize(vUsed)+nWires )
2316 {
2317 if ( Vec_IntSize(vGate) > 2 )
2318 {
2319 Vec_StrPrintF( vStr, " %s (", Acb_Oper2Name(Vec_IntEntry(vGate, 0)) );
2320 Vec_IntForEachEntryStart( vGate, iObj, k, 1 )
2321 Vec_StrPrintF( vStr, "%s %s", k > 1 ? ",":"", (char *)Vec_PtrEntry(vNames, iObj) );
2322 Vec_StrAppend( vStr, " );\n" );
2323 }
2324 else
2325 {
2326 assert( Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_F || Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T );
2327 Vec_StrPrintF( vStr, " %s (", Acb_Oper2Name( ABC_OPER_BIT_BUF ) );
2328 Vec_StrPrintF( vStr, " %s, ", (char *)Vec_PtrEntry(vNames, Vec_IntEntry(vGate, 1)) );
2329 Vec_StrPrintF( vStr, " 1\'b%d", Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T );
2330 Vec_StrPrintF( vStr, " );\n" );
2331 }
2332 }
2333 Vec_StrAppend( vStr, "\nendmodule\n\n" );
2334 Vec_StrPush( vStr, '\0' );
2335 Vec_PtrFreeFree( vNames );
2336 Vec_WecFree( vGates );
2337
2338// printf( "Synthesized patch with %d inputs, %d outputs and %d gates (const = %d buf = %d inv = %d other = %d).\n",
2339// Vec_IntSize(vUsed), nOuts, nWires, nConst, nBufs, nInvs, nNodes );
2340// printf( "Summary of the results\n" );
2341 printf( "\n" );
2342 printf( "Patch : in = %d out = %d : pi_in = %d po_out = %d : tfi = %d tfo = %d\n", Vec_IntSize(vUsed), nOuts, nPiCount, nPoCount, Vec_IntSize(vTfi), Vec_IntSize(vTfo) );
2343 printf( "Added : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n", nWires, nGates0[0], nGates0[1], nGates0[2], nGates0[3], nGates0[4] );
2344 if ( Abc_FrameReadSpecName() )
2345 printf( "Removed : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n", nMffc, nGates1[0], nGates1[1], nGates1[2], nGates1[3], nGates1[4] );
2346 if ( Abc_FrameReadSpecName() )
2347 printf( "TOTAL : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n", nWires-nMffc, nGates0[0]-nGates1[0], nGates0[1]-nGates1[1], nGates0[2]-nGates1[2], nGates0[3]-nGates1[3], nGates0[4]-nGates1[4] );
2348 printf( "\n" );
2349 return vStr;
2350}
2351
2363Vec_Str_t * Acb_GenerateInstance2( Vec_Ptr_t * vIns, Vec_Ptr_t * vOuts )
2364{
2365 char * pName; int i;
2366 Vec_Str_t * vStr = Vec_StrAlloc( 100 );
2367 Vec_StrAppend( vStr, " patch p0 (" );
2368 Vec_PtrForEachEntry( char *, vOuts, pName, i )
2369 Vec_StrPrintF( vStr, "%s .%s(t%d_%s)", i ? ",":"", pName, i, pName );
2370 Vec_PtrForEachEntry( char *, vIns, pName, i )
2371 Vec_StrPrintF( vStr, ", .%s(%s)", pName, pName );
2372 Vec_StrAppend( vStr, " );\n\n" );
2373 Vec_StrPush( vStr, '\0' );
2374 return vStr;
2375}
2376Vec_Ptr_t * Acb_GenerateSignalNames2( Vec_Wec_t * vGates, Vec_Ptr_t * vIns, Vec_Ptr_t * vOuts )
2377{
2378 int nIns = Vec_PtrSize(vIns), nOuts = Vec_PtrSize(vOuts);
2379 int nNodes = Vec_WecSize(vGates) - nIns - nOuts;
2380 Vec_Ptr_t * vRes = Vec_PtrStart( Vec_WecSize(vGates) ); char * pName;
2381 Vec_Str_t * vStr = Vec_StrAlloc(1000); int i, nWires = 1;
2382 // create input names
2383 Vec_PtrForEachEntry( char *, vIns, pName, i )
2384 Vec_PtrWriteEntry( vRes, i, Abc_UtilStrsav(pName) );
2385 // create names for nodes driving outputs
2386 Vec_PtrForEachEntry( char *, vOuts, pName, i )
2387 {
2388 Vec_Int_t * vGate = Vec_WecEntry( vGates, nIns + nNodes + i );
2389 assert( Vec_IntEntry(vGate, 0) == ABC_OPER_BIT_BUF );
2390 Vec_PtrWriteEntry( vRes, Vec_IntEntry(vGate, 1), Abc_UtilStrsav(pName) );
2391 }
2392 for ( i = nIns; i < nIns + nNodes; i++ )
2393 if ( Vec_PtrEntry(vRes, i) == NULL )
2394 {
2395 Vec_StrPrintF( vStr, "ww%d", nWires++ );
2396 Vec_StrPush( vStr, '\0' );
2397 Vec_PtrWriteEntry( vRes, i, Vec_StrReleaseArray(vStr) );
2398 }
2399 Vec_StrFree( vStr );
2400 return vRes;
2401}
2402Vec_Str_t * Acb_GeneratePatch2( Gia_Man_t * pGia, Vec_Ptr_t * vIns, Vec_Ptr_t * vOuts )
2403{
2404 extern Vec_Wec_t * Abc_GiaSynthesize( Vec_Ptr_t * vGias, Gia_Man_t * pMulti );
2405 Vec_Wec_t * vGates = Abc_GiaSynthesize( NULL, pGia ); Vec_Int_t * vGate;
2406 int nIns = Vec_PtrSize(vIns), nOuts = Vec_PtrSize(vOuts); char * pName;
2407 int i, k, iObj, nWires = Vec_WecSize(vGates) - nIns - nOuts, nTwoIns = 0, fFirst = 1;
2408 Vec_Ptr_t * vNames = Acb_GenerateSignalNames2( vGates, vIns, vOuts );
2409
2410 Vec_Str_t * vStr = Vec_StrAlloc( 100 );
2411 Vec_StrAppend( vStr, "module patch (" );
2412
2413 Vec_PtrForEachEntry( char *, vOuts, pName, i )
2414 Vec_StrPrintF( vStr, "%s %s", i ? ",":"", pName );
2415 Vec_PtrForEachEntry( char *, vIns, pName, i )
2416 Vec_StrPrintF( vStr, ", %s%s", i ? "":" ", pName );
2417 Vec_StrAppend( vStr, " );\n\n" );
2418
2419 Vec_StrAppend( vStr, " output" );
2420 Vec_PtrForEachEntry( char *, vOuts, pName, i )
2421 Vec_StrPrintF( vStr, "%s %s", i ? ",":"", pName );
2422 Vec_StrAppend( vStr, ";\n" );
2423
2424 Vec_StrAppend( vStr, " input" );
2425 Vec_PtrForEachEntry( char *, vIns, pName, i )
2426 Vec_StrPrintF( vStr, "%s %s", i ? ",":"", pName );
2427 Vec_StrAppend( vStr, ";\n" );
2428
2429 if ( nWires > nOuts )
2430 {
2431 Vec_StrAppend( vStr, " wire" );
2432 for ( i = 0; i < nWires; i++ )
2433 {
2434 char * pName = (char *)Vec_PtrEntry( vNames, nIns+i );
2435 if ( !strncmp(pName, "ww", 2) )
2436 Vec_StrPrintF( vStr, "%s %s", fFirst ? "":",", pName ), fFirst = 0;
2437 }
2438 Vec_StrAppend( vStr, ";\n" );
2439 }
2440 Vec_StrAppend( vStr, "\n" );
2441
2442 // create internal nodes
2443 Vec_WecForEachLevelStartStop( vGates, vGate, i, nIns, nIns+nWires )
2444 {
2445 if ( Vec_IntSize(vGate) > 2 )
2446 {
2447 Vec_StrPrintF( vStr, " %s (", Acb_Oper2Name(Vec_IntEntry(vGate, 0)) );
2448 Vec_IntForEachEntryStart( vGate, iObj, k, 1 )
2449 Vec_StrPrintF( vStr, "%s %s", k > 1 ? ",":"", (char *)Vec_PtrEntry(vNames, iObj) );
2450 Vec_StrAppend( vStr, " );\n" );
2451 nTwoIns += Vec_IntSize(vGate) - 3;
2452 }
2453 else
2454 {
2455 assert( Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_F || Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T );
2456 Vec_StrPrintF( vStr, " %s (", Acb_Oper2Name( ABC_OPER_BIT_BUF ) );
2457 Vec_StrPrintF( vStr, " %s, ", (char *)Vec_PtrEntry(vNames, Vec_IntEntry(vGate, 1)) );
2458 Vec_StrPrintF( vStr, " 1\'b%d", Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T );
2459 Vec_StrPrintF( vStr, " );\n" );
2460 }
2461 }
2462 Vec_StrAppend( vStr, "\nendmodule\n\n" );
2463 Vec_StrPush( vStr, '\0' );
2464 Vec_PtrFreeFree( vNames );
2465 Vec_WecFree( vGates );
2466
2467 printf( "Synthesized patch with %d inputs, %d outputs and %d gates (including %d two-input gates).\n", nIns, nOuts, nWires, nTwoIns );
2468 return vStr;
2469}
2470void Acb_GenerateFile2( Gia_Man_t * pGia, Vec_Ptr_t * vIns, Vec_Ptr_t * vOuts, char * pFileName, char * pFileNameOut, int fSkipMffc )
2471{
2472 extern void Acb_GenerateFilePatch( Vec_Str_t * p, char * pFileNamePatch );
2473 extern void Acb_GenerateFileOut( Vec_Str_t * vPatchLine, char * pFileNameF, char * pFileNameOut, Vec_Str_t * vPatch );
2474 extern void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames, int fNumber, int fSkipMffc );
2475 Vec_Str_t * vInst = Acb_GenerateInstance2( vIns, vOuts );
2476 Vec_Str_t * vPatch = Acb_GeneratePatch2( pGia, vIns, vOuts );
2477 //printf( "%s", Vec_StrArray(vPatch) );
2478 //Gia_AigerWrite( pGia, "test.aig", 0, 0, 0 );
2479 // generate output files
2480 Acb_GenerateFilePatch( vPatch, "patch.v" );
2481 printf( "Finished dumping patch file \"%s\".\n", "patch.v" );
2482 Acb_NtkInsert( pFileName, "temp.v", vOuts, 0, fSkipMffc );
2483 printf( "Finished dumping intermediate file \"%s\".\n", "temp.v" );
2484 Acb_GenerateFileOut( vInst, "temp.v", pFileNameOut, vPatch );
2485 printf( "Finished dumping the resulting file \"%s\".\n", pFileNameOut );
2486 Vec_StrFree( vInst );
2487 Vec_StrFree( vPatch );
2488}
2489
2501void Acb_GenerateFilePatch( Vec_Str_t * p, char * pFileNamePatch )
2502{
2503 FILE * pFile = fopen( pFileNamePatch, "wb" );
2504 if ( !pFile )
2505 return;
2506 fprintf( pFile, "%s", Vec_StrArray(p) );
2507 fclose( pFile );
2508}
2509void Acb_GenerateFileOut( Vec_Str_t * vPatchLine, char * pFileNameF, char * pFileNameOut, Vec_Str_t * vPatch )
2510{
2511 FILE * pFileOut;
2512 char * pBuffer = Extra_FileReadContents( pFileNameF );
2513 if ( pBuffer == NULL )
2514 return;
2515 pFileOut = fopen( pFileNameOut, "wb" );
2516 if ( pFileOut )
2517 {
2518 char * pTemp = strstr( pBuffer, "endmodule" );
2519 int nFirst = pTemp-pBuffer, nSecond = strlen(pBuffer) - nFirst;
2520 int Value = fwrite( pBuffer, nFirst, 1, pFileOut );
2521 fprintf( pFileOut, "\n%s", Vec_StrArray(vPatchLine) );
2522 Value = fwrite( pBuffer+nFirst, nSecond, 1, pFileOut );
2523 if ( vPatch )
2524 fprintf( pFileOut, "\n%s\n", Vec_StrArray(vPatch) );
2525 }
2526 ABC_FREE( pBuffer );
2527 fclose( pFileOut );
2528}
2529
2541void Acb_PrintPatch( Acb_Ntk_t * pNtkF, Vec_Int_t * vDivs, Vec_Int_t * vUsed, abctime clk )
2542{
2543 int i, iObj, Weight = 0;
2544 printf( "Patch has %d inputs: ", Vec_IntSize(vUsed) );
2545 Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i )
2546 {
2547 printf( "%d=%s(w=%d) ", Vec_IntEntry(vUsed, i), Acb_ObjNameStr(pNtkF, iObj), Acb_ObjWeight(pNtkF, iObj) );
2548 Weight += Acb_ObjWeight(pNtkF, iObj);
2549 }
2550 printf( "\nTotal weight = %d ", Weight );
2551 Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clk );
2552 printf( "\n" );
2553}
2554
2566Gia_Man_t * Acb_NtkEcoSynthesize( Gia_Man_t * p )
2567{
2568 int Iter, fVerbose = 0;
2569 Gia_Man_t * pNew = Gia_ManDup( p );
2570
2571 if ( fVerbose ) printf( "M_quo: " );
2572 if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
2573
2574 pNew = Gia_ManAreaBalance( p = pNew, 0, 0, 0, 0 );
2575 Gia_ManStop( p );
2576
2577 if ( fVerbose ) printf( "M_bal: " );
2578 if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
2579
2580 for ( Iter = 0; Iter < 2; Iter++ )
2581 {
2582 pNew = Gia_ManCompress2( p = pNew, 1, 0 );
2583 Gia_ManStop( p );
2584
2585 if ( fVerbose ) printf( "M_dc2: " );
2586 if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
2587 }
2588
2589 pNew = Gia_ManAigSyn2( p = pNew, 0, 1, 0, 100, 0, 0, 0 );
2590 Gia_ManStop( p );
2591
2592 if ( fVerbose ) printf( "M_sn2: " );
2593 if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
2594
2595 for ( Iter = 0; Iter < 2; Iter++ )
2596 {
2597 pNew = Gia_ManCompress2( p = pNew, 1, 0 );
2598 Gia_ManStop( p );
2599
2600 if ( fVerbose ) printf( "M_dc2: " );
2601 if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
2602 }
2603 return pNew;
2604}
2605Cnf_Dat_t * Acb_NtkDeriveMiterCnf( Gia_Man_t * p, int iTar, int nTars, int fVerbose )
2606{
2607 Gia_Man_t * pCof = Gia_ManDup( p );
2608 Cnf_Dat_t * pCnf; int v;
2609 for ( v = 0; v < iTar; v++ )
2610 {
2611 Gia_Man_t * pTemp;
2612 pCof = Gia_ManDupUniv( p = pCof, Gia_ManCiNum(pCof) - nTars + v );
2613 //pCof = Acb_NtkEcoSynthesize( pTemp = pCof );
2614 //pCof = Gia_ManCompress2( pTemp = pCof, 1, 0 );
2615 pCof = Gia_ManAigSyn2( pTemp = pCof, 0, 1, 0, 100, 0, 0, 0 );
2616 Gia_ManStop( pTemp );
2617 if ( Gia_ManAndNum(pCof) > 10000 )
2618 {
2619 printf( "Quantifying target %3d ", v );
2620 Gia_ManPrintStats( pCof, NULL );
2621 }
2622 assert( Gia_ManCiNum(pCof) == Gia_ManCiNum(p) );
2623 Gia_ManStop( p );
2624 }
2625 if ( fVerbose ) printf( "M_quo: " );
2626 if ( fVerbose ) Gia_ManPrintStats( pCof, NULL );
2627 //pCof = Acb_NtkEcoSynthesize( p = pCof );
2628 //Gia_ManStop( p );
2629 if ( fVerbose ) printf( "M_syn: " );
2630 if ( fVerbose ) Gia_ManPrintStats( pCof, NULL );
2631 if ( 0 && iTar < nTars )
2632 {
2633 Gia_Man_t * pCof0 = Gia_ManDupCofactorVar( pCof, Gia_ManCiNum(pCof) - nTars + iTar, 0 );
2634 Gia_Man_t * pCof1 = Gia_ManDupCofactorVar( pCof, Gia_ManCiNum(pCof) - nTars + iTar, 1 );
2635 pCof0 = Acb_NtkEcoSynthesize( p = pCof0 );
2636 Gia_ManStop( p );
2637 pCof1 = Acb_NtkEcoSynthesize( p = pCof1 );
2638 Gia_ManStop( p );
2639 Gia_AigerWrite( pCof0, "eco_qbf0.aig", 0, 0, 0 );
2640 Gia_AigerWrite( pCof1, "eco_qbf1.aig", 0, 0, 0 );
2641 Gia_ManStop( pCof0 );
2642 Gia_ManStop( pCof1 );
2643 printf( "Dumped cof0 into file \"%s\".\n", "eco_qbf0.aig" );
2644 printf( "Dumped cof1 into file \"%s\".\n", "eco_qbf1.aig" );
2645 }
2646// Gia_AigerWrite( pCof, "eco_qbf.aig", 0, 0, 0 );
2647// printf( "Dumped the result of quantification into file \"%s\".\n", "eco_qbf.aig" );
2648 pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCof, 8, 0, 0, 0, 0 );
2649 Gia_ManStop( pCof );
2650 return pCnf;
2651}
2652Gia_Man_t * Gia_ManInterOneInt( Gia_Man_t * pCof1, Gia_Man_t * pCof0, int Depth )
2653{
2654 extern Gia_Man_t * Gia_ManInterOne( Gia_Man_t * pNtkOn, Gia_Man_t * pNtkOff, int fVerbose );
2655 extern Gia_Man_t * Abc_GiaSynthesizeInter( Gia_Man_t * p );
2656 Gia_Man_t * pGia[2] = { pCof0, pCof1 };
2657 Gia_Man_t * pCof[2][2] = {{0}}, * pTemp;
2658 Gia_Man_t * pInter[2], * pFinal;
2659 Gia_Obj_t * pObj;
2660 int i, n, m, Count, CountBest = 0, iVarBest = -1;
2661 // find PIs with the highest fanout
2662 Vec_Int_t * vFanCount;
2663 if ( Gia_ManAndNum(pCof1) == 0 || Gia_ManAndNum(pCof0) == 0 )
2664 return Gia_ManDup(pCof1);
2665 vFanCount = Vec_IntStart( Gia_ManCiNum(pCof0) );
2666 for ( n = 0; n < 2; n++ )
2667 {
2668 Gia_ManForEachAnd( pGia[n], pObj, i )
2669 {
2670 if ( Gia_ObjIsCi(Gia_ObjFanin0(pObj)) )
2671 Vec_IntAddToEntry( vFanCount, Gia_ObjCioId(Gia_ObjFanin0(pObj)), 1 );
2672 if ( Gia_ObjIsCi(Gia_ObjFanin1(pObj)) )
2673 Vec_IntAddToEntry( vFanCount, Gia_ObjCioId(Gia_ObjFanin1(pObj)), 1 );
2674 }
2675 }
2676 Vec_IntForEachEntry( vFanCount, Count, i )
2677 if ( CountBest < Count )
2678 {
2679 CountBest = Count;
2680 iVarBest = i;
2681 }
2682 Vec_IntFree( vFanCount );
2683 // Gia_Man_t * Gia_ManDupCofactorVar( Gia_Man_t * p, int iVar, int Value )
2684 for ( n = 0; n < 2; n++ )
2685 for ( m = 0; m < 2; m++ )
2686 {
2687 pCof[n][m] = Gia_ManDupCofactorVar( pGia[n], iVarBest, m );
2688 pCof[n][m] = Acb_NtkEcoSynthesize( pTemp = pCof[n][m] );
2689 Gia_ManStop( pTemp );
2690 printf( "%*sCof%d%d : ", 8-Depth, "", n, m );
2691 Gia_ManPrintStats( pCof[n][m], NULL );
2692 }
2693 for ( m = 0; m < 2; m++ )
2694 {
2695 if ( Gia_ManAndNum(pCof[1][m]) == 0 || Gia_ManAndNum(pCof[0][m]) == 0 )
2696 pInter[m] = Gia_ManDup( pCof[1][m] );
2697 else if ( Depth == 1 )
2698 pInter[m] = Gia_ManInterOne( pCof[1][m], pCof[0][m], 1 );
2699 else
2700 pInter[m] = Gia_ManInterOneInt( pCof[1][m], pCof[0][m], Depth-1 );
2701 printf( "%*sInter%d : ", 8-Depth, "", m );
2702 Gia_ManPrintStats( pInter[m], NULL );
2703 pInter[m] = Abc_GiaSynthesizeInter( pTemp = pInter[m] );
2704 Gia_ManStop( pTemp );
2705 printf( "%*sInter%d : ", 8-Depth, "", m );
2706 Gia_ManPrintStats( pInter[m], NULL );
2707 }
2708 for ( n = 0; n < 2; n++ )
2709 for ( m = 0; m < 2; m++ )
2710 Gia_ManStop( pCof[n][m] );
2711 pFinal = Gia_ManDupMux( iVarBest, pInter[1], pInter[0] );
2712 for ( m = 0; m < 2; m++ )
2713 Gia_ManStop( pInter[m] );
2714 return pFinal;
2715}
2716Gia_Man_t * Acb_NtkDeriveMiterCnfInter2( Gia_Man_t * p, int iTar, int nTars )
2717{
2718// extern Gia_Man_t * Gia_ManInterOne( Gia_Man_t * pNtkOn, Gia_Man_t * pNtkOff, int fVerbose );
2719 extern Gia_Man_t * Abc_GiaSynthesizeInter( Gia_Man_t * p );
2720 Gia_Man_t * pInter, * pCof0, * pCof1, * pCof = Gia_ManDup( p ); int v;
2721 for ( v = 0; v < iTar; v++ )
2722 {
2723 pCof = Gia_ManDupUniv( p = pCof, Gia_ManCiNum(pCof) - nTars + v );
2724 assert( Gia_ManCiNum(pCof) == Gia_ManCiNum(p) );
2725 Gia_ManStop( p );
2726
2727 pCof = Acb_NtkEcoSynthesize( p = pCof );
2728 Gia_ManStop( p );
2729 }
2730 pCof0 = Gia_ManDupCofactorVar( pCof, Gia_ManCiNum(pCof) - nTars + iTar, 1 );
2731 pCof1 = Gia_ManDupCofactorVar( pCof, Gia_ManCiNum(pCof) - nTars + iTar, 0 );
2732 Gia_ManStop( pCof );
2733 pCof0 = Acb_NtkEcoSynthesize( p = pCof0 );
2734 Gia_ManStop( p );
2735 pCof1 = Acb_NtkEcoSynthesize( p = pCof1 );
2736 Gia_ManStop( p );
2737
2738 printf( "Cof0 : " );
2739 Gia_ManPrintStats( pCof0, NULL );
2740 printf( "Cof1 : " );
2741 Gia_ManPrintStats( pCof1, NULL );
2742
2743 if ( Gia_ManAndNum(pCof1) == 0 || Gia_ManAndNum(pCof0) == 0 )
2744 pInter = Gia_ManDup(pCof1);
2745 else
2746 pInter = Gia_ManInterOneInt( pCof1, pCof0, 7 );
2747 Gia_ManStop( pCof0 );
2748 Gia_ManStop( pCof1 );
2749 pInter = Abc_GiaSynthesizeInter( p = pInter );
2750 Gia_ManStop( p );
2751 //Gia_ManPrintStats( pInter, NULL );
2752 pInter = Gia_ManDupRemovePis( p = pInter, nTars );
2753 Gia_ManStop( p );
2754 //Gia_ManPrintStats( pInter, NULL );
2755 return pInter;
2756}
2757Gia_Man_t * Acb_NtkDeriveMiterCnfInter( Gia_Man_t * p, int iTar, int nTars )
2758{
2759 Gia_Man_t * pCof1, * pCof = Gia_ManDup( p ); int v;
2760 for ( v = 0; v < iTar; v++ )
2761 {
2762 pCof = Gia_ManDupUniv( p = pCof, Gia_ManCiNum(pCof) - nTars + v );
2763 assert( Gia_ManCiNum(pCof) == Gia_ManCiNum(p) );
2764 Gia_ManStop( p );
2765
2766 pCof = Acb_NtkEcoSynthesize( p = pCof );
2767 Gia_ManStop( p );
2768 }
2769 pCof1 = Gia_ManDupCofactorVar( pCof, Gia_ManCiNum(pCof) - nTars + iTar, 0 );
2770 Gia_ManStop( pCof );
2771
2772 pCof1 = Acb_NtkEcoSynthesize( p = pCof1 );
2773 Gia_ManStop( p );
2774
2775 pCof1 = Gia_ManDupRemovePis( p = pCof1, nTars );
2776 Gia_ManStop( p );
2777 return pCof1;
2778}
2779
2791char * Acb_RemapOneFunction( char * pStr, Vec_Int_t * vSupp, Vec_Int_t * vMap, int nVars )
2792{
2793 Vec_Str_t * vTempSop = Vec_StrAlloc( 100 );
2794 char * pToken = strtok( pStr, "\n" ); int i;
2795 while ( pToken != NULL )
2796 {
2797 for ( i = 0; i < nVars; i++ )
2798 Vec_StrPush( vTempSop, '-' );
2799 for ( i = 0; pToken[i] != ' '; i++ )
2800 if ( pToken[i] != '-' )
2801 {
2802 int iVar = Vec_IntEntry( vMap, Vec_IntEntry(vSupp, i) );
2803 assert( iVar >= 0 && iVar < nVars );
2804 Vec_StrWriteEntry( vTempSop, Vec_StrSize(vTempSop) - nVars + iVar, pToken[i] );
2805 }
2806 Vec_StrPrintF( vTempSop, " %d\n", pToken[i+1] - '0' );
2807 pToken = strtok( NULL, "\n" );
2808 }
2809 Vec_StrPush( vTempSop, '\0' );
2810 pToken = Vec_StrReleaseArray(vTempSop);
2811 Vec_StrFree( vTempSop );
2812 return pToken;
2813}
2814Vec_Ptr_t * Acb_TransformPatchFunctions( Vec_Ptr_t * vSops, Vec_Wec_t * vSupps, Vec_Int_t ** pvUsed, int nDivs )
2815{
2816 Vec_Ptr_t * vFuncs = Vec_PtrAlloc( Vec_PtrSize(vSops) );
2817 Vec_Int_t * vUsed = Vec_IntAlloc( 100 );
2818 Vec_Int_t * vMap = Vec_IntStartFull( nDivs );
2819 Vec_Int_t * vPres = Vec_IntStart( nDivs );
2820 Vec_Int_t * vLevel;
2821 int i, k, iVar;
2822 // check what divisors are used
2823 Vec_WecForEachLevel( vSupps, vLevel, i )
2824 {
2825 char * pSop = (char *)Vec_PtrEntry( vSops, i );
2826 char * pStrCopy = Abc_UtilStrsav( pSop );
2827 char * pToken = strtok( pStrCopy, "\n" );
2828 while ( pToken != NULL )
2829 {
2830 for ( k = 0; pToken[k] != ' '; k++ )
2831 if ( pToken[k] != '-' )
2832 Vec_IntWriteEntry( vPres, Vec_IntEntry(vLevel, k), 1 );
2833 pToken = strtok( NULL, "\n" );
2834 }
2835 ABC_FREE( pStrCopy );
2836 }
2837 // create common order
2838 Vec_WecForEachLevel( vSupps, vLevel, i )
2839 Vec_IntForEachEntry( vLevel, iVar, k )
2840 {
2841 if ( !Vec_IntEntry(vPres, iVar) )
2842 continue;
2843 if ( Vec_IntEntry(vMap, iVar) >= 0 )
2844 continue;
2845 Vec_IntWriteEntry( vMap, iVar, Vec_IntSize(vUsed) );
2846 Vec_IntPush( vUsed, iVar );
2847 }
2848 //printf( "The number of used variables %d (out of %d).\n", Vec_IntSum(vPres), Vec_IntSize(vPres) );
2849 // remap SOPs
2850 Vec_WecForEachLevel( vSupps, vLevel, i )
2851 {
2852 char * pSop = (char *)Vec_PtrEntry( vSops, i );
2853 pSop = Acb_RemapOneFunction( pSop, vLevel, vMap, Vec_IntSize(vUsed) );
2854 //printf( "Function %d\n%s", i, pSop );
2855 Vec_PtrPush( vFuncs, pSop );
2856 }
2857 Vec_IntFree( vPres );
2858 Vec_IntFree( vMap );
2859 *pvUsed = vUsed;
2860 return vFuncs;
2861}
2862
2874int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4], int nTimeout, int fCisOnly, int fInputs, int fCheck, int fUnitW, int fVerbose, int fVeryVerbose )
2875{
2876 extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp );
2877
2878 abctime clkStart = Abc_Clock();
2879 abctime clk = Abc_Clock();
2880 int nTargets = Vec_IntSize(&pNtkF->vTargets);
2881 int TimeOut = fCisOnly ? 0 : 120; // 60 seconds
2882 int RetValue = 1;
2883
2884 // compute various sets of nodes
2885 Vec_Bit_t * vBlock;
2886 Vec_Int_t * vRoots = Acb_NtkFindRoots( pNtkF, &pNtkF->vTargets, &vBlock );
2887 Vec_Int_t * vSuppF = Acb_NtkFindSupp( pNtkF, vRoots );
2888 Vec_Int_t * vSuppG = Acb_NtkFindSupp( pNtkG, vRoots );
2889 Vec_Int_t * vSupp = Vec_IntTwoMerge( vSuppF, vSuppG );
2890 Vec_Int_t * vDivs = (fCisOnly || fInputs) ? Acb_NtkFindDivsCis( pNtkF, vSupp ) : Acb_NtkFindDivs( pNtkF, vSupp, vBlock, fUnitW, fVerbose );
2891 Vec_Int_t * vNodesF = Acb_NtkFindNodes( pNtkF, vRoots, vDivs );
2892 Vec_Int_t * vNodesG = Acb_NtkFindNodes( pNtkG, vRoots, NULL );
2893
2894 // create AIGs
2895 Gia_Man_t * pGiaF = Acb_NtkToGia( pNtkF, vSupp, vNodesF, vRoots, vDivs, &pNtkF->vTargets );
2896 Gia_Man_t * pGiaG = Acb_NtkToGia( pNtkG, vSupp, vNodesG, vRoots, NULL, NULL );
2897 Gia_Man_t * pGiaM = Acb_CreateMiter( pGiaF, pGiaG );
2898
2899 Cnf_Dat_t * pCnf;
2900 Gia_Man_t * pTemp, * pOne;
2901 Vec_Ptr_t * vSops = Vec_PtrAlloc( nTargets );
2902 Vec_Wec_t * vSupps = Vec_WecAlloc( nTargets );
2903 Vec_Int_t * vSuppOld = Vec_IntAlloc( 100 );
2904
2905 Vec_Int_t * vUsed = NULL;
2906 Vec_Ptr_t * vFuncs = NULL;
2907 Vec_Ptr_t * vGias = fCisOnly ? Vec_PtrAlloc(nTargets) : NULL;
2908 Vec_Str_t * vInst = NULL, * vPatch = NULL;
2909
2910 char * pSop = NULL;
2911 int i;
2912
2913// int Value = Acb_NtkSaveNames( pNtkF, vSupp, vNodesF, vRoots, vDivs, &pNtkF->vTargets, pGiaF );
2914// Gia_AigerWrite( pGiaF, pFileBase, 0, 0, 0 );
2915// return 0;
2916
2917 if ( fVerbose )
2918 {
2919 printf( "The number of targets = %d.\n", nTargets );
2920
2921 printf( "NtkF: " );
2922 Gia_ManPrintStats( pGiaF, NULL );
2923 printf( "NtkG: " );
2924 Gia_ManPrintStats( pGiaG, NULL );
2925 printf( "Miter: " );
2926 Gia_ManPrintStats( pGiaM, NULL );
2927 }
2928
2929 // check that the problem has a solution
2930 if ( fCheck )//fCisOnly )
2931 {
2932 int Lit, status;
2933 sat_solver * pSat;
2934 pCnf = Acb_NtkDeriveMiterCnf( pGiaM, nTargets, nTargets, fVerbose );
2935 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
2936 Cnf_DataFree( pCnf );
2937 // add output clause
2938 Lit = Abc_Var2Lit( 1, 0 );
2939 status = sat_solver_addclause( pSat, &Lit, &Lit+1 );
2940 status = status == 0 ? l_False : sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
2941 sat_solver_delete( pSat );
2942 printf( "The ECO problem has %s solution. ", status == l_False ? "a" : "NO" );
2943 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2944 if ( status != l_False )
2945 {
2946 RetValue = 0;
2947 goto cleanup;
2948 }
2949 }
2950
2951 for ( i = nTargets-1; i >= 0; i-- )
2952 {
2953 Vec_Int_t * vSupp = NULL;
2954 printf( "\nConsidering target %d (out of %d)...\n", i, nTargets );
2955 // compute support of this target
2956 if ( fCisOnly )
2957 {
2958 vSupp = Vec_IntStartNatural( Vec_IntSize(vDivs) );
2959 printf( "Target %d has support with %d variables.\n", i, Vec_IntSize(vSupp) );
2960
2961 pOne = Acb_NtkDeriveMiterCnfInter( pGiaM, i, nTargets );
2962 printf( "Tar%02d: ", i );
2963 Gia_ManPrintStats( pOne, NULL );
2964
2965 // update miter
2966 pGiaM = Acb_UpdateMiter( pTemp = pGiaM, pOne, i, nTargets, vSupp, fCisOnly );
2967 Gia_ManStop( pTemp );
2968
2969 // add to functions
2970 Vec_PtrPush( vGias, pOne );
2971 }
2972 else
2973 {
2974 pCnf = Acb_NtkDeriveMiterCnf( pGiaM, i, nTargets, fVerbose );
2975// vSupp = Acb_DerivePatchSupportS( pCnf, i, nTargets, Vec_IntSize(vDivs), vDivs, pNtkF, NULL, TimeOut );
2976 vSupp = Acb_DerivePatchSupport( pCnf, i, nTargets, Vec_IntSize(vDivs), vDivs, pNtkF, vSuppOld, TimeOut );
2977 if ( vSupp == NULL )
2978 {
2979 Cnf_DataFree( pCnf );
2980 RetValue = 0;
2981 goto cleanup;
2982 }
2983 Vec_IntAppend( vSuppOld, vSupp );
2984 Vec_IntClear( vSupp );
2985 Vec_IntAppend( vSupp, vSuppOld );
2986 //Vec_IntClear( vSuppOld );
2987
2988 // derive function of this target
2989 pSop = Acb_DeriveOnePatchFunction( pCnf, i, nTargets, Vec_IntSize(vDivs), vSupp, fCisOnly );
2990 Cnf_DataFree( pCnf );
2991 if ( pSop == NULL )
2992 {
2993 RetValue = 0;
2994 goto cleanup;
2995 }
2996 if ( nTimeout && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= nTimeout )
2997 {
2998 Vec_IntFreeP( &vSupp );
2999 ABC_FREE( pSop );
3000 printf( "The target computation timed out after %d seconds.\n", nTimeout );
3001 RetValue = 0;
3002 goto cleanup;
3003 }
3004
3005 // add new function to the miter
3006 pOne = Abc_SopSynthesizeOne( pSop, 1 );
3007 printf( "Tar%02d: ", i );
3008 Gia_ManPrintStats( pOne, NULL );
3009
3010 // update miter
3011 pGiaM = Acb_UpdateMiter( pTemp = pGiaM, pOne, i, nTargets, vSupp, fCisOnly );
3012 Gia_ManStop( pTemp );
3013 Gia_ManStop( pOne );
3014
3015 // add to functions
3016 Vec_PtrPush( vSops, pSop );
3017 if ( fVeryVerbose )
3018 printf( "Function %d\n%s", i, pSop );
3019 }
3020 // add to supports
3021 Vec_IntAppend( Vec_WecPushLevel(vSupps), vSupp );
3022 Vec_IntFree( vSupp );
3023 }
3024
3025 // make sure the function is UNSAT
3026 printf( "\n" );
3027 if ( !fCisOnly )
3028 {
3029 int Res;
3030 abctime clk = Abc_Clock();
3031 pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGiaM, 8, 0, 0, 0, 0 );
3032 Res = Acb_CheckMiter( pCnf );
3033 Cnf_DataFree( pCnf );
3034 if ( Res == 1 )
3035 printf( "The ECO solution was verified successfully. " );
3036 else
3037 printf( "The ECO solution verification FAILED. " );
3038 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
3039 }
3040
3041 // derive new patch functions
3042 if ( fCisOnly )
3043 {
3044 vUsed = Vec_IntStartNatural( Vec_IntSize(vDivs) );
3045 Vec_PtrReverseOrder( vGias );
3046 }
3047 else
3048 {
3049 vFuncs = Acb_TransformPatchFunctions( vSops, vSupps, &vUsed, Vec_IntSize(vDivs) );
3050 Vec_PtrReverseOrder( vFuncs );
3051 }
3052
3053 // generate instance and patch
3054 vInst = Acb_GenerateInstance( pNtkF, vDivs, vUsed, &pNtkF->vTargets );
3055 vPatch = Acb_GeneratePatch( pNtkF, vDivs, vUsed, vFuncs, vGias, &pNtkF->vTargets );
3056
3057 // print the results
3058 //printf( "%s", Vec_StrArray(vPatch) );
3059 Acb_PrintPatch( pNtkF, vDivs, vUsed, clk );
3060
3061 // generate output files
3062 if ( pFileName[3] == NULL ) Acb_GenerateFilePatch( vPatch, "patch.v" );
3063 Acb_GenerateFileOut( vInst, pFileName[0], pFileName[3] ? pFileName[3] : (char *)"out.v", vPatch );
3064 printf( "Finished dumping resulting file \"%s\".\n\n", pFileName[3] ? pFileName[3] : "out.v" );
3065/*
3066 {
3067 char * pFileBase = Extra_FileNameGenericAppend( pFileName[0], "_patch.v" );
3068 Acb_GenerateFilePatch( vPatch, pFileBase );
3069 pFileBase = Extra_FileNameGenericAppend( pFileName[0], "_out.v" );
3070 Acb_GenerateFileOut( vInst, pFileName[0], pFileName[3] ? pFileName[3] : pFileBase, vPatch );
3071 Acb_GenerateFileOut( vInst, pFileName[0], pFileName[3] ? pFileName[3] : "out.v", vPatch );
3072 printf( "Finished dumping resulting file \"%s\".\n\n", pFileName[3] ? pFileName[3] : pFileBase );
3073 }
3074*/
3075 //Gia_AigerWrite( pGiaG, "test.aig", 0, 0, 0 );
3076cleanup:
3077 // cleanup
3078 if ( vGias )
3079 {
3080 Gia_Man_t * pTemp; int i;
3081 Vec_PtrForEachEntry( Gia_Man_t *, vGias, pTemp, i )
3082 Gia_ManStop( pTemp );
3083 Vec_PtrFree( vGias );
3084 }
3085 Vec_StrFreeP( &vPatch );
3086 Vec_StrFreeP( &vInst );
3087
3088 Vec_PtrFreeFree( vSops );
3089 Vec_WecFree( vSupps );
3090 Vec_IntFree( vSuppOld );
3091 Vec_IntFreeP( &vUsed );
3092 if ( vFuncs ) Vec_PtrFreeFree( vFuncs );
3093
3094 Gia_ManStop( pGiaF );
3095 Gia_ManStop( pGiaG );
3096 Gia_ManStop( pGiaM );
3097
3098 Vec_IntFreeP( &vSuppF );
3099 Vec_IntFreeP( &vSuppG );
3100 Vec_IntFreeP( &vSupp );
3101 Vec_IntFreeP( &vNodesF );
3102 Vec_IntFreeP( &vNodesG );
3103 Vec_IntFreeP( &vRoots );
3104 Vec_IntFreeP( &vDivs );
3105 Vec_BitFreeP( &vBlock );
3106 return RetValue;
3107}
3108
3120void Acb_NtkTestRun2( char * pFileNames[3], int fVerbose )
3121{
3122 char * pFileNameOut = Extra_FileNameGenericAppend( pFileNames[0], "_w.v" );
3123 Acb_Ntk_t * pNtk = Acb_VerilogSimpleRead( pFileNames[0], pFileNames[2] );
3124 Acb_VerilogSimpleWrite( pNtk, pFileNameOut );
3125 Acb_ManFree( pNtk->pDesign );
3126 Acb_IntallLibrary( 0 );
3127}
3128
3140void Acb_NtkRunEco( char * pFileNames[4], int nTimeout, int fCheck, int fRandom, int fInputs, int fUnitW, int fVerbose, int fVeryVerbose )
3141{
3142 char Command[1000]; int Result = 1;
3143 Acb_Ntk_t * pNtkF = Acb_VerilogSimpleRead( pFileNames[0], pFileNames[2] );
3144 Acb_Ntk_t * pNtkG = Acb_VerilogSimpleRead( pFileNames[1], NULL );
3145 if ( !pNtkF || !pNtkG )
3146 return;
3147 //int * pArray = Vec_IntArray( &pNtkF->vTargets );
3148 //ABC_SWAP( int, pArray[7], pArray[4] );
3149 //Vec_IntReverseOrder( &pNtkF->vTargets );
3150 if ( fRandom )
3151 {
3152 printf( "Permuting targets as follows: " );
3153 Vec_IntPermute( &pNtkF->vTargets );
3154 Vec_IntPrint( &pNtkF->vTargets );
3155 }
3156
3157 assert( Acb_NtkCiNum(pNtkF) == Acb_NtkCiNum(pNtkG) );
3158 assert( Acb_NtkCoNum(pNtkF) == Acb_NtkCoNum(pNtkG) );
3159
3160 Acb_IntallLibrary( Abc_FrameReadSignalNames() != NULL );
3161
3162 if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, nTimeout, 0, fInputs, fCheck, fUnitW, fVerbose, fVeryVerbose ) )
3163 {
3164// printf( "General computation timed out. Trying inputs only.\n\n" );
3165// if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, nTimeout, 1, fInputs, fCheck, fUnitW, fVerbose, fVeryVerbose ) )
3166// printf( "Input-only computation also timed out.\n\n" );
3167 printf( "Computation did not succeed.\n" );
3168 Result = 0;
3169 }
3170
3171 Acb_ManFree( pNtkF->pDesign );
3172 Acb_ManFree( pNtkG->pDesign );
3173
3174 // verify the result
3175 sprintf( Command, "read %s; strash; write temp1.aig; read %s; strash; write temp2.aig; &cec temp1.aig temp2.aig",
3176 pFileNames[1], pFileNames[3] ? pFileNames[3] : "out.v" );
3177 if ( Result && Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ) )
3178 fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
3179 printf( "\n" );
3180}
3181
3185
3186
3187ABC_NAMESPACE_IMPL_END
3188
Gia_ManInterOne
Gia_Man_t * Gia_ManInterOne(Gia_Man_t *pNtkOn, Gia_Man_t *pNtkOff, int fVerbose)
Definition abcDar.c:3884
nWords
int nWords
Definition abcNpn.c:127
ABC_OPER_CI
@ ABC_OPER_CI
Definition abcOper.h:45
ABC_OPER_CONST_F
@ ABC_OPER_CONST_F
Definition abcOper.h:50
ABC_OPER_CONST_X
@ ABC_OPER_CONST_X
Definition abcOper.h:52
ABC_OPER_BIT_NAND
@ ABC_OPER_BIT_NAND
Definition abcOper.h:58
ABC_OPER_BIT_XOR
@ ABC_OPER_BIT_XOR
Definition abcOper.h:61
ABC_OPER_TRI
@ ABC_OPER_TRI
Definition abcOper.h:131
ABC_OPER_BIT_MUX
@ ABC_OPER_BIT_MUX
Definition abcOper.h:65
ABC_OPER_CONST_T
@ ABC_OPER_CONST_T
Definition abcOper.h:51
ABC_OPER_BIT_INV
@ ABC_OPER_BIT_INV
Definition abcOper.h:56
ABC_OPER_BIT_AND
@ ABC_OPER_BIT_AND
Definition abcOper.h:57
ABC_OPER_BIT_NOR
@ ABC_OPER_BIT_NOR
Definition abcOper.h:60
ABC_OPER_BIT_OR
@ ABC_OPER_BIT_OR
Definition abcOper.h:59
ABC_OPER_BIT_BUF
@ ABC_OPER_BIT_BUF
Definition abcOper.h:55
ABC_OPER_BIT_NXOR
@ ABC_OPER_BIT_NXOR
Definition abcOper.h:62
ABC_OPER_CO
@ ABC_OPER_CO
Definition abcOper.h:46
Abc_SopSynthesize
Vec_Wec_t * Abc_SopSynthesize(Vec_Ptr_t *vSops)
Definition abcUtil.c:3118
Abc_GiaSynthesizeInter
Gia_Man_t * Abc_GiaSynthesizeInter(Gia_Man_t *p)
Definition abcUtil.c:3177
Abc_GiaSynthesize
Vec_Wec_t * Abc_GiaSynthesize(Vec_Ptr_t *vGias, Gia_Man_t *pMulti)
Definition abcUtil.c:3148
Abc_SopSynthesizeOne
ABC_DLL Gia_Man_t * Abc_SopSynthesizeOne(char *pSop, int fClp)
Definition abcUtil.c:3244
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Abc_FrameGetGlobalFrame
ABC_DLL Abc_Frame_t * Abc_FrameGetGlobalFrame()
Definition mainFrame.c:643
Acb_NtkFromNdr
Acb_Ntk_t * Acb_NtkFromNdr(char *pFileName, void *pModule, Abc_Nam_t *pNames, Vec_Int_t *vWeights, int nNameIdMax)
Definition acbAbc.c:164
Gia_FileSimpleParse
Gia_Man_t * Gia_FileSimpleParse(Vec_Int_t *vBuffer, Abc_Nam_t *pNames, int fNames, char *pFileW)
Definition acbFunc.c:443
Acb_ReadWeightMap
Vec_Int_t * Acb_ReadWeightMap(char *pFileName, Abc_Nam_t *pNames)
Definition acbFunc.c:577
Acb_KeyWords_t
Acb_KeyWords_t
DECLARATIONS ///.
Definition acbFunc.c:38
ACB_NOT
@ ACB_NOT
Definition acbFunc.c:46
ACB_NAND
@ ACB_NAND
Definition acbFunc.c:48
ACB_NOR
@ ACB_NOR
Definition acbFunc.c:50
ACB_XOR
@ ACB_XOR
Definition acbFunc.c:51
ACB_MODULE
@ ACB_MODULE
Definition acbFunc.c:40
ACB_NONE
@ ACB_NONE
Definition acbFunc.c:39
ACB_DC
@ ACB_DC
Definition acbFunc.c:54
ACB_MUX
@ ACB_MUX
Definition acbFunc.c:53
ACB_BUF
@ ACB_BUF
Definition acbFunc.c:45
ACB_ENDMODULE
@ ACB_ENDMODULE
Definition acbFunc.c:41
ACB_AND
@ ACB_AND
Definition acbFunc.c:47
ACB_XNOR
@ ACB_XNOR
Definition acbFunc.c:52
ACB_UNUSED
@ ACB_UNUSED
Definition acbFunc.c:55
ACB_INPUT
@ ACB_INPUT
Definition acbFunc.c:42
ACB_OUTPUT
@ ACB_OUTPUT
Definition acbFunc.c:43
ACB_OR
@ ACB_OR
Definition acbFunc.c:49
ACB_WIRE
@ ACB_WIRE
Definition acbFunc.c:44
Gia_FileSimpleRead
Gia_Man_t * Gia_FileSimpleRead(char *pFileName, int fNames, char *pFileW)
Definition acbFunc.c:554
Acb_FindSupportMinOne
Vec_Int_t * Acb_FindSupportMinOne(sat_solver *pSat, int iFirstDiv, Vec_Wrd_t *vPats, int *pnPats, Vec_Int_t *vSupp, int iVar)
Definition acbFunc.c:1345
Acb_PrintPatch
void Acb_PrintPatch(Acb_Ntk_t *pNtkF, Vec_Int_t *vDivs, Vec_Int_t *vUsed, abctime clk)
Definition acbFunc.c:2541
Acb_DerivePatchSupportS
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)
Definition acbFunc.c:1686
Acb_GetUsedDivs
Vec_Int_t * Acb_GetUsedDivs(Vec_Int_t *vDivs, Vec_Int_t *vUsed)
Definition acbFunc.c:2223
Acb_VerilogSimpleRead
Acb_Ntk_t * Acb_VerilogSimpleRead(char *pFileName, char *pFileNameW)
Definition acbFunc.c:622
Acb_PrepareNames
char ** Acb_PrepareNames(Abc_Nam_t *p)
Definition acbFunc.c:614
Acb_GenerateSignalNames
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)
Definition acbFunc.c:2198
Acb_NtkFindDivs_rec
int Acb_NtkFindDivs_rec(Acb_Ntk_t *p, int iObj)
Definition acbFunc.c:833
Acb_VerilogSimpleReadTest
void Acb_VerilogSimpleReadTest(char *pFileName)
Definition acbFunc.c:653
Acb_NtkEcoPerform
int Acb_NtkEcoPerform(Acb_Ntk_t *pNtkF, Acb_Ntk_t *pNtkG, char *pFileName[4], int nTimeout, int fCisOnly, int fInputs, int fCheck, int fUnitW, int fVerbose, int fVeryVerbose)
Definition acbFunc.c:2874
Gia_FileSimpleParse_rec
int Gia_FileSimpleParse_rec(Gia_Man_t *pNew, int Token, Vec_Int_t *vMapType, Vec_Int_t *vTypes, Vec_Int_t *vFanins, Vec_Int_t *vMap)
Definition acbFunc.c:401
Acb_CollectIntNodes_rec
void Acb_CollectIntNodes_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vNodes)
Definition acbFunc.c:2091
NWORDS
#define NWORDS
Definition acbFunc.c:1122
Acb_NtkDeriveMiterCnfInter2
Gia_Man_t * Acb_NtkDeriveMiterCnfInter2(Gia_Man_t *p, int iTar, int nTars)
Definition acbFunc.c:2716
Acb_WireIsTarget
int Acb_WireIsTarget(int Token, Abc_Nam_t *pNames)
Definition acbFunc.c:301
Acb_DerivePatchSupport
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)
Definition acbFunc.c:1493
Acb_VerilogSimpleParse
void * Acb_VerilogSimpleParse(Vec_Int_t *vBuffer, Abc_Nam_t *pNames)
Definition acbFunc.c:306
Acb_NtkRunEco
void Acb_NtkRunEco(char *pFileNames[4], int nTimeout, int fCheck, int fRandom, int fInputs, int fUnitW, int fVerbose, int fVeryVerbose)
Definition acbFunc.c:3140
Acb_FindArgMaxUnderMask
int Acb_FindArgMaxUnderMask(Vec_Wrd_t *vPats, word Mask[NWORDS], Vec_Int_t *vWeights, int nPats)
Definition acbFunc.c:1253
Acb_NtkFindSupp_rec
void Acb_NtkFindSupp_rec(Acb_Ntk_t *p, int iObj, Vec_Int_t *vSupp)
Definition acbFunc.c:799
Acb_DeriveOnePatchFunction
char * Acb_DeriveOnePatchFunction(Cnf_Dat_t *pCnf, int iTar, int nTargets, int nCoDivs, Vec_Int_t *vUsed, int fCisOnly)
Definition acbFunc.c:2011
Acb_ObjToGia
int Acb_ObjToGia(Gia_Man_t *pNew, Acb_Ntk_t *p, int iObj, Vec_Int_t *vTemp)
Definition acbFunc.c:962
Acb_RemapOneFunction
char * Acb_RemapOneFunction(char *pStr, Vec_Int_t *vSupp, Vec_Int_t *vMap, int nVars)
Definition acbFunc.c:2791
Acb_GenerateSignalNames2
Vec_Ptr_t * Acb_GenerateSignalNames2(Vec_Wec_t *vGates, Vec_Ptr_t *vIns, Vec_Ptr_t *vOuts)
Definition acbFunc.c:2376
Acb_GeneratePatch
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)
Definition acbFunc.c:2239
Acb_GenerateInstance
Vec_Str_t * Acb_GenerateInstance(Acb_Ntk_t *p, Vec_Int_t *vDivs, Vec_Int_t *vUsed, Vec_Int_t *vTars)
Definition acbFunc.c:2185
Acb_FindSupportStart
Vec_Int_t * Acb_FindSupportStart(sat_solver *pSat, int iFirstDiv, Vec_Int_t *vWeights, Vec_Wrd_t **pvPats, int *piPats)
Definition acbFunc.c:1207
Acb_DeriveWeights
Vec_Int_t * Acb_DeriveWeights(Vec_Int_t *vDivs, Acb_Ntk_t *pNtkF)
Definition acbFunc.c:1192
Acb_NtkFindNodes
Vec_Int_t * Acb_NtkFindNodes(Acb_Ntk_t *p, Vec_Int_t *vRoots, Vec_Int_t *vDivs)
Definition acbFunc.c:938
Acb_NtkFindDivsCis
Vec_Int_t * Acb_NtkFindDivsCis(Acb_Ntk_t *p, Vec_Int_t *vSupp)
Definition acbFunc.c:847
Acb_NtkSaveNames
int Acb_NtkSaveNames(Acb_Ntk_t *p, Vec_Int_t *vSupp, Vec_Int_t *vNodes, Vec_Int_t *vRoots, Vec_Int_t *vDivs, Vec_Int_t *vTargets, Gia_Man_t *pNew)
Definition acbFunc.c:1040
Vec_IntPermute
void Vec_IntPermute(Vec_Int_t *p)
Definition acbFunc.c:1124
Acb_GenerateFilePatch
void Acb_GenerateFilePatch(Vec_Str_t *p, char *pFileNamePatch)
Definition acbFunc.c:2501
Acb_NtkTestRun2
void Acb_NtkTestRun2(char *pFileNames[3], int fVerbose)
Definition acbFunc.c:3120
Acb_EnumerateSatAssigns
char * Acb_EnumerateSatAssigns(sat_solver *pSat, int PivotVar, int FreeVar, Vec_Int_t *vDivVars, Vec_Int_t *vTempLits, Vec_Str_t *vTempSop)
Definition acbFunc.c:1828
Acb_FindSupportMin
Vec_Int_t * Acb_FindSupportMin(sat_solver *pSat, int iFirstDiv, Vec_Wrd_t *vPats, int *pnPats, Vec_Int_t *vSuppStart)
Definition acbFunc.c:1371
Acb_NtkFindNodes_rec
void Acb_NtkFindNodes_rec(Acb_Ntk_t *p, int iObj, Vec_Int_t *vNodes)
Definition acbFunc.c:926
Acb_FindArgMaxUnderMask2
int Acb_FindArgMaxUnderMask2(Vec_Wrd_t *vPats, word Mask[NWORDS], Vec_Int_t *vWeights, int nPats)
Definition acbFunc.c:1273
Acb_NtkToGia
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)
Definition acbFunc.c:1006
Acb_ComputeSuppCost
int Acb_ComputeSuppCost(Vec_Int_t *vSupp, Vec_Int_t *vWeights, int iFirstDiv)
Definition acbFunc.c:1200
Acb_FindReplace
void Acb_FindReplace(sat_solver *pSat, int iFirstDiv, Vec_Int_t *vWeights, Vec_Wrd_t *vPats, int nPats, Vec_Int_t *vSupp)
Definition acbFunc.c:1384
Acb_VerilogStartNames
Abc_Nam_t * Acb_VerilogStartNames()
Definition acbFunc.c:189
Acb_NtkFindDivs
Vec_Int_t * Acb_NtkFindDivs(Acb_Ntk_t *p, Vec_Int_t *vSupp, Vec_Bit_t *vBlock, int fUnitW, int fVerbose)
Definition acbFunc.c:859
Acb_NtkEcoSynthesize
Gia_Man_t * Acb_NtkEcoSynthesize(Gia_Man_t *p)
Definition acbFunc.c:2566
Acb_PrintPatterns
void Acb_PrintPatterns(Vec_Wrd_t *vPats, int nPats, Vec_Int_t *vWeights)
Definition acbFunc.c:1151
Acb_NtkFindRoots
Vec_Int_t * Acb_NtkFindRoots(Acb_Ntk_t *p, Vec_Int_t *vTargets, Vec_Bit_t **pvBlock)
Definition acbFunc.c:759
Acb_NtkDeriveMiterCnfInter
Gia_Man_t * Acb_NtkDeriveMiterCnfInter(Gia_Man_t *p, int iTar, int nTars)
Definition acbFunc.c:2757
Acb_FindSupport
Vec_Int_t * Acb_FindSupport(sat_solver *pSat, int iFirstDiv, Vec_Int_t *vWeights, Vec_Int_t *vSuppStart, int TimeOut)
Definition acbFunc.c:1432
Acb_GeneratePatch2
Vec_Str_t * Acb_GeneratePatch2(Gia_Man_t *pGia, Vec_Ptr_t *vIns, Vec_Ptr_t *vOuts)
Definition acbFunc.c:2402
Acb_UpdateMiter
Gia_Man_t * Acb_UpdateMiter(Gia_Man_t *pM, Gia_Man_t *pOne, int iTar, int nTargets, Vec_Int_t *vUsed, int fCisOnly)
Definition acbFunc.c:2117
Acb_IntallLibrary
void Acb_IntallLibrary(int f2Ins)
Definition acbFunc.c:160
Acb_GenerateFile2
void Acb_GenerateFile2(Gia_Man_t *pGia, Vec_Ptr_t *vIns, Vec_Ptr_t *vOuts, char *pFileName, char *pFileNameOut, int fSkipMffc)
Definition acbFunc.c:2470
pLibStr2
char * pLibStr2[25]
Definition acbFunc.c:148
Acb_NtkFindRoots_rec
int Acb_NtkFindRoots_rec(Acb_Ntk_t *p, int iObj, Vec_Bit_t *vBlock)
Definition acbFunc.c:745
Acb_CollectIntNodes
void Acb_CollectIntNodes(Gia_Man_t *p, Vec_Int_t *vNodes0, Vec_Int_t *vNodes1)
Definition acbFunc.c:2101
Acb_TransformPatchFunctions
Vec_Ptr_t * Acb_TransformPatchFunctions(Vec_Ptr_t *vSops, Vec_Wec_t *vSupps, Vec_Int_t **pvUsed, int nDivs)
Definition acbFunc.c:2814
Acb_FindSupportNext
Vec_Int_t * Acb_FindSupportNext(sat_solver *pSat, int iFirstDiv, Vec_Int_t *vWeights, Vec_Wrd_t *vPats, int *pnPats)
Definition acbFunc.c:1305
Acb_GenerateInstance2
Vec_Str_t * Acb_GenerateInstance2(Vec_Ptr_t *vIns, Vec_Ptr_t *vOuts)
Definition acbFunc.c:2363
Acb_VerilogSimpleLex
Vec_Int_t * Acb_VerilogSimpleLex(char *pFileName, Abc_Nam_t *pNames)
Definition acbFunc.c:208
Acb_VerilogRemoveComments
void Acb_VerilogRemoveComments(char *pBuffer)
Definition acbFunc.c:200
Acb_SignalNames
Vec_Ptr_t * Acb_SignalNames(Acb_Ntk_t *p, Vec_Int_t *vObjs)
Definition acbFunc.c:2231
Gia_ManInterOneInt
Gia_Man_t * Gia_ManInterOneInt(Gia_Man_t *pCof1, Gia_Man_t *pCof0, int Depth)
Definition acbFunc.c:2652
Acb_CreateMiter
Gia_Man_t * Acb_CreateMiter(Gia_Man_t *pF, Gia_Man_t *pG)
Definition acbFunc.c:1077
Acb_CheckMiter
int Acb_CheckMiter(Cnf_Dat_t *pCnf)
Definition acbFunc.c:2061
Acb_VerilogSimpleWrite
void Acb_VerilogSimpleWrite(Acb_Ntk_t *p, char *pFileName)
Definition acbFunc.c:670
pLibStr
char * pLibStr[25]
FUNCTION DEFINITIONS ///.
Definition acbFunc.c:128
Acb_NtkFindSupp
Vec_Int_t * Acb_NtkFindSupp(Acb_Ntk_t *p, Vec_Int_t *vRoots)
Definition acbFunc.c:810
Acb_NtkDeriveMiterCnf
Cnf_Dat_t * Acb_NtkDeriveMiterCnf(Gia_Man_t *p, int iTar, int nTars, int fVerbose)
Definition acbFunc.c:2605
Vec_IntPermute2
void Vec_IntPermute2(Vec_Int_t *p)
Definition acbFunc.c:1136
Acb_GenerateFileOut
void Acb_GenerateFileOut(Vec_Str_t *vPatchLine, char *pFileNameF, char *pFileNameOut, Vec_Str_t *vPatch)
Definition acbFunc.c:2509
Acb_NtkCollectMfsGates
int Acb_NtkCollectMfsGates(char *pFileName, Vec_Ptr_t *vNamesRefed, Vec_Ptr_t *vNamesDerefed, int nGates[5])
Definition acbUtil.c:268
Acb_NtkInsert
void Acb_NtkInsert(char *pFileNameIn, char *pFileNameOut, Vec_Ptr_t *vNames, int fNumber, int fSkipMffc)
Definition acbUtil.c:1076
Acb_NtkForEachCoDriver
#define Acb_NtkForEachCoDriver(p, iObj, i)
Definition acb.h:340
Acb_NtkForEachCi
#define Acb_NtkForEachCi(p, iObj, i)
Definition acb.h:336
Acb_Ntk_t
struct Acb_Ntk_t_ Acb_Ntk_t
Definition acb.h:47
Acb_NtkCountPiBuffers
int Acb_NtkCountPiBuffers(Acb_Ntk_t *p, Vec_Int_t *vObjs)
Definition acbUtil.c:139
Acb_NtkForEachCiVec
#define Acb_NtkForEachCiVec(vVec, p, iObj, i)
Definition acb.h:345
Acb_ObjCollectTfoVec
Vec_Int_t * Acb_ObjCollectTfoVec(Acb_Ntk_t *p, Vec_Int_t *vObjs)
Definition acbUtil.c:108
Acb_NtkCountPoDrivers
int Acb_NtkCountPoDrivers(Acb_Ntk_t *p, Vec_Int_t *vObjs)
Definition acbUtil.c:146
Acb_ObjCollectTfiVec
Vec_Int_t * Acb_ObjCollectTfiVec(Acb_Ntk_t *p, Vec_Int_t *vObjs)
Definition acbUtil.c:75
Acb_NtkForEachCoDriverVec
#define Acb_NtkForEachCoDriverVec(vVec, p, iObj, i)
Definition acb.h:349
Acb_NtkForEachPo
#define Acb_NtkForEachPo(p, iObj, i)
Definition acb.h:333
Acb_NtkForEachPi
#define Acb_NtkForEachPi(p, iObj, i)
Definition acb.h:331
Acb_NtkForEachNode
#define Acb_NtkForEachNode(p, i)
Definition acb.h:362
Acb_ObjForEachFaninFast
#define Acb_ObjForEachFaninFast(p, iObj, pFanins, iFanin, k)
Definition acb.h:375
Abc_FrameReadSignalNames
ABC_DLL Vec_Ptr_t * Abc_FrameReadSignalNames()
Definition mainFrame.c:70
Abc_FrameReadSpecName
ABC_DLL char * Abc_FrameReadSpecName()
Definition mainFrame.c:71
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Vec_Str_t
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
l_True
#define l_True
Definition bmcBmcS.c:35
l_Undef
#define l_Undef
Definition bmcBmcS.c:34
l_False
#define l_False
Definition bmcBmcS.c:36
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
sat_solver_add_xor
#define sat_solver_add_xor
Definition cecSatG2.c:39
sat_solver
#define sat_solver
Definition cecSatG2.c:34
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
Cmd_CommandExecute
ABC_DLL int Cmd_CommandExecute(Abc_Frame_t *pAbc, const char *sCommand)
Definition cmdApi.c:193
Cnf_Dat_t
struct Cnf_Dat_t_ Cnf_Dat_t
Definition cnf.h:52
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition cnfMan.c:207
Cnf_DataLift
void Cnf_DataLift(Cnf_Dat_t *p, int nVarsPlus)
Definition cnfMan.c:232
p
Cube * p
Definition exorList.c:222
Extra_FileNameGenericAppend
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition extraUtilFile.c:192
Extra_FileReadContents
char * Extra_FileReadContents(char *pFileName)
Definition extraUtilFile.c:407
Gia_ManCompress2
Gia_Man_t * Gia_ManCompress2(Gia_Man_t *p, int fUpdateLevel, int fVerbose)
Definition giaAig.c:592
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ManDup
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition giaDup.c:720
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_ManDupRemovePis
Gia_Man_t * Gia_ManDupRemovePis(Gia_Man_t *p, int nRemPis)
Definition giaDup.c:802
Gia_ManDupUniv
Gia_Man_t * Gia_ManDupUniv(Gia_Man_t *p, int iVar)
Definition giaDup.c:2059
Gia_ManAreaBalance
Gia_Man_t * Gia_ManAreaBalance(Gia_Man_t *p, int fSimpleAnd, int nNewNodesMax, int fVerbose, int fVeryVerbose)
Definition giaBalAig.c:1047
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
Gia_ManDupCofactorVar
Gia_Man_t * Gia_ManDupCofactorVar(Gia_Man_t *p, int iVar, int Value)
Definition giaDup.c:1861
Gia_ManDupMux
Gia_Man_t * Gia_ManDupMux(int iVar, Gia_Man_t *pCof1, Gia_Man_t *pCof0)
Definition giaDup.c:1887
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_ManHashOr
int Gia_ManHashOr(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:621
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManHashXor
int Gia_ManHashXor(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:668
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition giaUtil.c:369
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
Gia_ManAigSyn2
Gia_Man_t * Gia_ManAigSyn2(Gia_Man_t *p, int fOldAlgo, int fCoarsen, int fCutMin, int nRelaxRatio, int fDelayMin, int fVerbose, int fVeryVerbose)
Definition giaScript.c:69
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
Gia_ManPrintStats
void Gia_ManPrintStats(Gia_Man_t *p, Gps_Par_t *pPars)
Definition giaMan.c:495
Mf_ManGenerateCnf
void * Mf_ManGenerateCnf(Gia_Man_t *pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fMapping, int fVerbose)
Definition giaMf.c:1877
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine)
Definition giaAiger.c:1595
Gia_ManDupDfsRehash
Gia_Man_t * Gia_ManDupDfsRehash(Gia_Man_t *p)
Definition giaDup.c:1815
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Mio_LibraryReadBuffer
Mio_Library_t * Mio_LibraryReadBuffer(char *pBuffer, int fExtendedFormat, st__table *tExcludeGate, int nFaninLimit, int fVerbose)
Definition mioRead.c:156
Mio_UpdateGenlib
void Mio_UpdateGenlib(Mio_Library_t *pLib)
FUNCTION DEFINITIONS ///.
Definition mio.c:243
Mio_Library_t
struct Mio_LibraryStruct_t_ Mio_Library_t
Definition mio.h:42
Mio_LibrarySetName
void Mio_LibrarySetName(Mio_Library_t *pLib, char *pName)
Definition mioApi.c:68
NDR_INPUT
@ NDR_INPUT
Definition ndr.h:103
NDR_OUTPUT
@ NDR_OUTPUT
Definition ndr.h:104
NDR_TARGET
@ NDR_TARGET
Definition ndr.h:109
Ndr_Data_t
struct Ndr_Data_t_ Ndr_Data_t
BASIC TYPES ///.
Definition ndr.h:119
Cnf_DataWriteIntoSolver
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition cnfMan.c:579
sat_solver_new
sat_solver * sat_solver_new(void)
Definition satSolver.c:1137
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition satSolver.c:1272
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition satSolver.c:2369
sat_solver_push
int sat_solver_push(sat_solver *s, int p)
Definition satSolver.c:2002
sat_solver_pop
void sat_solver_pop(sat_solver *s)
Definition satSolver.c:2045
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
sat_solver_minimize_assumptions
int sat_solver_minimize_assumptions(sat_solver *s, int *pLits, int nLits, int nConfLimit)
Definition satSolver.c:2209
satoko_setnvars
void satoko_setnvars(satoko_t *, int)
Definition solver_api.c:230
satoko_solve_assumptions
int satoko_solve_assumptions(satoko_t *s, int *plits, int nlits)
Definition solver_api.c:347
satoko_final_conflict
int satoko_final_conflict(satoko_t *, int **)
Definition solver_api.c:427
satoko_minimize_assumptions
int satoko_minimize_assumptions(satoko_t *s, int *plits, int nlits, int nconflim)
Definition solver_api.c:372
satoko_add_clause
int satoko_add_clause(satoko_t *, int *, int)
Definition solver_api.c:255
satoko_t
struct solver_t_ satoko_t
Definition satoko.h:35
satoko_destroy
void satoko_destroy(satoko_t *)
Definition solver_api.c:132
satoko_create
satoko_t * satoko_create(void)
Definition solver_api.c:88
satoko_options
satoko_opts_t * satoko_options(satoko_t *)
Definition solver_api.c:438
Acb_Ntk_t_::pDesign
Acb_Man_t * pDesign
Definition acb.h:53
Acb_Ntk_t_::vTargets
Vec_Int_t vTargets
Definition acb.h:86
Acb_Ntk_t_::vObjWeight
Vec_Int_t vObjWeight
Definition acb.h:77
Cnf_Dat_t_::nVars
int nVars
Definition cnf.h:59
Cnf_Dat_t_::pClauses
int ** pClauses
Definition cnf.h:62
Cnf_Dat_t_::nClauses
int nClauses
Definition cnf.h:61
Cnf_Dat_t_::pMan
Aig_Man_t * pMan
Definition cnf.h:58
Gia_Man_t_::vNamesIn
Vec_Ptr_t * vNamesIn
Definition gia.h:181
Gia_Man_t_::vPolars
Vec_Bit_t * vPolars
Definition gia.h:220
Gia_Man_t_::pSpec
char * pSpec
Definition gia.h:100
Gia_Man_t_::vNamesOut
Vec_Ptr_t * vNamesOut
Definition gia.h:182
Gia_Man_t_::fGiaSimple
int fGiaSimple
Definition gia.h:116
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Man_t_::vNamesNode
Vec_Ptr_t * vNamesNode
Definition gia.h:183
Gia_Man_t_::vWeights
Vec_Int_t * vWeights
Definition gia.h:174
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
satoko_opts::no_simplify
char no_simplify
Definition satoko.h:69
st__table
Definition st.h:52
Abc_NamStrFind
int Abc_NamStrFind(Abc_Nam_t *p, char *pStr)
Definition utilNam.c:433
Abc_NamStrFindOrAdd
int Abc_NamStrFindOrAdd(Abc_Nam_t *p, char *pStr, int *pfFound)
Definition utilNam.c:453
Abc_NamObjNumMax
int Abc_NamObjNumMax(Abc_Nam_t *p)
Definition utilNam.c:231
Abc_NamStart
Abc_Nam_t * Abc_NamStart(int nObjs, int nAveSize)
FUNCTION DEFINITIONS ///.
Definition utilNam.c:80
Abc_NamDeref
void Abc_NamDeref(Abc_Nam_t *p)
Definition utilNam.c:212
Abc_NamStr
char * Abc_NamStr(Abc_Nam_t *p, int NameId)
Definition utilNam.c:555
Abc_Nam_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Nam_t_ Abc_Nam_t
INCLUDES ///.
Definition utilNam.h:39
assert
#define assert(ex)
Definition util_old.h:213
strncmp
int strncmp()
strlen
int strlen()
strcmp
int strcmp()
sprintf
char * sprintf()
strtok
char * strtok()
strstr
char * strstr()
Vec_Bit_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition vecBit.h:42
Vec_IntForEachEntryDouble
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition vecInt.h:72
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryInVec
#define Vec_IntForEachEntryInVec(vVec2, vVec, Entry, i)
Definition vecInt.h:80
Vec_IntForEachEntryStop
#define Vec_IntForEachEntryStop(vVec, Entry, i, Stop)
Definition vecInt.h:58
Vec_IntForEachEntryReverse
#define Vec_IntForEachEntryReverse(vVec, pEntry, i)
Definition vecInt.h:62
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Vec_WecForEachLevel
#define Vec_WecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition vecWec.h:55
Vec_WecForEachLevelStartStop
#define Vec_WecForEachLevelStartStop(vGlob, vVec, i, LevelStart, LevelStop)
Definition vecWec.h:63
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42