1 /**CFile****************************************************************
2
3 FileName [abcExact.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Network and node package.]
8
9 Synopsis [Find minimum size networks with a SAT solver.]
10
11 Author [Mathias Soeken]
12
13 Affiliation [EPFL]
14
15 Date [Ver. 1.0. Started - July 15, 2016.]
16
17 Revision [$Id: abcFanio.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 /* This implementation is based on Exercises 477 and 478 in
22 * Donald E. Knuth TAOCP Fascicle 6 (Satisfiability) Section 7.2.2.2
23 */
24
25 #include "base/abc/abc.h"
26
27 #include "aig/gia/gia.h"
28 #include "misc/util/utilTruth.h"
29 #include "misc/vec/vecInt.h"
30 #include "misc/vec/vecPtr.h"
31 #include "proof/cec/cec.h"
32 #include "sat/bsat/satSolver.h"
33
34 ABC_NAMESPACE_IMPL_START
35
36
37 ////////////////////////////////////////////////////////////////////////
38 /// DECLARATIONS ///
39 ////////////////////////////////////////////////////////////////////////
40
41 /***********************************************************************
42
43 Synopsis [Some truth table helper functions.]
44
45 ***********************************************************************/
46
47 static word s_Truths8[32] = {
48 ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA),
49 ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC),
50 ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0),
51 ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00),
52 ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000),
53 ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000),
54 ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF),
55 ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0xFFFFFFFFFFFFFFFF)
56 };
57
58 static word s_Truths8Neg[32] = {
59 ABC_CONST(0x5555555555555555), ABC_CONST(0x5555555555555555), ABC_CONST(0x5555555555555555), ABC_CONST(0x5555555555555555),
60 ABC_CONST(0x3333333333333333), ABC_CONST(0x3333333333333333), ABC_CONST(0x3333333333333333), ABC_CONST(0x3333333333333333),
61 ABC_CONST(0x0F0F0F0F0F0F0F0F), ABC_CONST(0x0F0F0F0F0F0F0F0F), ABC_CONST(0x0F0F0F0F0F0F0F0F), ABC_CONST(0x0F0F0F0F0F0F0F0F),
62 ABC_CONST(0x00FF00FF00FF00FF), ABC_CONST(0x00FF00FF00FF00FF), ABC_CONST(0x00FF00FF00FF00FF), ABC_CONST(0x00FF00FF00FF00FF),
63 ABC_CONST(0x0000FFFF0000FFFF), ABC_CONST(0x0000FFFF0000FFFF), ABC_CONST(0x0000FFFF0000FFFF), ABC_CONST(0x0000FFFF0000FFFF),
64 ABC_CONST(0x00000000FFFFFFFF), ABC_CONST(0x00000000FFFFFFFF), ABC_CONST(0x00000000FFFFFFFF), ABC_CONST(0x00000000FFFFFFFF),
65 ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000),
66 ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000)
67 };
68
Abc_TtIsSubsetWithMask(word * pSmall,word * pLarge,word * pMask,int nWords)69 static int Abc_TtIsSubsetWithMask( word * pSmall, word * pLarge, word * pMask, int nWords )
70 {
71 int w;
72 for ( w = 0; w < nWords; ++w )
73 if ( ( pSmall[w] & pLarge[w] & pMask[w] ) != ( pSmall[w] & pMask[w] ) )
74 return 0;
75 return 1;
76 }
77
Abc_TtCofsOppositeWithMask(word * pTruth,word * pMask,int nWords,int iVar)78 static int Abc_TtCofsOppositeWithMask( word * pTruth, word * pMask, int nWords, int iVar )
79 {
80 if ( iVar < 6 )
81 {
82 int w, Shift = ( 1 << iVar );
83 for ( w = 0; w < nWords; ++w )
84 if ( ( ( pTruth[w] << Shift ) & s_Truths6[iVar] & pMask[w] ) != ( ~pTruth[w] & s_Truths6[iVar] & pMask[w] ) )
85 return 0;
86 return 1;
87 }
88 else
89 {
90 int w, Step = ( 1 << ( iVar - 6 ) );
91 word * p = pTruth, * m = pMask, * pLimit = pTruth + nWords;
92 for ( ; p < pLimit; p += 2 * Step, m += 2 * Step )
93 for ( w = 0; w < Step; ++w )
94 if ( ( p[w] & m[w] ) != ( ~p[w + Step] & m[w + Step] ) )
95 return 0;
96 return 1;
97 }
98 }
99
100 // checks whether we can decompose as OP(x^p, g) where OP in {AND, OR} and p in {0, 1}
101 // returns p if OP = AND, and 2 + p if OP = OR
Abc_TtIsTopDecomposable(word * pTruth,word * pMask,int nWords,int iVar)102 static int Abc_TtIsTopDecomposable( word * pTruth, word * pMask, int nWords, int iVar )
103 {
104 assert( iVar < 8 );
105
106 if ( Abc_TtIsSubsetWithMask( pTruth, &s_Truths8[iVar << 2], pMask, nWords ) ) return 1;
107 if ( Abc_TtIsSubsetWithMask( pTruth, &s_Truths8Neg[iVar << 2], pMask, nWords ) ) return 2;
108 if ( Abc_TtIsSubsetWithMask( &s_Truths8[iVar << 2], pTruth, pMask, nWords ) ) return 3;
109 if ( Abc_TtIsSubsetWithMask( &s_Truths8Neg[iVar << 2], pTruth, pMask, nWords ) ) return 4;
110 if ( Abc_TtCofsOppositeWithMask( pTruth, pMask, nWords, iVar ) ) return 5;
111
112 return 0;
113 }
114
115 // checks whether we can decompose as OP(x1, OP(x2, OP(x3, ...))) where pVars = {x1, x2, x3, ...}
116 // OP can be different and vars can be complemented
Abc_TtIsStairDecomposable(word * pTruth,int nWords,int * pVars,int nSize,int * pStairFunc)117 static int Abc_TtIsStairDecomposable( word * pTruth, int nWords, int * pVars, int nSize, int * pStairFunc )
118 {
119 int i, d;
120 word pMask[4];
121 word pCopy[4];
122
123 Abc_TtCopy( pCopy, pTruth, nWords, 0 );
124 Abc_TtMask( pMask, nWords, nWords * 64 );
125
126 for ( i = 0; i < nSize; ++i )
127 {
128 d = Abc_TtIsTopDecomposable( pCopy, pMask, nWords, pVars[i] );
129 if ( !d )
130 return 0; /* not decomposable */
131
132 pStairFunc[i] = d;
133
134 switch ( d )
135 {
136 case 1: /* AND(x, g) */
137 case 4: /* OR(!x, g) */
138 Abc_TtAnd( pMask, pMask, &s_Truths8[pVars[i] << 2], nWords, 0 );
139 break;
140 case 2: /* AND(!x, g) */
141 case 3: /* OR(x, g) */
142 Abc_TtAnd( pMask, pMask, &s_Truths8Neg[pVars[i] << 2], nWords, 0 );
143 break;
144 case 5:
145 Abc_TtXor( pCopy, pCopy, &s_Truths8[pVars[i] << 2], nWords, 0 );
146 break;
147 }
148 }
149
150 return 1; /* decomposable */
151 }
152
153 /***********************************************************************
154
155 Synopsis [Some printing utilities.]
156
157 ***********************************************************************/
158
Abc_DebugPrint(const char * str,int fCond)159 static inline void Abc_DebugPrint( const char* str, int fCond )
160 {
161 if ( fCond )
162 {
163 printf( "%s", str );
164 fflush( stdout );
165 }
166 }
167
Abc_DebugPrintInt(const char * fmt,int n,int fCond)168 static inline void Abc_DebugPrintInt( const char* fmt, int n, int fCond )
169 {
170 if ( fCond )
171 {
172 printf( fmt, n );
173 fflush( stdout );
174 }
175 }
176
Abc_DebugPrintIntInt(const char * fmt,int n1,int n2,int fCond)177 static inline void Abc_DebugPrintIntInt( const char* fmt, int n1, int n2, int fCond )
178 {
179 if ( fCond )
180 {
181 printf( fmt, n1, n2 );
182 fflush( stdout );
183 }
184 }
185
Abc_DebugErase(int n,int fCond)186 static inline void Abc_DebugErase( int n, int fCond )
187 {
188 int i;
189 if ( fCond )
190 {
191 for ( i = 0; i < n; ++i )
192 printf( "\b" );
193 fflush( stdout );
194 }
195 }
196
197 /***********************************************************************
198
199 Synopsis [BMS.]
200
201 ***********************************************************************/
202
203 #define ABC_EXACT_SOL_NVARS 0
204 #define ABC_EXACT_SOL_NFUNC 1
205 #define ABC_EXACT_SOL_NGATES 2
206
207 #define ANSI_COLOR_RED "\x1b[31m"
208 #define ANSI_COLOR_GREEN "\x1b[32m"
209 #define ANSI_COLOR_YELLOW "\x1b[33m"
210 #define ANSI_COLOR_BLUE "\x1b[34m"
211 #define ANSI_COLOR_MAGENTA "\x1b[35m"
212 #define ANSI_COLOR_CYAN "\x1b[36m"
213 #define ANSI_COLOR_RESET "\x1b[0m"
214
215 typedef struct Ses_Man_t_ Ses_Man_t;
216 struct Ses_Man_t_
217 {
218 sat_solver * pSat; /* SAT solver */
219
220 word * pSpec; /* specification */
221 int bSpecInv; /* remembers whether spec was inverted for normalization */
222 int nSpecVars; /* number of variables in specification */
223 int nSpecFunc; /* number of functions to synthesize */
224 int nSpecWords; /* number of words for function */
225 int nRows; /* number of rows in the specification (without 0) */
226 int nMaxDepth; /* maximum depth (-1 if depth is not constrained) */
227 int nMaxDepthTmp; /* temporary copy to modify nMaxDepth temporarily */
228 int * pArrTimeProfile; /* arrival times of inputs (NULL if arrival times are ignored) */
229 int pArrTimeProfileTmp[8]; /* temporary copy to modify pArrTimeProfile temporarily */
230 int nArrTimeDelta; /* delta to the original arrival times (arrival times are normalized to have 0 as minimum element) */
231 int nArrTimeMax; /* maximum normalized arrival time */
232 int nBTLimit; /* conflict limit */
233 int fMakeAIG; /* create AIG instead of general network */
234 int fVerbose; /* be verbose */
235 int fVeryVerbose; /* be very verbose */
236 int fExtractVerbose; /* be verbose about solution extraction */
237 int fSatVerbose; /* be verbose about SAT solving */
238 int fReasonVerbose; /* be verbose about give-up reasons */
239 word pTtValues[4]; /* truth table values to assign */
240 Vec_Int_t * vPolar; /* variables with positive polarity */
241 Vec_Int_t * vAssump; /* assumptions */
242 int nRandRowAssigns; /* number of random row assignments to initialize CEGAR */
243 int fKeepRowAssigns; /* if 1, keep counter examples in CEGAR for next number of gates */
244
245 int nGates; /* number of gates */
246 int nStartGates; /* number of gates to start search (-1), i.e., to start from 1 gate, one needs to specify 0 */
247 int nMaxGates; /* maximum number of gates given max. delay and arrival times */
248 int fDecStructure; /* set to 1 or higher if nSpecFunc = 1 and f = x_i OP g(X \ {x_i}), otherwise 0 (determined when solving) */
249 int pDecVars; /* mask of variables that can be decomposed at top-level */
250 Vec_Int_t * vStairDecVars; /* list of stair decomposable variables */
251 int pStairDecFunc[8]; /* list of stair decomposable functions */
252 word pTtObjs[100]; /* temporary truth tables */
253
254 int nSimVars; /* number of simulation vars x(i, t) */
255 int nOutputVars; /* number of output variables g(h, i) */
256 int nGateVars; /* number of gate variables f(i, p, q) */
257 int nSelectVars; /* number of select variables s(i, j, k) */
258 int nDepthVars; /* number of depth variables d(i, j) */
259
260 int nSimOffset; /* offset where gate variables start */
261 int nOutputOffset; /* offset where output variables start */
262 int nGateOffset; /* offset where gate variables start */
263 int nSelectOffset; /* offset where select variables start */
264 int nDepthOffset; /* offset where depth variables start */
265
266 int fHitResLimit; /* SAT solver gave up due to resource limit */
267
268 abctime timeSat; /* SAT runtime */
269 abctime timeSatSat; /* SAT runtime (sat instance) */
270 abctime timeSatUnsat; /* SAT runtime (unsat instance) */
271 abctime timeSatUndef; /* SAT runtime (undef instance) */
272 abctime timeInstance; /* creating instance runtime */
273 abctime timeTotal; /* all runtime */
274
275 int nSatCalls; /* number of SAT calls */
276 int nUnsatCalls; /* number of UNSAT calls */
277 int nUndefCalls; /* number of UNDEF calls */
278
279 int nDebugOffset; /* for debug printing */
280 };
281
282 /***********************************************************************
283
284 Synopsis [Store truth tables based on normalized arrival times.]
285
286 ***********************************************************************/
287
288 // The hash table is a list of pointers to Ses_TruthEntry_t elements, which
289 // are arranged in a linked list, each of which pointing to a linked list
290 // of Ses_TimesEntry_t elements which contain the char* representation of the
291 // optimum netlist according to then normalized arrival times:
292
293 typedef struct Ses_TimesEntry_t_ Ses_TimesEntry_t;
294 struct Ses_TimesEntry_t_
295 {
296 int pArrTimeProfile[8]; /* normalized arrival time profile */
297 int fResLimit; /* solution found after resource limit */
298 Ses_TimesEntry_t * next; /* linked list pointer */
299 char * pNetwork; /* pointer to char array representation of optimum network */
300 };
301
302 typedef struct Ses_TruthEntry_t_ Ses_TruthEntry_t;
303 struct Ses_TruthEntry_t_
304 {
305 word pTruth[4]; /* truth table for comparison */
306 int nVars; /* number of variables */
307 Ses_TruthEntry_t * next; /* linked list pointer */
308 Ses_TimesEntry_t * head; /* pointer to head of sub list with arrival times */
309 };
310
311 #define SES_STORE_TABLE_SIZE 1024
312 typedef struct Ses_Store_t_ Ses_Store_t;
313 struct Ses_Store_t_
314 {
315 int fMakeAIG; /* create AIG instead of general network */
316 int fVerbose; /* be verbose */
317 int fVeryVerbose; /* be very verbose */
318 int nBTLimit; /* conflict limit */
319 int nEntriesCount; /* number of entries */
320 int nValidEntriesCount; /* number of entries with network */
321 Ses_TruthEntry_t * pEntries[SES_STORE_TABLE_SIZE]; /* hash table for truth table entries */
322 sat_solver * pSat; /* own SAT solver instance to reuse when calling exact algorithm */
323 FILE * pDebugEntries; /* debug unsynth. (rl) entries */
324 char * szDBName; /* if given, database is written every time a new entry is added */
325
326 /* statistics */
327 unsigned long nCutCount; /* number of cuts investigated */
328 unsigned long pCutCount[9]; /* -> per cut size */
329 unsigned long nUnsynthesizedImp; /* number of cuts which couldn't be optimized at all, opt. stopped because of imp. constraints */
330 unsigned long pUnsynthesizedImp[9]; /* -> per cut size */
331 unsigned long nUnsynthesizedRL; /* number of cuts which couldn't be optimized at all, opt. stopped because of resource limits */
332 unsigned long pUnsynthesizedRL[9]; /* -> per cut size */
333 unsigned long nSynthesizedTrivial; /* number of cuts which could be synthesized trivially (n < 2) */
334 unsigned long pSynthesizedTrivial[9]; /* -> per cut size */
335 unsigned long nSynthesizedImp; /* number of cuts which could be synthesized, opt. stopped because of imp. constraints */
336 unsigned long pSynthesizedImp[9]; /* -> per cut size */
337 unsigned long nSynthesizedRL; /* number of cuts which could be synthesized, opt. stopped because of resource limits */
338 unsigned long pSynthesizedRL[9]; /* -> per cut size */
339 unsigned long nCacheHits; /* number of cache hits */
340 unsigned long pCacheHits[9]; /* -> per cut size */
341
342 unsigned long nSatCalls; /* number of total SAT calls */
343 unsigned long nUnsatCalls; /* number of total UNSAT calls */
344 unsigned long nUndefCalls; /* number of total UNDEF calls */
345
346 abctime timeExact; /* Exact synthesis runtime */
347 abctime timeSat; /* SAT runtime */
348 abctime timeSatSat; /* SAT runtime (sat instance) */
349 abctime timeSatUnsat; /* SAT runtime (unsat instance) */
350 abctime timeSatUndef; /* SAT runtime (undef instance) */
351 abctime timeInstance; /* creating instance runtime */
352 abctime timeTotal; /* all runtime */
353 };
354
355 static Ses_Store_t * s_pSesStore = NULL;
356
357 ////////////////////////////////////////////////////////////////////////
358 /// FUNCTION DEFINITIONS ///
359 ////////////////////////////////////////////////////////////////////////
360
Abc_NormalizeArrivalTimes(int * pArrTimeProfile,int nVars,int * maxNormalized)361 static int Abc_NormalizeArrivalTimes( int * pArrTimeProfile, int nVars, int * maxNormalized )
362 {
363 int * p = pArrTimeProfile, * pEnd = pArrTimeProfile + nVars;
364 int delta = *p;
365
366 while ( ++p < pEnd )
367 if ( *p < delta )
368 delta = *p;
369
370 *maxNormalized = 0;
371 p = pArrTimeProfile;
372 while ( p < pEnd )
373 {
374 *p -= delta;
375 if ( *p > *maxNormalized )
376 *maxNormalized = *p;
377 ++p;
378 }
379
380 *maxNormalized += 1;
381
382 return delta;
383 }
384
Ses_StoreAlloc(int nBTLimit,int fMakeAIG,int fVerbose)385 static inline Ses_Store_t * Ses_StoreAlloc( int nBTLimit, int fMakeAIG, int fVerbose )
386 {
387 Ses_Store_t * pStore = ABC_CALLOC( Ses_Store_t, 1 );
388 pStore->fMakeAIG = fMakeAIG;
389 pStore->fVerbose = fVerbose;
390 pStore->nBTLimit = nBTLimit;
391 memset( pStore->pEntries, 0, sizeof(pStore->pEntries) );
392
393 pStore->pSat = sat_solver_new();
394
395 return pStore;
396 }
397
Ses_StoreClean(Ses_Store_t * pStore)398 static inline void Ses_StoreClean( Ses_Store_t * pStore )
399 {
400 int i;
401 Ses_TruthEntry_t * pTEntry, * pTEntry2;
402 Ses_TimesEntry_t * pTiEntry, * pTiEntry2;
403
404 for ( i = 0; i < SES_STORE_TABLE_SIZE; ++i )
405 if ( pStore->pEntries[i] )
406 {
407 pTEntry = pStore->pEntries[i];
408
409 while ( pTEntry )
410 {
411 pTiEntry = pTEntry->head;
412 while ( pTiEntry )
413 {
414 ABC_FREE( pTiEntry->pNetwork );
415 pTiEntry2 = pTiEntry;
416 pTiEntry = pTiEntry->next;
417 ABC_FREE( pTiEntry2 );
418 }
419 pTEntry2 = pTEntry;
420 pTEntry = pTEntry->next;
421 ABC_FREE( pTEntry2 );
422 }
423 }
424
425 sat_solver_delete( pStore->pSat );
426
427 if ( pStore->szDBName )
428 ABC_FREE( pStore->szDBName );
429 ABC_FREE( pStore );
430 }
431
Ses_StoreTableHash(word * pTruth,int nVars)432 static inline int Ses_StoreTableHash( word * pTruth, int nVars )
433 {
434 static int s_Primes[4] = { 1291, 1699, 1999, 2357 };
435 int i;
436 unsigned uHash = 0;
437 for ( i = 0; i < Abc_TtWordNum( nVars ); ++i )
438 uHash ^= pTruth[i] * s_Primes[i & 0xf];
439 return (int)(uHash % SES_STORE_TABLE_SIZE );
440 }
441
Ses_StoreTruthEqual(Ses_TruthEntry_t * pEntry,word * pTruth,int nVars)442 static inline int Ses_StoreTruthEqual( Ses_TruthEntry_t * pEntry, word * pTruth, int nVars )
443 {
444 int i;
445
446 if ( pEntry->nVars != nVars )
447 return 0;
448
449 for ( i = 0; i < Abc_TtWordNum( nVars ); ++i )
450 if ( pEntry->pTruth[i] != pTruth[i] )
451 return 0;
452 return 1;
453 }
454
Ses_StoreTruthCopy(Ses_TruthEntry_t * pEntry,word * pTruthSrc,int nVars)455 static inline void Ses_StoreTruthCopy( Ses_TruthEntry_t * pEntry, word * pTruthSrc, int nVars )
456 {
457 int i;
458 pEntry->nVars = nVars;
459 for ( i = 0; i < Abc_TtWordNum( nVars ); ++i )
460 pEntry->pTruth[i] = pTruthSrc[i];
461 }
462
Ses_StoreTimesEqual(int * pTimes1,int * pTimes2,int nVars)463 static inline int Ses_StoreTimesEqual( int * pTimes1, int * pTimes2, int nVars )
464 {
465 int i;
466 for ( i = 0; i < nVars; ++i )
467 if ( pTimes1[i] != pTimes2[i] )
468 return 0;
469 return 1;
470 }
471
Ses_StoreTimesCopy(int * pTimesDest,int * pTimesSrc,int nVars)472 static inline void Ses_StoreTimesCopy( int * pTimesDest, int * pTimesSrc, int nVars )
473 {
474 int i;
475 for ( i = 0; i < nVars; ++i )
476 pTimesDest[i] = pTimesSrc[i];
477 }
478
Ses_StorePrintEntry(Ses_TruthEntry_t * pEntry,Ses_TimesEntry_t * pTiEntry)479 static inline void Ses_StorePrintEntry( Ses_TruthEntry_t * pEntry, Ses_TimesEntry_t * pTiEntry )
480 {
481 int i;
482
483 printf( "f = " );
484 Abc_TtPrintHexRev( stdout, pEntry->pTruth, pEntry->nVars );
485 printf( ", n = %d", pEntry->nVars );
486 printf( ", arrival =" );
487 for ( i = 0; i < pEntry->nVars; ++i )
488 printf( " %d", pTiEntry->pArrTimeProfile[i] );
489 printf( "\n" );
490 }
491
Ses_StorePrintDebugEntry(Ses_Store_t * pStore,word * pTruth,int nVars,int * pNormalArrTime,int nMaxDepth,char * pSol,int nStartGates)492 static inline void Ses_StorePrintDebugEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pNormalArrTime, int nMaxDepth, char * pSol, int nStartGates )
493 {
494 int l;
495
496 fprintf( pStore->pDebugEntries, "abc -c \"exact -v -C %d", pStore->nBTLimit );
497 if ( s_pSesStore->fMakeAIG ) fprintf( pStore->pDebugEntries, " -a" );
498 fprintf( pStore->pDebugEntries, " -S %d -D %d -A", nStartGates + 1, nMaxDepth );
499 for ( l = 0; l < nVars; ++l )
500 fprintf( pStore->pDebugEntries, "%c%d", ( l == 0 ? ' ' : ',' ), pNormalArrTime[l] );
501 fprintf( pStore->pDebugEntries, " " );
502 Abc_TtPrintHexRev( pStore->pDebugEntries, pTruth, nVars );
503 fprintf( pStore->pDebugEntries, "\" # " );
504
505 if ( !pSol )
506 fprintf( pStore->pDebugEntries, "no " );
507 fprintf( pStore->pDebugEntries, "solution found before\n" );
508 }
509
Abc_ExactNormalizeArrivalTimesForNetwork(int nVars,int * pArrTimeProfile,char * pSol)510 static void Abc_ExactNormalizeArrivalTimesForNetwork( int nVars, int * pArrTimeProfile, char * pSol )
511 {
512 int nGates, i, j, k, nMax;
513 Vec_Int_t * vLevels;
514
515 nGates = pSol[ABC_EXACT_SOL_NGATES];
516
517 /* printf( "NORMALIZE\n" ); */
518 /* printf( " #vars = %d\n", nVars ); */
519 /* printf( " #gates = %d\n", nGates ); */
520
521 vLevels = Vec_IntAllocArrayCopy( pArrTimeProfile, nVars );
522
523 /* compute level of each gate based on arrival time profile (to compute depth) */
524 for ( i = 0; i < nGates; ++i )
525 {
526 j = pSol[3 + i * 4 + 2];
527 k = pSol[3 + i * 4 + 3];
528
529 Vec_IntPush( vLevels, Abc_MaxInt( Vec_IntEntry( vLevels, j ), Vec_IntEntry( vLevels, k ) ) + 1 );
530
531 /* printf( " gate %d = (%d,%d)\n", nVars + i, j, k ); */
532 }
533
534 /* Vec_IntPrint( vLevels ); */
535
536 /* reset all levels except for the last one */
537 for ( i = 0; i < nVars + nGates - 1; ++i )
538 Vec_IntSetEntry( vLevels, i, Vec_IntEntry( vLevels, nVars + nGates - 1 ) );
539
540 /* Vec_IntPrint( vLevels ); */
541
542 /* compute levels from top to bottom */
543 for ( i = nGates - 1; i >= 0; --i )
544 {
545 j = pSol[3 + i * 4 + 2];
546 k = pSol[3 + i * 4 + 3];
547
548 Vec_IntSetEntry( vLevels, j, Abc_MinInt( Vec_IntEntry( vLevels, j ), Vec_IntEntry( vLevels, nVars + i ) - 1 ) );
549 Vec_IntSetEntry( vLevels, k, Abc_MinInt( Vec_IntEntry( vLevels, k ), Vec_IntEntry( vLevels, nVars + i ) - 1 ) );
550 }
551
552 /* Vec_IntPrint( vLevels ); */
553
554 /* normalize arrival times */
555 Abc_NormalizeArrivalTimes( Vec_IntArray( vLevels ), nVars, &nMax );
556 memcpy( pArrTimeProfile, Vec_IntArray( vLevels ), sizeof(int) * nVars );
557
558 /* printf( " nMax = %d\n", nMax ); */
559 /* Vec_IntPrint( vLevels ); */
560
561 Vec_IntFree( vLevels );
562 }
563
Ses_StoreWrite(Ses_Store_t * pStore,const char * pFilename,int fSynthImp,int fSynthRL,int fUnsynthImp,int fUnsynthRL)564 static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename, int fSynthImp, int fSynthRL, int fUnsynthImp, int fUnsynthRL )
565 {
566 int i;
567 char zero = '\0';
568 unsigned long nEntries = 0;
569 Ses_TruthEntry_t * pTEntry;
570 Ses_TimesEntry_t * pTiEntry;
571 FILE * pFile;
572
573 pFile = fopen( pFilename, "wb" );
574 if (pFile == NULL)
575 {
576 printf( "cannot open file \"%s\" for writing\n", pFilename );
577 return;
578 }
579
580 if ( fSynthImp ) nEntries += pStore->nSynthesizedImp;
581 if ( fSynthRL ) nEntries += pStore->nSynthesizedRL;
582 if ( fUnsynthImp ) nEntries += pStore->nUnsynthesizedImp;
583 if ( fUnsynthRL ) nEntries += pStore->nUnsynthesizedRL;
584 fwrite( &nEntries, sizeof( unsigned long ), 1, pFile );
585
586 for ( i = 0; i < SES_STORE_TABLE_SIZE; ++i )
587 if ( pStore->pEntries[i] )
588 {
589 pTEntry = pStore->pEntries[i];
590
591 while ( pTEntry )
592 {
593 pTiEntry = pTEntry->head;
594 while ( pTiEntry )
595 {
596 if ( !fSynthImp && pTiEntry->pNetwork && !pTiEntry->fResLimit ) { pTiEntry = pTiEntry->next; continue; }
597 if ( !fSynthRL && pTiEntry->pNetwork && pTiEntry->fResLimit ) { pTiEntry = pTiEntry->next; continue; }
598 if ( !fUnsynthImp && !pTiEntry->pNetwork && !pTiEntry->fResLimit ) { pTiEntry = pTiEntry->next; continue; }
599 if ( !fUnsynthRL && !pTiEntry->pNetwork && pTiEntry->fResLimit ) { pTiEntry = pTiEntry->next; continue; }
600
601 fwrite( pTEntry->pTruth, sizeof( word ), 4, pFile );
602 fwrite( &pTEntry->nVars, sizeof( int ), 1, pFile );
603 fwrite( pTiEntry->pArrTimeProfile, sizeof( int ), 8, pFile );
604 fwrite( &pTiEntry->fResLimit, sizeof( int ), 1, pFile );
605
606 if ( pTiEntry->pNetwork )
607 {
608 fwrite( pTiEntry->pNetwork, sizeof( char ), 3 + 4 * pTiEntry->pNetwork[ABC_EXACT_SOL_NGATES] + 2 + pTiEntry->pNetwork[ABC_EXACT_SOL_NVARS], pFile );
609 }
610 else
611 {
612 fwrite( &zero, sizeof( char ), 1, pFile );
613 fwrite( &zero, sizeof( char ), 1, pFile );
614 fwrite( &zero, sizeof( char ), 1, pFile );
615 }
616
617 pTiEntry = pTiEntry->next;
618 }
619 pTEntry = pTEntry->next;
620 }
621 }
622
623
624 fclose( pFile );
625 }
626
627 // pArrTimeProfile is normalized
628 // returns 1 if and only if a new TimesEntry has been created
Ses_StoreAddEntry(Ses_Store_t * pStore,word * pTruth,int nVars,int * pArrTimeProfile,char * pSol,int fResLimit)629 int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile, char * pSol, int fResLimit )
630 {
631 int key, fAdded;
632 Ses_TruthEntry_t * pTEntry;
633 Ses_TimesEntry_t * pTiEntry;
634
635 if ( pSol )
636 Abc_ExactNormalizeArrivalTimesForNetwork( nVars, pArrTimeProfile, pSol );
637
638 key = Ses_StoreTableHash( pTruth, nVars );
639 pTEntry = pStore->pEntries[key];
640
641 /* does truth table already exist? */
642 while ( pTEntry )
643 {
644 if ( Ses_StoreTruthEqual( pTEntry, pTruth, nVars ) )
645 break;
646 else
647 pTEntry = pTEntry->next;
648 }
649
650 /* entry does not yet exist, so create new one and enqueue */
651 if ( !pTEntry )
652 {
653 pTEntry = ABC_CALLOC( Ses_TruthEntry_t, 1 );
654 Ses_StoreTruthCopy( pTEntry, pTruth, nVars );
655 pTEntry->next = pStore->pEntries[key];
656 pStore->pEntries[key] = pTEntry;
657 }
658
659 /* does arrival time already exist? */
660 pTiEntry = pTEntry->head;
661 while ( pTiEntry )
662 {
663 if ( Ses_StoreTimesEqual( pArrTimeProfile, pTiEntry->pArrTimeProfile, nVars ) )
664 break;
665 else
666 pTiEntry = pTiEntry->next;
667 }
668
669 /* entry does not yet exist, so create new one and enqueue */
670 if ( !pTiEntry )
671 {
672 pTiEntry = ABC_CALLOC( Ses_TimesEntry_t, 1 );
673 Ses_StoreTimesCopy( pTiEntry->pArrTimeProfile, pArrTimeProfile, nVars );
674 pTiEntry->pNetwork = pSol;
675 pTiEntry->fResLimit = fResLimit;
676 pTiEntry->next = pTEntry->head;
677 pTEntry->head = pTiEntry;
678
679 /* item has been added */
680 fAdded = 1;
681 pStore->nEntriesCount++;
682 if ( pSol )
683 pStore->nValidEntriesCount++;
684 }
685 else
686 {
687 //assert( 0 );
688 /* item was already present */
689 fAdded = 0;
690 }
691
692 /* statistics */
693 if ( pSol )
694 {
695 if ( fResLimit )
696 {
697 pStore->nSynthesizedRL++;
698 pStore->pSynthesizedRL[nVars]++;
699 }
700 else
701 {
702 pStore->nSynthesizedImp++;
703 pStore->pSynthesizedImp[nVars]++;
704 }
705 }
706 else
707 {
708 if ( fResLimit )
709 {
710 pStore->nUnsynthesizedRL++;
711 pStore->pUnsynthesizedRL[nVars]++;
712 }
713 else
714 {
715 pStore->nUnsynthesizedImp++;
716 pStore->pUnsynthesizedImp[nVars]++;
717 }
718 }
719
720 if ( fAdded && pStore->szDBName )
721 Ses_StoreWrite( pStore, pStore->szDBName, 1, 0, 0, 0 );
722
723 return fAdded;
724 }
725
726 // pArrTimeProfile is normalized
727 // returns 1 if entry was in store, pSol may still be 0 if it couldn't be computed
Ses_StoreGetEntrySimple(Ses_Store_t * pStore,word * pTruth,int nVars,int * pArrTimeProfile,char ** pSol)728 int Ses_StoreGetEntrySimple( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile, char ** pSol )
729 {
730 int key;
731 Ses_TruthEntry_t * pTEntry;
732 Ses_TimesEntry_t * pTiEntry;
733
734 key = Ses_StoreTableHash( pTruth, nVars );
735 pTEntry = pStore->pEntries[key];
736
737 /* find truth table entry */
738 while ( pTEntry )
739 {
740 if ( Ses_StoreTruthEqual( pTEntry, pTruth, nVars ) )
741 break;
742 else
743 pTEntry = pTEntry->next;
744 }
745
746 /* no entry found? */
747 if ( !pTEntry )
748 return 0;
749
750 /* find times entry */
751 pTiEntry = pTEntry->head;
752 while ( pTiEntry )
753 {
754 if ( Ses_StoreTimesEqual( pArrTimeProfile, pTiEntry->pArrTimeProfile, nVars ) )
755 break;
756 else
757 pTiEntry = pTiEntry->next;
758 }
759
760 /* no entry found? */
761 if ( !pTiEntry )
762 return 0;
763
764 *pSol = pTiEntry->pNetwork;
765 return 1;
766 }
767
Ses_StoreGetEntry(Ses_Store_t * pStore,word * pTruth,int nVars,int * pArrTimeProfile,char ** pSol)768 int Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile, char ** pSol )
769 {
770 int key;
771 Ses_TruthEntry_t * pTEntry;
772 Ses_TimesEntry_t * pTiEntry;
773 int pTimes[8];
774
775 key = Ses_StoreTableHash( pTruth, nVars );
776 pTEntry = pStore->pEntries[key];
777
778 /* find truth table entry */
779 while ( pTEntry )
780 {
781 if ( Ses_StoreTruthEqual( pTEntry, pTruth, nVars ) )
782 break;
783 else
784 pTEntry = pTEntry->next;
785 }
786
787 /* no entry found? */
788 if ( !pTEntry )
789 return 0;
790
791 /* find times entry */
792 pTiEntry = pTEntry->head;
793 while ( pTiEntry )
794 {
795 /* found after normalization wrt. to network */
796 if ( pTiEntry->pNetwork )
797 {
798 memcpy( pTimes, pArrTimeProfile, sizeof(int) * nVars );
799 Abc_ExactNormalizeArrivalTimesForNetwork( nVars, pTimes, pTiEntry->pNetwork );
800
801 if ( Ses_StoreTimesEqual( pTimes, pTiEntry->pArrTimeProfile, nVars ) )
802 break;
803 }
804 /* found for non synthesized network */
805 else if ( Ses_StoreTimesEqual( pArrTimeProfile, pTiEntry->pArrTimeProfile, nVars ) )
806 break;
807 else
808 pTiEntry = pTiEntry->next;
809 }
810
811 /* no entry found? */
812 if ( !pTiEntry )
813 return 0;
814
815 *pSol = pTiEntry->pNetwork;
816 return 1;
817 }
818
Ses_StoreRead(Ses_Store_t * pStore,const char * pFilename,int fSynthImp,int fSynthRL,int fUnsynthImp,int fUnsynthRL)819 static void Ses_StoreRead( Ses_Store_t * pStore, const char * pFilename, int fSynthImp, int fSynthRL, int fUnsynthImp, int fUnsynthRL )
820 {
821 int i;
822 unsigned long nEntries;
823 word pTruth[4];
824 int nVars, fResLimit;
825 int pArrTimeProfile[8];
826 char pHeader[3];
827 char * pNetwork;
828 FILE * pFile;
829 int value;
830
831 if ( pStore->szDBName )
832 {
833 printf( "cannot read from database when szDBName is set" );
834 return;
835 }
836
837 pFile = fopen( pFilename, "rb" );
838 if (pFile == NULL)
839 {
840 printf( "cannot open file \"%s\" for reading\n", pFilename );
841 return;
842 }
843
844 value = fread( &nEntries, sizeof( unsigned long ), 1, pFile );
845
846 for ( i = 0; i < (int)nEntries; ++i )
847 {
848 value = fread( pTruth, sizeof( word ), 4, pFile );
849 value = fread( &nVars, sizeof( int ), 1, pFile );
850 value = fread( pArrTimeProfile, sizeof( int ), 8, pFile );
851 value = fread( &fResLimit, sizeof( int ), 1, pFile );
852 value = fread( pHeader, sizeof( char ), 3, pFile );
853
854 if ( pHeader[0] == '\0' )
855 pNetwork = NULL;
856 else
857 {
858 pNetwork = ABC_CALLOC( char, 3 + 4 * pHeader[ABC_EXACT_SOL_NGATES] + 2 + pHeader[ABC_EXACT_SOL_NVARS] );
859 pNetwork[0] = pHeader[0];
860 pNetwork[1] = pHeader[1];
861 pNetwork[2] = pHeader[2];
862
863 value = fread( pNetwork + 3, sizeof( char ), 4 * pHeader[ABC_EXACT_SOL_NGATES] + 2 + pHeader[ABC_EXACT_SOL_NVARS], pFile );
864 }
865
866 if ( !fSynthImp && pNetwork && !fResLimit ) continue;
867 if ( !fSynthRL && pNetwork && fResLimit ) continue;
868 if ( !fUnsynthImp && !pNetwork && !fResLimit ) continue;
869 if ( !fUnsynthRL && !pNetwork && fResLimit ) continue;
870
871 Ses_StoreAddEntry( pStore, pTruth, nVars, pArrTimeProfile, pNetwork, fResLimit );
872 }
873
874 fclose( pFile );
875
876 printf( "read %lu entries from file\n", (long)nEntries );
877 }
878
879 // computes top decomposition of variables wrt. to AND and OR
Ses_ManComputeTopDec(Ses_Man_t * pSes)880 static inline void Ses_ManComputeTopDec( Ses_Man_t * pSes )
881 {
882 int l;
883 word pMask[4];
884
885 Abc_TtMask( pMask, pSes->nSpecWords, pSes->nSpecWords * 64 );
886
887 for ( l = 0; l < pSes->nSpecVars; ++l )
888 if ( Abc_TtIsTopDecomposable( pSes->pSpec, pMask, pSes->nSpecWords, l ) )
889 pSes->pDecVars |= ( 1 << l );
890 }
891
Ses_ManAlloc(word * pTruth,int nVars,int nFunc,int nMaxDepth,int * pArrTimeProfile,int fMakeAIG,int nBTLimit,int fVerbose)892 static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int fMakeAIG, int nBTLimit, int fVerbose )
893 {
894 int h, i;
895
896 Ses_Man_t * p = ABC_CALLOC( Ses_Man_t, 1 );
897 p->pSat = NULL;
898 p->bSpecInv = 0;
899 for ( h = 0; h < nFunc; ++h )
900 if ( pTruth[h << 2] & 1 )
901 {
902 for ( i = 0; i < 4; ++i )
903 pTruth[(h << 2) + i] = ~pTruth[(h << 2) + i];
904 p->bSpecInv |= ( 1 << h );
905 }
906 p->pSpec = pTruth;
907 p->nSpecVars = nVars;
908 p->nSpecFunc = nFunc;
909 p->nSpecWords = Abc_TtWordNum( nVars );
910 p->nRows = ( 1 << nVars ) - 1;
911 p->nMaxDepth = nMaxDepth;
912 p->pArrTimeProfile = nMaxDepth >= 0 ? pArrTimeProfile : NULL;
913 if ( p->pArrTimeProfile )
914 p->nArrTimeDelta = Abc_NormalizeArrivalTimes( p->pArrTimeProfile, nVars, &p->nArrTimeMax );
915 else
916 p->nArrTimeDelta = p->nArrTimeMax = 0;
917 p->fMakeAIG = fMakeAIG;
918 p->nBTLimit = nBTLimit;
919 p->fVerbose = fVerbose;
920 p->fVeryVerbose = 0;
921 p->fExtractVerbose = 0;
922 p->fSatVerbose = 0;
923 p->vPolar = Vec_IntAlloc( 100 );
924 p->vAssump = Vec_IntAlloc( 10 );
925 p->vStairDecVars = Vec_IntAlloc( nVars );
926 p->nRandRowAssigns = 2 * nVars;
927 p->fKeepRowAssigns = 0;
928
929 if ( p->nSpecFunc == 1 )
930 Ses_ManComputeTopDec( p );
931
932 srand( 0xCAFE );
933
934 return p;
935 }
936
Ses_ManCleanLight(Ses_Man_t * pSes)937 static inline void Ses_ManCleanLight( Ses_Man_t * pSes )
938 {
939 int h, i;
940 for ( h = 0; h < pSes->nSpecFunc; ++h )
941 if ( ( pSes->bSpecInv >> h ) & 1 )
942 for ( i = 0; i < 4; ++i )
943 pSes->pSpec[(h << 2) + i] = ~( pSes->pSpec[(h << 2) + i] );
944
945 if ( pSes->pArrTimeProfile )
946 for ( i = 0; i < pSes->nSpecVars; ++i )
947 pSes->pArrTimeProfile[i] += pSes->nArrTimeDelta;
948
949 Vec_IntFree( pSes->vPolar );
950 Vec_IntFree( pSes->vAssump );
951 Vec_IntFree( pSes->vStairDecVars );
952
953 ABC_FREE( pSes );
954 }
955
Ses_ManClean(Ses_Man_t * pSes)956 static inline void Ses_ManClean( Ses_Man_t * pSes )
957 {
958 if ( pSes->pSat )
959 sat_solver_delete( pSes->pSat );
960 Ses_ManCleanLight( pSes );
961 }
962
963 /**Function*************************************************************
964
965 Synopsis [Access variables based on indexes.]
966
967 ***********************************************************************/
Ses_ManSimVar(Ses_Man_t * pSes,int i,int t)968 static inline int Ses_ManSimVar( Ses_Man_t * pSes, int i, int t )
969 {
970 assert( i < pSes->nGates );
971 assert( t < pSes->nRows );
972
973 return pSes->nSimOffset + pSes->nRows * i + t;
974 }
975
Ses_ManOutputVar(Ses_Man_t * pSes,int h,int i)976 static inline int Ses_ManOutputVar( Ses_Man_t * pSes, int h, int i )
977 {
978 assert( h < pSes->nSpecFunc );
979 assert( i < pSes->nGates );
980
981 return pSes->nOutputOffset + pSes->nGates * h + i;
982 }
983
Ses_ManGateVar(Ses_Man_t * pSes,int i,int p,int q)984 static inline int Ses_ManGateVar( Ses_Man_t * pSes, int i, int p, int q )
985 {
986 assert( i < pSes->nGates );
987 assert( p < 2 );
988 assert( q < 2 );
989 assert( p > 0 || q > 0 );
990
991 return pSes->nGateOffset + i * 3 + ( p << 1 ) + q - 1;
992 }
993
Ses_ManSelectVar(Ses_Man_t * pSes,int i,int j,int k)994 static inline int Ses_ManSelectVar( Ses_Man_t * pSes, int i, int j, int k )
995 {
996 int a;
997 int offset;
998
999 assert( i < pSes->nGates );
1000 assert( k < pSes->nSpecVars + i );
1001 assert( j < k );
1002
1003 offset = pSes->nSelectOffset;
1004 for ( a = pSes->nSpecVars; a < pSes->nSpecVars + i; ++a )
1005 offset += a * ( a - 1 ) / 2;
1006
1007 return offset + ( -j * ( 1 + j - 2 * ( pSes->nSpecVars + i ) ) ) / 2 + ( k - j - 1 );
1008 }
1009
Ses_ManDepthVar(Ses_Man_t * pSes,int i,int j)1010 static inline int Ses_ManDepthVar( Ses_Man_t * pSes, int i, int j )
1011 {
1012 assert( i < pSes->nGates );
1013 assert( j <= pSes->nArrTimeMax + i );
1014
1015 return pSes->nDepthOffset + i * pSes->nArrTimeMax + ( ( i * ( i + 1 ) ) / 2 ) + j;
1016 }
1017
1018 /**Function*************************************************************
1019
1020 Synopsis [Compute truth table from a solution.]
1021
1022 ***********************************************************************/
Ses_ManDeriveTruth(Ses_Man_t * pSes,char * pSol,int fInvert)1023 static word * Ses_ManDeriveTruth( Ses_Man_t * pSes, char * pSol, int fInvert )
1024 {
1025 int i, f, j, k, w, nGates = pSol[ABC_EXACT_SOL_NGATES];
1026 char * p;
1027 word * pTruth = NULL, * pTruth0, * pTruth1;
1028 assert( pSol[ABC_EXACT_SOL_NFUNC] == 1 );
1029
1030 p = pSol + 3;
1031
1032 memset( pSes->pTtObjs, 0, sizeof( word ) * 4 * nGates );
1033
1034 for ( i = 0; i < nGates; ++i )
1035 {
1036 f = *p++;
1037 assert( *p++ == 2 );
1038 j = *p++;
1039 k = *p++;
1040
1041 pTruth0 = j < pSes->nSpecVars ? &s_Truths8[j << 2] : &pSes->pTtObjs[( j - pSes->nSpecVars ) << 2];
1042 pTruth1 = k < pSes->nSpecVars ? &s_Truths8[k << 2] : &pSes->pTtObjs[( k - pSes->nSpecVars ) << 2];
1043
1044 pTruth = &pSes->pTtObjs[i << 2];
1045
1046 if ( f & 1 )
1047 for ( w = 0; w < pSes->nSpecWords; ++w )
1048 pTruth[w] |= ~pTruth0[w] & pTruth1[w];
1049 if ( ( f >> 1 ) & 1 )
1050 for ( w = 0; w < pSes->nSpecWords; ++w )
1051 pTruth[w] |= pTruth0[w] & ~pTruth1[w];
1052 if ( ( f >> 2 ) & 1 )
1053 for ( w = 0; w < pSes->nSpecWords; ++w )
1054 pTruth[w] |= pTruth0[w] & pTruth1[w];
1055 }
1056
1057 assert( Abc_Lit2Var( *p ) == nGates - 1 );
1058 if ( fInvert && Abc_LitIsCompl( *p ) )
1059 Abc_TtNot( pTruth, pSes->nSpecWords );
1060
1061 return pTruth;
1062 }
1063
1064 /**Function*************************************************************
1065
1066 Synopsis [Setup variables to find network with nGates gates.]
1067
1068 ***********************************************************************/
Ses_ManCreateVars(Ses_Man_t * pSes,int nGates)1069 static void Ses_ManCreateVars( Ses_Man_t * pSes, int nGates )
1070 {
1071 int i;
1072
1073 if ( pSes->fSatVerbose )
1074 {
1075 printf( "create variables for network with %d functions over %d variables and %d/%d gates\n", pSes->nSpecFunc, pSes->nSpecVars, nGates, pSes->nMaxGates );
1076 }
1077
1078 pSes->nGates = nGates;
1079 pSes->nSimVars = nGates * pSes->nRows;
1080 pSes->nOutputVars = pSes->nSpecFunc * nGates;
1081 pSes->nGateVars = nGates * 3;
1082 pSes->nSelectVars = 0;
1083 for ( i = pSes->nSpecVars; i < pSes->nSpecVars + nGates; ++i )
1084 pSes->nSelectVars += ( i * ( i - 1 ) ) / 2;
1085 pSes->nDepthVars = pSes->nMaxDepth > 0 ? nGates * pSes->nArrTimeMax + ( nGates * ( nGates + 1 ) ) / 2 : 0;
1086
1087 /* pSes->nSimOffset = 0; */
1088 /* pSes->nOutputOffset = pSes->nSimVars; */
1089 /* pSes->nGateOffset = pSes->nSimVars + pSes->nOutputVars; */
1090 /* pSes->nSelectOffset = pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars; */
1091 /* pSes->nDepthOffset = pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars + pSes->nSelectVars; */
1092
1093 pSes->nDepthOffset = 0;
1094 pSes->nSelectOffset = pSes->nDepthVars;
1095 pSes->nGateOffset = pSes->nDepthVars + pSes->nSelectVars;
1096 pSes->nOutputOffset = pSes->nDepthVars + pSes->nSelectVars + pSes->nGateVars;
1097 pSes->nSimOffset = pSes->nDepthVars + pSes->nSelectVars + pSes->nGateVars + pSes->nOutputVars;
1098
1099 /* pSes->nDepthOffset = 0; */
1100 /* pSes->nSelectOffset = pSes->nDepthVars; */
1101 /* pSes->nOutputOffset = pSes->nDepthVars + pSes->nSelectVars; */
1102 /* pSes->nGateOffset = pSes->nDepthVars + pSes->nSelectVars + pSes->nOutputVars; */
1103 /* pSes->nSimOffset = pSes->nDepthVars + pSes->nSelectVars + pSes->nOutputVars + pSes->nGateVars; */
1104
1105 /* if we already have a SAT solver, then restart it (this saves a lot of time) */
1106 if ( pSes->pSat )
1107 sat_solver_restart( pSes->pSat );
1108 else
1109 pSes->pSat = sat_solver_new();
1110 sat_solver_setnvars( pSes->pSat, pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars + pSes->nSelectVars + pSes->nDepthVars );
1111 }
1112
1113 /**Function*************************************************************
1114
1115 Synopsis [Create clauses.]
1116
1117 ***********************************************************************/
Ses_ManGateCannotHaveChild(Ses_Man_t * pSes,int i,int j)1118 static inline void Ses_ManGateCannotHaveChild( Ses_Man_t * pSes, int i, int j )
1119 {
1120 int k;
1121
1122 for ( k = 0; k < j; ++k )
1123 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, k, j ), 1 ) );
1124 for ( k = j + 1; k < pSes->nSpecVars + i; ++k )
1125 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 ) );
1126 }
1127
Ses_ManCreateMainClause(Ses_Man_t * pSes,int t,int i,int j,int k,int a,int b,int c)1128 static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int j, int k, int a, int b, int c )
1129 {
1130 int pLits[5], ctr = 0;
1131
1132 pLits[ctr++] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
1133 pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), a );
1134
1135 if ( j < pSes->nSpecVars )
1136 {
1137 if ( ( ( ( t + 1 ) & ( 1 << j ) ) ? 1 : 0 ) != b )
1138 return;
1139 }
1140 else
1141 pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, j - pSes->nSpecVars, t ), b );
1142
1143 if ( k < pSes->nSpecVars )
1144 {
1145 if ( ( ( ( t + 1 ) & ( 1 << k ) ) ? 1 : 0 ) != c )
1146 return;
1147 }
1148 else
1149 pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, k - pSes->nSpecVars, t ), c );
1150
1151 if ( b > 0 || c > 0 )
1152 pLits[ctr++] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, b, c ), 1 - a );
1153
1154 sat_solver_addclause( pSes->pSat, pLits, pLits + ctr );
1155 }
1156
Ses_ManCreateTruthTableClause(Ses_Man_t * pSes,int t)1157 static int inline Ses_ManCreateTruthTableClause( Ses_Man_t * pSes, int t )
1158 {
1159 int i, j, k, h;
1160 int pLits[3];
1161
1162 for ( i = 0; i < pSes->nGates; ++i )
1163 {
1164 /* main clauses */
1165 for ( j = 0; j < pSes->nSpecVars + i; ++j )
1166 for ( k = j + 1; k < pSes->nSpecVars + i; ++k )
1167 {
1168 Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 0, 1 );
1169 Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 0 );
1170 Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 1 );
1171 Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 0 );
1172 Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 1 );
1173 Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 0 );
1174 Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 1 );
1175 }
1176
1177 /* output clauses */
1178 if ( pSes->nSpecFunc != 1 )
1179 for ( h = 0; h < pSes->nSpecFunc; ++h )
1180 {
1181 pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 );
1182 pLits[1] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), 1 - Abc_TtGetBit( &pSes->pSpec[h << 2], t + 1 ) );
1183 if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) )
1184 return 0;
1185 }
1186 }
1187
1188 if ( pSes->nSpecFunc == 1 )
1189 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManSimVar( pSes, pSes->nGates - 1, t ), 1 - Abc_TtGetBit( pSes->pSpec, t + 1 ) ) );
1190
1191 return 1;
1192 }
1193
Ses_ManCreateClauses(Ses_Man_t * pSes)1194 static int Ses_ManCreateClauses( Ses_Man_t * pSes )
1195 {
1196 extern int Extra_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 );
1197
1198 int h, i, j, k, t, ii, jj, kk, iii, p, q;
1199 int pLits[3];
1200 Vec_Int_t * vLits = NULL;
1201
1202 for ( t = 0; t < pSes->nRows; ++t )
1203 {
1204 if ( Abc_TtGetBit( pSes->pTtValues, t ) )
1205 if ( !Ses_ManCreateTruthTableClause( pSes, t ) )
1206 return 0;
1207 }
1208
1209 /* if there is only one output, we know it must point to the last gate */
1210 if ( pSes->nSpecFunc == 1 )
1211 {
1212 for ( i = 0; i < pSes->nGates - 1; ++i )
1213 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManOutputVar( pSes, 0, i ), 1 ) );
1214 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManOutputVar( pSes, 0, pSes->nGates - 1 ), 0 ) );
1215
1216 vLits = Vec_IntAlloc( 0u );
1217 }
1218 else
1219 {
1220 vLits = Vec_IntAlloc( 0u );
1221
1222 /* some output is selected */
1223 for ( h = 0; h < pSes->nSpecFunc; ++h )
1224 {
1225 Vec_IntGrowResize( vLits, pSes->nGates );
1226 for ( i = 0; i < pSes->nGates; ++i )
1227 Vec_IntSetEntry( vLits, i, Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 0 ) );
1228 sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntArray( vLits ) + pSes->nGates );
1229 }
1230 }
1231
1232 /* each gate has two operands */
1233 for ( i = 0; i < pSes->nGates; ++i )
1234 {
1235 Vec_IntGrowResize( vLits, ( ( pSes->nSpecVars + i ) * ( pSes->nSpecVars + i - 1 ) ) / 2 );
1236 jj = 0;
1237 for ( j = 0; j < pSes->nSpecVars + i; ++j )
1238 for ( k = j + 1; k < pSes->nSpecVars + i; ++k )
1239 Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 0 ) );
1240 sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntArray( vLits ) + jj );
1241 }
1242
1243 /* gate decomposition (makes it worse) */
1244 /* if ( fDecVariable >= 0 && pSes->nGates >= 2 ) */
1245 /* { */
1246 /* pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, pSes->nGates - 1, fDecVariable, pSes->nSpecVars + pSes->nGates - 2 ), 0 ); */
1247 /* if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ) */
1248 /* { */
1249 /* Vec_IntFree( vLits ); */
1250 /* return 0; */
1251 /* } */
1252
1253 /* for ( k = 1; k < pSes->nSpecVars + pSes->nGates - 1; ++k ) */
1254 /* for ( j = 0; j < k; ++j ) */
1255 /* if ( j != fDecVariable || k != pSes->nSpecVars + pSes->nGates - 2 ) */
1256 /* { */
1257 /* pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, pSes->nGates - 1, j, k ), 1 ); */
1258 /* if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ) */
1259 /* { */
1260 /* Vec_IntFree( vLits ); */
1261 /* return 0; */
1262 /* } */
1263 /* } */
1264 /* } */
1265
1266 /* only AIG */
1267 if ( pSes->fMakeAIG )
1268 {
1269 for ( i = 0; i < pSes->nGates; ++i )
1270 {
1271 /* not 2 ones */
1272 pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 1 );
1273 pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 1 );
1274 pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 0 );
1275 sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
1276
1277 pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 1 );
1278 pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 0 );
1279 pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 );
1280 sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
1281
1282 pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 0 );
1283 pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 1 );
1284 pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 );
1285 sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
1286 }
1287 }
1288
1289 /* only binary clauses */
1290 if ( 1 ) /* TODO: add some meaningful parameter */
1291 {
1292 for ( i = 0; i < pSes->nGates; ++i )
1293 {
1294 pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 0 );
1295 pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 0 );
1296 pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 0 );
1297 sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
1298
1299 pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 1 );
1300 pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 0 );
1301 pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 );
1302 sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
1303
1304 pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 0 );
1305 pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 1 );
1306 pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 );
1307 sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
1308 }
1309
1310 for ( i = 0; i < pSes->nGates; ++i )
1311 for ( k = 1; k < pSes->nSpecVars + i; ++k )
1312 for ( j = 0; j < k; ++j )
1313 {
1314 pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
1315
1316 for ( kk = 1; kk < pSes->nSpecVars + i; ++kk )
1317 for ( jj = 0; jj < kk; ++jj )
1318 {
1319 if ( k == kk && j == jj ) continue;
1320 pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, jj, kk ), 1 );
1321
1322 if ( pLits[0] < pLits[1] )
1323 sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
1324 }
1325 }
1326
1327 /* Vec_IntGrowResize( vLits, pSes->nGates * ( pSes->nSpecVars + pSes->nGates - 2 ) ); */
1328
1329 /* for ( j = 0; j < pSes->nSpecVars; ++j ) */
1330 /* { */
1331 /* jj = 0; */
1332 /* for ( i = 0; i < pSes->nGates; ++i ) */
1333 /* { */
1334 /* for ( k = 0; k < j; ++k ) */
1335 /* Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, k, j ), 0 ) ); */
1336 /* for ( k = j + 1; k < pSes->nSpecVars + i; ++k ) */
1337 /* Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 0 ) ); */
1338 /* } */
1339 /* sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntArray( vLits ) + jj ); */
1340 /* } */
1341 }
1342
1343 /* EXTRA stair decomposition */
1344 if (Vec_IntSize( pSes->vStairDecVars ) )
1345 {
1346 Vec_IntForEachEntry( pSes->vStairDecVars, j, i )
1347 {
1348 if ( pSes->nGates - 2 - i < j )
1349 {
1350 continue;
1351 }
1352 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManSelectVar( pSes, pSes->nGates - 1 - i, j, pSes->nSpecVars + pSes->nGates - 2 - i ), 0 ) );
1353
1354 //printf( "dec %d for var %d\n", pSes->pStairDecFunc[i], j );
1355
1356 switch ( pSes->pStairDecFunc[i] )
1357 {
1358 case 1: /* AND(x,g) */
1359 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 1 ) );
1360 //Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 1 ) );
1361 //Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 0 ) );
1362 break;
1363 case 2: /* AND(!x,g) */
1364 //Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 0 ) );
1365 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 1 ) );
1366 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 1 ) );
1367 break;
1368 case 3: /* OR(x,g) */
1369 //Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 0 ) );
1370 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 0 ) );
1371 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 0 ) );
1372 break;
1373 case 4: /* OR(!x,g) */
1374 ////Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 0 ) );
1375 ////Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 1 ) );
1376 ////Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 0 ) );
1377 break;
1378 case 5: /* XOR(x,g) */
1379 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 0 ) );
1380 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 0 ) );
1381 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 1 ) );
1382 break;
1383 default:
1384 printf( "func: %d\n", pSes->pStairDecFunc[i] );
1385 assert( 0 );
1386 }
1387 }
1388 }
1389
1390 /* EXTRA clauses: use gate i at least once */
1391 Vec_IntGrowResize( vLits, pSes->nSpecFunc + pSes->nGates * ( pSes->nSpecVars + pSes->nGates - 2 ) );
1392 for ( i = 0; i < pSes->nGates; ++i )
1393 {
1394 jj = 0;
1395 for ( h = 0; h < pSes->nSpecFunc; ++h )
1396 Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 0 ) );
1397 for ( ii = i + 1; ii < pSes->nGates; ++ii )
1398 {
1399 for ( j = 0; j < pSes->nSpecVars + i; ++j )
1400 Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, j, pSes->nSpecVars + i ), 0 ) );
1401 for ( j = pSes->nSpecVars + i + 1; j < pSes->nSpecVars + ii; ++j )
1402 Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, pSes->nSpecVars + i, j ), 0 ) );
1403 }
1404 sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntArray( vLits ) + jj );
1405 }
1406 Vec_IntFree( vLits );
1407
1408 /* EXTRA clauses: no reapplying operand */
1409 if ( pSes->nGates > 1 )
1410 for ( i = 0; i < pSes->nGates - 1; ++i )
1411 for ( ii = i + 1; ii < pSes->nGates; ++ii )
1412 for ( k = 1; k < pSes->nSpecVars + i; ++k )
1413 for ( j = 0; j < k; ++j )
1414 {
1415 pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
1416 pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, j, pSes->nSpecVars + i ), 1 );
1417 sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
1418
1419 pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, k, pSes->nSpecVars + i ), 1 );
1420 sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
1421 }
1422 if ( pSes->nGates > 2 )
1423 for ( i = 0; i < pSes->nGates - 2; ++i )
1424 for ( ii = i + 1; ii < pSes->nGates - 1; ++ii )
1425 for ( iii = ii + 1; iii < pSes->nGates; ++iii )
1426 for ( k = 1; k < pSes->nSpecVars + i; ++k )
1427 for ( j = 0; j < k; ++j )
1428 {
1429 pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
1430 pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, j, k ), 1 );
1431 pLits[2] = Abc_Var2Lit( Ses_ManSelectVar( pSes, iii, i, ii ), 1 );
1432 sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
1433 }
1434
1435 /* EXTRA clauses: co-lexicographic order */
1436 for ( i = 0; i < pSes->nGates - 1; ++i )
1437 {
1438 for ( k = 2; k < pSes->nSpecVars + i; ++k )
1439 {
1440 for ( j = 1; j < k; ++j )
1441 for ( jj = 0; jj < j; ++jj )
1442 {
1443 pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
1444 pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i + 1, jj, k ), 1 );
1445 sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
1446 }
1447
1448 for ( j = 0; j < k; ++j )
1449 for ( kk = 1; kk < k; ++kk )
1450 for ( jj = 0; jj < kk; ++jj )
1451 {
1452 pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
1453 pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i + 1, jj, kk ), 1 );
1454 sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
1455 }
1456 }
1457 }
1458
1459 /* EXTRA clauses: symmetric variables */
1460 if ( /*pSes->nMaxDepth == -1 &&*/ pSes->nSpecFunc == 1 ) /* only check if there is one output function */
1461 for ( q = 1; q < pSes->nSpecVars; ++q )
1462 for ( p = 0; p < q; ++p )
1463 if ( Extra_TruthVarsSymm( (unsigned*)( pSes->pSpec ), pSes->nSpecVars, p, q ) &&
1464 ( !pSes->pArrTimeProfile || ( pSes->pArrTimeProfile[p] <= pSes->pArrTimeProfile[q] ) ) )
1465 {
1466 if ( pSes->fSatVerbose )
1467 printf( "variables %d and %d are symmetric\n", p, q );
1468 for ( i = 0; i < pSes->nGates; ++i )
1469 for ( j = 0; j < q; ++j )
1470 {
1471 if ( j == p ) continue;
1472
1473 vLits = Vec_IntAlloc( 0 );
1474 Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, q ), 1 ) );
1475 for ( ii = 0; ii < i; ++ii )
1476 for ( kk = 1; kk < pSes->nSpecVars + ii; ++kk )
1477 for ( jj = 0; jj < kk; ++jj )
1478 if ( jj == p || kk == p )
1479 Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, jj, kk ), 0 ) );
1480 sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) );
1481 Vec_IntFree( vLits );
1482 }
1483 }
1484
1485 return 1;
1486 }
1487
Ses_ManCreateDepthClauses(Ses_Man_t * pSes)1488 static int Ses_ManCreateDepthClauses( Ses_Man_t * pSes )
1489 {
1490 int i, j, k, jj, kk, d, h;
1491 int pLits[3];
1492
1493 for ( i = 0; i < pSes->nGates; ++i )
1494 {
1495 /* propagate depths from children */
1496 for ( k = 1; k < i; ++k )
1497 for ( j = 0; j < k; ++j )
1498 {
1499 pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, pSes->nSpecVars + j, pSes->nSpecVars + k ), 1 );
1500 for ( jj = 0; jj <= pSes->nArrTimeMax + j; ++jj )
1501 {
1502 pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, j, jj ), 1 );
1503 pLits[2] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, jj + 1 ), 0 );
1504 sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
1505 }
1506 }
1507
1508 for ( k = 0; k < i; ++k )
1509 for ( j = 0; j < pSes->nSpecVars + k; ++j )
1510 {
1511 pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, pSes->nSpecVars + k ), 1 );
1512 for ( kk = 0; kk <= pSes->nArrTimeMax + k; ++kk )
1513 {
1514 pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, k, kk ), 1 );
1515 pLits[2] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, kk + 1 ), 0 );
1516 sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
1517 }
1518 }
1519
1520 /* propagate depths from arrival times at PIs */
1521 if ( pSes->pArrTimeProfile )
1522 {
1523 for ( k = 1; k < pSes->nSpecVars + i; ++k )
1524 for ( j = 0; j < ( ( k < pSes->nSpecVars ) ? k : pSes->nSpecVars ); ++j )
1525 {
1526 d = pSes->pArrTimeProfile[j];
1527 if ( k < pSes->nSpecVars && pSes->pArrTimeProfile[k] > d )
1528 d = pSes->pArrTimeProfile[k];
1529
1530 pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
1531 pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, d ), 0 );
1532 sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
1533 }
1534 }
1535 else
1536 /* arrival times are 0 */
1537 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManDepthVar( pSes, i, 0 ), 0 ) );
1538
1539 /* reverse order encoding of depth variables */
1540 for ( j = 1; j <= pSes->nArrTimeMax + i; ++j )
1541 {
1542 pLits[0] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, j ), 1 );
1543 pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, j - 1 ), 0 );
1544 sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
1545 }
1546
1547 /* constrain maximum depth */
1548 if ( pSes->nMaxDepth < pSes->nArrTimeMax + i )
1549 for ( h = 0; h < pSes->nSpecFunc; ++h )
1550 {
1551 pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 );
1552 pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, pSes->nMaxDepth ), 1 );
1553 if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) )
1554 return 0;
1555 }
1556 }
1557
1558 return 1;
1559 }
1560
1561 /**Function*************************************************************
1562
1563 Synopsis [Solve.]
1564
1565 ***********************************************************************/
Sat_Wrd2Dbl(word w)1566 static inline double Sat_Wrd2Dbl( word w ) { return (double)(unsigned)(w&0x3FFFFFFF) + (double)(1<<30)*(unsigned)(w>>30); }
1567
Ses_ManSolve(Ses_Man_t * pSes)1568 static inline int Ses_ManSolve( Ses_Man_t * pSes )
1569 {
1570 int status;
1571 abctime timeStart, timeDelta;
1572
1573 if ( pSes->fSatVerbose )
1574 {
1575 printf( "SAT CL: %7d VA: %5d", sat_solver_nclauses( pSes->pSat ), sat_solver_nvars( pSes->pSat ) );
1576 fflush( stdout );
1577 }
1578
1579 timeStart = Abc_Clock();
1580 status = sat_solver_solve( pSes->pSat, Vec_IntArray( pSes->vAssump ), Vec_IntLimit( pSes->vAssump ), pSes->nBTLimit, 0, 0, 0 );
1581 timeDelta = Abc_Clock() - timeStart;
1582
1583 if ( pSes->fSatVerbose )
1584 printf( " RE: %2d ST: %4.f CO: %7.0f DE: %6.0f PR: %6.0f\n",
1585 status,
1586 Sat_Wrd2Dbl( pSes->pSat->stats.starts ), Sat_Wrd2Dbl( pSes->pSat->stats.conflicts ),
1587 Sat_Wrd2Dbl( pSes->pSat->stats.decisions ), Sat_Wrd2Dbl( pSes->pSat->stats.propagations ) );
1588 //Sat_SolverPrintStats( stdout, pSes->pSat );
1589
1590 pSes->timeSat += timeDelta;
1591
1592 if ( status == l_True )
1593 {
1594 pSes->nSatCalls++;
1595 pSes->timeSatSat += timeDelta;
1596 return 1;
1597 }
1598 else if ( status == l_False )
1599 {
1600 pSes->nUnsatCalls++;
1601 pSes->timeSatUnsat += timeDelta;
1602 return 0;
1603 }
1604 else
1605 {
1606 pSes->nUndefCalls++;
1607 pSes->timeSatUndef += timeDelta;
1608 if ( pSes->fSatVerbose )
1609 {
1610 //Sat_SolverWriteDimacs( pSes->pSat, "/tmp/test.cnf", Vec_IntArray( pSes->vAssump ), Vec_IntLimit( pSes->vAssump ), 1 );
1611 //exit( 42 );
1612
1613 printf( "resource limit reached\n" );
1614 }
1615 return 2;
1616 }
1617 }
1618
1619 /**Function*************************************************************
1620
1621 Synopsis [Extract solution.]
1622
1623 ***********************************************************************/
1624 // char is an array of short integers that stores the synthesized network
1625 // using the following format
1626 // | nvars | nfunc | ngates | gate[1] | ... | gate[ngates] | func[1] | .. | func[nfunc] |
1627 // nvars: integer with number of variables
1628 // nfunc: integer with number of functions
1629 // ngates: integer with number of gates
1630 // gate[i]: | op | nfanin | fanin[1] | ... | fanin[nfanin] |
1631 // op: integer of gate's truth table (divided by 2, because gate is normal)
1632 // nfanin: integer with number of fanins
1633 // fanin[i]: integer to primary input or other gate
1634 // func[i]: | fanin | delay | pin[1] | ... | pin[nvars] |
1635 // fanin: integer as literal to some gate (not primary input), can be complemented
1636 // delay: maximum delay to output (taking arrival times into account, not normalized) or 0 if not specified
1637 // pin[i]: pin to pin delay to input i or 0 if not specified or if there is no connection to input i
1638 // NOTE: since outputs can only point to gates, delay and pin-to-pin times cannot be 0
Ses_ManExtractSolution(Ses_Man_t * pSes)1639 static char * Ses_ManExtractSolution( Ses_Man_t * pSes )
1640 {
1641 int nSol, h, i, j, k, l, aj, ak, d, nOp;
1642 char * pSol, * p;
1643 int * pPerm = NULL; /* will be a 2d array [i][l] where is is gate id and l is PI id */
1644
1645 /* compute length of solution, for now all gates have 2 inputs */
1646 nSol = 3 + pSes->nGates * 4 + pSes->nSpecFunc * ( 2 + pSes->nSpecVars );
1647
1648 p = pSol = ABC_CALLOC( char, nSol );
1649
1650 /* header */
1651 *p++ = pSes->nSpecVars;
1652 *p++ = pSes->nSpecFunc;
1653 *p++ = pSes->nGates;
1654
1655 /* gates */
1656 for ( i = 0; i < pSes->nGates; ++i )
1657 {
1658 nOp = sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 0, 1 ) );
1659 nOp |= sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 0 ) ) << 1;
1660 nOp |= sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 1 ) ) << 2;
1661
1662 *p++ = nOp;
1663 *p++ = 2;
1664
1665 if ( pSes->fExtractVerbose )
1666 printf( "add gate %d with operation %d", pSes->nSpecVars + i, nOp );
1667
1668 for ( k = 0; k < pSes->nSpecVars + i; ++k )
1669 for ( j = 0; j < k; ++j )
1670 if ( sat_solver_var_value( pSes->pSat, Ses_ManSelectVar( pSes, i, j, k ) ) )
1671 {
1672 if ( pSes->fExtractVerbose )
1673 printf( " and operands %d and %d", j, k );
1674 *p++ = j;
1675 *p++ = k;
1676 k = pSes->nSpecVars + i;
1677 break;
1678 }
1679
1680 if ( pSes->fExtractVerbose )
1681 {
1682 if ( pSes->nMaxDepth > 0 )
1683 {
1684 printf( " and depth vector " );
1685 for ( j = 0; j <= pSes->nArrTimeMax + i; ++j )
1686 printf( "%d", sat_solver_var_value( pSes->pSat, Ses_ManDepthVar( pSes, i, j ) ) );
1687 }
1688 printf( "\n" );
1689 }
1690 }
1691
1692 /* pin-to-pin delay */
1693 if ( pSes->nMaxDepth != -1 )
1694 {
1695 pPerm = ABC_CALLOC( int, pSes->nGates * pSes->nSpecVars );
1696 for ( i = 0; i < pSes->nGates; ++i )
1697 {
1698 /* since all gates are binary for now */
1699 j = pSol[3 + i * 4 + 2];
1700 k = pSol[3 + i * 4 + 3];
1701
1702 for ( l = 0; l < pSes->nSpecVars; ++l )
1703 {
1704 /* pin-to-pin delay to input l of child nodes */
1705 aj = j < pSes->nSpecVars ? 0 : pPerm[(j - pSes->nSpecVars) * pSes->nSpecVars + l];
1706 ak = k < pSes->nSpecVars ? 0 : pPerm[(k - pSes->nSpecVars) * pSes->nSpecVars + l];
1707
1708 if ( aj == 0 && ak == 0 )
1709 pPerm[i * pSes->nSpecVars + l] = ( l == j || l == k ) ? 1 : 0;
1710 else
1711 pPerm[i * pSes->nSpecVars + l] = Abc_MaxInt( aj, ak ) + 1;
1712 }
1713 }
1714 }
1715
1716 /* outputs */
1717 for ( h = 0; h < pSes->nSpecFunc; ++h )
1718 for ( i = 0; i < pSes->nGates; ++i )
1719 if ( sat_solver_var_value( pSes->pSat, Ses_ManOutputVar( pSes, h, i ) ) )
1720 {
1721 *p++ = Abc_Var2Lit( i, ( pSes->bSpecInv >> h ) & 1 );
1722 d = 0;
1723 if ( pSes->nMaxDepth != -1 )
1724 for ( l = 0; l < pSes->nSpecVars; ++l )
1725 {
1726 if ( pSes->pArrTimeProfile )
1727 d = Abc_MaxInt( d, pSes->pArrTimeProfile[l] + pPerm[i * pSes->nSpecVars + l] );
1728 else
1729 d = Abc_MaxInt( d, pPerm[i * pSes->nSpecVars + l] );
1730 }
1731 *p++ = d;
1732 if ( pSes->pArrTimeProfile && pSes->fExtractVerbose )
1733 printf( "output %d points to gate %d and has normalized delay %d (nArrTimeDelta = %d)\n", h, pSes->nSpecVars + i, d, pSes->nArrTimeDelta );
1734 for ( l = 0; l < pSes->nSpecVars; ++l )
1735 {
1736 d = ( pSes->nMaxDepth != -1 ) ? pPerm[i * pSes->nSpecVars + l] : 0;
1737 if ( pSes->pArrTimeProfile && pSes->fExtractVerbose )
1738 printf( " pin-to-pin arrival time from input %d is %d (pArrTimeProfile = %d)\n", l, d, pSes->pArrTimeProfile[l] );
1739 *p++ = d;
1740 }
1741 }
1742
1743 /* pin-to-pin delays */
1744 if ( pSes->nMaxDepth != -1 )
1745 ABC_FREE( pPerm );
1746
1747 /* have we used all the fields? */
1748 assert( ( p - pSol ) == nSol );
1749
1750 /* printf( "found network: " ); */
1751 /* Abc_TtPrintHexRev( stdout, Ses_ManDeriveTruth( pSes, pSol, 1 ), pSes->nSpecVars ); */
1752 /* printf( "\n" ); */
1753
1754 return pSol;
1755 }
1756
Ses_ManExtractNtk(char const * pSol)1757 static Abc_Ntk_t * Ses_ManExtractNtk( char const * pSol )
1758 {
1759 int h, i;
1760 char const * p;
1761 Abc_Ntk_t * pNtk;
1762 Abc_Obj_t * pObj;
1763 Vec_Ptr_t * pGates, * vNames;
1764 char pGateTruth[5];
1765 char * pSopCover;
1766
1767 pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
1768 pNtk->pName = Extra_UtilStrsav( "exact" );
1769 pGates = Vec_PtrAlloc( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NGATES] );
1770 pGateTruth[3] = '0';
1771 pGateTruth[4] = '\0';
1772 vNames = Abc_NodeGetFakeNames( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NFUNC] );
1773
1774 /* primary inputs */
1775 Vec_PtrPush( pNtk->vObjs, NULL );
1776 for ( i = 0; i < pSol[ABC_EXACT_SOL_NVARS]; ++i )
1777 {
1778 pObj = Abc_NtkCreatePi( pNtk );
1779 Abc_ObjAssignName( pObj, (char*)Vec_PtrEntry( vNames, i ), NULL );
1780 Vec_PtrPush( pGates, pObj );
1781 }
1782
1783 /* gates */
1784 p = pSol + 3;
1785 for ( i = 0; i < pSol[ABC_EXACT_SOL_NGATES]; ++i )
1786 {
1787 pGateTruth[2] = '0' + ( *p & 1 );
1788 pGateTruth[1] = '0' + ( ( *p >> 1 ) & 1 );
1789 pGateTruth[0] = '0' + ( ( *p >> 2 ) & 1 );
1790 ++p;
1791
1792 assert( *p == 2 ); /* binary gate */
1793 ++p;
1794
1795 pSopCover = Abc_SopFromTruthBin( pGateTruth );
1796 pObj = Abc_NtkCreateNode( pNtk );
1797 pObj->pData = Abc_SopRegister( (Mem_Flex_t*)pNtk->pManFunc, pSopCover );
1798 Vec_PtrPush( pGates, pObj );
1799 ABC_FREE( pSopCover );
1800
1801 Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) );
1802 Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) );
1803 }
1804
1805 /* outputs */
1806 for ( h = 0; h < pSol[ABC_EXACT_SOL_NFUNC]; ++h )
1807 {
1808 pObj = Abc_NtkCreatePo( pNtk );
1809 Abc_ObjAssignName( pObj, (char*)Vec_PtrEntry( vNames, pSol[ABC_EXACT_SOL_NVARS] + h ), NULL );
1810 if ( Abc_LitIsCompl( *p ) )
1811 Abc_ObjAddFanin( pObj, Abc_NtkCreateNodeInv( pNtk, (Abc_Obj_t *)Vec_PtrEntry( pGates, pSol[ABC_EXACT_SOL_NVARS] + Abc_Lit2Var( *p ) ) ) );
1812 else
1813 Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, pSol[ABC_EXACT_SOL_NVARS] + Abc_Lit2Var( *p ) ) );
1814 p += ( 2 + pSol[ABC_EXACT_SOL_NVARS] );
1815 }
1816 Abc_NodeFreeNames( vNames );
1817
1818 Vec_PtrFree( pGates );
1819
1820 if ( !Abc_NtkCheck( pNtk ) )
1821 printf( "Ses_ManExtractSolution(): Network check has failed.\n" );
1822
1823 return pNtk;
1824 }
1825
Ses_ManExtractGia(char const * pSol)1826 static Gia_Man_t * Ses_ManExtractGia( char const * pSol )
1827 {
1828 int h, i;
1829 char const * p;
1830 Gia_Man_t * pGia;
1831 Vec_Int_t * pGates;
1832 Vec_Ptr_t * vNames;
1833 int nObj, nChild1, nChild2, fChild1Comp, fChild2Comp;
1834
1835 pGia = Gia_ManStart( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NGATES] + pSol[ABC_EXACT_SOL_NFUNC] + 1 );
1836 pGia->nConstrs = 0;
1837 pGia->pName = Extra_UtilStrsav( "exact" );
1838
1839 pGates = Vec_IntAlloc( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NGATES] );
1840 vNames = Abc_NodeGetFakeNames( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NFUNC] );
1841
1842 /* primary inputs */
1843 pGia->vNamesIn = Vec_PtrStart( pSol[ABC_EXACT_SOL_NVARS] );
1844 for ( i = 0; i < pSol[ABC_EXACT_SOL_NVARS]; ++i )
1845 {
1846 nObj = Gia_ManAppendCi( pGia );
1847 Vec_IntPush( pGates, nObj );
1848 Vec_PtrSetEntry( pGia->vNamesIn, i, Extra_UtilStrsav( (const char*)Vec_PtrEntry( vNames, i ) ) );
1849 }
1850
1851 /* gates */
1852 p = pSol + 3;
1853 for ( i = 0; i < pSol[ABC_EXACT_SOL_NGATES]; ++i )
1854 {
1855 assert( p[1] == 2 );
1856 nChild1 = Vec_IntEntry( pGates, p[2] );
1857 nChild2 = Vec_IntEntry( pGates, p[3] );
1858 fChild1Comp = fChild2Comp = 0;
1859
1860 if ( *p & 1 )
1861 {
1862 nChild1 = Abc_LitNot( nChild1 );
1863 fChild1Comp = 1;
1864 }
1865 if ( ( *p >> 1 ) & 1 )
1866 {
1867 nChild2 = Abc_LitNot( nChild2 );
1868 fChild2Comp = 1;
1869 }
1870 nObj = Gia_ManAppendAnd( pGia, nChild1, nChild2 );
1871 if ( fChild1Comp && fChild2Comp )
1872 {
1873 assert( ( *p >> 2 ) & 1 );
1874 nObj = Abc_LitNot( nObj );
1875 }
1876
1877 Vec_IntPush( pGates, nObj );
1878
1879 p += 4;
1880 }
1881
1882 /* outputs */
1883 pGia->vNamesOut = Vec_PtrStart( pSol[ABC_EXACT_SOL_NFUNC] );
1884 for ( h = 0; h < pSol[ABC_EXACT_SOL_NFUNC]; ++h )
1885 {
1886 nObj = Vec_IntEntry( pGates, pSol[ABC_EXACT_SOL_NVARS] + Abc_Lit2Var( *p ) );
1887 if ( Abc_LitIsCompl( *p ) )
1888 nObj = Abc_LitNot( nObj );
1889 Gia_ManAppendCo( pGia, nObj );
1890 Vec_PtrSetEntry( pGia->vNamesOut, h, Extra_UtilStrsav( (const char*)Vec_PtrEntry( vNames, pSol[ABC_EXACT_SOL_NVARS] + h ) ) );
1891 p += ( 2 + pSol[ABC_EXACT_SOL_NVARS] );
1892 }
1893 Abc_NodeFreeNames( vNames );
1894
1895 Vec_IntFree( pGates );
1896
1897 return pGia;
1898 }
1899
1900 /**Function*************************************************************
1901
1902 Synopsis [Debug.]
1903
1904 ***********************************************************************/
Ses_ManPrintRuntime(Ses_Man_t * pSes)1905 static void Ses_ManPrintRuntime( Ses_Man_t * pSes )
1906 {
1907 printf( "Runtime breakdown:\n" );
1908 ABC_PRTP( "Sat ", pSes->timeSat, pSes->timeTotal );
1909 ABC_PRTP( " Sat ", pSes->timeSatSat, pSes->timeTotal );
1910 ABC_PRTP( " Unsat ", pSes->timeSatUnsat, pSes->timeTotal );
1911 ABC_PRTP( " Undef ", pSes->timeSatUndef, pSes->timeTotal );
1912 ABC_PRTP( "Instance", pSes->timeInstance, pSes->timeTotal );
1913 ABC_PRTP( "ALL ", pSes->timeTotal, pSes->timeTotal );
1914 }
1915
Ses_ManPrintFuncs(Ses_Man_t * pSes)1916 static inline void Ses_ManPrintFuncs( Ses_Man_t * pSes )
1917 {
1918 int h;
1919
1920 printf( "find optimum circuit for %d %d-variable functions:\n", pSes->nSpecFunc, pSes->nSpecVars );
1921 for ( h = 0; h < pSes->nSpecFunc; ++h )
1922 {
1923 printf( " func %d: ", h + 1 );
1924 Abc_TtPrintHexRev( stdout, &pSes->pSpec[h << 2], pSes->nSpecVars );
1925 printf( "\n" );
1926 }
1927
1928 if ( pSes->nMaxDepth != -1 )
1929 {
1930 printf( " max depth = %d\n", pSes->nMaxDepth );
1931 if ( pSes->pArrTimeProfile )
1932 {
1933 printf( " arrival times =" );
1934 for ( h = 0; h < pSes->nSpecVars; ++h )
1935 printf( " %d", pSes->pArrTimeProfile[h] );
1936 printf( "\n" );
1937 }
1938 }
1939 }
1940
Ses_ManPrintVars(Ses_Man_t * pSes)1941 static inline void Ses_ManPrintVars( Ses_Man_t * pSes )
1942 {
1943 int h, i, j, k, p, q, t;
1944
1945 for ( i = 0; i < pSes->nGates; ++i )
1946 for ( t = 0; t < pSes->nRows; ++t )
1947 printf( "x(%d, %d) : %d\n", i, t, Ses_ManSimVar( pSes, i, t ) );
1948
1949 for ( h = 0; h < pSes->nSpecFunc; ++h )
1950 for ( i = 0; i < pSes->nGates; ++i )
1951 printf( "h(%d, %d) : %d\n", h, i, Ses_ManOutputVar( pSes, h, i ) );
1952
1953 for ( i = 0; i < pSes->nGates; ++i )
1954 for ( p = 0; p <= 1; ++p )
1955 for ( q = 0; q <= 1; ++ q)
1956 {
1957 if ( p == 0 && q == 0 ) { continue; }
1958 printf( "f(%d, %d, %d) : %d\n", i, p, q, Ses_ManGateVar( pSes, i, p, q ) );
1959 }
1960
1961 for ( i = 0; i < pSes->nGates; ++i )
1962 for ( j = 0; j < pSes->nSpecVars + i; ++j )
1963 for ( k = j + 1; k < pSes->nSpecVars + i; ++k )
1964 printf( "s(%d, %d, %d) : %d\n", i, j, k, Ses_ManSelectVar( pSes, i, j, k ) );
1965
1966 if ( pSes->nMaxDepth > 0 )
1967 for ( i = 0; i < pSes->nGates; ++i )
1968 for ( j = 0; j <= i; ++j )
1969 printf( "d(%d, %d) : %d\n", i, j, Ses_ManDepthVar( pSes, i, j ) );
1970
1971 }
1972
1973 /**Function*************************************************************
1974
1975 Synopsis [Synthesis algorithm.]
1976
1977 ***********************************************************************/
Ses_ManComputeMaxGates(Ses_Man_t * pSes)1978 static void Ses_ManComputeMaxGates( Ses_Man_t * pSes )
1979 {
1980 int s = 1, lvl = pSes->nMaxDepth, avail = pSes->nSpecVars, l;
1981
1982 pSes->nMaxGates = 0;
1983
1984 /* s is the number of gates we have in the current level */
1985 while ( s && /* while there are nodes to branch from */
1986 lvl && /* while we are at some level */
1987 avail * 2 > s /* while there are still enough available nodes (heuristic) */ )
1988 {
1989 /* erase from s if we have arriving nodes */
1990 for ( l = 0; l < pSes->nSpecVars; ++l )
1991 if ( pSes->pArrTimeProfile[l] == lvl )
1992 {
1993 --s;
1994 --avail;
1995 }
1996
1997 --lvl;
1998 pSes->nMaxGates += s;
1999 s *= 2;
2000 }
2001 }
2002
2003 // returns 0, if current max depth and arrival times are not consistent
Ses_CheckDepthConsistency(Ses_Man_t * pSes)2004 static int Ses_CheckDepthConsistency( Ses_Man_t * pSes )
2005 {
2006 int l, i, fAdded, nLevel;
2007 int fMaxGatesLevel2 = 1;
2008
2009 Vec_IntClear( pSes->vStairDecVars );
2010 pSes->fDecStructure = 0;
2011
2012 for ( l = 0; l < pSes->nSpecVars; ++l )
2013 {
2014 if ( pSes->pArrTimeProfile[l] >= pSes->nMaxDepth )
2015 {
2016 if ( pSes->fReasonVerbose )
2017 printf( "give up due to impossible arrival time (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
2018 return 0;
2019 }
2020 else if ( pSes->nSpecFunc == 1 && pSes->pArrTimeProfile[l] + 1 == pSes->nMaxDepth )
2021 {
2022 if ( ( pSes->fDecStructure == 1 && pSes->nSpecVars > 2 ) || pSes->fDecStructure == 2 )
2023 {
2024 if ( pSes->fReasonVerbose )
2025 printf( "give up due to impossible decomposition (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
2026 return 0;
2027 }
2028
2029 pSes->fDecStructure++;
2030
2031 /* A subset B <=> A and B = A */
2032 if ( !( ( pSes->pDecVars >> l ) & 1 ) )
2033 {
2034 if ( pSes->fReasonVerbose )
2035 printf( "give up due to impossible decomposition (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
2036 return 0;
2037 }
2038 }
2039 }
2040
2041 /* more complicated decomposition */
2042 if ( pSes->fDecStructure )
2043 {
2044 nLevel = 1;
2045 while ( 1 )
2046 {
2047 fAdded = 0;
2048
2049 for ( l = 0; l < pSes->nSpecVars; ++l )
2050 if ( pSes->pArrTimeProfile[l] + nLevel == pSes->nMaxDepth )
2051 {
2052 if ( fAdded )
2053 {
2054 assert( nLevel == Vec_IntSize( pSes->vStairDecVars ) );
2055 if ( fAdded > 1 || ( nLevel + 1 < pSes->nSpecVars ) )
2056 {
2057 if ( pSes->fReasonVerbose )
2058 printf( "give up due to impossible decomposition at level %d", nLevel );
2059 return 0;
2060 }
2061 }
2062 else
2063 {
2064 Vec_IntPush( pSes->vStairDecVars, l );
2065 }
2066 fAdded++;
2067 }
2068
2069 if ( !fAdded ) break;
2070 ++nLevel;
2071 }
2072
2073 if ( Vec_IntSize( pSes->vStairDecVars ) && !Abc_TtIsStairDecomposable( pSes->pSpec, pSes->nSpecWords, Vec_IntArray( pSes->vStairDecVars ), Vec_IntSize( pSes->vStairDecVars ), pSes->pStairDecFunc ) )
2074 {
2075 if ( pSes->fReasonVerbose )
2076 {
2077 printf( "give up due to impossible stair decomposition at level %d: ", nLevel );
2078 Vec_IntPrint( pSes->vStairDecVars );
2079 }
2080 return 0;
2081 }
2082 }
2083
2084 /* check if depth's match with structure at second level from top */
2085 if ( pSes->fDecStructure )
2086 fMaxGatesLevel2 = ( pSes->nSpecVars == 3 ) ? 2 : 1;
2087 else
2088 fMaxGatesLevel2 = ( pSes->nSpecVars == 4 ) ? 4 : 3;
2089
2090 i = 0;
2091 for ( l = 0; l < pSes->nSpecVars; ++l )
2092 if ( pSes->pArrTimeProfile[l] + 2 == pSes->nMaxDepth )
2093 if ( ++i > fMaxGatesLevel2 )
2094 {
2095 if ( pSes->fReasonVerbose )
2096 printf( "give up due to impossible decomposition at second level (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
2097 return 0;
2098 }
2099
2100 /* check if depth's match with structure at third level from top */
2101 if ( pSes->nSpecVars > 4 && pSes->fDecStructure && i == 1 ) /* we have f = AND(x_i, AND(x_j, g)) (x_i and x_j may be complemented) */
2102 {
2103 i = 0;
2104 for ( l = 0; l < pSes->nSpecVars; ++l )
2105 if ( pSes->pArrTimeProfile[l] + 3 == pSes->nMaxDepth )
2106 if ( ++i > 1 )
2107 {
2108 if ( pSes->fReasonVerbose )
2109 printf( "give up due to impossible decomposition at third level (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
2110 return 0;
2111 }
2112 }
2113
2114 return 1;
2115 }
2116
2117 // returns 0, if current max depth and #gates are not consistent
Ses_CheckGatesConsistency(Ses_Man_t * pSes,int nGates)2118 static int Ses_CheckGatesConsistency( Ses_Man_t * pSes, int nGates )
2119 {
2120 /* give up if number of gates is impossible for given depth */
2121 if ( pSes->nMaxDepth != -1 && nGates >= ( 1 << pSes->nMaxDepth ) )
2122 {
2123 if ( pSes->fReasonVerbose )
2124 printf( "give up due to impossible depth (depth = %d, gates = %d)", pSes->nMaxDepth, nGates );
2125 return 0;
2126 }
2127
2128 /* give up if number of gates is impossible for given depth and arrival times */
2129 if ( pSes->nMaxDepth != -1 && pSes->pArrTimeProfile && nGates > pSes->nMaxGates )
2130 {
2131 if ( pSes->fReasonVerbose )
2132 printf( "give up due to impossible depth and arrival times (depth = %d, gates = %d)", pSes->nMaxDepth, nGates );
2133 return 0;
2134 }
2135
2136 if ( pSes->fDecStructure && nGates >= ( 1 << ( pSes->nMaxDepth - 1 ) ) + 1 )
2137 {
2138 if ( pSes->fReasonVerbose )
2139 printf( "give up due to impossible depth in AND-dec structure (depth = %d, gates = %d)", pSes->nMaxDepth, nGates );
2140 return 0;
2141 }
2142
2143 /* give up if number of gates gets practically too large */
2144 if ( nGates >= ( 1 << pSes->nSpecVars ) )
2145 {
2146 if ( pSes->fReasonVerbose )
2147 printf( "give up due to impossible number of gates" );
2148 return 0;
2149 }
2150
2151 return 1;
2152 }
2153
Abc_ExactCopyDepthAndArrivalTimes(int nVars,int nDepthFrom,int * nDepthTo,int * pTimesFrom,int * pTimesTo)2154 static void Abc_ExactCopyDepthAndArrivalTimes( int nVars, int nDepthFrom, int * nDepthTo, int * pTimesFrom, int * pTimesTo )
2155 {
2156 int l;
2157
2158 *nDepthTo = nDepthFrom;
2159 for ( l = 0; l < nVars; ++l )
2160 pTimesTo[l] = pTimesFrom[l];
2161 }
2162
Ses_ManStoreDepthAndArrivalTimes(Ses_Man_t * pSes)2163 static void Ses_ManStoreDepthAndArrivalTimes( Ses_Man_t * pSes )
2164 {
2165 if ( pSes->nMaxDepth == -1 ) return;
2166 Abc_ExactCopyDepthAndArrivalTimes( pSes->nSpecVars, pSes->nMaxDepth, &pSes->nMaxDepthTmp, pSes->pArrTimeProfile, pSes->pArrTimeProfileTmp );
2167 }
2168
Ses_ManRestoreDepthAndArrivalTimes(Ses_Man_t * pSes)2169 static void Ses_ManRestoreDepthAndArrivalTimes( Ses_Man_t * pSes )
2170 {
2171 if ( pSes->nMaxDepth == -1 ) return;
2172 Abc_ExactCopyDepthAndArrivalTimes( pSes->nSpecVars, pSes->nMaxDepthTmp, &pSes->nMaxDepth, pSes->pArrTimeProfileTmp, pSes->pArrTimeProfile );
2173 }
2174
Abc_ExactAdjustDepthAndArrivalTimes(int nVars,int nGates,int nDepthFrom,int * nDepthTo,int * pTimesFrom,int * pTimesTo,int nTimesMax)2175 static void Abc_ExactAdjustDepthAndArrivalTimes( int nVars, int nGates, int nDepthFrom, int * nDepthTo, int * pTimesFrom, int * pTimesTo, int nTimesMax )
2176 {
2177 int l;
2178
2179 *nDepthTo = Abc_MinInt( nDepthFrom, nGates );
2180 for ( l = 0; l < nVars; ++l )
2181 pTimesTo[l] = Abc_MinInt( pTimesFrom[l], Abc_MaxInt( 0, nGates - 1 - nTimesMax + pTimesFrom[l] ) );
2182 }
2183
Ses_AdjustDepthAndArrivalTimes(Ses_Man_t * pSes,int nGates)2184 static void Ses_AdjustDepthAndArrivalTimes( Ses_Man_t * pSes, int nGates )
2185 {
2186 Abc_ExactAdjustDepthAndArrivalTimes( pSes->nSpecVars, nGates, pSes->nMaxDepthTmp, &pSes->nMaxDepth, pSes->pArrTimeProfileTmp, pSes->pArrTimeProfile, pSes->nArrTimeMax - 1 );
2187 }
2188
2189 /* return: (2: continue, 1: found, 0: gave up) */
Ses_ManFindNetworkExact(Ses_Man_t * pSes,int nGates)2190 static int Ses_ManFindNetworkExact( Ses_Man_t * pSes, int nGates )
2191 {
2192 int f, fSat;
2193 abctime timeStart;
2194
2195 /* solve */
2196 timeStart = Abc_Clock();
2197 Vec_IntClear( pSes->vPolar );
2198 Vec_IntClear( pSes->vAssump );
2199 Ses_ManCreateVars( pSes, nGates );
2200
2201 if ( pSes->nMaxDepth != -1 )
2202 {
2203 f = Ses_ManCreateDepthClauses( pSes );
2204 pSes->timeInstance += ( Abc_Clock() - timeStart );
2205 if ( !f ) return 2; /* proven UNSAT while creating clauses */
2206 }
2207
2208 sat_solver_set_polarity( pSes->pSat, Vec_IntArray( pSes->vPolar ), Vec_IntSize( pSes->vPolar ) );
2209
2210 /* first solve */
2211 fSat = Ses_ManSolve( pSes );
2212 if ( fSat == 0 )
2213 return 2; /* UNSAT, continue with next # of gates */
2214 else if ( fSat == 2 )
2215 {
2216 pSes->fHitResLimit = 1;
2217 return 0;
2218 }
2219
2220 timeStart = Abc_Clock();
2221 f = Ses_ManCreateClauses( pSes );
2222 pSes->timeInstance += ( Abc_Clock() - timeStart );
2223 if ( !f ) return 2; /* proven UNSAT while creating clauses */
2224
2225 fSat = Ses_ManSolve( pSes );
2226 if ( fSat == 1 )
2227 return 1;
2228 else if ( fSat == 2 )
2229 {
2230 pSes->fHitResLimit = 1;
2231 return 0;
2232 }
2233
2234 return 2; /* UNSAT continue */
2235 }
2236
2237 // is there a network for a given number of gates
2238 /* return: (3: impossible, 2: continue, 1: found, 0: gave up) */
Ses_ManFindNetworkExactCEGAR(Ses_Man_t * pSes,int nGates,char ** pSol)2239 static int Ses_ManFindNetworkExactCEGAR( Ses_Man_t * pSes, int nGates, char ** pSol )
2240 {
2241 int fRes, iMint, fSat, i;
2242 word pTruth[4];
2243
2244 /* debug */
2245 Abc_DebugErase( pSes->nDebugOffset + ( nGates > 10 ? 5 : 4 ), pSes->fVeryVerbose );
2246 Abc_DebugPrintIntInt( " (%d/%d)", nGates, pSes->nMaxGates, pSes->fVeryVerbose );
2247
2248 /* do #gates and max depth allow for a network? */
2249 if ( !Ses_CheckGatesConsistency( pSes, nGates ) )
2250 return 3;
2251
2252 for ( i = 0; i < pSes->nRandRowAssigns; ++i )
2253 Abc_TtSetBit( pSes->pTtValues, rand() % pSes->nRows );
2254
2255 fRes = Ses_ManFindNetworkExact( pSes, nGates );
2256 if ( fRes != 1 ) return fRes;
2257
2258 while ( true )
2259 {
2260 *pSol = Ses_ManExtractSolution( pSes );
2261 Abc_TtXor( pTruth, Ses_ManDeriveTruth( pSes, *pSol, 0 ), pSes->pSpec, pSes->nSpecWords, 0 );
2262 iMint = Abc_TtFindFirstBit( pTruth, pSes->nSpecVars );
2263
2264 if ( iMint == -1 || (pSes->nSpecVars < 6 && iMint > pSes->nRows) )
2265 {
2266 assert( fRes == 1 );
2267 return 1;
2268 }
2269 ABC_FREE( *pSol );
2270
2271 if ( pSes->fKeepRowAssigns )
2272 Abc_TtSetBit( pSes->pTtValues, iMint - 1 );
2273 if ( !Ses_ManCreateTruthTableClause( pSes, iMint - 1 ) ) /* UNSAT, continue */
2274 return 2;
2275
2276 if ( ( fSat = Ses_ManSolve( pSes ) ) == 1 ) continue;
2277
2278 return ( fSat == 2 ) ? 0 : 2;
2279 }
2280 }
2281
2282 // find minimum size by increasing the number of gates
Ses_ManFindMinimumSizeBottomUp(Ses_Man_t * pSes)2283 static char * Ses_ManFindMinimumSizeBottomUp( Ses_Man_t * pSes )
2284 {
2285 int nGates = pSes->nStartGates, fRes;
2286 char * pSol = NULL;
2287
2288 /* store whether call was unsuccessful due to resource limit and not due to impossible constraint */
2289 pSes->fHitResLimit = 0;
2290
2291 pSes->nDebugOffset = pSes->nMaxGates >= 10 ? 3 : 2;
2292
2293 /* adjust number of gates if there is a stair decomposition */
2294 if ( Vec_IntSize( pSes->vStairDecVars ) )
2295 nGates = Abc_MaxInt( nGates, Vec_IntSize( pSes->vStairDecVars ) - 1 );
2296
2297 //Ses_ManStoreDepthAndArrivalTimes( pSes );
2298
2299 memset( pSes->pTtValues, 0, 4 * sizeof( word ) );
2300
2301 Abc_DebugPrintIntInt( " (%d/%d)", nGates, pSes->nMaxGates, pSes->fVeryVerbose );
2302
2303 while ( true )
2304 {
2305 ++nGates;
2306
2307 fRes = Ses_ManFindNetworkExactCEGAR( pSes, nGates, &pSol );
2308
2309 if ( fRes == 0 )
2310 {
2311 pSes->fHitResLimit = 1;
2312 break;
2313 }
2314 else if ( fRes == 1 || fRes == 3 )
2315 break;
2316 }
2317
2318 Abc_DebugErase( pSes->nDebugOffset + ( nGates >= 10 ? 5 : 4 ), pSes->fVeryVerbose );
2319
2320 return pSol;
2321 }
2322
Ses_ManFindMinimumSizeTopDown(Ses_Man_t * pSes,int nMinGates)2323 static char * Ses_ManFindMinimumSizeTopDown( Ses_Man_t * pSes, int nMinGates )
2324 {
2325 int nGates = pSes->nMaxGates, fRes;
2326 char * pSol = NULL, * pSol2 = NULL;
2327
2328 pSes->fHitResLimit = 0;
2329
2330 Abc_DebugPrintIntInt( " (%d/%d)", nGates, pSes->nMaxGates, pSes->fVeryVerbose );
2331
2332 while ( true )
2333 {
2334 fRes = Ses_ManFindNetworkExactCEGAR( pSes, nGates, &pSol2 );
2335
2336 if ( fRes == 0 )
2337 {
2338 pSes->fHitResLimit = 1;
2339 break;
2340 }
2341 else if ( fRes == 2 || fRes == 3 )
2342 break;
2343
2344 pSol = pSol2;
2345
2346 if ( nGates == nMinGates )
2347 break;
2348
2349 --nGates;
2350 }
2351
2352 Abc_DebugErase( pSes->nDebugOffset + ( nGates >= 10 ? 5 : 4 ), pSes->fVeryVerbose );
2353
2354 return pSol;
2355 }
2356
Ses_ManFindMinimumSize(Ses_Man_t * pSes)2357 static char * Ses_ManFindMinimumSize( Ses_Man_t * pSes )
2358 {
2359 char * pSol = NULL;
2360 int i = pSes->nStartGates + 1, fRes;
2361
2362 /* if more than one function, no CEGAR */
2363 if ( pSes->nSpecFunc > 1 )
2364 {
2365 while ( true )
2366 {
2367 if ( pSes->fVerbose )
2368 {
2369 printf( "try with %d gates\n", i );
2370 }
2371
2372 memset( pSes->pTtValues, ~0, 4 * sizeof( word ) );
2373 fRes = Ses_ManFindNetworkExact( pSes, i++ );
2374 if ( fRes == 2 ) continue;
2375 if ( fRes == 0 ) break;
2376
2377 pSol = Ses_ManExtractSolution( pSes );
2378 break;
2379 }
2380
2381 return pSol;
2382 }
2383
2384 /* do the arrival times allow for a network? */
2385 if ( pSes->nMaxDepth != -1 && pSes->pArrTimeProfile )
2386 {
2387 if ( !Ses_CheckDepthConsistency( pSes ) )
2388 return 0;
2389 Ses_ManComputeMaxGates( pSes );
2390 }
2391
2392 pSol = Ses_ManFindMinimumSizeBottomUp( pSes );
2393
2394 if ( !pSol && pSes->nMaxDepth != -1 && pSes->fHitResLimit && pSes->nGates != pSes->nMaxGates )
2395 return Ses_ManFindMinimumSizeTopDown( pSes, pSes->nGates + 1 );
2396 else
2397 return pSol;
2398 }
2399
2400
2401 /**Function*************************************************************
2402
2403 Synopsis [Find minimum size networks with a SAT solver.]
2404
2405 Description [If nMaxDepth is -1, then depth constraints are ignored.
2406 If nMaxDepth is not -1, one can set pArrTimeProfile which should have the length of nVars.
2407 One can ignore pArrTimeProfile by setting it to NULL.]
2408
2409 SideEffects []
2410
2411 SeeAlso []
2412
2413 ***********************************************************************/
Abc_NtkFindExact(word * pTruth,int nVars,int nFunc,int nMaxDepth,int * pArrTimeProfile,int nBTLimit,int nStartGates,int fVerbose)2414 Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int nBTLimit, int nStartGates, int fVerbose )
2415 {
2416 Ses_Man_t * pSes;
2417 char * pSol;
2418 Abc_Ntk_t * pNtk = NULL;
2419 abctime timeStart;
2420
2421 /* some checks */
2422 assert( nVars >= 2 && nVars <= 8 );
2423
2424 timeStart = Abc_Clock();
2425
2426 pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 0, nBTLimit, fVerbose );
2427 pSes->nStartGates = nStartGates;
2428 pSes->fReasonVerbose = 0;
2429 pSes->fSatVerbose = 0;
2430 if ( fVerbose )
2431 Ses_ManPrintFuncs( pSes );
2432
2433 if ( ( pSol = Ses_ManFindMinimumSize( pSes ) ) != NULL )
2434 {
2435 pNtk = Ses_ManExtractNtk( pSol );
2436 ABC_FREE( pSol );
2437 }
2438
2439 pSes->timeTotal = Abc_Clock() - timeStart;
2440
2441 if ( fVerbose )
2442 Ses_ManPrintRuntime( pSes );
2443
2444 /* cleanup */
2445 Ses_ManClean( pSes );
2446
2447 return pNtk;
2448 }
2449
Gia_ManFindExact(word * pTruth,int nVars,int nFunc,int nMaxDepth,int * pArrTimeProfile,int nBTLimit,int nStartGates,int fVerbose)2450 Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int nBTLimit, int nStartGates, int fVerbose )
2451 {
2452 Ses_Man_t * pSes;
2453 char * pSol;
2454 Gia_Man_t * pGia = NULL;
2455 abctime timeStart;
2456
2457 /* some checks */
2458 assert( nVars >= 2 && nVars <= 8 );
2459
2460 timeStart = Abc_Clock();
2461
2462 pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 1, nBTLimit, fVerbose );
2463 pSes->nStartGates = nStartGates;
2464 pSes->fVeryVerbose = 1;
2465 pSes->fExtractVerbose = 0;
2466 pSes->fSatVerbose = 0;
2467 pSes->fReasonVerbose = 1;
2468 if ( fVerbose )
2469 Ses_ManPrintFuncs( pSes );
2470
2471 if ( ( pSol = Ses_ManFindMinimumSize( pSes ) ) != NULL )
2472 {
2473 pGia = Ses_ManExtractGia( pSol );
2474 ABC_FREE( pSol );
2475 }
2476
2477 pSes->timeTotal = Abc_Clock() - timeStart;
2478
2479 if ( fVerbose )
2480 Ses_ManPrintRuntime( pSes );
2481
2482 /* cleanup */
2483 Ses_ManClean( pSes );
2484
2485 return pGia;
2486 }
2487
2488 /**Function*************************************************************
2489
2490 Synopsis [Some test cases.]
2491
2492 ***********************************************************************/
2493
Abc_NtkFromTruthTable(word * pTruth,int nVars)2494 Abc_Ntk_t * Abc_NtkFromTruthTable( word * pTruth, int nVars )
2495 {
2496 Abc_Ntk_t * pNtk;
2497 Mem_Flex_t * pMan;
2498 char * pSopCover;
2499
2500 pMan = Mem_FlexStart();
2501 pSopCover = Abc_SopCreateFromTruth( pMan, nVars, (unsigned*)pTruth );
2502 pNtk = Abc_NtkCreateWithNode( pSopCover );
2503 Abc_NtkShortNames( pNtk );
2504 Mem_FlexStop( pMan, 0 );
2505
2506 return pNtk;
2507 }
2508
Abc_ExactTestSingleOutput(int fVerbose)2509 void Abc_ExactTestSingleOutput( int fVerbose )
2510 {
2511 extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit );
2512
2513 word pTruth[4] = {0xcafe, 0, 0, 0};
2514 Abc_Ntk_t * pNtk, * pNtk2, * pNtk3, * pNtk4;
2515 int pArrTimeProfile[4] = {6, 2, 8, 5};
2516
2517 pNtk = Abc_NtkFromTruthTable( pTruth, 4 );
2518
2519 pNtk2 = Abc_NtkFindExact( pTruth, 4, 1, -1, NULL, 0, 0, fVerbose );
2520 Abc_NtkShortNames( pNtk2 );
2521 Abc_NtkCecSat( pNtk, pNtk2, 10000, 0 );
2522 assert( pNtk2 );
2523 assert( Abc_NtkNodeNum( pNtk2 ) == 6 );
2524 Abc_NtkDelete( pNtk2 );
2525
2526 pNtk3 = Abc_NtkFindExact( pTruth, 4, 1, 3, NULL, 0, 0, fVerbose );
2527 Abc_NtkShortNames( pNtk3 );
2528 Abc_NtkCecSat( pNtk, pNtk3, 10000, 0 );
2529 assert( pNtk3 );
2530 assert( Abc_NtkLevel( pNtk3 ) <= 3 );
2531 Abc_NtkDelete( pNtk3 );
2532
2533 pNtk4 = Abc_NtkFindExact( pTruth, 4, 1, 9, pArrTimeProfile, 50000, 0, fVerbose );
2534 Abc_NtkShortNames( pNtk4 );
2535 Abc_NtkCecSat( pNtk, pNtk4, 10000, 0 );
2536 assert( pNtk4 );
2537 assert( Abc_NtkLevel( pNtk4 ) <= 9 );
2538 Abc_NtkDelete( pNtk4 );
2539
2540 assert( !Abc_NtkFindExact( pTruth, 4, 1, 2, NULL, 50000, 0, fVerbose ) );
2541
2542 assert( !Abc_NtkFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, 0, fVerbose ) );
2543
2544 Abc_NtkDelete( pNtk );
2545 }
2546
Abc_ExactTestSingleOutputAIG(int fVerbose)2547 void Abc_ExactTestSingleOutputAIG( int fVerbose )
2548 {
2549 word pTruth[4] = {0xcafe, 0, 0, 0};
2550 Abc_Ntk_t * pNtk;
2551 Gia_Man_t * pGia, * pGia2, * pGia3, * pGia4, * pMiter;
2552 Cec_ParCec_t ParsCec, * pPars = &ParsCec;
2553 int pArrTimeProfile[4] = {6, 2, 8, 5};
2554
2555 Cec_ManCecSetDefaultParams( pPars );
2556
2557 pNtk = Abc_NtkFromTruthTable( pTruth, 4 );
2558 Abc_NtkToAig( pNtk );
2559 pGia = Abc_NtkAigToGia( pNtk, 1 );
2560
2561 pGia2 = Gia_ManFindExact( pTruth, 4, 1, -1, NULL, 0, 0, fVerbose );
2562 pMiter = Gia_ManMiter( pGia, pGia2, 0, 1, 0, 0, 1 );
2563 assert( pMiter );
2564 Cec_ManVerify( pMiter, pPars );
2565 Gia_ManStop( pMiter );
2566
2567 pGia3 = Gia_ManFindExact( pTruth, 4, 1, 3, NULL, 0, 0, fVerbose );
2568 pMiter = Gia_ManMiter( pGia, pGia3, 0, 1, 0, 0, 1 );
2569 assert( pMiter );
2570 Cec_ManVerify( pMiter, pPars );
2571 Gia_ManStop( pMiter );
2572
2573 pGia4 = Gia_ManFindExact( pTruth, 4, 1, 9, pArrTimeProfile, 50000, 0, fVerbose );
2574 pMiter = Gia_ManMiter( pGia, pGia4, 0, 1, 0, 0, 1 );
2575 assert( pMiter );
2576 Cec_ManVerify( pMiter, pPars );
2577 Gia_ManStop( pMiter );
2578
2579 assert( !Gia_ManFindExact( pTruth, 4, 1, 2, NULL, 50000, 0, fVerbose ) );
2580
2581 assert( !Gia_ManFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, 0, fVerbose ) );
2582
2583 Gia_ManStop( pGia );
2584 Gia_ManStop( pGia2 );
2585 Gia_ManStop( pGia3 );
2586 Gia_ManStop( pGia4 );
2587 }
2588
Abc_ExactTest(int fVerbose)2589 void Abc_ExactTest( int fVerbose )
2590 {
2591 Abc_ExactTestSingleOutput( fVerbose );
2592 Abc_ExactTestSingleOutputAIG( fVerbose );
2593
2594 printf( "\n" );
2595 }
2596
2597
2598 /**Function*************************************************************
2599
2600 Synopsis [APIs for integraging with the mapper.]
2601
2602 ***********************************************************************/
2603 // may need to have a static pointer to the SAT-based synthesis engine and/or loaded library
2604 // this procedure should return 1, if the engine/library are available, and 0 otherwise
Abc_ExactIsRunning()2605 int Abc_ExactIsRunning()
2606 {
2607 return s_pSesStore != NULL;
2608 }
2609 // this procedure returns the number of inputs of the library
2610 // for example, somebody may try to map into 10-cuts while the library only contains 8-functions
Abc_ExactInputNum()2611 int Abc_ExactInputNum()
2612 {
2613 return 8;
2614 }
2615 // start exact store manager
Abc_ExactStart(int nBTLimit,int fMakeAIG,int fVerbose,int fVeryVerbose,const char * pFilename)2616 void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, int fVeryVerbose, const char * pFilename )
2617 {
2618 if ( !s_pSesStore )
2619 {
2620 s_pSesStore = Ses_StoreAlloc( nBTLimit, fMakeAIG, fVerbose );
2621 s_pSesStore->fVeryVerbose = fVeryVerbose;
2622 if ( pFilename )
2623 {
2624 Ses_StoreRead( s_pSesStore, pFilename, 1, 0, 0, 0 );
2625
2626 s_pSesStore->szDBName = ABC_CALLOC( char, strlen( pFilename ) + 1 );
2627 strcpy( s_pSesStore->szDBName, pFilename );
2628 }
2629 if ( s_pSesStore->fVeryVerbose )
2630 {
2631 s_pSesStore->pDebugEntries = fopen( "bms.debug", "w" );
2632 }
2633 }
2634 else
2635 printf( "BMS manager already started\n" );
2636 }
2637 // stop exact store manager
Abc_ExactStop(const char * pFilename)2638 void Abc_ExactStop( const char * pFilename )
2639 {
2640 if ( s_pSesStore )
2641 {
2642 if ( pFilename )
2643 Ses_StoreWrite( s_pSesStore, pFilename, 1, 0, 0, 0 );
2644 if ( s_pSesStore->pDebugEntries )
2645 fclose( s_pSesStore->pDebugEntries );
2646 Ses_StoreClean( s_pSesStore );
2647 }
2648 else
2649 printf( "BMS manager has not been started\n" );
2650 }
2651 // show statistics about store manager
Abc_ExactStats()2652 void Abc_ExactStats()
2653 {
2654 int i;
2655
2656 if ( !s_pSesStore )
2657 {
2658 printf( "BMS manager has not been started\n" );
2659 return;
2660 }
2661
2662 printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
2663 printf( " 0 1 2 3 4 5 6 7 8 total\n" );
2664 printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
2665 printf( "number of considered cuts :" );
2666 for ( i = 0; i < 9; ++i )
2667 printf( "%10lu", s_pSesStore->pCutCount[i] );
2668 printf( "%10lu\n", s_pSesStore->nCutCount );
2669 printf( " - trivial :" );
2670 for ( i = 0; i < 9; ++i )
2671 printf( "%10lu", s_pSesStore->pSynthesizedTrivial[i] );
2672 printf( "%10lu\n", s_pSesStore->nSynthesizedTrivial );
2673 printf( " - synth (imp) :" );
2674 for ( i = 0; i < 9; ++i )
2675 printf( "%10lu", s_pSesStore->pSynthesizedImp[i] );
2676 printf( "%10lu\n", s_pSesStore->nSynthesizedImp );
2677 printf( " - synth (res) :" );
2678 for ( i = 0; i < 9; ++i )
2679 printf( "%10lu", s_pSesStore->pSynthesizedRL[i] );
2680 printf( "%10lu\n", s_pSesStore->nSynthesizedRL );
2681 printf( " - not synth (imp) :" );
2682 for ( i = 0; i < 9; ++i )
2683 printf( "%10lu", s_pSesStore->pUnsynthesizedImp[i] );
2684 printf( "%10lu\n", s_pSesStore->nUnsynthesizedImp );
2685 printf( " - not synth (res) :" );
2686 for ( i = 0; i < 9; ++i )
2687 printf( "%10lu", s_pSesStore->pUnsynthesizedRL[i] );
2688 printf( "%10lu\n", s_pSesStore->nUnsynthesizedRL );
2689 printf( " - cache hits :" );
2690 for ( i = 0; i < 9; ++i )
2691 printf( "%10lu", s_pSesStore->pCacheHits[i] );
2692 printf( "%10lu\n", s_pSesStore->nCacheHits );
2693 printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
2694 printf( "number of entries : %d\n", s_pSesStore->nEntriesCount );
2695 printf( "number of valid entries : %d\n", s_pSesStore->nValidEntriesCount );
2696 printf( "number of invalid entries : %d\n", s_pSesStore->nEntriesCount - s_pSesStore->nValidEntriesCount );
2697 printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
2698 printf( "number of SAT calls : %lu\n", s_pSesStore->nSatCalls );
2699 printf( "number of UNSAT calls : %lu\n", s_pSesStore->nUnsatCalls );
2700 printf( "number of UNDEF calls : %lu\n", s_pSesStore->nUndefCalls );
2701
2702 printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
2703 printf( "Runtime breakdown:\n" );
2704 ABC_PRTP( "Exact ", s_pSesStore->timeExact, s_pSesStore->timeTotal );
2705 ABC_PRTP( " Sat ", s_pSesStore->timeSat, s_pSesStore->timeTotal );
2706 ABC_PRTP( " Sat ", s_pSesStore->timeSatSat, s_pSesStore->timeTotal );
2707 ABC_PRTP( " Unsat ", s_pSesStore->timeSatUnsat, s_pSesStore->timeTotal );
2708 ABC_PRTP( " Undef ", s_pSesStore->timeSatUndef, s_pSesStore->timeTotal );
2709 ABC_PRTP( " Instance", s_pSesStore->timeInstance, s_pSesStore->timeTotal );
2710 ABC_PRTP( "Other ", s_pSesStore->timeTotal - s_pSesStore->timeExact, s_pSesStore->timeTotal );
2711 ABC_PRTP( "ALL ", s_pSesStore->timeTotal, s_pSesStore->timeTotal );
2712 }
2713 // this procedure takes TT and input arrival times (pArrTimeProfile) and return the smallest output arrival time;
2714 // it also returns the pin-to-pin delays (pPerm) between each cut leaf and the cut output and the cut area cost (Cost)
2715 // the area cost should not exceed 2048, if the cut is implementable; otherwise, it should be ABC_INFINITY
Abc_ExactDelayCost(word * pTruth,int nVars,int * pArrTimeProfile,char * pPerm,int * Cost,int AigLevel)2716 int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * pPerm, int * Cost, int AigLevel )
2717 {
2718 int i, nMaxArrival, nDelta, l;
2719 Ses_Man_t * pSes = NULL;
2720 char * pSol = NULL, * pSol2 = NULL, * p;
2721 int pNormalArrTime[8];
2722 int Delay = ABC_INFINITY, nMaxDepth, fResLimit;
2723 abctime timeStart = Abc_Clock(), timeStartExact;
2724
2725 /* some checks */
2726 if ( nVars < 0 || nVars > 8 )
2727 {
2728 printf( "invalid truth table size %d\n", nVars );
2729 assert( 0 );
2730 }
2731
2732 /* statistics */
2733 s_pSesStore->nCutCount++;
2734 s_pSesStore->pCutCount[nVars]++;
2735
2736 if ( nVars == 0 )
2737 {
2738 s_pSesStore->nSynthesizedTrivial++;
2739 s_pSesStore->pSynthesizedTrivial[0]++;
2740
2741 *Cost = 0;
2742 s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
2743 return 0;
2744 }
2745
2746 if ( nVars == 1 )
2747 {
2748 s_pSesStore->nSynthesizedTrivial++;
2749 s_pSesStore->pSynthesizedTrivial[1]++;
2750
2751 *Cost = 0;
2752 pPerm[0] = (char)0;
2753 s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
2754 return pArrTimeProfile[0];
2755 }
2756
2757 for ( l = 0; l < nVars; ++l )
2758 pNormalArrTime[l] = pArrTimeProfile[l];
2759
2760 nDelta = Abc_NormalizeArrivalTimes( pNormalArrTime, nVars, &nMaxArrival );
2761
2762 *Cost = ABC_INFINITY;
2763
2764 if ( Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, &pSol ) )
2765 {
2766 s_pSesStore->nCacheHits++;
2767 s_pSesStore->pCacheHits[nVars]++;
2768 }
2769 else
2770 {
2771 if ( s_pSesStore->fVeryVerbose )
2772 {
2773 printf( ANSI_COLOR_CYAN );
2774 Abc_TtPrintHexRev( stdout, pTruth, nVars );
2775 printf( ANSI_COLOR_RESET );
2776 printf( " [%d", pNormalArrTime[0] );
2777 for ( l = 1; l < nVars; ++l )
2778 printf( " %d", pNormalArrTime[l] );
2779 printf( "]@%d:", AigLevel );
2780 fflush( stdout );
2781 }
2782
2783 nMaxDepth = pNormalArrTime[0];
2784 for ( i = 1; i < nVars; ++i )
2785 nMaxDepth = Abc_MaxInt( nMaxDepth, pNormalArrTime[i] );
2786 nMaxDepth += nVars + 1;
2787 if ( AigLevel != -1 )
2788 nMaxDepth = Abc_MinInt( AigLevel - nDelta, nMaxDepth + nVars + 1 );
2789
2790 timeStartExact = Abc_Clock();
2791
2792 pSes = Ses_ManAlloc( pTruth, nVars, 1 /* nSpecFunc */, nMaxDepth, pNormalArrTime, s_pSesStore->fMakeAIG, s_pSesStore->nBTLimit, s_pSesStore->fVerbose );
2793 pSes->fVeryVerbose = s_pSesStore->fVeryVerbose;
2794 pSes->pSat = s_pSesStore->pSat;
2795 pSes->nStartGates = nVars - 2;
2796
2797 while ( pSes->nMaxDepth ) /* there is improvement */
2798 {
2799 if ( s_pSesStore->fVeryVerbose )
2800 {
2801 printf( " %d", pSes->nMaxDepth );
2802 fflush( stdout );
2803 }
2804
2805 if ( ( pSol2 = Ses_ManFindMinimumSize( pSes ) ) != NULL )
2806 {
2807 if ( s_pSesStore->fVeryVerbose )
2808 {
2809 if ( pSes->nMaxDepth >= 10 ) printf( "\b" );
2810 printf( "\b" ANSI_COLOR_GREEN "%d" ANSI_COLOR_RESET, pSes->nMaxDepth );
2811 }
2812 if ( pSol )
2813 ABC_FREE( pSol );
2814 pSol = pSol2;
2815 pSes->nMaxDepth--;
2816 }
2817 else
2818 {
2819 if ( s_pSesStore->fVeryVerbose )
2820 {
2821 if ( pSes->nMaxDepth >= 10 ) printf( "\b" );
2822 printf( "\b%s%d" ANSI_COLOR_RESET, pSes->fHitResLimit ? ANSI_COLOR_RED : ANSI_COLOR_YELLOW, pSes->nMaxDepth );
2823 }
2824 break;
2825 }
2826 }
2827
2828 if ( s_pSesStore->fVeryVerbose )
2829 printf( " \n" );
2830
2831 /* log unsuccessful case for debugging */
2832 if ( s_pSesStore->pDebugEntries && pSes->fHitResLimit )
2833 Ses_StorePrintDebugEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, pSes->nMaxDepth, pSol, nVars - 2 );
2834
2835 pSes->timeTotal = Abc_Clock() - timeStartExact;
2836
2837 /* statistics */
2838 s_pSesStore->nSatCalls += pSes->nSatCalls;
2839 s_pSesStore->nUnsatCalls += pSes->nUnsatCalls;
2840 s_pSesStore->nUndefCalls += pSes->nUndefCalls;
2841
2842 s_pSesStore->timeSat += pSes->timeSat;
2843 s_pSesStore->timeSatSat += pSes->timeSatSat;
2844 s_pSesStore->timeSatUnsat += pSes->timeSatUnsat;
2845 s_pSesStore->timeSatUndef += pSes->timeSatUndef;
2846 s_pSesStore->timeInstance += pSes->timeInstance;
2847 s_pSesStore->timeExact += pSes->timeTotal;
2848
2849 /* cleanup (we need to clean before adding since pTruth may have been modified by pSes) */
2850 fResLimit = pSes->fHitResLimit;
2851 Ses_ManCleanLight( pSes );
2852
2853 /* store solution */
2854 Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, pSol, fResLimit );
2855 }
2856
2857 if ( pSol )
2858 {
2859 *Cost = pSol[ABC_EXACT_SOL_NGATES];
2860 p = pSol + 3 + 4 * pSol[ABC_EXACT_SOL_NGATES] + 1;
2861 Delay = *p++;
2862 for ( l = 0; l < nVars; ++l )
2863 pPerm[l] = *p++;
2864 }
2865
2866 if ( pSol )
2867 {
2868 int Delay2 = 0;
2869 for ( l = 0; l < nVars; ++l )
2870 {
2871 //printf( "%d ", pPerm[l] );
2872 Delay2 = Abc_MaxInt( Delay2, pArrTimeProfile[l] + pPerm[l] );
2873 }
2874 //printf( " output arrival = %d recomputed = %d\n", Delay, Delay2 );
2875 //if ( Delay != Delay2 )
2876 //{
2877 // printf( "^--- BUG!\n" );
2878 // assert( 0 );
2879 //}
2880
2881 s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
2882 return Delay2;
2883 }
2884 else
2885 {
2886 assert( *Cost == ABC_INFINITY );
2887
2888 s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
2889 return ABC_INFINITY;
2890 }
2891 }
2892 // this procedure returns a new node whose output in terms of the given fanins
2893 // has the smallest possible arrival time (in agreement with the above Abc_ExactDelayCost)
Abc_ExactBuildNode(word * pTruth,int nVars,int * pArrTimeProfile,Abc_Obj_t ** pFanins,Abc_Ntk_t * pNtk)2894 Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins, Abc_Ntk_t * pNtk )
2895 {
2896 char * pSol = NULL;
2897 int i, j, nMaxArrival;
2898 int pNormalArrTime[8];
2899 char const * p;
2900 Abc_Obj_t * pObj;
2901 Vec_Ptr_t * pGates;
2902 char pGateTruth[5];
2903 char * pSopCover;
2904 abctime timeStart = Abc_Clock();
2905
2906 if ( nVars == 0 )
2907 {
2908 s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
2909 return (pTruth[0] & 1) ? Abc_NtkCreateNodeConst1(pNtk) : Abc_NtkCreateNodeConst0(pNtk);
2910 }
2911 if ( nVars == 1 )
2912 {
2913 s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
2914 return (pTruth[0] & 1) ? Abc_NtkCreateNodeInv(pNtk, pFanins[0]) : Abc_NtkCreateNodeBuf(pNtk, pFanins[0]);
2915 }
2916
2917 for ( i = 0; i < nVars; ++i )
2918 pNormalArrTime[i] = pArrTimeProfile[i];
2919 Abc_NormalizeArrivalTimes( pNormalArrTime, nVars, &nMaxArrival );
2920 assert( Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, &pSol ) );
2921 if ( !pSol )
2922 {
2923 s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
2924 return NULL;
2925 }
2926
2927 assert( pSol[ABC_EXACT_SOL_NVARS] == nVars );
2928 assert( pSol[ABC_EXACT_SOL_NFUNC] == 1 );
2929
2930 pGates = Vec_PtrAlloc( nVars + pSol[ABC_EXACT_SOL_NGATES] );
2931 pGateTruth[3] = '0';
2932 pGateTruth[4] = '\0';
2933
2934 /* primary inputs */
2935 for ( i = 0; i < nVars; ++i )
2936 {
2937 assert( pFanins[i] );
2938 Vec_PtrPush( pGates, pFanins[i] );
2939 }
2940
2941 /* gates */
2942 p = pSol + 3;
2943 for ( i = 0; i < pSol[ABC_EXACT_SOL_NGATES]; ++i )
2944 {
2945 pGateTruth[2] = '0' + ( *p & 1 );
2946 pGateTruth[1] = '0' + ( ( *p >> 1 ) & 1 );
2947 pGateTruth[0] = '0' + ( ( *p >> 2 ) & 1 );
2948 ++p;
2949
2950 assert( *p == 2 ); /* binary gate */
2951 ++p;
2952
2953 /* invert truth table if we are last gate and inverted */
2954 if ( i + 1 == pSol[ABC_EXACT_SOL_NGATES] && Abc_LitIsCompl( *( p + 2 ) ) )
2955 for ( j = 0; j < 4; ++j )
2956 pGateTruth[j] = ( pGateTruth[j] == '0' ) ? '1' : '0';
2957
2958 pSopCover = Abc_SopFromTruthBin( pGateTruth );
2959 pObj = Abc_NtkCreateNode( pNtk );
2960 assert( pObj );
2961 pObj->pData = Abc_SopRegister( (Mem_Flex_t*)pNtk->pManFunc, pSopCover );
2962 Vec_PtrPush( pGates, pObj );
2963 ABC_FREE( pSopCover );
2964
2965 Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) );
2966 Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) );
2967 }
2968
2969 /* output */
2970 pObj = (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) );
2971
2972 Vec_PtrFree( pGates );
2973
2974 s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
2975 return pObj;
2976 }
2977
Abc_ExactStoreTest(int fVerbose)2978 void Abc_ExactStoreTest( int fVerbose )
2979 {
2980 int i;
2981 word pTruth[4] = {0xcafe, 0, 0, 0};
2982 int pArrTimeProfile[4] = {6, 2, 8, 5};
2983 Abc_Ntk_t * pNtk;
2984 Abc_Obj_t * pFanins[4];
2985 Vec_Ptr_t * vNames;
2986 char pPerm[4] = {0};
2987 int Cost = 0;
2988
2989 pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
2990 pNtk->pName = Extra_UtilStrsav( "exact" );
2991 vNames = Abc_NodeGetFakeNames( 4u );
2992
2993 /* primary inputs */
2994 Vec_PtrPush( pNtk->vObjs, NULL );
2995 for ( i = 0; i < 4; ++i )
2996 {
2997 pFanins[i] = Abc_NtkCreatePi( pNtk );
2998 Abc_ObjAssignName( pFanins[i], (char*)Vec_PtrEntry( vNames, i ), NULL );
2999 }
3000 Abc_NodeFreeNames( vNames );
3001
3002 Abc_ExactStart( 10000, 1, fVerbose, 0, NULL );
3003
3004 assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins, pNtk ) );
3005
3006 assert( Abc_ExactDelayCost( pTruth, 4, pArrTimeProfile, pPerm, &Cost, 12 ) == 1 );
3007
3008 assert( Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins, pNtk ) );
3009
3010 (*pArrTimeProfile)++;
3011 assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins, pNtk ) );
3012 (*pArrTimeProfile)--;
3013
3014 Abc_ExactStop( NULL );
3015
3016 Abc_NtkDelete( pNtk );
3017 }
3018
3019 ////////////////////////////////////////////////////////////////////////
3020 /// END OF FILE ///
3021 ////////////////////////////////////////////////////////////////////////
3022
3023
3024 ABC_NAMESPACE_IMPL_END
3025