ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
bmcMaj.c
Go to the documentation of this file.
1
20
21#include "bmc.h"
22#include "misc/extra/extra.h"
23#include "misc/util/utilTruth.h"
24#include "sat/glucose/AbcGlucose.h"
25#include "aig/miniaig/miniaig.h"
26#include "base/io/ioResub.h"
27#include "base/main/main.h"
28#include "base/cmd/cmd.h"
29
30ABC_NAMESPACE_IMPL_START
31
32
33#ifdef WIN32
34#include <process.h>
35#define unlink _unlink
36#else
37#include <unistd.h>
38#endif
39
43
44#define MAJ_NOBJS 64 // Const0 + Const1 + nVars + nNodes
45
46typedef struct Maj_Man_t_ Maj_Man_t;
47struct Maj_Man_t_
48{
49 int nVars; // inputs
50 int nNodes; // internal nodes
51 int nObjs; // total objects (2 consts, nVars inputs, nNodes internal nodes)
52 int nWords; // the truth table size in 64-bit words
53 int iVar; // the next available SAT variable
54 int fUseConst; // use constant fanins
55 int fUseLine; // use cascade topology
56 Vec_Wrd_t * vInfo; // Const0 + Const1 + nVars + nNodes + Maj(nVars)
57 int VarMarks[MAJ_NOBJS][3][MAJ_NOBJS]; // variable marks
58 int VarVals[MAJ_NOBJS+2]; // values of the first 2 + nVars variables
59 Vec_Wec_t * vOutLits; // output vars
60 bmcg_sat_solver * pSat; // SAT solver
61};
62
63static inline word * Maj_ManTruth( Maj_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); }
64
68
80int Maj_ManValue( int iMint, int nVars )
81{
82 int k, Count = 0;
83 for ( k = 0; k < nVars; k++ )
84 Count += (iMint >> k) & 1;
85 return (int)(Count > nVars/2);
86}
87Vec_Wrd_t * Maj_ManTruthTables( Maj_Man_t * p )
88{
89 Vec_Wrd_t * vInfo = p->vInfo = Vec_WrdStart( p->nWords * (p->nObjs + 1) );
90 int i, nMints = Abc_MaxInt( 64, 1 << p->nVars );
91 Abc_TtFill( Maj_ManTruth(p, 1), p->nWords );
92 for ( i = 0; i < p->nVars; i++ )
93 Abc_TtIthVar( Maj_ManTruth(p, i+2), i, p->nVars );
94 for ( i = 0; i < nMints; i++ )
95 if ( Maj_ManValue(i, p->nVars) )
96 Abc_TtSetBit( Maj_ManTruth(p, p->nObjs), i );
97 //Dau_DsdPrintFromTruth( Maj_ManTruth(p, p->nObjs), p->nVars );
98 return vInfo;
99}
100int Maj_ManMarkup( Maj_Man_t * p )
101{
102 int i, k, j;
103 p->iVar = 1;
104 assert( p->nObjs <= MAJ_NOBJS );
105 // make exception for the first node
106 i = p->nVars + 2;
107 for ( k = 0; k < 3; k++ )
108 {
109 j = 4-k;
110 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
111 p->VarMarks[i][k][j] = p->iVar++;
112 }
113 // assign variables for other nodes
114 for ( i = p->nVars + 3; i < p->nObjs; i++ )
115 {
116 for ( k = 0; k < 3; k++ )
117 {
118 if ( p->fUseLine && k == 0 )
119 {
120 j = i-1;
121 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
122 p->VarMarks[i][k][j] = p->iVar++;
123 continue;
124 }
125 for ( j = (p->fUseConst && k == 2) ? 0 : 2; j < i - k; j++ )
126 {
127 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
128 p->VarMarks[i][k][j] = p->iVar++;
129 }
130 }
131 }
132 printf( "The number of parameter variables = %d.\n", p->iVar );
133 return p->iVar;
134 // printout
135 for ( i = p->nVars + 2; i < p->nObjs; i++ )
136 {
137 printf( "Node %d\n", i );
138 for ( j = 0; j < p->nObjs; j++ )
139 {
140 for ( k = 0; k < 3; k++ )
141 printf( "%3d ", p->VarMarks[i][k][j] );
142 printf( "\n" );
143 }
144 }
145 return p->iVar;
146}
147Maj_Man_t * Maj_ManAlloc( int nVars, int nNodes, int fUseConst, int fUseLine )
148{
149 Maj_Man_t * p = ABC_CALLOC( Maj_Man_t, 1 );
150 p->nVars = nVars;
151 p->nNodes = nNodes;
152 p->nObjs = 2 + nVars + nNodes;
153 p->fUseConst = fUseConst;
154 p->fUseLine = fUseLine;
155 p->nWords = Abc_TtWordNum(nVars);
156 p->vOutLits = Vec_WecStart( p->nObjs );
157 p->iVar = Maj_ManMarkup( p );
158 p->VarVals[1] = 1;
159 p->vInfo = Maj_ManTruthTables( p );
160 p->pSat = bmcg_sat_solver_start();
161 bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
162 return p;
163}
164void Maj_ManFree( Maj_Man_t * p )
165{
166 bmcg_sat_solver_stop( p->pSat );
167 Vec_WrdFree( p->vInfo );
168 Vec_WecFree( p->vOutLits );
169 ABC_FREE( p );
170}
171
172
184static inline int Maj_ManFindFanin( Maj_Man_t * p, int i, int k )
185{
186 int j, Count = 0, iVar = -1;
187 for ( j = 0; j < p->nObjs; j++ )
188 if ( p->VarMarks[i][k][j] && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k][j]) )
189 {
190 iVar = j;
191 Count++;
192 }
193 assert( Count == 1 );
194 return iVar;
195}
196static inline int Maj_ManEval( Maj_Man_t * p )
197{
198 int fUseMiddle = 1;
199 static int Flag = 0;
200 int i, k, iMint; word * pFanins[3];
201 for ( i = p->nVars + 2; i < p->nObjs; i++ )
202 {
203 for ( k = 0; k < 3; k++ )
204 pFanins[k] = Maj_ManTruth( p, Maj_ManFindFanin(p, i, k) );
205 Abc_TtMaj( Maj_ManTruth(p, i), pFanins[0], pFanins[1], pFanins[2], p->nWords );
206 }
207 if ( fUseMiddle )
208 {
209 iMint = -1;
210 for ( i = 0; i < (1 << p->nVars); i++ )
211 {
212 int nOnes = Abc_TtBitCount16(i);
213 if ( nOnes < p->nVars/2 || nOnes > p->nVars/2+1 )
214 continue;
215 if ( Abc_TtGetBit(Maj_ManTruth(p, p->nObjs), i) == Abc_TtGetBit(Maj_ManTruth(p, p->nObjs-1), i) )
216 continue;
217 iMint = i;
218 break;
219 }
220 }
221 else
222 {
223 if ( Flag && p->nVars >= 6 )
224 iMint = Abc_TtFindLastDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
225 else
226 iMint = Abc_TtFindFirstDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
227 }
228 //Flag ^= 1;
229 assert( iMint < (1 << p->nVars) );
230 return iMint;
231}
232
244void Maj_ManPrintSolution( Maj_Man_t * p )
245{
246 int i, k, iVar;
247 printf( "Realization of %d-input majority using %d MAJ3 gates:\n", p->nVars, p->nNodes );
248// for ( i = p->nVars + 2; i < p->nObjs; i++ )
249 for ( i = p->nObjs - 1; i >= p->nVars + 2; i-- )
250 {
251 printf( "%02d = MAJ(", i-2 );
252 for ( k = 2; k >= 0; k-- )
253 {
254 iVar = Maj_ManFindFanin( p, i, k );
255 if ( iVar >= 2 && iVar < p->nVars + 2 )
256 printf( " %c", 'a'+iVar-2 );
257 else if ( iVar < 2 )
258 printf( " %d", iVar );
259 else
260 printf( " %02d", iVar-2 );
261 }
262 printf( " )\n" );
263 }
264}
265
266
278int Maj_ManAddCnfStart( Maj_Man_t * p )
279{
280 int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m;
281 // input constraints
282 for ( i = p->nVars + 2; i < p->nObjs; i++ )
283 {
284 for ( k = 0; k < 3; k++ )
285 {
286 int nLits = 0;
287 for ( j = 0; j < p->nObjs; j++ )
288 if ( p->VarMarks[i][k][j] )
289 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
290 assert( nLits > 0 );
291 // input uniqueness
292 if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
293 return 0;
294 for ( n = 0; n < nLits; n++ )
295 for ( m = n+1; m < nLits; m++ )
296 {
297 pLits2[0] = Abc_LitNot(pLits[n]);
298 pLits2[1] = Abc_LitNot(pLits[m]);
299 if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
300 return 0;
301 }
302 if ( k == 2 )
303 break;
304 // symmetry breaking
305 for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
306 for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] )
307 {
308 pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
309 pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 );
310 if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
311 return 0;
312 }
313 }
314 }
315 // outputs should be used
316 for ( i = 2; i < p->nObjs - 1; i++ )
317 {
318 Vec_Int_t * vArray = Vec_WecEntry(p->vOutLits, i);
319 assert( Vec_IntSize(vArray) > 0 );
320 if ( !bmcg_sat_solver_addclause( p->pSat, Vec_IntArray(vArray), Vec_IntSize(vArray) ) )
321 return 0;
322 }
323 return 1;
324}
325int Maj_ManAddCnf( Maj_Man_t * p, int iMint )
326{
327 // save minterm values
328 int i, k, n, j, Value = Maj_ManValue(iMint, p->nVars);
329 for ( i = 0; i < p->nVars; i++ )
330 p->VarVals[i+2] = (iMint >> i) & 1;
331 bmcg_sat_solver_set_nvars( p->pSat, p->iVar + 4*p->nNodes );
332 //printf( "Adding clauses for minterm %d.\n", iMint );
333 for ( i = p->nVars + 2; i < p->nObjs; i++ )
334 {
335 // fanin connectivity
336 int iBaseSatVarI = p->iVar + 4*(i - p->nVars - 2);
337 for ( k = 0; k < 3; k++ )
338 {
339 for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
340 {
341 int iBaseSatVarJ = p->iVar + 4*(j - p->nVars - 2);
342 for ( n = 0; n < 2; n++ )
343 {
344 int pLits[3], nLits = 0;
345 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
346 pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + k, n );
347 if ( j >= p->nVars + 2 )
348 pLits[nLits++] = Abc_Var2Lit( iBaseSatVarJ + 3, !n );
349 else if ( p->VarVals[j] == n )
350 continue;
351 if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
352 return 0;
353 }
354 }
355 }
356 // node functionality
357 for ( n = 0; n < 2; n++ )
358 {
359 if ( i == p->nObjs - 1 && n == Value )
360 continue;
361 for ( k = 0; k < 3; k++ )
362 {
363 int pLits[3], nLits = 0;
364 if ( k != 0 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 0, n );
365 if ( k != 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 1, n );
366 if ( k != 2 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 2, n );
367 if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 3, !n );
368 assert( nLits <= 3 );
369 if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
370 return 0;
371 }
372 }
373 }
374 p->iVar += 4*p->nNodes;
375 return 1;
376}
377int Maj_ManExactSynthesis( int nVars, int nNodes, int fUseConst, int fUseLine, int fVerbose )
378{
379 int i, iMint = 0;
380 abctime clkTotal = Abc_Clock();
381 Maj_Man_t * p = Maj_ManAlloc( nVars, nNodes, fUseConst, fUseLine );
382 int status = Maj_ManAddCnfStart( p );
383 assert( status );
384 printf( "Running exact synthesis for %d-input majority with %d MAJ3 gates...\n", p->nVars, p->nNodes );
385 for ( i = 0; iMint != -1; i++ )
386 {
387 abctime clk = Abc_Clock();
388 if ( !Maj_ManAddCnf( p, iMint ) )
389 break;
390 status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
391 if ( fVerbose )
392 {
393 printf( "Iter %3d : ", i );
394 Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
395 printf( " Var =%5d ", p->iVar );
396 printf( "Cla =%6d ", bmcg_sat_solver_clausenum(p->pSat) );
397 printf( "Conf =%9d ", bmcg_sat_solver_conflictnum(p->pSat) );
398 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
399 }
400 if ( status == GLUCOSE_UNSAT )
401 {
402 printf( "The problem has no solution.\n" );
403 break;
404 }
405 iMint = Maj_ManEval( p );
406 }
407 if ( iMint == -1 )
408 Maj_ManPrintSolution( p );
409 Maj_ManFree( p );
410 Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
411 return iMint == -1;
412}
413
414
415
416
417
418
419
420
421typedef struct Exa_Man_t_ Exa_Man_t;
422struct Exa_Man_t_
423{
424 Bmc_EsPar_t * pPars; // parameters
425 int nVars; // inputs
426 int nNodes; // internal nodes
427 int nObjs; // total objects (nVars inputs + nNodes internal nodes)
428 int nWords; // the truth table size in 64-bit words
429 int iVar; // the next available SAT variable
430 word * pTruth; // truth table
431 Vec_Wrd_t * vInfo; // nVars + nNodes + 1
432 int VarMarks[MAJ_NOBJS][2][MAJ_NOBJS]; // variable marks
433 int VarVals[MAJ_NOBJS]; // values of the first nVars variables
434 Vec_Wec_t * vOutLits; // output vars
435 bmcg_sat_solver * pSat; // SAT solver
436 FILE * pFile;
437 int nCnfClauses;
438};
439
440static inline word * Exa_ManTruth( Exa_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); }
441
442
454Vec_Wrd_t * Exa_ManTruthTables( Exa_Man_t * p )
455{
456 Vec_Wrd_t * vInfo = p->vInfo = Vec_WrdStart( p->nWords * (p->nObjs+1) ); int i;
457 for ( i = 0; i < p->nVars; i++ )
458 Abc_TtIthVar( Exa_ManTruth(p, i), i, p->nVars );
459 //Dau_DsdPrintFromTruth( Exa_ManTruth(p, p->nObjs), p->nVars );
460 return vInfo;
461}
462int Exa_ManMarkup( Exa_Man_t * p )
463{
464 int i, k, j;
465 assert( p->nObjs <= MAJ_NOBJS );
466 // assign functionality
467 p->iVar = 1 + 3*p->nNodes;//
468 // assign connectivity variables
469 for ( i = p->nVars; i < p->nObjs; i++ )
470 {
471 for ( k = 0; k < 2; k++ )
472 {
473 if ( p->pPars->fFewerVars && i == p->nObjs - 1 && k == 0 )
474 {
475 j = p->nObjs - 2;
476 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
477 p->VarMarks[i][k][j] = p->iVar++;
478 continue;
479 }
480 for ( j = p->pPars->fFewerVars ? 1 - k : 0; j < i - k; j++ )
481 {
482 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
483 p->VarMarks[i][k][j] = p->iVar++;
484 }
485 }
486 }
487 printf( "The number of parameter variables = %d.\n", p->iVar );
488 return p->iVar;
489 // printout
490 for ( i = p->nVars; i < p->nObjs; i++ )
491 {
492 printf( "Node %d\n", i );
493 for ( j = 0; j < p->nObjs; j++ )
494 {
495 for ( k = 0; k < 2; k++ )
496 printf( "%3d ", p->VarMarks[i][k][j] );
497 printf( "\n" );
498 }
499 }
500 return p->iVar;
501}
502Exa_Man_t * Exa_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
503{
504 Exa_Man_t * p = ABC_CALLOC( Exa_Man_t, 1 );
505 p->pPars = pPars;
506 p->nVars = pPars->nVars;
507 p->nNodes = pPars->nNodes;
508 p->nObjs = pPars->nVars + pPars->nNodes;
509 p->nWords = Abc_TtWordNum(pPars->nVars);
510 p->pTruth = pTruth;
511 p->vOutLits = Vec_WecStart( p->nObjs );
512 p->iVar = Exa_ManMarkup( p );
513 p->vInfo = Exa_ManTruthTables( p );
514 p->pSat = bmcg_sat_solver_start();
515 bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
516 if ( pPars->RuntimeLim )
517 bmcg_sat_solver_set_runtime_limit( p->pSat, Abc_Clock() + pPars->RuntimeLim * CLOCKS_PER_SEC );
518 if ( pPars->fDumpCnf )
519 {
520 char Buffer[1000];
521 sprintf( Buffer, "%s_%d_%d.cnf", p->pPars->pTtStr, 2, p->nNodes );
522 p->pFile = fopen( Buffer, "wb" );
523 fputs( "p cnf \n", p->pFile );
524 }
525 return p;
526}
527void Exa_ManFree( Exa_Man_t * p )
528{
529 if ( p->pFile )
530 {
531 char Buffer[1000];
532 sprintf( Buffer, "%s_%d_%d.cnf", p->pPars->pTtStr, 2, p->nNodes );
533 rewind( p->pFile );
534 fprintf( p->pFile, "p cnf %d %d", bmcg_sat_solver_varnum(p->pSat), p->nCnfClauses );
535 fclose( p->pFile );
536 printf( "CNF was dumped into file \"%s\".\n", Buffer );
537 }
538 bmcg_sat_solver_stop( p->pSat );
539 Vec_WrdFree( p->vInfo );
540 Vec_WecFree( p->vOutLits );
541 ABC_FREE( p );
542}
543
544
556static inline int Exa_ManFindFanin( Exa_Man_t * p, int i, int k )
557{
558 int j, Count = 0, iVar = -1;
559 for ( j = 0; j < p->nObjs; j++ )
560 if ( p->VarMarks[i][k][j] && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k][j]) )
561 {
562 iVar = j;
563 Count++;
564 }
565 assert( Count == 1 );
566 return iVar;
567}
568static inline int Exa_ManEval( Exa_Man_t * p )
569{
570 static int Flag = 0;
571 int i, k, iMint; word * pFanins[2];
572 for ( i = p->nVars; i < p->nObjs; i++ )
573 {
574 int iVarStart = 1 + 3*(i - p->nVars);//
575 for ( k = 0; k < 2; k++ )
576 pFanins[k] = Exa_ManTruth( p, Exa_ManFindFanin(p, i, k) );
577 Abc_TtConst0( Exa_ManTruth(p, i), p->nWords );
578 for ( k = 1; k < 4; k++ )
579 {
580 if ( !bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+k-1) )
581 continue;
582 Abc_TtAndCompl( Exa_ManTruth(p, p->nObjs), pFanins[0], !(k&1), pFanins[1], !(k>>1), p->nWords );
583 Abc_TtOr( Exa_ManTruth(p, i), Exa_ManTruth(p, i), Exa_ManTruth(p, p->nObjs), p->nWords );
584 }
585 }
586 if ( Flag && p->nVars >= 6 )
587 iMint = Abc_TtFindLastDiffBit( Exa_ManTruth(p, p->nObjs-1), p->pTruth, p->nVars );
588 else
589 iMint = Abc_TtFindFirstDiffBit( Exa_ManTruth(p, p->nObjs-1), p->pTruth, p->nVars );
590 //Flag ^= 1;
591 assert( iMint < (1 << p->nVars) );
592 return iMint;
593}
594
606void Exa_ManDumpBlif( Exa_Man_t * p, int fCompl )
607{
608 char Buffer[1000];
609 char FileName[1100];
610 FILE * pFile;
611 int i, k, iVar;
612 if ( fCompl )
613 Abc_TtNot( p->pTruth, p->nWords );
614 Extra_PrintHexadecimalString( Buffer, (unsigned *)p->pTruth, p->nVars );
615 if ( fCompl )
616 Abc_TtNot( p->pTruth, p->nWords );
617 sprintf( FileName, "%s_%d_%d.blif", Buffer, 2, p->nNodes );
618 pFile = fopen( FileName, "wb" );
619 fprintf( pFile, "# Realization of the %d-input function %s using %d two-input gates:\n", p->nVars, Buffer, p->nNodes );
620 fprintf( pFile, ".model %s_%d_%d\n", Buffer, 2, p->nNodes );
621 fprintf( pFile, ".inputs" );
622 for ( i = 0; i < p->nVars; i++ )
623 fprintf( pFile, " %c", 'a'+i );
624 fprintf( pFile, "\n" );
625 fprintf( pFile, ".outputs F\n" );
626 for ( i = p->nObjs - 1; i >= p->nVars; i-- )
627 {
628 int iVarStart = 1 + 3*(i - p->nVars);//
629 int Val1 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart);
630 int Val2 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+1);
631 int Val3 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+2);
632
633 fprintf( pFile, ".names" );
634 for ( k = 1; k >= 0; k-- )
635 {
636 iVar = Exa_ManFindFanin( p, i, k );
637 if ( iVar >= 0 && iVar < p->nVars )
638 fprintf( pFile, " %c", 'a'+iVar );
639 else
640 fprintf( pFile, " %02d", iVar );
641 }
642 if ( i == p->nObjs - 1 )
643 fprintf( pFile, " F\n" );
644 else
645 fprintf( pFile, " %02d\n", i );
646 if ( i == p->nObjs - 1 && fCompl )
647 fprintf( pFile, "00 1\n" );
648 if ( (i == p->nObjs - 1 && fCompl) ^ Val1 )
649 fprintf( pFile, "01 1\n" );
650 if ( (i == p->nObjs - 1 && fCompl) ^ Val2 )
651 fprintf( pFile, "10 1\n" );
652 if ( (i == p->nObjs - 1 && fCompl) ^ Val3 )
653 fprintf( pFile, "11 1\n" );
654 }
655 fprintf( pFile, ".end\n\n" );
656 fclose( pFile );
657 printf( "Solution was dumped into file \"%s\".\n", FileName );
658}
659void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl )
660{
661 int i, k, iVar;
662 printf( "Realization of given %d-input function using %d two-input gates:\n", p->nVars, p->nNodes );
663// for ( i = p->nVars + 2; i < p->nObjs; i++ )
664 for ( i = p->nObjs - 1; i >= p->nVars; i-- )
665 {
666 int iVarStart = 1 + 3*(i - p->nVars);//
667 int Val1 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart);
668 int Val2 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+1);
669 int Val3 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+2);
670 if ( i == p->nObjs - 1 && fCompl )
671 printf( "%02d = 4\'b%d%d%d1(", i, !Val3, !Val2, !Val1 );
672 else
673 printf( "%02d = 4\'b%d%d%d0(", i, Val3, Val2, Val1 );
674 for ( k = 1; k >= 0; k-- )
675 {
676 iVar = Exa_ManFindFanin( p, i, k );
677 if ( iVar >= 0 && iVar < p->nVars )
678 printf( " %c", 'a'+iVar );
679 else
680 printf( " %02d", iVar );
681 }
682 printf( " )\n" );
683 }
684}
685
686
698static inline int Exa_ManAddClause( Exa_Man_t * p, int * pLits, int nLits )
699{
700 int i;
701 if ( p->pFile )
702 {
703 p->nCnfClauses++;
704 for ( i = 0; i < nLits; i++ )
705 fprintf( p->pFile, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) );
706 fprintf( p->pFile, "0\n" );
707 }
708 return bmcg_sat_solver_addclause( p->pSat, pLits, nLits );
709}
710int Exa_ManAddCnfAdd( Exa_Man_t * p, int * pnAdded )
711{
712 int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m;
713 *pnAdded = 0;
714 for ( i = p->nVars; i < p->nObjs; i++ )
715 {
716 for ( k = 0; k < 2; k++ )
717 {
718 int nLits = 0;
719 for ( j = 0; j < p->nObjs; j++ )
720 if ( p->VarMarks[i][k][j] && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k][j]) )
721 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
722 assert( nLits > 0 );
723 // input uniqueness
724 for ( n = 0; n < nLits; n++ )
725 for ( m = n+1; m < nLits; m++ )
726 {
727 (*pnAdded)++;
728 pLits2[0] = Abc_LitNot(pLits[n]);
729 pLits2[1] = Abc_LitNot(pLits[m]);
730 if ( !Exa_ManAddClause( p, pLits2, 2 ) )
731 return 0;
732 }
733 if ( k == 1 )
734 break;
735 // symmetry breaking
736 for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k][j]) )
737 for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k+1][j]) )
738 {
739 (*pnAdded)++;
740 pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
741 pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 );
742 if ( !Exa_ManAddClause( p, pLits2, 2 ) )
743 return 0;
744 }
745 }
746 }
747 return 1;
748}
749int Exa_ManSolverSolve( Exa_Man_t * p )
750{
751 int nAdded = 1;
752 while ( nAdded )
753 {
754 int status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
755 if ( status != GLUCOSE_SAT )
756 return status;
757 status = Exa_ManAddCnfAdd( p, &nAdded );
758 //printf( "Added %d clauses.\n", nAdded );
759 if ( status != GLUCOSE_SAT )
760 return status;
761 }
762 return GLUCOSE_SAT;
763}
764int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
765{
766 extern Vec_Int_t * Gia_ManKSatGenLevels( char * pGuide, int nIns, int nNodes );
767 Vec_Int_t * vRes = p->pPars->pGuide ? Gia_ManKSatGenLevels( p->pPars->pGuide, p->nVars, p->nNodes ) : NULL;
768 int pLits[MAJ_NOBJS], pLits2[3], i, j, k, n, m, Start, Stop;
769 if ( vRes ) {
770 n = p->nVars;
771 Vec_IntForEachEntryDoubleStart( vRes, Start, Stop, i, 2*p->nVars ) {
772 for ( j = 0; j < Start; j++ )
773 if ( p->VarMarks[n][0][j] ) {
774 pLits[0] = Abc_Var2Lit( p->VarMarks[n][0][j], 1 );
775 Exa_ManAddClause( p, pLits, 1 );
776 }
777 for ( k = 0; k < 2; k++ )
778 for ( j = Stop; j < n; j++ )
779 if ( p->VarMarks[n][k][j] ) {
780 pLits[0] = Abc_Var2Lit( p->VarMarks[n][k][j], 1 );
781 Exa_ManAddClause( p, pLits, 1 );
782 }
783 n++;
784 }
785 assert( n == p->nVars + p->nNodes );
786 Vec_IntFreeP( &vRes );
787 }
788 // input constraints
789 for ( i = p->nVars; i < p->nObjs; i++ )
790 {
791 int iVarStart = 1 + 3*(i - p->nVars);//
792 for ( k = 0; k < 2; k++ )
793 {
794 int nLits = 0;
795 for ( j = 0; j < p->nObjs; j++ )
796 if ( p->VarMarks[i][k][j] )
797 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
798 assert( nLits > 0 );
799 if ( !Exa_ManAddClause( p, pLits, nLits ) )
800 return 0;
801 // input uniqueness
802 if ( !p->pPars->fDynConstr )
803 {
804 for ( n = 0; n < nLits; n++ )
805 for ( m = n+1; m < nLits; m++ )
806 {
807 pLits2[0] = Abc_LitNot(pLits[n]);
808 pLits2[1] = Abc_LitNot(pLits[m]);
809 if ( !Exa_ManAddClause( p, pLits2, 2 ) )
810 return 0;
811 }
812 }
813 if ( k == 1 )
814 break;
815 // symmetry breaking
816 if ( !p->pPars->fDynConstr )
817 {
818 for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
819 for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] )
820 {
821 pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
822 pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 );
823 if ( !Exa_ManAddClause( p, pLits2, 2 ) )
824 return 0;
825 }
826 }
827 }
828#ifdef USE_NODE_ORDER
829 // node ordering
830 for ( j = p->nVars; j < i; j++ )
831 for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
832 for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
833 {
834 pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 );
835 pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 );
836 if ( !Exa_ManAddClause( p, pLits2, 2 ) )
837 return 0;
838 }
839#endif
840 // unique functions
841 for ( j = p->nVars; j < i; j++ )
842 for ( k = 0; k < 2; k++ ) if ( p->VarMarks[i][k][j] )
843 {
844 pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
845 for ( n = 0; n < p->nObjs; n++ )
846 for ( m = 0; m < 2; m++ )
847 {
848 if ( p->VarMarks[i][!k][n] && p->VarMarks[j][m][n] )
849 {
850 pLits2[1] = Abc_Var2Lit( p->VarMarks[i][!k][n], 1 );
851 pLits2[2] = Abc_Var2Lit( p->VarMarks[j][m][n], 1 );
852 if ( !Exa_ManAddClause( p, pLits2, 3 ) )
853 return 0;
854 }
855 }
856 }
857 // two input functions
858 for ( k = 0; k < 3; k++ )
859 {
860 pLits[0] = Abc_Var2Lit( iVarStart, k==1 );
861 pLits[1] = Abc_Var2Lit( iVarStart+1, k==2 );
862 pLits[2] = Abc_Var2Lit( iVarStart+2, k!=0 );
863 if ( !Exa_ManAddClause( p, pLits, 3 ) )
864 return 0;
865 }
866 if ( fOnlyAnd )
867 {
868 pLits[0] = Abc_Var2Lit( iVarStart, 1 );
869 pLits[1] = Abc_Var2Lit( iVarStart+1, 1 );
870 pLits[2] = Abc_Var2Lit( iVarStart+2, 0 );
871 if ( !Exa_ManAddClause( p, pLits, 3 ) )
872 return 0;
873 }
874 }
875 // outputs should be used
876 for ( i = 0; i < p->nObjs - 1; i++ )
877 {
878 Vec_Int_t * vArray = Vec_WecEntry(p->vOutLits, i);
879 assert( Vec_IntSize(vArray) > 0 );
880 if ( !Exa_ManAddClause( p, Vec_IntArray(vArray), Vec_IntSize(vArray) ) )
881 return 0;
882 }
883 return 1;
884}
885int Exa_ManAddCnf( Exa_Man_t * p, int iMint )
886{
887 // save minterm values
888 int i, k, n, j, Value = Abc_TtGetBit(p->pTruth, iMint);
889 for ( i = 0; i < p->nVars; i++ )
890 p->VarVals[i] = (iMint >> i) & 1;
891 bmcg_sat_solver_set_nvars( p->pSat, p->iVar + 3*p->nNodes );
892 //printf( "Adding clauses for minterm %d with value %d.\n", iMint, Value );
893 for ( i = p->nVars; i < p->nObjs; i++ )
894 {
895 // fanin connectivity
896 int iVarStart = 1 + 3*(i - p->nVars);//
897 int iBaseSatVarI = p->iVar + 3*(i - p->nVars);
898 for ( k = 0; k < 2; k++ )
899 {
900 for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
901 {
902 int iBaseSatVarJ = p->iVar + 3*(j - p->nVars);
903 for ( n = 0; n < 2; n++ )
904 {
905 int pLits[3], nLits = 0;
906 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
907 pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + k, n );
908 if ( j >= p->nVars )
909 pLits[nLits++] = Abc_Var2Lit( iBaseSatVarJ + 2, !n );
910 else if ( p->VarVals[j] == n )
911 continue;
912 if ( !Exa_ManAddClause( p, pLits, nLits ) )
913 return 0;
914 }
915 }
916 }
917 // node functionality
918 for ( n = 0; n < 2; n++ )
919 {
920 if ( i == p->nObjs - 1 && n == Value )
921 continue;
922 for ( k = 0; k < 4; k++ )
923 {
924 int pLits[4], nLits = 0;
925 if ( k == 0 && n == 1 )
926 continue;
927 pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 0, (k&1) );
928 pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 1, (k>>1) );
929 if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 2, !n );
930 if ( k > 0 ) pLits[nLits++] = Abc_Var2Lit( iVarStart + k-1, n );
931 assert( nLits <= 4 );
932 if ( !Exa_ManAddClause( p, pLits, nLits ) )
933 return 0;
934 }
935 }
936 }
937 p->iVar += 3*p->nNodes;
938 return 1;
939}
940void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars )
941{
942 int i, status, iMint = 1;
943 abctime clkTotal = Abc_Clock();
944 Exa_Man_t * p; int fCompl = 0;
945 word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr );
946 assert( pPars->nVars <= 10 );
947 p = Exa_ManAlloc( pPars, pTruth );
948 if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); }
949 status = Exa_ManAddCnfStart( p, pPars->fOnlyAnd );
950 assert( status );
951 printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes );
952 for ( i = 0; iMint != -1; i++ )
953 {
954 abctime clk = Abc_Clock();
955 if ( !Exa_ManAddCnf( p, iMint ) )
956 break;
957 if ( pPars->fDynConstr )
958 status = Exa_ManSolverSolve( p );
959 else
960 status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
961 if ( pPars->fVerbose )
962 {
963 printf( "Iter %3d : ", i );
964 Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
965 printf( " Var =%5d ", p->iVar );
966 printf( "Cla =%6d ", bmcg_sat_solver_clausenum(p->pSat) );
967 printf( "Conf =%9d ", bmcg_sat_solver_conflictnum(p->pSat) );
968 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
969 }
970 if ( status == GLUCOSE_UNSAT )
971 {
972 printf( "The problem has no solution.\n" );
973 break;
974 }
975 if ( status == GLUCOSE_UNDEC )
976 {
977 printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
978 break;
979 }
980 iMint = Exa_ManEval( p );
981 }
982 if ( iMint == -1 )
983 {
984 Exa_ManPrintSolution( p, fCompl );
985 Exa_ManDumpBlif( p, fCompl );
986 }
987 Exa_ManFree( p );
988 Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
989}
990
991
992
993
994typedef struct Exa3_Man_t_ Exa3_Man_t;
995struct Exa3_Man_t_
996{
997 Bmc_EsPar_t * pPars; // parameters
998 int nVars; // inputs
999 int nNodes; // internal nodes
1000 int nLutSize; // lut size
1001 int LutMask; // lut mask
1002 int nObjs; // total objects (nVars inputs + nNodes internal nodes)
1003 int nWords; // the truth table size in 64-bit words
1004 int iVar; // the next available SAT variable
1005 word * pTruth; // truth table
1006 Vec_Wrd_t * vInfo; // nVars + nNodes + 1
1007 Vec_Bit_t * vUsed2; // bit masks
1008 Vec_Bit_t * vUsed3; // bit masks
1009 int VarMarks[MAJ_NOBJS][6][MAJ_NOBJS]; // variable marks
1010 int VarVals[MAJ_NOBJS]; // values of the first nVars variables
1011 Vec_Wec_t * vOutLits; // output vars
1012 Vec_Wec_t * vInVars; // input vars
1013 bmcg_sat_solver * pSat; // SAT solver
1014 int nUsed[2];
1015};
1016
1017static inline word * Exa3_ManTruth( Exa3_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); }
1018
1019static inline int Exa3_ManIsUsed2( Exa3_Man_t * p, int m, int n, int i, int j )
1020{
1021 int Pos = ((m * p->pPars->nNodes + n - p->pPars->nVars) * p->nObjs + i) * p->nObjs + j;
1022 p->nUsed[0]++;
1023 assert( i < n && j < n && i < j );
1024 if ( Vec_BitEntry(p->vUsed2, Pos) )
1025 return 1;
1026 p->nUsed[1]++;
1027 Vec_BitWriteEntry( p->vUsed2, Pos, 1 );
1028 return 0;
1029}
1030
1031static inline int Exa3_ManIsUsed3( Exa3_Man_t * p, int m, int n, int i, int j, int k )
1032{
1033 int Pos = (((m * p->pPars->nNodes + n - p->pPars->nVars) * p->nObjs + i) * p->nObjs + j) * p->nObjs + k;
1034 p->nUsed[0]++;
1035 assert( i < n && j < n && k < n && i < j && j < k );
1036 if ( Vec_BitEntry(p->vUsed3, Pos) )
1037 return 1;
1038 p->nUsed[1]++;
1039 Vec_BitWriteEntry( p->vUsed3, Pos, 1 );
1040 return 0;
1041}
1042
1043
1055Vec_Wec_t * Exa3_ChooseInputVars_int( int nVars, int nLuts, int nLutSize )
1056{
1057 Vec_Wec_t * p = Vec_WecStart( nLuts );
1058 Vec_Int_t * vLevel; int i;
1059 Vec_WecForEachLevel( p, vLevel, i ) {
1060 do {
1061 int iVar = (Abc_Random(0) ^ Abc_Random(0) ^ Abc_Random(0)) % nVars;
1062 Vec_IntPushUniqueOrder( vLevel, iVar );
1063 }
1064 while ( Vec_IntSize(vLevel) < nLutSize-(int)(i>0) );
1065 }
1066 return p;
1067}
1068Vec_Int_t * Exa3_CountInputVars( int nVars, Vec_Wec_t * p )
1069{
1070 Vec_Int_t * vLevel; int i, k, Obj;
1071 Vec_Int_t * vCounts = Vec_IntStart( nVars );
1072 Vec_WecForEachLevel( p, vLevel, i )
1073 Vec_IntForEachEntry( vLevel, Obj, k )
1074 Vec_IntAddToEntry( vCounts, Obj, 1 );
1075 return vCounts;
1076}
1077Vec_Wec_t * Exa3_ChooseInputVars( int nVars, int nLuts, int nLutSize )
1078{
1079 for ( int i = 0; i < 1000; i++ ) {
1080 Vec_Wec_t * p = Exa3_ChooseInputVars_int( nVars, nLuts, nLutSize );
1081 Vec_Int_t * q = Exa3_CountInputVars( nVars, p );
1082 int RetValue = Vec_IntFind( q, 0 );
1083 Vec_IntFree( q );
1084 if ( RetValue == -1 )
1085 return p;
1086 Vec_WecFree( p );
1087 }
1088 assert( 0 );
1089 return NULL;
1090}
1091
1103static Vec_Wrd_t * Exa3_ManTruthTables( Exa3_Man_t * p )
1104{
1105 Vec_Wrd_t * vInfo = p->vInfo = Vec_WrdStart( p->nWords * (p->nObjs+1) ); int i;
1106 for ( i = 0; i < p->nVars; i++ )
1107 Abc_TtIthVar( Exa3_ManTruth(p, i), i, p->nVars );
1108 //Dau_DsdPrintFromTruth( Exa3_ManTruth(p, p->nObjs), p->nVars );
1109 return vInfo;
1110}
1111static int Exa3_ManMarkup( Exa3_Man_t * p )
1112{
1113 int i, k, j;
1114 assert( p->nObjs <= MAJ_NOBJS );
1115 // assign functionality variables
1116 p->iVar = 1 + p->LutMask * p->nNodes;
1117 // assign connectivity variables
1118 for ( i = p->nVars; i < p->nObjs; i++ )
1119 {
1120 if ( p->pPars->fLutCascade )
1121 {
1122 if ( i > p->nVars )
1123 {
1124 Vec_WecPush( p->vOutLits, i-1, Abc_Var2Lit(p->iVar, 0) );
1125 p->VarMarks[i][0][i-1] = p->iVar++;
1126 }
1127 for ( k = (int)(i > p->nVars); k < p->nLutSize; k++ )
1128 {
1129 for ( j = 0; j < p->nVars - k + (int)(i > p->nVars); j++ )
1130 {
1131 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
1132 p->VarMarks[i][k][j] = p->iVar++;
1133 }
1134 }
1135 continue;
1136 }
1137 for ( k = 0; k < p->nLutSize; k++ )
1138 {
1139 if ( p->pPars->fFewerVars && i == p->nObjs - 1 && k == 0 )
1140 {
1141 j = p->nObjs - 2;
1142 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
1143 p->VarMarks[i][k][j] = p->iVar++;
1144 continue;
1145 }
1146 for ( j = p->pPars->fFewerVars ? p->nLutSize - 1 - k : 0; j < i - k; j++ )
1147 {
1148 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
1149 p->VarMarks[i][k][j] = p->iVar++;
1150 }
1151 }
1152 }
1153 printf( "The number of parameter variables = %d.\n", p->iVar );
1154 if ( p->pPars->fLutCascade && p->pPars->fLutInFixed ) {
1155 p->vInVars = Exa3_ChooseInputVars( p->nVars, p->nNodes, p->nLutSize );
1156 if ( 1 ) {
1157 Vec_Int_t * vLevel; int i, Var;
1158 printf( "Using fixed input assignment:\n" );
1159 Vec_WecForEachLevelReverse( p->vInVars, vLevel, i ) {
1160 printf( "%02d : ", p->nVars+i );
1161 Vec_IntForEachEntry( vLevel, Var, k )
1162 printf( "%c ", 'a'+Var );
1163 printf( "\n" );
1164 }
1165 }
1166 }
1167 return p->iVar;
1168 // printout
1169 for ( i = p->nObjs - 1; i >= p->nVars; i-- )
1170 {
1171 printf( " Node %2d\n", i );
1172 for ( j = 0; j < p->nObjs; j++ )
1173 {
1174 printf( "Fanin %2d : ", j );
1175 for ( k = 0; k < p->nLutSize; k++ )
1176 printf( "%3d ", p->VarMarks[i][k][j] );
1177 printf( "\n" );
1178 }
1179 }
1180 return p->iVar;
1181}
1182static Exa3_Man_t * Exa3_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
1183{
1184 Exa3_Man_t * p = ABC_CALLOC( Exa3_Man_t, 1 );
1185 p->pPars = pPars;
1186 p->nVars = pPars->nVars;
1187 p->nNodes = pPars->nNodes;
1188 p->nLutSize = pPars->nLutSize;
1189 p->LutMask = (1 << pPars->nLutSize) - 1;
1190 p->nObjs = pPars->nVars + pPars->nNodes;
1191 p->nWords = Abc_TtWordNum(pPars->nVars);
1192 p->pTruth = pTruth;
1193 p->vOutLits = Vec_WecStart( p->nObjs );
1194 p->iVar = Exa3_ManMarkup( p );
1195 p->vInfo = Exa3_ManTruthTables( p );
1196 if ( p->pPars->nLutSize == 2 )
1197 p->vUsed2 = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs );
1198 else if ( p->pPars->nLutSize == 3 )
1199 p->vUsed3 = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs * p->nObjs );
1200 p->pSat = bmcg_sat_solver_start();
1201 bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
1202 if ( pPars->RuntimeLim )
1203 bmcg_sat_solver_set_runtime_limit( p->pSat, Abc_Clock() + pPars->RuntimeLim * CLOCKS_PER_SEC );
1204 return p;
1205}
1206static void Exa3_ManFree( Exa3_Man_t * p )
1207{
1208 bmcg_sat_solver_stop( p->pSat );
1209 Vec_WrdFree( p->vInfo );
1210 Vec_BitFreeP( &p->vUsed2 );
1211 Vec_BitFreeP( &p->vUsed3 );
1212 Vec_WecFree( p->vOutLits );
1213 Vec_WecFreeP( &p->vInVars );
1214 ABC_FREE( p );
1215}
1216
1217
1229static inline int Exa3_ManFindFanin( Exa3_Man_t * p, int i, int k )
1230{
1231 int j, Count = 0, iVar = -1;
1232 for ( j = 0; j < p->nObjs; j++ )
1233 if ( p->VarMarks[i][k][j] && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k][j]) )
1234 {
1235 iVar = j;
1236 Count++;
1237 }
1238 assert( Count == 1 );
1239 return iVar;
1240}
1241static inline int Exa3_ManEval( Exa3_Man_t * p )
1242{
1243 static int Flag = 0;
1244 int i, k, j, iMint; word * pFanins[6];
1245 for ( i = p->nVars; i < p->nObjs; i++ )
1246 {
1247 int iVarStart = 1 + p->LutMask*(i - p->nVars);
1248 for ( k = 0; k < p->nLutSize; k++ )
1249 pFanins[k] = Exa3_ManTruth( p, Exa3_ManFindFanin(p, i, k) );
1250 Abc_TtConst0( Exa3_ManTruth(p, i), p->nWords );
1251 for ( k = 1; k <= p->LutMask; k++ )
1252 {
1253 if ( !bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+k-1) )
1254 continue;
1255// Abc_TtAndCompl( Exa3_ManTruth(p, p->nObjs), pFanins[0], !(k&1), pFanins[1], !(k>>1), p->nWords );
1256 Abc_TtConst1( Exa3_ManTruth(p, p->nObjs), p->nWords );
1257 for ( j = 0; j < p->nLutSize; j++ )
1258 Abc_TtAndCompl( Exa3_ManTruth(p, p->nObjs), Exa3_ManTruth(p, p->nObjs), 0, pFanins[j], !((k >> j) & 1), p->nWords );
1259 Abc_TtOr( Exa3_ManTruth(p, i), Exa3_ManTruth(p, i), Exa3_ManTruth(p, p->nObjs), p->nWords );
1260 }
1261 }
1262 if ( Flag && p->nVars >= 6 )
1263 iMint = Abc_TtFindLastDiffBit( Exa3_ManTruth(p, p->nObjs-1), p->pTruth, p->nVars );
1264 else
1265 iMint = Abc_TtFindFirstDiffBit( Exa3_ManTruth(p, p->nObjs-1), p->pTruth, p->nVars );
1266 //Flag ^= 1;
1267 assert( iMint < (1 << p->nVars) );
1268 return iMint;
1269}
1270
1282static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl )
1283{
1284 int i, k, iVar;
1285 printf( "Realization of given %d-input function using %d %d-input LUTs:\n", p->nVars, p->nNodes, p->nLutSize );
1286 for ( i = p->nObjs - 1; i >= p->nVars; i-- )
1287 {
1288 int Val, iVarStart = 1 + p->LutMask*(i - p->nVars);
1289 printf( "%02d = %d\'b", i, 1 << p->nLutSize );
1290 for ( k = p->LutMask - 1; k >= 0; k-- )
1291 {
1292 Val = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+k);
1293 if ( i == p->nObjs - 1 && fCompl )
1294 printf( "%d", !Val );
1295 else
1296 printf( "%d", Val );
1297 }
1298 if ( i == p->nObjs - 1 && fCompl )
1299 printf( "1(" );
1300 else
1301 printf( "0(" );
1302
1303 for ( k = p->nLutSize - 1; k >= 0; k-- )
1304 {
1305 iVar = Exa3_ManFindFanin( p, i, k );
1306 if ( iVar >= 0 && iVar < p->nVars )
1307 printf( " %c", 'a'+iVar );
1308 else
1309 printf( " %02d", iVar );
1310 }
1311 printf( " )\n" );
1312 }
1313}
1314
1326static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl )
1327{
1328 int i, k, b, iVar;
1329 char pFileName[1000];
1330 sprintf( pFileName, "%s.blif", p->pPars->pTtStr );
1331 FILE * pFile = fopen( pFileName, "wb" );
1332 if ( pFile == NULL ) return;
1333 fprintf( pFile, "# Realization of given %d-input function using %d %d-input LUTs synthesized by ABC on %s\n", p->nVars, p->nNodes, p->nLutSize, Extra_TimeStamp() );
1334 fprintf( pFile, ".model %s\n", p->pPars->pTtStr );
1335 fprintf( pFile, ".inputs" );
1336 for ( k = 0; k < p->nVars; k++ )
1337 fprintf( pFile, " %c", 'a'+k );
1338 fprintf( pFile, "\n.outputs F\n" );
1339 for ( i = p->nObjs - 1; i >= p->nVars; i-- )
1340 {
1341 fprintf( pFile, ".names" );
1342 for ( k = 0; k < p->nLutSize; k++ )
1343 {
1344 iVar = Exa3_ManFindFanin( p, i, k );
1345 if ( iVar >= 0 && iVar < p->nVars )
1346 fprintf( pFile, " %c", 'a'+iVar );
1347 else
1348 fprintf( pFile, " %02d", iVar );
1349 }
1350 if ( i == p->nObjs - 1 )
1351 fprintf( pFile, " F\n" );
1352 else
1353 fprintf( pFile, " %02d\n", i );
1354 int iVarStart = 1 + p->LutMask*(i - p->nVars);
1355 for ( k = 0; k < p->LutMask; k++ )
1356 {
1357 int Val = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+k);
1358 if ( Val == 0 )
1359 continue;
1360 for ( b = 0; b < p->nLutSize; b++ )
1361 fprintf( pFile, "%d", ((k+1) >> b) & 1 );
1362 fprintf( pFile, " %d\n", i != p->nObjs - 1 || !fCompl );
1363 }
1364 }
1365 fprintf( pFile, ".end\n\n" );
1366 fclose( pFile );
1367 printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName );
1368}
1369
1370
1382static int Exa3_ManAddCnfStart( Exa3_Man_t * p, int fOnlyAnd )
1383{
1384 int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m;
1385 // input constraints
1386 for ( i = p->nVars; i < p->nObjs; i++ )
1387 {
1388 int iVarStart = 1 + p->LutMask*(i - p->nVars);
1389 for ( k = 0; k < p->nLutSize; k++ )
1390 {
1391 int nLits = 0;
1392 for ( j = 0; j < p->nObjs; j++ )
1393 if ( p->VarMarks[i][k][j] )
1394 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
1395 assert( nLits > 0 );
1396 // input uniqueness
1397 if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
1398 return 0;
1399 for ( n = 0; n < nLits; n++ )
1400 for ( m = n+1; m < nLits; m++ )
1401 {
1402 pLits2[0] = Abc_LitNot(pLits[n]);
1403 pLits2[1] = Abc_LitNot(pLits[m]);
1404 if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
1405 return 0;
1406 }
1407 if ( k == p->nLutSize - 1 )
1408 break;
1409 // symmetry breaking
1410 for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
1411 for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] )
1412 {
1413 pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
1414 pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 );
1415 if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
1416 return 0;
1417 }
1418 }
1419//#ifdef USE_NODE_ORDER
1420 // node ordering
1421 if ( p->pPars->fOrderNodes )
1422 {
1423 for ( j = p->nVars; j < i; j++ )
1424 for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
1425 for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
1426 {
1427 pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 );
1428 pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 );
1429 if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
1430 return 0;
1431 }
1432 }
1433//#endif
1434 if ( p->nLutSize != 2 )
1435 continue;
1436 // two-input functions
1437 for ( k = 0; k < 3; k++ )
1438 {
1439 pLits[0] = Abc_Var2Lit( iVarStart, k==1 );
1440 pLits[1] = Abc_Var2Lit( iVarStart+1, k==2 );
1441 pLits[2] = Abc_Var2Lit( iVarStart+2, k!=0 );
1442 if ( !bmcg_sat_solver_addclause( p->pSat, pLits, 3 ) )
1443 return 0;
1444 }
1445 if ( fOnlyAnd )
1446 {
1447 pLits[0] = Abc_Var2Lit( iVarStart, 1 );
1448 pLits[1] = Abc_Var2Lit( iVarStart+1, 1 );
1449 pLits[2] = Abc_Var2Lit( iVarStart+2, 0 );
1450 if ( !bmcg_sat_solver_addclause( p->pSat, pLits, 3 ) )
1451 return 0;
1452 }
1453 }
1454 // outputs should be used
1455 for ( i = 0; i < p->nObjs - 1; i++ )
1456 {
1457 Vec_Int_t * vArray = Vec_WecEntry(p->vOutLits, i);
1458 assert( Vec_IntSize(vArray) > 0 );
1459 if ( !bmcg_sat_solver_addclause( p->pSat, Vec_IntArray(vArray), Vec_IntSize(vArray) ) )
1460 return 0;
1461 }
1462 if ( p->vInVars ) {
1463 Vec_Int_t * vLevel; int Var;
1464 Vec_WecForEachLevel( p->vInVars, vLevel, i )
1465 {
1466 assert( Vec_IntSize(vLevel) > 0 );
1467 Vec_IntForEachEntry( vLevel, Var, k ) {
1468 pLits[0] = Abc_Var2Lit( p->VarMarks[p->nVars+i][p->nLutSize-1-k][Var], 0 ); assert(pLits[0]);
1469 if ( !bmcg_sat_solver_addclause( p->pSat, pLits, 1 ) )
1470 return 0;
1471 }
1472 }
1473 }
1474 return 1;
1475}
1476static int Exa3_ManAddCnf( Exa3_Man_t * p, int iMint )
1477{
1478 // save minterm values
1479 int i, k, n, j, Value = Abc_TtGetBit(p->pTruth, iMint);
1480 for ( i = 0; i < p->nVars; i++ )
1481 p->VarVals[i] = (iMint >> i) & 1;
1482// sat_solver_setnvars( p->pSat, p->iVar + (p->nLutSize+1)*p->nNodes );
1483 bmcg_sat_solver_set_nvars( p->pSat, p->iVar + (p->nLutSize+1)*p->nNodes );
1484 //printf( "Adding clauses for minterm %d with value %d.\n", iMint, Value );
1485 for ( i = p->nVars; i < p->nObjs; i++ )
1486 {
1487 // fanin connectivity
1488 int iVarStart = 1 + p->LutMask*(i - p->nVars);
1489 int iBaseSatVarI = p->iVar + (p->nLutSize+1)*(i - p->nVars);
1490 for ( k = 0; k < p->nLutSize; k++ )
1491 {
1492 for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
1493 {
1494 int iBaseSatVarJ = p->iVar + (p->nLutSize+1)*(j - p->nVars);
1495 for ( n = 0; n < 2; n++ )
1496 {
1497 int pLits[3], nLits = 0;
1498 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
1499 pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + k, n );
1500 if ( j >= p->nVars )
1501 pLits[nLits++] = Abc_Var2Lit( iBaseSatVarJ + p->nLutSize, !n );
1502 else if ( p->VarVals[j] == n )
1503 continue;
1504 if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
1505 return 0;
1506 }
1507 }
1508 }
1509 // node functionality
1510 for ( n = 0; n < 2; n++ )
1511 {
1512 if ( i == p->nObjs - 1 && n == Value )
1513 continue;
1514 for ( k = 0; k <= p->LutMask; k++ )
1515 {
1516 int pLits[16], nLits = 0;
1517 if ( k == 0 && n == 1 )
1518 continue;
1519 //pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 0, (k&1) );
1520 //pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 1, (k>>1) );
1521 //if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 2, !n );
1522 for ( j = 0; j < p->nLutSize; j++ )
1523 pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + j, (k >> j) & 1 );
1524 if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + j, !n );
1525 if ( k > 0 ) pLits[nLits++] = Abc_Var2Lit( iVarStart + k-1, n );
1526 assert( nLits <= p->nLutSize+2 );
1527 if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
1528 return 0;
1529 }
1530 }
1531 }
1532 p->iVar += (p->nLutSize+1)*p->nNodes;
1533 return 1;
1534}
1535
1536static int Exa3_ManAddCnf2( Exa3_Man_t * p, int iMint )
1537{
1538 int iBaseSatVar = p->iVar + p->nNodes*iMint;
1539 // save minterm values
1540 int i, k, n, j, Value = Abc_TtGetBit(p->pTruth, iMint);
1541 for ( i = 0; i < p->nVars; i++ )
1542 p->VarVals[i] = (iMint >> i) & 1;
1543 //printf( "Adding clauses for minterm %d with value %d.\n", iMint, Value );
1544 for ( i = p->nVars; i < p->nObjs; i++ )
1545 {
1546// int iBaseSatVarI = p->iVar + (p->nLutSize+1)*(i - p->nVars);
1547 int iVarStart = 1 + p->LutMask*(i - p->nVars);
1548 // collect fanin variables
1549 int pFanins[16];
1550 for ( j = 0; j < p->nLutSize; j++ )
1551 pFanins[j] = Exa3_ManFindFanin(p, i, j);
1552 // check cache
1553 if ( p->pPars->nLutSize == 2 && Exa3_ManIsUsed2(p, iMint, i, pFanins[1], pFanins[0]) )
1554 continue;
1555 if ( p->pPars->nLutSize == 3 && Exa3_ManIsUsed3(p, iMint, i, pFanins[2], pFanins[1], pFanins[0]) )
1556 continue;
1557 // node functionality
1558 for ( n = 0; n < 2; n++ )
1559 {
1560 if ( i == p->nObjs - 1 && n == Value )
1561 continue;
1562 for ( k = 0; k <= p->LutMask; k++ )
1563 {
1564 int pLits[16], nLits = 0;
1565 if ( k == 0 && n == 1 )
1566 continue;
1567 for ( j = 0; j < p->nLutSize; j++ )
1568 {
1569// pLits[nLits++] = Abc_Var2Lit( iBaseSatVar + j, (k >> j) & 1 );
1570 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][j][pFanins[j]], 1 );
1571 if ( pFanins[j] >= p->nVars )
1572 pLits[nLits++] = Abc_Var2Lit( iBaseSatVar + pFanins[j] - p->nVars, (k >> j) & 1 );
1573 else if ( p->VarVals[pFanins[j]] != ((k >> j) & 1) )
1574 break;
1575 }
1576 if ( j < p->nLutSize )
1577 continue;
1578// if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVar + j, !n );
1579 if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVar + i - p->nVars, !n );
1580 if ( k > 0 ) pLits[nLits++] = Abc_Var2Lit( iVarStart + k-1, n );
1581 assert( nLits <= 2*p->nLutSize+2 );
1582 if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
1583 return 0;
1584 }
1585 }
1586 }
1587 return 1;
1588}
1589void Exa3_ManPrint( Exa3_Man_t * p, int i, int iMint, abctime clk )
1590{
1591 printf( "Iter%6d : ", i );
1592 Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
1593 printf( " Var =%5d ", bmcg_sat_solver_varnum(p->pSat) );
1594 printf( "Cla =%6d ", bmcg_sat_solver_clausenum(p->pSat) );
1595 printf( "Conf =%9d ", bmcg_sat_solver_conflictnum(p->pSat) );
1596 Abc_PrintTime( 1, "Time", clk );
1597}
1598int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
1599{
1600 int i, status, Res = 0, iMint = 1;
1601 abctime clkTotal = Abc_Clock();
1602 Exa3_Man_t * p; int fCompl = 0;
1603 word pTruth[16];
1604 if ( pPars->pSymStr ) {
1605 word * pFun = Abc_TtSymFunGenerate( pPars->pSymStr, pPars->nVars );
1606 pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 );
1607 Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars );
1608 printf( "Generated symmetric function: %s\n", pPars->pTtStr );
1609 ABC_FREE( pFun );
1610 }
1611 if ( pPars->pTtStr )
1612 Abc_TtReadHex( pTruth, pPars->pTtStr );
1613 else assert( 0 );
1614 assert( pPars->nVars <= 10 );
1615 assert( pPars->nLutSize <= 6 );
1616 p = Exa3_ManAlloc( pPars, pTruth );
1617 if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); }
1618 status = Exa3_ManAddCnfStart( p, pPars->fOnlyAnd );
1619 assert( status );
1620 printf( "Running exact synthesis for %d-input function with %d %d-input LUTs...\n", p->nVars, p->nNodes, p->nLutSize );
1621 if ( pPars->fUseIncr )
1622 {
1623 bmcg_sat_solver_set_nvars( p->pSat, p->iVar + p->nNodes*(1 << p->nVars) );
1624 status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
1625 assert( status == GLUCOSE_SAT );
1626 }
1627 for ( i = 0; iMint != -1; i++ )
1628 {
1629 if ( pPars->fUseIncr ? !Exa3_ManAddCnf2( p, iMint ) : !Exa3_ManAddCnf( p, iMint ) )
1630 break;
1631 status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
1632 if ( pPars->fVerbose && (!pPars->fUseIncr || i % 100 == 0) )
1633 Exa3_ManPrint( p, i, iMint, Abc_Clock() - clkTotal );
1634 if ( status == GLUCOSE_UNSAT || status == GLUCOSE_UNDEC )
1635 break;
1636 iMint = Exa3_ManEval( p );
1637 }
1638 if ( pPars->fVerbose && status != GLUCOSE_UNDEC )
1639 Exa3_ManPrint( p, i, iMint, Abc_Clock() - clkTotal );
1640 if ( iMint == -1 )
1641 Exa3_ManPrintSolution( p, fCompl ), Res = 1;
1642 else if ( status == GLUCOSE_UNDEC )
1643 printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
1644 else
1645 printf( "The problem has no solution.\n" );
1646 printf( "Added = %d. Tried = %d. ", p->nUsed[1], p->nUsed[0] );
1647 Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
1648 if ( iMint == -1 )
1649 Exa3_ManDumpBlif( p, fCompl );
1650 if ( pPars->pSymStr )
1651 ABC_FREE( pPars->pTtStr );
1652 Exa3_ManFree( p );
1653 return Res;
1654}
1655void Exa3_ManExactSynthesisRand( Bmc_EsPar_t * pPars )
1656{
1657 int i, k, nDecs = 0, nWords = Abc_TtWordNum(pPars->nVars);
1658 word * pFun = ABC_ALLOC( word, nWords );
1659 unsigned Rand0 = Abc_Random(1);
1660 for ( i = 0; i < pPars->Seed; i++ )
1661 Rand0 = Abc_Random(0);
1662 for ( i = 0; i < pPars->nRandFuncs; i++ ) {
1663 if ( pPars->nMintNum == 0 )
1664 for ( k = 0; k < nWords; k++ )
1665 pFun[k] = Rand0 ^ Abc_RandomW(0);
1666 else {
1667 Abc_TtClear( pFun, nWords );
1668 for ( k = 0; k < pPars->nMintNum; k++ ) {
1669 int iMint = 0;
1670 do iMint = (Rand0 ^ Abc_Random(0)) % (1 << pPars->nVars);
1671 while ( Abc_TtGetBit(pFun, iMint) );
1672 Abc_TtSetBit( pFun, iMint );
1673 }
1674 }
1675 pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 );
1676 Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars );
1677 printf( "\nFunction %4d : ", i );
1678 if ( pPars->nMintNum )
1679 printf( "Random function has %d positive minterms.", pPars->nMintNum );
1680 printf( "\n" );
1681 if ( pPars->fVerbose )
1682 printf( "Truth table : %s\n", pPars->pTtStr );
1683 nDecs += Exa3_ManExactSynthesis( pPars );
1684 ABC_FREE( pPars->pTtStr );
1685 }
1686 printf( "\nDecomposable are %d (out of %d) functions (%.2f %%).\n\n", nDecs, pPars->nRandFuncs, 100.0*nDecs/pPars->nRandFuncs );
1687 ABC_FREE( pFun );
1688}
1689
1690
1702void Exa_ManIsNormalized( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut )
1703{
1704 int i, Count = 0; word Temp;
1705 Vec_WrdForEachEntry( vSimsIn, Temp, i )
1706 if ( Temp & 1 )
1707 Count++;
1708 if ( Count )
1709 printf( "The data for %d divisors are not normalized.\n", Count );
1710 if ( !(Vec_WrdEntry(vSimsOut, 0) & 1) )
1711 printf( "The output data is not normalized.\n" );
1712// else if ( Count == 0 )
1713// printf( "The data is fully normalized.\n" );
1714}
1715static inline void Exa_ManPrintFanin( int nIns, int nDivs, int iNode, int fComp )
1716{
1717 if ( iNode == 0 )
1718 printf( " %s", fComp ? "const1" : "const0" );
1719 else if ( iNode > 0 && iNode <= nIns )
1720 printf( " %s%c", fComp ? "~" : "", 'a'+iNode-1 );
1721 else if ( iNode > nIns && iNode < nDivs )
1722 printf( " %s%c", fComp ? "~" : "", 'A'+iNode-nIns-1 );
1723 else
1724 printf( " %s%d", fComp ? "~" : "", iNode );
1725}
1726void Exa_ManMiniPrint( Mini_Aig_t * p, int nIns )
1727{
1728 int i, nDivs = 1 + Mini_AigPiNum(p), nNodes = Mini_AigAndNum(p);
1729 printf( "This %d-var function (%d divisors) has %d gates (%d xor) and %d levels:\n",
1730 nIns, nDivs, nNodes, Mini_AigXorNum(p), Mini_AigLevelNum(p) );
1731 for ( i = nDivs + nNodes; i < Mini_AigNodeNum(p); i++ )
1732 {
1733 int Lit0 = Mini_AigNodeFanin0( p, i );
1734 printf( "%2d = ", i );
1735 Exa_ManPrintFanin( nIns, nDivs, Abc_Lit2Var(Lit0), Abc_LitIsCompl(Lit0) );
1736 printf( "\n" );
1737 }
1738 for ( i = nDivs + nNodes - 1; i >= nDivs; i-- )
1739 {
1740 int Lit0 = Mini_AigNodeFanin0( p, i );
1741 int Lit1 = Mini_AigNodeFanin1( p, i );
1742 printf( "%2d = ", i );
1743 if ( Lit0 < Lit1 )
1744 {
1745 Exa_ManPrintFanin( nIns, nDivs, Abc_Lit2Var(Lit0), Abc_LitIsCompl(Lit0) );
1746 printf( " &" );
1747 Exa_ManPrintFanin( nIns, nDivs, Abc_Lit2Var(Lit1), Abc_LitIsCompl(Lit1) );
1748 }
1749 else
1750 {
1751 Exa_ManPrintFanin( nIns, nDivs, Abc_Lit2Var(Lit1), Abc_LitIsCompl(Lit1) );
1752 printf( " ^" );
1753 Exa_ManPrintFanin( nIns, nDivs, Abc_Lit2Var(Lit0), Abc_LitIsCompl(Lit0) );
1754 }
1755 printf( "\n" );
1756 }
1757}
1758void Exa_ManMiniVerify( Mini_Aig_t * p, Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut )
1759{
1760 extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut );
1761 int i, nDivs = 1 + Mini_AigPiNum(p), nNodes = Mini_AigAndNum(p);
1762 int k, nOuts = Mini_AigPoNum(p), nErrors = 0; word Outs[6] = {0};
1763 Vec_Wrd_t * vSimsIn2 = Vec_WrdStart( 64 );
1764 assert( nOuts <= 6 );
1765 assert( Vec_WrdSize(vSimsIn) <= 64 );
1766 assert( Vec_WrdSize(vSimsIn) == Vec_WrdSize(vSimsOut) );
1767 Vec_WrdFillExtra( vSimsIn, 64, 0 );
1768 Extra_BitMatrixTransposeP( vSimsIn, 1, vSimsIn2, 1 );
1769 assert( Mini_AigNodeNum(p) <= 64 );
1770 for ( i = nDivs; i < nDivs + nNodes; i++ )
1771 {
1772 int Lit0 = Mini_AigNodeFanin0( p, i );
1773 int Lit1 = Mini_AigNodeFanin1( p, i );
1774 word Sim0 = Vec_WrdEntry( vSimsIn2, Abc_Lit2Var(Lit0) );
1775 word Sim1 = Vec_WrdEntry( vSimsIn2, Abc_Lit2Var(Lit1) );
1776 Sim0 = Abc_LitIsCompl(Lit0) ? ~Sim0 : Sim0;
1777 Sim1 = Abc_LitIsCompl(Lit1) ? ~Sim1 : Sim1;
1778 Vec_WrdWriteEntry( vSimsIn2, i, Lit0 < Lit1 ? Sim0 & Sim1 : Sim0 ^ Sim1 );
1779 }
1780 for ( i = nDivs + nNodes; i < Mini_AigNodeNum(p); i++ )
1781 {
1782 int Lit0 = Mini_AigNodeFanin0( p, i );
1783 word Sim0 = Vec_WrdEntry( vSimsIn2, Abc_Lit2Var(Lit0) );
1784 Outs[i - (nDivs + nNodes)] = Abc_LitIsCompl(Lit0) ? ~Sim0 : Sim0;
1785 }
1786 Vec_WrdFree( vSimsIn2 );
1787 for ( i = 0; i < Vec_WrdSize(vSimsOut); i++ )
1788 {
1789 int iOutMint = 0;
1790 for ( k = 0; k < nOuts; k++ )
1791 if ( (Outs[k] >> i) & 1 )
1792 iOutMint |= 1 << k;
1793 nErrors += !Abc_TtGetBit(Vec_WrdEntryP(vSimsOut, i), iOutMint);
1794 }
1795 if ( nErrors == 0 )
1796 printf( "Verification successful. " );
1797 else
1798 printf( "Verification failed for %d (out of %d) minterms.\n", nErrors, Vec_WrdSize(vSimsOut) );
1799}
1800
1812Vec_Int_t * Exa4_ManParse( char * pFileName )
1813{
1814 Vec_Int_t * vRes = NULL;
1815 char * pToken, pBuffer[1000];
1816 FILE * pFile = fopen( pFileName, "rb" );
1817 if ( pFile == NULL )
1818 {
1819 Abc_Print( -1, "Cannot open file \"%s\".\n", pFileName );
1820 return NULL;
1821 }
1822 while ( fgets( pBuffer, 1000, pFile ) != NULL )
1823 {
1824 if ( pBuffer[0] == 's' )
1825 {
1826 if ( strncmp(pBuffer+2, "SAT", 3) )
1827 break;
1828 assert( vRes == NULL );
1829 vRes = Vec_IntAlloc( 100 );
1830 }
1831 else if ( pBuffer[0] == 'v' )
1832 {
1833 pToken = strtok( pBuffer+1, " \n\r\t" );
1834 while ( pToken )
1835 {
1836 int Token = atoi(pToken);
1837 if ( Token == 0 )
1838 break;
1839 Vec_IntSetEntryFull( vRes, Abc_AbsInt(Token), Token > 0 );
1840 pToken = strtok( NULL, " \n\r\t" );
1841 }
1842 }
1843 else if ( pBuffer[0] != 'c' )
1844 assert( 0 );
1845 }
1846 fclose( pFile );
1847 unlink( pFileName );
1848 return vRes;
1849}
1850Vec_Int_t * Exa4_ManSolve( char * pFileNameIn, char * pFileNameOut, int TimeOut, int fVerbose )
1851{
1852 int fVerboseSolver = 0;
1853 abctime clkTotal = Abc_Clock();
1854 Vec_Int_t * vRes = NULL;
1855#ifdef _WIN32
1856 char * pKissat = "kissat.exe";
1857#else
1858 char * pKissat = "kissat";
1859#endif
1860 char Command[1000], * pCommand = (char *)&Command;
1861 if ( TimeOut )
1862 sprintf( pCommand, "%s --time=%d %s %s > %s", pKissat, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
1863 else
1864 sprintf( pCommand, "%s %s %s > %s", pKissat, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
1865#ifdef __wasm
1866 if ( 1 )
1867#else
1868 if ( system( pCommand ) == -1 )
1869#endif
1870 {
1871 fprintf( stdout, "Command \"%s\" did not succeed.\n", pCommand );
1872 return 0;
1873 }
1874 vRes = Exa4_ManParse( pFileNameOut );
1875 if ( fVerbose )
1876 {
1877 if ( vRes )
1878 printf( "The problem has a solution. " );
1879 else if ( vRes == NULL && TimeOut == 0 )
1880 printf( "The problem has no solution. " );
1881 else if ( vRes == NULL )
1882 printf( "The problem has no solution or timed out after %d sec. ", TimeOut );
1883 Abc_PrintTime( 1, "SAT solver time", Abc_Clock() - clkTotal );
1884 }
1885 return vRes;
1886}
1887
1888
1889typedef struct Exa4_Man_t_ Exa4_Man_t;
1890struct Exa4_Man_t_
1891{
1892 Vec_Wrd_t * vSimsIn; // input signatures (nWords = 1, nIns <= 64)
1893 Vec_Wrd_t * vSimsOut; // output signatures (nWords = 1, nOuts <= 6)
1894 int fVerbose;
1895 int nIns;
1896 int nDivs; // divisors (const + inputs + tfi + sidedivs)
1897 int nNodes;
1898 int nOuts;
1899 int nObjs;
1900 int VarMarks[MAJ_NOBJS][2][MAJ_NOBJS];
1901 int nCnfVars;
1902 int nCnfClauses;
1903 FILE * pFile;
1904};
1905
1917int Exa4_ManMarkup( Exa4_Man_t * p )
1918{
1919 int i, k, j, nVars[3] = {1 + 5*p->nNodes, 0, 3*p->nNodes*Vec_WrdSize(p->vSimsIn)};
1920 assert( p->nObjs <= MAJ_NOBJS );
1921 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
1922 for ( k = 0; k < 2; k++ )
1923 for ( j = 1+!k; j < i-k; j++ )
1924 p->VarMarks[i][k][j] = nVars[0] + nVars[1]++;
1925 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
1926 for ( j = p->nOuts == 1 ? p->nDivs + p->nNodes - 1 : 0; j < p->nDivs + p->nNodes; j++ )
1927 p->VarMarks[i][0][j] = nVars[0] + nVars[1]++;
1928 if ( p->fVerbose )
1929 printf( "Variables: Function = %d. Structure = %d. Internal = %d. Total = %d.\n",
1930 nVars[0], nVars[1], nVars[2], nVars[0] + nVars[1] + nVars[2] );
1931 if ( 0 )
1932 {
1933 for ( j = 0; j < 2; j++ )
1934 {
1935 printf( " : " );
1936 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
1937 {
1938 for ( k = 0; k < 2; k++ )
1939 printf( "%3d ", j ? k : i );
1940 printf( " " );
1941 }
1942 printf( " " );
1943 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
1944 {
1945 printf( "%3d ", j ? 0 : i );
1946 printf( " " );
1947 }
1948 printf( "\n" );
1949 }
1950 for ( j = 0; j < 5 + p->nNodes*9 + p->nOuts*5; j++ )
1951 printf( "-" );
1952 printf( "\n" );
1953 for ( j = p->nObjs - 2; j >= 0; j-- )
1954 {
1955 if ( j > 0 && j <= p->nIns )
1956 printf( " %c : ", 'a'+j-1 );
1957 else
1958 printf( "%2d : ", j );
1959 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
1960 {
1961 for ( k = 0; k < 2; k++ )
1962 printf( "%3d ", p->VarMarks[i][k][j] );
1963 printf( " " );
1964 }
1965 printf( " " );
1966 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
1967 {
1968 printf( "%3d ", p->VarMarks[i][0][j] );
1969 printf( " " );
1970 }
1971 printf( "\n" );
1972 }
1973 }
1974 return nVars[0] + nVars[1] + nVars[2];
1975}
1976Exa4_Man_t * Exa4_ManAlloc( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int fVerbose )
1977{
1978 Exa4_Man_t * p = ABC_CALLOC( Exa4_Man_t, 1 );
1979 assert( Vec_WrdSize(vSimsIn) == Vec_WrdSize(vSimsOut) );
1980 p->vSimsIn = vSimsIn;
1981 p->vSimsOut = vSimsOut;
1982 p->fVerbose = fVerbose;
1983 p->nIns = nIns;
1984 p->nDivs = nDivs;
1985 p->nNodes = nNodes;
1986 p->nOuts = nOuts;
1987 p->nObjs = p->nDivs + p->nNodes + p->nOuts;
1988 p->nCnfVars = Exa4_ManMarkup( p );
1989 return p;
1990}
1991void Exa4_ManFree( Exa4_Man_t * p )
1992{
1993 ABC_FREE( p );
1994}
1995
1996
2008static inline int Exa4_ManAddClause( Exa4_Man_t * p, int * pLits, int nLits )
2009{
2010 int i, k = 0;
2011 for ( i = 0; i < nLits; i++ )
2012 if ( pLits[i] == 1 )
2013 return 0;
2014 else if ( pLits[i] == 0 )
2015 continue;
2016 else if ( pLits[i] <= 2*p->nCnfVars )
2017 pLits[k++] = pLits[i];
2018 else assert( 0 );
2019 nLits = k;
2020 assert( nLits > 0 );
2021 if ( p->pFile )
2022 {
2023 p->nCnfClauses++;
2024 for ( i = 0; i < nLits; i++ )
2025 fprintf( p->pFile, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) );
2026 fprintf( p->pFile, "0\n" );
2027 }
2028 if ( 0 )
2029 {
2030 for ( i = 0; i < nLits; i++ )
2031 fprintf( stdout, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) );
2032 fprintf( stdout, "\n" );
2033 }
2034 return 1;
2035}
2036static inline int Exa4_ManAddClause4( Exa4_Man_t * p, int Lit0, int Lit1, int Lit2, int Lit3 )
2037{
2038 int pLits[4] = { Lit0, Lit1, Lit2, Lit3 };
2039 return Exa4_ManAddClause( p, pLits, 4 );
2040}
2041int Exa4_ManGenStart( Exa4_Man_t * p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard, char * pGuide )
2042{
2043 extern Vec_Int_t * Gia_ManKSatGenLevels( char * pGuide, int nIns, int nNodes );
2044 Vec_Int_t * vRes = pGuide ? Gia_ManKSatGenLevels( pGuide, p->nDivs, p->nNodes ) : NULL;
2045 int pLits[2*MAJ_NOBJS], i, j, k, n, m, nLits, Start, Stop;
2046 if ( vRes ) {
2047 n = p->nDivs;
2048 Vec_IntForEachEntryDoubleStart( vRes, Start, Stop, i, 2*p->nDivs ) {
2049 for ( j = 0; j < Start; j++ )
2050 if ( p->VarMarks[n][0][j] )
2051 Exa4_ManAddClause4( p, Abc_Var2Lit( p->VarMarks[n][0][j], 1 ), 0, 0, 0 );
2052 for ( k = 0; k < 2; k++ )
2053 for ( j = Stop; j < n; j++ )
2054 if ( p->VarMarks[n][k][j] )
2055 Exa4_ManAddClause4( p, Abc_Var2Lit( p->VarMarks[n][k][j], 1 ), 0, 0, 0 );
2056 n++;
2057 }
2058 assert( n == p->nDivs + p->nNodes );
2059 Vec_IntFreeP( &vRes );
2060 }
2061 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2062 {
2063 int iVarStart = 1 + 5*(i - p->nDivs);//
2064 for ( k = 0; k < 2; k++ )
2065 {
2066 nLits = 0;
2067 for ( j = 0; j < p->nObjs; j++ )
2068 if ( p->VarMarks[i][k][j] )
2069 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
2070 assert( nLits > 0 );
2071 Exa4_ManAddClause( p, pLits, nLits );
2072 if ( !fCard ) {
2073 for ( n = 0; n < nLits; n++ )
2074 for ( m = n+1; m < nLits; m++ )
2075 Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
2076 }
2077 else {
2078 fprintf( p->pFile, "k %d ", nLits-1 );
2079 for ( n = 0; n < nLits; n++ )
2080 pLits[n] = Abc_LitNot(pLits[n]);
2081 Exa4_ManAddClause( p, pLits, nLits );
2082 }
2083 if ( k == 1 )
2084 break;
2085 for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][0][j] )
2086 for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][1][n] )
2087 Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][j], 1), Abc_Var2Lit(p->VarMarks[i][1][n], 1), 0, 0 );
2088 }
2089 if ( fOrderNodes )
2090 for ( j = p->nDivs; j < i; j++ )
2091 for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
2092 for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
2093 Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][n], 1), Abc_Var2Lit(p->VarMarks[j][0][m], 1), 0, 0 );
2094 for ( j = p->nDivs; j < i; j++ )
2095 for ( k = 0; k < 2; k++ ) if ( p->VarMarks[i][k][j] )
2096 for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][!k][n] )
2097 for ( m = 0; m < 2; m++ ) if ( p->VarMarks[j][m][n] )
2098 Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][k][j], 1), Abc_Var2Lit(p->VarMarks[i][!k][n], 1), Abc_Var2Lit(p->VarMarks[j][m][n], 1), 0 );
2099 if ( fFancy )
2100 {
2101 nLits = 0;
2102 for ( k = 0; k < 5-fOnlyAnd; k++ )
2103 pLits[nLits++] = Abc_Var2Lit( iVarStart+k, 0 );
2104 Exa4_ManAddClause( p, pLits, nLits );
2105 for ( n = 0; n < nLits; n++ )
2106 for ( m = n+1; m < nLits; m++ )
2107 Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
2108 }
2109 else
2110 {
2111 for ( k = 0; k < 3; k++ )
2112 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart, k==1), Abc_Var2Lit(iVarStart+1, k==2), Abc_Var2Lit(iVarStart+2, k!=0), 0);
2113 if ( fOnlyAnd )
2114 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart, 1), Abc_Var2Lit(iVarStart+1, 1), Abc_Var2Lit(iVarStart+2, 0), 0);
2115 }
2116 }
2117 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2118 {
2119 nLits = 0;
2120 for ( k = 0; k < 2; k++ )
2121 for ( j = i+1; j < p->nObjs; j++ )
2122 if ( p->VarMarks[j][k][i] )
2123 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[j][k][i], 0 );
2124 Exa4_ManAddClause( p, pLits, nLits );
2125 if ( fUniqFans )
2126 for ( n = 0; n < nLits; n++ )
2127 for ( m = n+1; m < nLits; m++ )
2128 Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
2129 }
2130 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2131 {
2132 nLits = 0;
2133 for ( j = 0; j < p->nDivs + p->nNodes; j++ ) if ( p->VarMarks[i][0][j] )
2134 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][0][j], 0 );
2135 Exa4_ManAddClause( p, pLits, nLits );
2136 for ( n = 0; n < nLits; n++ )
2137 for ( m = n+1; m < nLits; m++ )
2138 Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
2139 }
2140 return 1;
2141}
2142void Exa4_ManGenMint( Exa4_Man_t * p, int iMint, int fOnlyAnd, int fFancy )
2143{
2144 int iNodeVar = p->nCnfVars + 3*p->nNodes*(iMint - Vec_WrdSize(p->vSimsIn));
2145 int iOutMint = Abc_Tt6FirstBit( Vec_WrdEntry(p->vSimsOut, iMint) );
2146 int i, k, n, j, VarVals[MAJ_NOBJS];
2147 assert( p->nObjs <= MAJ_NOBJS );
2148 assert( iMint < Vec_WrdSize(p->vSimsIn) );
2149 for ( i = 0; i < p->nDivs; i++ )
2150 VarVals[i] = (Vec_WrdEntry(p->vSimsIn, iMint) >> i) & 1;
2151 for ( i = 0; i < p->nNodes; i++ )
2152 VarVals[p->nDivs + i] = Abc_Var2Lit(iNodeVar + 3*i + 2, 0);
2153 for ( i = 0; i < p->nOuts; i++ )
2154 VarVals[p->nDivs + p->nNodes + i] = (iOutMint >> i) & 1;
2155 if ( 0 )
2156 {
2157 printf( "Adding minterm %d: ", iMint );
2158 for ( i = 0; i < p->nObjs; i++ )
2159 printf( " %d=%d", i, VarVals[i] );
2160 printf( "\n" );
2161 }
2162 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2163 {
2164 int iVarStart = 1 + 5*(i - p->nDivs);//
2165 int iBaseVarI = iNodeVar + 3*(i - p->nDivs);
2166 for ( k = 0; k < 2; k++ )
2167 for ( j = 0; j < i; j++ ) if ( p->VarMarks[i][k][j] )
2168 for ( n = 0; n < 2; n++ )
2169 Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][k][j], 1), Abc_Var2Lit(iBaseVarI + k, n), Abc_LitNotCond(VarVals[j], !n), 0);
2170 if ( fFancy )
2171 {
2172 // Clauses for a*b = c
2173 // a + ~c
2174 // b + ~c
2175 // ~a + ~b + c
2176 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 0, 1), Abc_Var2Lit(iBaseVarI + 0, 0), 0, Abc_Var2Lit(iBaseVarI + 2, 1) );
2177 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 0, 1), 0, Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 1) );
2178 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 0, 1), Abc_Var2Lit(iBaseVarI + 0, 1), Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 0) );
2179
2180 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 1, 1), Abc_Var2Lit(iBaseVarI + 0, 1), 0, Abc_Var2Lit(iBaseVarI + 2, 1) );
2181 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 1, 1), 0, Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 1) );
2182 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 1, 1), Abc_Var2Lit(iBaseVarI + 0, 0), Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 0) );
2183
2184 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 2, 1), Abc_Var2Lit(iBaseVarI + 0, 0), 0, Abc_Var2Lit(iBaseVarI + 2, 1) );
2185 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 2, 1), 0, Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 1) );
2186 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 2, 1), Abc_Var2Lit(iBaseVarI + 0, 1), Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 0) );
2187 // Clauses for a+b = c
2188 // ~a + c
2189 // ~b + c
2190 // a + b + ~c
2191 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 3, 1), Abc_Var2Lit(iBaseVarI + 0, 1), 0, Abc_Var2Lit(iBaseVarI + 2, 0) );
2192 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 3, 1), 0, Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 0) );
2193 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 3, 1), Abc_Var2Lit(iBaseVarI + 0, 0), Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 1) );
2194 // Clauses for a^b = c
2195 // ~a + ~b + ~c
2196 // ~a + b + c
2197 // a + ~b + c
2198 // a + b + ~c
2199 if ( !fOnlyAnd )
2200 {
2201 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 4, 1), Abc_Var2Lit(iBaseVarI + 0, 1), Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 1) );
2202 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 4, 1), Abc_Var2Lit(iBaseVarI + 0, 1), Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 0) );
2203 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 4, 1), Abc_Var2Lit(iBaseVarI + 0, 0), Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 0) );
2204 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 4, 1), Abc_Var2Lit(iBaseVarI + 0, 0), Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 1) );
2205 }
2206 }
2207 else
2208 {
2209 for ( k = 0; k < 4; k++ )
2210 for ( n = 0; n < 2; n++ )
2211 Exa4_ManAddClause4( p, Abc_Var2Lit(iBaseVarI + 0, k&1), Abc_Var2Lit(iBaseVarI + 1, k>>1), Abc_Var2Lit(iBaseVarI + 2, !n), Abc_Var2Lit(k ? iVarStart + k-1 : 0, n));
2212 }
2213 }
2214 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2215 {
2216 for ( j = 0; j < p->nDivs + p->nNodes; j++ ) if ( p->VarMarks[i][0][j] )
2217 for ( n = 0; n < 2; n++ )
2218 Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][j], 1), Abc_LitNotCond(VarVals[j], n), Abc_LitNotCond(VarVals[i], !n), 0);
2219 }
2220}
2221void Exa4_ManGenCnf( Exa4_Man_t * p, char * pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard, char * pGuide )
2222{
2223 int m;
2224 assert( p->pFile == NULL );
2225 p->pFile = fopen( pFileName, "wb" );
2226 fputs( "p cnf \n", p->pFile );
2227 Exa4_ManGenStart( p, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fCard, pGuide );
2228 for ( m = 1; m < Vec_WrdSize(p->vSimsIn); m++ )
2229 Exa4_ManGenMint( p, m, fOnlyAnd, fFancy );
2230 rewind( p->pFile );
2231 fprintf( p->pFile, "p %cnf %d %d", fCard ? 'k' : 'c', p->nCnfVars, p->nCnfClauses );
2232 fclose( p->pFile );
2233}
2234
2246static inline int Exa4_ManFindFanin( Exa4_Man_t * p, Vec_Int_t * vValues, int i, int k )
2247{
2248 int j, Count = 0, iVar = -1;
2249 for ( j = 0; j < p->nObjs; j++ )
2250 if ( p->VarMarks[i][k][j] && Vec_IntEntry(vValues, p->VarMarks[i][k][j]) )
2251 {
2252 iVar = j;
2253 Count++;
2254 }
2255 if ( Count != 1 )
2256 printf( "Fanin count is %d instead of %d.\n", Count, 1 );
2257 assert( Count == 1 );
2258 return iVar;
2259}
2260static inline void Exa4_ManPrintFanin( Exa4_Man_t * p, int iNode, int fComp )
2261{
2262 if ( iNode == 0 )
2263 printf( " %s", fComp ? "const1" : "const0" );
2264 else if ( iNode > 0 && iNode <= p->nIns )
2265 printf( " %s%c", fComp ? "~" : "", 'a'+iNode-1 );
2266 else if ( iNode > p->nIns && iNode < p->nDivs )
2267 printf( " %s%c", fComp ? "~" : "", 'A'+iNode-p->nIns-1 );
2268 else
2269 printf( " %s%d", fComp ? "~" : "", iNode );
2270}
2271void Exa4_ManPrintSolution( Exa4_Man_t * p, Vec_Int_t * vValues, int fFancy )
2272{
2273 int i, k;
2274 printf( "Circuit for %d-var function with %d divisors contains %d two-input gates:\n", p->nIns, p->nDivs, p->nNodes );
2275 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2276 {
2277 int iVar = Exa4_ManFindFanin( p, vValues, i, 0 );
2278 printf( "%2d = ", i );
2279 Exa4_ManPrintFanin( p, iVar, 0 );
2280 printf( "\n" );
2281 }
2282 for ( i = p->nDivs + p->nNodes - 1; i >= p->nDivs; i-- )
2283 {
2284 int iVarStart = 1 + 5*(i - p->nDivs);//
2285 if ( fFancy )
2286 {
2287 int Val1 = Vec_IntEntry(vValues, iVarStart);
2288 int Val2 = Vec_IntEntry(vValues, iVarStart+1);
2289 int Val3 = Vec_IntEntry(vValues, iVarStart+2);
2290 int Val4 = Vec_IntEntry(vValues, iVarStart+3);
2291 //int Val5 = Vec_IntEntry(vValues, iVarStart+4);
2292 printf( "%2d = ", i );
2293 for ( k = 0; k < 2; k++ )
2294 {
2295 int iNode = Exa4_ManFindFanin( p, vValues, i, !k );
2296 int fComp = k ? Val1 | Val3 : Val2 | Val3;
2297 Exa4_ManPrintFanin( p, iNode, fComp );
2298 if ( k ) break;
2299 printf( " %c", (Val1 || Val2 || Val3) ? '&' : (Val4 ? '|' : '^') );
2300 }
2301 }
2302 else
2303 {
2304 int Val1 = Vec_IntEntry(vValues, iVarStart);
2305 int Val2 = Vec_IntEntry(vValues, iVarStart+1);
2306 int Val3 = Vec_IntEntry(vValues, iVarStart+2);
2307 printf( "%2d = ", i );
2308 for ( k = 0; k < 2; k++ )
2309 {
2310 int iNode = Exa4_ManFindFanin( p, vValues, i, !k );
2311 int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3;
2312 Exa4_ManPrintFanin( p, iNode, fComp );
2313 if ( k ) break;
2314 printf( " %c", (Val1 && Val2) ? (Val3 ? '|' : '^') : '&' );
2315 }
2316 }
2317 printf( "\n" );
2318 }
2319}
2320Mini_Aig_t * Exa4_ManMiniAig( Exa4_Man_t * p, Vec_Int_t * vValues, int fFancy )
2321{
2322 int i, k, Compl[MAJ_NOBJS] = {0};
2323 Mini_Aig_t * pMini = Mini_AigStartSupport( p->nDivs-1, p->nObjs );
2324 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2325 {
2326 int iNodes[2] = {0};
2327 int iVarStart = 1 + 5*(i - p->nDivs);//
2328 if ( fFancy )
2329 {
2330 int Val1 = Vec_IntEntry(vValues, iVarStart);
2331 int Val2 = Vec_IntEntry(vValues, iVarStart+1);
2332 int Val3 = Vec_IntEntry(vValues, iVarStart+2);
2333 int Val4 = Vec_IntEntry(vValues, iVarStart+3);
2334 int Val5 = Vec_IntEntry(vValues, iVarStart+4);
2335 for ( k = 0; k < 2; k++ )
2336 {
2337 int iNode = Exa4_ManFindFanin( p, vValues, i, !k );
2338 int fComp = k ? Val1 | Val3 : Val2 | Val3;
2339 iNodes[k] = Abc_Var2Lit(iNode, fComp ^ Compl[iNode]);
2340 }
2341 if ( Val1 || Val2 || Val3 )
2342 Mini_AigAnd( pMini, iNodes[0], iNodes[1] );
2343 else
2344 {
2345 if ( Val4 )
2346 Mini_AigOr( pMini, iNodes[0], iNodes[1] );
2347 else if ( Val5 )
2348 Mini_AigXorSpecial( pMini, iNodes[0], iNodes[1] );
2349 else assert( 0 );
2350 }
2351 }
2352 else
2353 {
2354 int Val1 = Vec_IntEntry(vValues, iVarStart);
2355 int Val2 = Vec_IntEntry(vValues, iVarStart+1);
2356 int Val3 = Vec_IntEntry(vValues, iVarStart+2);
2357 Compl[i] = Val1 && Val2 && Val3;
2358 for ( k = 0; k < 2; k++ )
2359 {
2360 int iNode = Exa4_ManFindFanin( p, vValues, i, !k );
2361 int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3;
2362 iNodes[k] = Abc_Var2Lit(iNode, fComp ^ Compl[iNode]);
2363 }
2364 if ( Val1 && Val2 )
2365 {
2366 if ( Val3 )
2367 Mini_AigOr( pMini, iNodes[0], iNodes[1] );
2368 else
2369 Mini_AigXorSpecial( pMini, iNodes[0], iNodes[1] );
2370 }
2371 else
2372 Mini_AigAnd( pMini, iNodes[0], iNodes[1] );
2373 }
2374 }
2375 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2376 {
2377 int iVar = Exa4_ManFindFanin( p, vValues, i, 0 );
2378 Mini_AigCreatePo( pMini, Abc_Var2Lit(iVar, Compl[iVar]) );
2379 }
2380 assert( p->nObjs == Mini_AigNodeNum(pMini) );
2381 return pMini;
2382}
2383
2395Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard, char * pGuide )
2396{
2397 extern Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int Seed, int nBTLimit, int TimeOut, int fVerbose, int * pStatus );
2398 Mini_Aig_t * pMini = NULL;
2399 abctime clkTotal = Abc_Clock();
2400 Vec_Int_t * vValues = NULL;
2401 srand(time(NULL));
2402 int Status = 0, Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFF;
2403 char pFileNameIn[32]; sprintf( pFileNameIn, "_%05x_.cnf", Rand );
2404 char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand );
2405 Exa4_Man_t * p = Exa4_ManAlloc( vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, fVerbose );
2406 Exa_ManIsNormalized( vSimsIn, vSimsOut );
2407 Exa4_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fCard, pGuide );
2408 if ( fVerbose )
2409 printf( "Timeout = %d. OnlyAnd = %d. Fancy = %d. OrderNodes = %d. UniqueFans = %d. Verbose = %d.\n", TimeOut, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fVerbose );
2410 if ( fVerbose )
2411 printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", p->nCnfVars, p->nCnfClauses, pFileNameIn );
2412 if ( fCard )
2413 vValues = Gia_RunKadical( pFileNameIn, pFileNameOut, 0, 0, TimeOut, fVerbose, &Status );
2414 else
2415 vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, TimeOut, fVerbose );
2416 if ( vValues ) pMini = Exa4_ManMiniAig( p, vValues, fFancy );
2417 //if ( vValues ) Exa4_ManPrintSolution( p, vValues, fFancy );
2418 if ( vValues ) Exa_ManMiniPrint( pMini, p->nIns );
2419 if ( vValues ) Exa_ManMiniVerify( pMini, vSimsIn, vSimsOut );
2420 Vec_IntFreeP( &vValues );
2421 Exa4_ManFree( p );
2422 unlink( pFileNameIn );
2423 Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
2424 return pMini;
2425}
2426void Exa_ManExactSynthesis4_( Bmc_EsPar_t * pPars )
2427{
2428 Mini_Aig_t * pMini = NULL;
2429 int i, m;
2430 Vec_Wrd_t * vSimsIn = Vec_WrdStart( 8 );
2431 Vec_Wrd_t * vSimsOut = Vec_WrdStart( 8 );
2432 int Truths[2] = { 0x96, 0xE8 };
2433 for ( m = 0; m < 8; m++ )
2434 {
2435 int iOutMint = 0;
2436 for ( i = 0; i < 2; i++ )
2437 if ( (Truths[i] >> m) & 1 )
2438 iOutMint |= 1 << i;
2439 Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, m), iOutMint );
2440 for ( i = 0; i < 3; i++ )
2441 if ( (m >> i) & 1 )
2442 Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i );
2443 }
2444 pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, 3, 4, 2, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose, 0, pPars->pGuide );
2445 if ( pMini ) Mini_AigStop( pMini );
2446 Vec_WrdFree( vSimsIn );
2447 Vec_WrdFree( vSimsOut );
2448}
2449void Exa_ManExactSynthesis4( Bmc_EsPar_t * pPars )
2450{
2451 Mini_Aig_t * pMini = NULL;
2452 int i, m, nMints = 1 << pPars->nVars, fCompl = 0;
2453 Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints );
2454 Vec_Wrd_t * vSimsOut = Vec_WrdStart( nMints );
2455 word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr );
2456 if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, Abc_TtWordNum(pPars->nVars) ); }
2457 assert( pPars->nVars <= 10 );
2458 for ( m = 0; m < nMints; m++ )
2459 {
2460 Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, m), Abc_TtGetBit(pTruth, m) );
2461 for ( i = 0; i < pPars->nVars; i++ )
2462 if ( (m >> i) & 1 )
2463 Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i );
2464 }
2465 assert( Vec_WrdSize(vSimsIn) == (1 << pPars->nVars) );
2466 pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, pPars->nVars, 1+pPars->nVars, 1, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose, pPars->fCard, pPars->pGuide );
2467 if ( pMini ) Mini_AigStop( pMini );
2468 if ( fCompl ) printf( "The resulting circuit, if computed, will be complemented.\n" );
2469 Vec_WrdFree( vSimsIn );
2470 Vec_WrdFree( vSimsOut );
2471}
2472
2473
2474
2475typedef struct Exa5_Man_t_ Exa5_Man_t;
2476struct Exa5_Man_t_
2477{
2478 Vec_Wrd_t * vSimsIn;
2479 Vec_Wrd_t * vSimsOut;
2480 int fVerbose;
2481 int nIns;
2482 int nDivs; // divisors (const + inputs + tfi + sidedivs)
2483 int nNodes;
2484 int nOuts;
2485 int nObjs;
2486 int VarMarks[MAJ_NOBJS][MAJ_NOBJS];
2487 int nCnfVars;
2488 int nCnfClauses;
2489 FILE * pFile;
2490 Vec_Int_t * vFans;
2491};
2492
2493
2505int Exa5_ManMarkup( Exa5_Man_t * p )
2506{
2507 int i, j, k, nVars[3] = {1 + 3*p->nNodes, 0, p->nNodes*Vec_WrdSize(p->vSimsIn)};
2508 assert( p->nObjs <= MAJ_NOBJS );
2509 Vec_IntFill( p->vFans, 1 + 3*p->nNodes, 0 );
2510 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2511 for ( j = 2; j < i; j++ )
2512 {
2513 p->VarMarks[i][j] = nVars[0] + nVars[1];
2514 Vec_IntPush( p->vFans, 0 );
2515 for ( k = 1; k < j; k++ )
2516 Vec_IntPush( p->vFans, (i << 16) | (j << 8) | k );
2517 nVars[1] += j;
2518 }
2519 assert( Vec_IntSize(p->vFans) == nVars[0] + nVars[1] );
2520 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2521 for ( j = p->nOuts == 1 ? p->nDivs + p->nNodes - 1 : 0; j < p->nDivs + p->nNodes; j++ )
2522 p->VarMarks[i][j] = nVars[0] + nVars[1]++;
2523 if ( p->fVerbose )
2524 printf( "Variables: Function = %d. Structure = %d. Internal = %d. Total = %d.\n",
2525 nVars[0], nVars[1], nVars[2], nVars[0] + nVars[1] + nVars[2] );
2526 if ( 0 )
2527 {
2528 {
2529 printf( " : " );
2530 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2531 {
2532 printf( "%3d ", i );
2533 printf( " " );
2534 }
2535 printf( " " );
2536 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2537 {
2538 printf( "%3d ", i );
2539 printf( " " );
2540 }
2541 printf( "\n" );
2542 }
2543 for ( j = 0; j < 5 + p->nNodes*5 + p->nOuts*5; j++ )
2544 printf( "-" );
2545 printf( "\n" );
2546 for ( j = p->nObjs - 2; j >= 0; j-- )
2547 {
2548 if ( j > 0 && j <= p->nIns )
2549 printf( " %c : ", 'a'+j-1 );
2550 else
2551 printf( "%2d : ", j );
2552 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2553 {
2554 printf( "%3d ", p->VarMarks[i][j] );
2555 printf( " " );
2556 }
2557 printf( " " );
2558 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2559 {
2560 printf( "%3d ", p->VarMarks[i][j] );
2561 printf( " " );
2562 }
2563 printf( "\n" );
2564 }
2565 }
2566 return nVars[0] + nVars[1] + nVars[2];
2567}
2568Exa5_Man_t * Exa5_ManAlloc( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int fVerbose )
2569{
2570 Exa5_Man_t * p = ABC_CALLOC( Exa5_Man_t, 1 );
2571 assert( Vec_WrdSize(vSimsIn) == Vec_WrdSize(vSimsOut) );
2572 p->vSimsIn = vSimsIn;
2573 p->vSimsOut = vSimsOut;
2574 p->fVerbose = fVerbose;
2575 p->nIns = nIns;
2576 p->nDivs = nDivs;
2577 p->nNodes = nNodes;
2578 p->nOuts = nOuts;
2579 p->nObjs = p->nDivs + p->nNodes + p->nOuts;
2580 p->vFans = Vec_IntAlloc( 5000 );
2581 p->nCnfVars = Exa5_ManMarkup( p );
2582 return p;
2583}
2584void Exa5_ManFree( Exa5_Man_t * p )
2585{
2586 Vec_IntFree( p->vFans );
2587 ABC_FREE( p );
2588}
2589
2590
2602static inline int Exa5_ManAddClause( Exa5_Man_t * p, int * pLits, int nLits )
2603{
2604 int i, k = 0;
2605 for ( i = 0; i < nLits; i++ )
2606 if ( pLits[i] == 1 )
2607 return 0;
2608 else if ( pLits[i] == 0 )
2609 continue;
2610 else if ( pLits[i] <= 2*p->nCnfVars )
2611 pLits[k++] = pLits[i];
2612 else assert( 0 );
2613 nLits = k;
2614 assert( nLits > 0 );
2615 if ( p->pFile )
2616 {
2617 p->nCnfClauses++;
2618 for ( i = 0; i < nLits; i++ )
2619 fprintf( p->pFile, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) );
2620 fprintf( p->pFile, "0\n" );
2621 }
2622 if ( 0 )
2623 {
2624 for ( i = 0; i < nLits; i++ )
2625 fprintf( stdout, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) );
2626 fprintf( stdout, "\n" );
2627 }
2628 return 1;
2629}
2630static inline int Exa5_ManAddClause4( Exa5_Man_t * p, int Lit0, int Lit1, int Lit2, int Lit3, int Lit4 )
2631{
2632 int pLits[5] = { Lit0, Lit1, Lit2, Lit3, Lit4 };
2633 return Exa5_ManAddClause( p, pLits, 5 );
2634}
2635static inline void Exa5_ManAddOneHot( Exa5_Man_t * p, int * pLits, int nLits )
2636{
2637 int n, m;
2638 for ( n = 0; n < nLits; n++ )
2639 for ( m = n+1; m < nLits; m++ )
2640 Exa5_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0, 0 );
2641}
2642static inline void Exa5_ManAddGroup( Exa5_Man_t * p, int iVar, int nVars )
2643{
2644 int i, pLits[MAJ_NOBJS];
2645 assert( nVars+1 <= MAJ_NOBJS );
2646 pLits[0] = Abc_Var2Lit( iVar, 1 );
2647 for ( i = 1; i <= nVars; i++ )
2648 pLits[i] = Abc_Var2Lit( iVar+i, 0 );
2649 Exa5_ManAddClause( p, pLits, nVars+1 );
2650 Exa5_ManAddOneHot( p, pLits+1, nVars );
2651 for ( i = 1; i <= nVars; i++ )
2652 Exa5_ManAddClause4( p, Abc_LitNot(pLits[0]), Abc_LitNot(pLits[i]), 0, 0, 0 );
2653}
2654int Exa5_ManGenStart( Exa5_Man_t * p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans )
2655{
2656 Vec_Int_t * vArray = Vec_IntAlloc( 100 );
2657 int pLits[MAJ_NOBJS], i, j, k, n, m, nLits, iObj;
2658 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2659 {
2660 int iVarStart = 1 + 3*(i - p->nDivs);//
2661 nLits = 0;
2662 for ( j = 0; j < i; j++ ) if ( p->VarMarks[i][j] )
2663 Exa5_ManAddGroup( p, p->VarMarks[i][j], j-1 ), pLits[nLits++] = Abc_Var2Lit(p->VarMarks[i][j], 0);
2664 Exa5_ManAddClause( p, pLits, nLits );
2665 Exa5_ManAddOneHot( p, pLits, nLits );
2666 if ( fOrderNodes )
2667 for ( j = p->nDivs; j < i; j++ )
2668 for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][n] )
2669 for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][m] )
2670 Exa5_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][n], 1), Abc_Var2Lit(p->VarMarks[j][m], 1), 0, 0, 0 );
2671 for ( j = p->nDivs; j < i; j++ ) if ( p->VarMarks[i][j] )
2672 {
2673 // go through all variables of i that point to j and k
2674 for ( n = 1; n < j; n++ )
2675 {
2676 int iVar = p->VarMarks[i][j] + n; // variable of i pointing to j
2677 int iObj = Vec_IntEntry( p->vFans, iVar );
2678 int iNode0 = (iObj >> 0) & 0xFF;
2679 int iNode1 = (iObj >> 8) & 0xFF;
2680 int iNode2 = (iObj >> 16) & 0xFF;
2681 assert( iObj > 0 );
2682 assert( iNode1 == j );
2683 assert( iNode2 == i );
2684 // go through all variables of j and block those that point to k
2685 assert( p->VarMarks[j][2] > 0 );
2686 assert( p->VarMarks[j+1][2] > 0 );
2687 for ( m = p->VarMarks[j][2]+1; m < p->VarMarks[j+1][2]; m++ )
2688 {
2689 int jObj = Vec_IntEntry( p->vFans, m );
2690 int jNode0 = (jObj >> 0) & 0xFF;
2691 int jNode1 = (jObj >> 8) & 0xFF;
2692 int jNode2 = (jObj >> 16) & 0xFF;
2693 if ( jObj == 0 )
2694 continue;
2695 assert( jNode2 == j );
2696 if ( iNode0 == jNode0 || iNode0 == jNode1 )
2697 Exa5_ManAddClause4( p, Abc_Var2Lit(iVar, 1), Abc_Var2Lit(m, 1), 0, 0, 0 );
2698 }
2699 }
2700 }
2701 for ( k = 0; k < 3; k++ )
2702 Exa5_ManAddClause4( p, Abc_Var2Lit(iVarStart, k==1), Abc_Var2Lit(iVarStart+1, k==2), Abc_Var2Lit(iVarStart+2, k!=0), 0, 0);
2703 if ( fOnlyAnd )
2704 Exa5_ManAddClause4( p, Abc_Var2Lit(iVarStart, 1), Abc_Var2Lit(iVarStart+1, 1), Abc_Var2Lit(iVarStart+2, 0), 0, 0);
2705 }
2706 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2707 {
2708 Vec_IntClear( vArray );
2709 Vec_IntForEachEntry( p->vFans, iObj, k )
2710 if ( iObj && ((iObj & 0xFF) == i || ((iObj >> 8) & 0xFF) == i) )
2711 Vec_IntPush( vArray, Abc_Var2Lit(k, 0) );
2712 for ( k = p->nDivs + p->nNodes; k < p->nObjs; k++ ) if ( p->VarMarks[k][i] )
2713 Vec_IntPush( vArray, Abc_Var2Lit(p->VarMarks[k][i], 0) );
2714 Exa5_ManAddClause( p, Vec_IntArray(vArray), Vec_IntSize(vArray) );
2715 if ( fUniqFans )
2716 Exa5_ManAddOneHot( p, Vec_IntArray(vArray), Vec_IntSize(vArray) );
2717 }
2718 Vec_IntFree( vArray );
2719 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2720 {
2721 nLits = 0;
2722 for ( j = 0; j < p->nDivs + p->nNodes; j++ ) if ( p->VarMarks[i][j] )
2723 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][j], 0 );
2724 Exa5_ManAddClause( p, pLits, nLits );
2725 Exa5_ManAddOneHot( p, pLits, nLits );
2726 }
2727 return 1;
2728}
2729void Exa5_ManGenMint( Exa5_Man_t * p, int iMint, int fOnlyAnd, int fFancy )
2730{
2731 int iNodeVar = p->nCnfVars + p->nNodes*(iMint - Vec_WrdSize(p->vSimsIn));
2732 int iOutMint = Abc_Tt6FirstBit( Vec_WrdEntry(p->vSimsOut, iMint) );
2733 int i, k, n, j, VarVals[MAJ_NOBJS], iNodes[3], iVarStart, iObj;
2734 assert( p->nObjs <= MAJ_NOBJS );
2735 assert( iMint < Vec_WrdSize(p->vSimsIn) );
2736 for ( i = 0; i < p->nDivs; i++ )
2737 VarVals[i] = (Vec_WrdEntry(p->vSimsIn, iMint) >> i) & 1;
2738 for ( i = 0; i < p->nNodes; i++ )
2739 VarVals[p->nDivs + i] = Abc_Var2Lit(iNodeVar + i, 0);
2740 for ( i = 0; i < p->nOuts; i++ )
2741 VarVals[p->nDivs + p->nNodes + i] = (iOutMint >> i) & 1;
2742 if ( 0 )
2743 {
2744 printf( "Adding minterm %d: ", iMint );
2745 for ( i = 0; i < p->nObjs; i++ )
2746 printf( " %d=%d", i, VarVals[i] );
2747 printf( "\n" );
2748 }
2749 Vec_IntForEachEntry( p->vFans, iObj, i )
2750 {
2751 if ( iObj == 0 ) continue;
2752 iNodes[1] = (iObj >> 0) & 0xFF;
2753 iNodes[0] = (iObj >> 8) & 0xFF;
2754 iNodes[2] = (iObj >> 16) & 0xFF;
2755 iVarStart = 1 + 3*(iNodes[2] - p->nDivs);//
2756 for ( k = 0; k < 4; k++ )
2757 for ( n = 0; n < 2; n++ )
2758 Exa5_ManAddClause4( p, Abc_Var2Lit(i, 1), Abc_LitNotCond(VarVals[iNodes[0]], k&1), Abc_LitNotCond(VarVals[iNodes[1]], k>>1), Abc_LitNotCond(VarVals[iNodes[2]], !n), Abc_Var2Lit(k ? iVarStart + k-1 : 0, n));
2759 }
2760 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2761 {
2762 for ( j = 0; j < p->nDivs + p->nNodes; j++ ) if ( p->VarMarks[i][j] )
2763 for ( n = 0; n < 2; n++ )
2764 Exa5_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][j], 1), Abc_LitNotCond(VarVals[j], n), Abc_LitNotCond(VarVals[i], !n), 0, 0);
2765 }
2766}
2767void Exa5_ManGenCnf( Exa5_Man_t * p, char * pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans )
2768{
2769 int m;
2770 assert( p->pFile == NULL );
2771 p->pFile = fopen( pFileName, "wb" );
2772 fputs( "p cnf \n", p->pFile );
2773 Exa5_ManGenStart( p, fOnlyAnd, fFancy, fOrderNodes, fUniqFans );
2774 for ( m = 1; m < Vec_WrdSize(p->vSimsIn); m++ )
2775 Exa5_ManGenMint( p, m, fOnlyAnd, fFancy );
2776 rewind( p->pFile );
2777 fprintf( p->pFile, "p cnf %d %d", p->nCnfVars, p->nCnfClauses );
2778 fclose( p->pFile );
2779}
2780
2792static inline int Exa5_ManFindFanin( Exa5_Man_t * p, Vec_Int_t * vValues, int i )
2793{
2794 int j, Count = 0, iVar = -1;
2795 for ( j = 0; j < p->nObjs; j++ )
2796 if ( p->VarMarks[i][j] && Vec_IntEntry(vValues, p->VarMarks[i][j]) )
2797 {
2798 iVar = j;
2799 Count++;
2800 }
2801 assert( Count == 1 );
2802 return iVar;
2803}
2804static inline void Exa5_ManPrintFanin( Exa5_Man_t * p, int iNode, int fComp )
2805{
2806 if ( iNode == 0 )
2807 printf( " %s", fComp ? "const1" : "const0" );
2808 else if ( iNode > 0 && iNode <= p->nIns )
2809 printf( " %s%c", fComp ? "~" : "", 'a'+iNode-1 );
2810 else if ( iNode > p->nIns && iNode < p->nDivs )
2811 printf( " %s%c", fComp ? "~" : "", 'A'+iNode-p->nIns-1 );
2812 else
2813 printf( " %s%d", fComp ? "~" : "", iNode );
2814}
2815void Exa5_ManPrintSolution( Exa5_Man_t * p, Vec_Int_t * vValues, int fFancy )
2816{
2817 int Fan0[MAJ_NOBJS] = {0};
2818 int Fan1[MAJ_NOBJS] = {0};
2819 int Count[MAJ_NOBJS] = {0};
2820 int i, k, iObj, iNodes[3];
2821 printf( "Circuit for %d-var function with %d divisors contains %d two-input gates:\n", p->nIns, p->nDivs, p->nNodes );
2822 Vec_IntForEachEntry( p->vFans, iObj, i )
2823 {
2824 if ( iObj == 0 || Vec_IntEntry(vValues, i) == 0 )
2825 continue;
2826 iNodes[0] = (iObj >> 0) & 0xFF;
2827 iNodes[1] = (iObj >> 8) & 0xFF;
2828 iNodes[2] = (iObj >> 16) & 0xFF;
2829 assert( p->nDivs <= iNodes[2] && iNodes[2] < p->nDivs + p->nNodes );
2830 Fan0[iNodes[2]] = iNodes[0];
2831 Fan1[iNodes[2]] = iNodes[1];
2832 Count[iNodes[2]]++;
2833 }
2834 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2835 {
2836 int iVar = Exa5_ManFindFanin( p, vValues, i );
2837 printf( "%2d = ", i );
2838 Exa5_ManPrintFanin( p, iVar, 0 );
2839 printf( "\n" );
2840 }
2841 for ( i = p->nDivs + p->nNodes - 1; i >= p->nDivs; i-- )
2842 {
2843 int iVarStart = 1 + 3*(i - p->nDivs);//
2844 int Val1 = Vec_IntEntry(vValues, iVarStart);
2845 int Val2 = Vec_IntEntry(vValues, iVarStart+1);
2846 int Val3 = Vec_IntEntry(vValues, iVarStart+2);
2847 assert( Count[i] == 1 );
2848 printf( "%2d = ", i );
2849 for ( k = 0; k < 2; k++ )
2850 {
2851 int iNode = k ? Fan1[i] : Fan0[i];
2852 int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3;
2853 Exa5_ManPrintFanin( p, iNode, fComp );
2854 if ( k ) break;
2855 printf( " %c", (Val1 && Val2) ? (Val3 ? '|' : '^') : '&' );
2856 }
2857 printf( "\n" );
2858 }
2859}
2860Mini_Aig_t * Exa5_ManMiniAig( Exa5_Man_t * p, Vec_Int_t * vValues )
2861{
2862 Mini_Aig_t * pMini = Mini_AigStartSupport( p->nDivs-1, p->nObjs );
2863 int Compl[MAJ_NOBJS] = {0};
2864 int Fan0[MAJ_NOBJS] = {0};
2865 int Fan1[MAJ_NOBJS] = {0};
2866 int Count[MAJ_NOBJS] = {0};
2867 int i, k, iObj, iNodes[3];
2868 Vec_IntForEachEntry( p->vFans, iObj, i )
2869 {
2870 if ( iObj == 0 || Vec_IntEntry(vValues, i) == 0 )
2871 continue;
2872 iNodes[0] = (iObj >> 0) & 0xFF;
2873 iNodes[1] = (iObj >> 8) & 0xFF;
2874 iNodes[2] = (iObj >> 16) & 0xFF;
2875 assert( p->nDivs <= iNodes[2] && iNodes[2] < p->nDivs + p->nNodes );
2876 Fan0[iNodes[2]] = iNodes[0];
2877 Fan1[iNodes[2]] = iNodes[1];
2878 Count[iNodes[2]]++;
2879 }
2880 assert( p->nDivs == Mini_AigNodeNum(pMini) );
2881 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2882 {
2883 int iNodes[2] = {0};
2884 int iVarStart = 1 + 3*(i - p->nDivs);//
2885 int Val1 = Vec_IntEntry(vValues, iVarStart);
2886 int Val2 = Vec_IntEntry(vValues, iVarStart+1);
2887 int Val3 = Vec_IntEntry(vValues, iVarStart+2);
2888 assert( Count[i] == 1 );
2889 Compl[i] = Val1 && Val2 && Val3;
2890 for ( k = 0; k < 2; k++ )
2891 {
2892 int iNode = k ? Fan1[i] : Fan0[i];
2893 int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3;
2894 iNodes[k] = Abc_Var2Lit(iNode, fComp ^ Compl[iNode]);
2895 }
2896 if ( Val1 && Val2 )
2897 {
2898 if ( Val3 )
2899 Mini_AigOr( pMini, iNodes[0], iNodes[1] );
2900 else
2901 Mini_AigXorSpecial( pMini, iNodes[0], iNodes[1] );
2902 }
2903 else
2904 Mini_AigAnd( pMini, iNodes[0], iNodes[1] );
2905 }
2906 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2907 {
2908 int iVar = Exa5_ManFindFanin( p, vValues, i );
2909 Mini_AigCreatePo( pMini, Abc_Var2Lit(iVar, Compl[iVar]) );
2910 }
2911 assert( p->nObjs == Mini_AigNodeNum(pMini) );
2912 return pMini;
2913}
2914
2926Mini_Aig_t * Exa5_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose )
2927{
2928 abctime clkTotal = Abc_Clock();
2929 Mini_Aig_t * pMini = NULL;
2930 Vec_Int_t * vValues = NULL;
2931 srand(time(NULL));
2932 int Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFF;
2933 char pFileNameIn[32]; sprintf( pFileNameIn, "_%05x_.cnf", Rand );
2934 char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand );
2935 Exa5_Man_t * p = Exa5_ManAlloc( vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, fVerbose );
2936 Exa_ManIsNormalized( vSimsIn, vSimsOut );
2937 Exa5_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans );
2938 if ( fVerbose )
2939 printf( "Timeout = %d. OnlyAnd = %d. Fancy = %d. OrderNodes = %d. UniqueFans = %d. Verbose = %d.\n", TimeOut, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fVerbose );
2940 if ( fVerbose )
2941 printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", p->nCnfVars, p->nCnfClauses, pFileNameIn );
2942 vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, TimeOut, fVerbose );
2943 if ( vValues ) pMini = Exa5_ManMiniAig( p, vValues );
2944 //if ( vValues ) Exa5_ManPrintSolution( p, vValues, fFancy );
2945 if ( vValues ) Exa_ManMiniPrint( pMini, p->nIns );
2946 if ( vValues ) Exa_ManMiniVerify( pMini, vSimsIn, vSimsOut );
2947 Vec_IntFreeP( &vValues );
2948 Exa5_ManFree( p );
2949 unlink( pFileNameIn );
2950 Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
2951 return pMini;
2952}
2953void Exa_ManExactSynthesis5( Bmc_EsPar_t * pPars )
2954{
2955 Mini_Aig_t * pMini = NULL;
2956 int i, m, nMints = 1 << pPars->nVars, fCompl = 0;
2957 Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints );
2958 Vec_Wrd_t * vSimsOut = Vec_WrdStart( nMints );
2959 word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr );
2960 if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, Abc_TtWordNum(pPars->nVars) ); }
2961 assert( pPars->nVars <= 10 );
2962 for ( m = 0; m < nMints; m++ )
2963 {
2964 Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, m), Abc_TtGetBit(pTruth, m) );
2965 for ( i = 0; i < pPars->nVars; i++ )
2966 if ( (m >> i) & 1 )
2967 Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i );
2968 }
2969 assert( Vec_WrdSize(vSimsIn) == (1 << pPars->nVars) );
2970 pMini = Exa5_ManGenTest( vSimsIn, vSimsOut, pPars->nVars, 1+pPars->nVars, 1, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose );
2971 if ( pMini ) Mini_AigStop( pMini );
2972 if ( fCompl ) printf( "The resulting circuit, if computed, will be complemented.\n" );
2973 Vec_WrdFree( vSimsIn );
2974 Vec_WrdFree( vSimsOut );
2975}
2976
2988void Mini_AigPrintArray( FILE * pFile, Mini_Aig_t * p )
2989{
2990 int i, Count = 0;
2991 fprintf( pFile, " { " );
2992 Mini_AigForEachAnd( p, i )
2993 fprintf( pFile, "%2d,%2d, ", Mini_AigNodeFanin0(p, i), Mini_AigNodeFanin1(p, i) ), Count++;
2994 Mini_AigForEachPo( p, i )
2995 fprintf( pFile, "%2d,%2d", Mini_AigNodeFanin0(p, i), Mini_AigNodeFanin0(p, i) ), Count++;
2996 for ( i = Count; i < 8; i++ )
2997 fprintf( pFile, ", %2d,%2d", 0, 0 );
2998 fprintf( pFile, " }" );
2999}
3000word Mini_AigWriteEntry( Mini_Aig_t * p )
3001{
3002 word Res = 0; int i, k = 0;
3003 Mini_AigForEachAnd( p, i )
3004 {
3005 int iLit0 = Mini_AigNodeFanin0(p, i);
3006 int iLit1 = Mini_AigNodeFanin1(p, i);
3007 int Pair;
3008 if ( k < 4 )
3009 {
3010 assert( (iLit1 & 0xF) != (iLit0 & 0xF) );
3011 Pair = ((iLit1 & 0xF) << 4) | (iLit0 & 0xF);
3012 Res |= (word)Pair << (k*8);
3013 }
3014 else
3015 {
3016 assert( (iLit1 & 0x1F) != (iLit0 & 0x1F) );
3017 Pair = ((iLit1 & 0x1F) << 5) | (iLit0 & 0x1F);
3018 Res |= (word)Pair << (32 + (k-4)*10);
3019 }
3020 k++;
3021 }
3022 Mini_AigForEachPo( p, i )
3023 if ( Mini_AigNodeFanin0(p, i) & 1 )
3024 Res |= (word)1 << 62;
3025 return Res;
3026}
3027word Abc_TtConvertEntry( word Res )
3028{
3029 unsigned First = (unsigned)Res;
3030 unsigned Second = (unsigned)(Res >> 32);
3031 word Fun0, Fun1, Nodes[16] = {0}; int i, k = 5;
3032 for ( i = 0; i < 4; i++ )
3033 Nodes[i+1] = s_Truths6[i];
3034 for ( i = 0; i < 4; i++ )
3035 {
3036 int Lit0, Lit1, Pair = (First >> (i*8)) & 0xFF;
3037 if ( Pair == 0 )
3038 break;
3039 Lit0 = Pair & 0xF;
3040 Lit1 = Pair >> 4;
3041 assert( Lit0 != Lit1 );
3042 Fun0 = (Lit0 & 1) ? ~Nodes[Lit0 >> 1] : Nodes[Lit0 >> 1];
3043 Fun1 = (Lit1 & 1) ? ~Nodes[Lit1 >> 1] : Nodes[Lit1 >> 1];
3044 Nodes[k++] = Lit0 < Lit1 ? Fun0 & Fun1 : Fun0 ^ Fun1;
3045 }
3046 for ( i = 0; i < 3; i++ )
3047 {
3048 int Lit0, Lit1, Pair = (Second >> (i*10)) & 0x3FF;
3049 if ( Pair == 0 )
3050 break;
3051 Lit0 = Pair & 0x1F;
3052 Lit1 = Pair >> 5;
3053 assert( Lit0 != Lit1 );
3054 Fun0 = (Lit0 & 1) ? ~Nodes[Lit0 >> 1] : Nodes[Lit0 >> 1];
3055 Fun1 = (Lit1 & 1) ? ~Nodes[Lit1 >> 1] : Nodes[Lit1 >> 1];
3056 Nodes[k++] = Lit0 < Lit1 ? Fun0 & Fun1 : Fun0 ^ Fun1;
3057 }
3058 return (Res >> 62) ? ~Nodes[k-1] : Nodes[k-1];
3059}
3060word Exa_ManExactSynthesis4VarsOne( int Index, int Truth, int nNodes )
3061{
3062 Mini_Aig_t * pMini = NULL;
3063 int i, m, nMints = 16, fCompl = 0;
3064 Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints );
3065 Vec_Wrd_t * vSimsOut = Vec_WrdStart( nMints );
3066 word pTruth[16] = { Abc_Tt6Stretch((word)Truth, 4) };
3067 if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, 1 ); }
3068 for ( m = 0; m < nMints; m++ )
3069 {
3070 Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, m), Abc_TtGetBit(pTruth, m) );
3071 for ( i = 0; i < 4; i++ )
3072 if ( (m >> i) & 1 )
3073 Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i );
3074 }
3075 assert( Vec_WrdSize(vSimsIn) == 16 );
3076 pMini = Exa5_ManGenTest( vSimsIn, vSimsOut, 4, 5, 1, nNodes, 0, 0, 0, 0, 0, 0 );
3077 if ( pMini && fCompl ) Mini_AigFlipLastPo( pMini );
3078 Vec_WrdFree( vSimsIn );
3079 Vec_WrdFree( vSimsOut );
3080 if ( pMini )
3081 {
3082 /*
3083 FILE * pTable = fopen( "min_xaig4.txt", "a+" );
3084 Mini_AigPrintArray( pTable, pMini );
3085 fprintf( pTable, ", // %d : 0x%04x (%d)\n", Index, Truth, nNodes );
3086 fclose( pTable );
3087 */
3088 word Res = Mini_AigWriteEntry( pMini );
3089 int uTruth = 0xFFFF & (int)Abc_TtConvertEntry( Res );
3090 if ( uTruth == Truth )
3091 printf( "Check ok.\n" );
3092 else
3093 printf( "Check NOT ok!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\n" );
3094 Mini_AigStop( pMini );
3095 return Res;
3096 }
3097 return 0;
3098}
3099void Exa_ManExactSynthesis4Vars()
3100{
3101 int i, k, nFuncs = 1 << 15;
3102 Vec_Wrd_t * vRes = Vec_WrdAlloc( nFuncs );
3103 Vec_WrdPush( vRes, 0 );
3104 for ( i = 1; i < nFuncs; i++ )
3105 {
3106 word Res = 0;
3107 printf( "\nFunction %d:\n", i );
3108 for ( k = 1; k < 8; k++ )
3109 if ( (Res = Exa_ManExactSynthesis4VarsOne( i, i, k )) )
3110 break;
3111 assert( Res );
3112 Vec_WrdPush( vRes, Res );
3113 }
3114 Vec_WrdDumpBin( "minxaig4.data", vRes, 1 );
3115 Vec_WrdFree( vRes );
3116}
3117
3118
3130void Exa6_SortSims( Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut )
3131{
3132 word * pSims = Vec_WrdArray( vSimsDiv );
3133 word * pOuts = Vec_WrdArray( vSimsOut ), temp;
3134 int i, j, best_i, nSize = Vec_WrdSize(vSimsDiv);
3135 assert( Vec_WrdSize(vSimsOut) == nSize );
3136 for ( i = 0; i < nSize-1; i++ )
3137 {
3138 best_i = i;
3139 for ( j = i+1; j < nSize; j++ )
3140 if ( pSims[j] < pSims[best_i] )
3141 best_i = j;
3142 if ( i == best_i )
3143 continue;
3144 temp = pSims[i];
3145 pSims[i] = pSims[best_i];
3146 pSims[best_i] = temp;
3147 temp = pOuts[i];
3148 pOuts[i] = pOuts[best_i];
3149 pOuts[best_i] = temp;
3150 }
3151}
3152
3164int Exa6_ReadFile( char * pFileName, Vec_Wrd_t ** pvSimsDiv, Vec_Wrd_t ** pvSimsOut, int * pnDivs, int * pnOuts )
3165{
3166 int nIns = 0, nDivs = 0, nOuts = 0, nPats = 0, iLine = 0;
3167 int iIns = 0, iDivs = 0, iOuts = 0, Value, i;
3168 char pBuffer[1000];
3169 FILE * pFile = fopen( pFileName, "rb" );
3170 if ( pFile == NULL )
3171 {
3172 Abc_Print( -1, "Cannot open file \"%s\".\n", pFileName );
3173 return 0;
3174 }
3175 while ( fgets( pBuffer, 1000, pFile ) != NULL )
3176 {
3177 if ( pBuffer[0] == 'c' )
3178 break;
3179 if ( iLine++ == 0 )
3180 {
3181 char * pLine = pBuffer;
3182 while ( (*pLine >= 'a' && *pLine <= 'z') || (*pLine >= 'A' && *pLine <= 'Z') )
3183 pLine++;
3184 Value = sscanf( pLine, "%d %d %d %d", &nIns, &nDivs, &nOuts, &nPats );
3185 if ( Value != 4 )
3186 {
3187 Abc_Print( -1, "Cannot read the parameter line in file \"%s\".\n", pFileName );
3188 fclose( pFile );
3189 return 0;
3190 }
3191 if ( nIns + nDivs >= 64 )
3192 {
3193 printf( "The number of variables and divisors should not exceed 64.\n" );
3194 return 0;
3195 }
3196 if ( nOuts > 6 )
3197 {
3198 printf( "The number of outputs should not exceed 6.\n" );
3199 return 0;
3200 }
3201 if ( nPats >= 1000 )
3202 {
3203 printf( "The number of patterns should not exceed 1000.\n" );
3204 return 0;
3205 }
3206 assert( nIns + nDivs < 64 && nOuts <= 6 && (nIns == 0 || nPats <= (1 << nIns)) && nPats < 1000 );
3207 *pvSimsDiv = Vec_WrdStart( nPats );
3208 *pvSimsOut = Vec_WrdStart( nPats );
3209 continue;
3210 }
3211 if ( pBuffer[0] == '\n' || pBuffer[0] == '\r' || pBuffer[0] == ' ' )
3212 continue;
3213 for ( i = 0; i < nPats; i++ )
3214 {
3215 if ( pBuffer[i] == '0' )
3216 continue;
3217 assert( pBuffer[i] == '1' );
3218 if ( iIns < nIns )
3219 Abc_TtSetBit( Vec_WrdEntryP(*pvSimsDiv, nPats-1-i), 1+iIns );
3220 else if ( iDivs < nDivs )
3221 Abc_TtSetBit( Vec_WrdEntryP(*pvSimsDiv, nPats-1-i), 1+nIns+iDivs );
3222 else if ( iOuts < (1 << nOuts) )
3223 Abc_TtSetBit( Vec_WrdEntryP(*pvSimsOut, nPats-1-i), iOuts );
3224 }
3225 assert( pBuffer[nPats] != '0' && pBuffer[nPats] != '1' );
3226 if ( iIns < nIns )
3227 iIns++;
3228 else if ( iDivs < nDivs )
3229 iDivs++;
3230 else if ( iOuts < (1 << nOuts) )
3231 iOuts++;
3232 }
3233 printf( "Finished reading file \"%s\" with %d inputs, %d divisors, %d outputs, and %d patterns.\n", pFileName, nIns, nDivs, nOuts, nPats );
3234 fclose( pFile );
3235 assert( iIns == nIns && iDivs == nDivs && iOuts == (1 << nOuts) );
3236 if ( pnDivs )
3237 *pnDivs = nDivs;
3238 if ( pnOuts )
3239 *pnOuts = nOuts;
3240 return nIns;
3241}
3242void Exa6_WriteFile( char * pFileName, int nVars, word * pTruths, int nTruths )
3243{
3244 int i, o, m, nMintsI = 1 << nVars, nMintsO = 1 << nTruths;
3245 FILE * pFile = fopen( pFileName, "wb" );
3246 fprintf( pFile, "%d %d %d %d\n", nVars, 0, nTruths, nMintsI );
3247 fprintf( pFile, "\n" );
3248 for ( i = 0; i < nVars; i++, fprintf( pFile, "\n" ) )
3249 for ( m = nMintsI - 1; m >= 0; m-- )
3250 fprintf( pFile, "%d", (m >> i) & 1 );
3251 fprintf( pFile, "\n" );
3252 for ( o = 0; o < nMintsO; o++, fprintf( pFile, "\n" ) )
3253 for ( m = nMintsI - 1; m >= 0; m-- )
3254 {
3255 int oMint = 0;
3256 for ( i = 0; i < nTruths; i++ )
3257 if ( Abc_TtGetBit(pTruths+i, m) )
3258 oMint |= (word)1 << i;
3259 fprintf( pFile, "%d", oMint == o );
3260 }
3261 fclose( pFile );
3262}
3263void Exa6_WriteFile2( char * pFileName, int nVars, int nDivs, int nOuts, Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut )
3264{
3265 int i, o, m, nMintsO = 1 << nOuts;
3266 FILE * pFile = fopen( pFileName, "wb" );
3267 assert( Vec_WrdSize(vSimsDiv) == Vec_WrdSize(vSimsOut) );
3268 fprintf( pFile, "%d %d %d %d\n", nVars, nDivs, nOuts, Vec_WrdSize(vSimsOut) );
3269 fprintf( pFile, "\n" );
3270 for ( i = 0; i < nVars+nDivs; i++, fprintf( pFile, "\n%s", (i == nVars && nDivs) ? "\n":"" ) )
3271 for ( m = Vec_WrdSize(vSimsOut) - 1; m >= 0; m-- )
3272 fprintf( pFile, "%d", Abc_TtGetBit(Vec_WrdEntryP(vSimsDiv, m), 1+i) );
3273 fprintf( pFile, "\n" );
3274 for ( o = 0; o < nMintsO; o++, fprintf( pFile, "\n" ) )
3275 for ( m = Vec_WrdSize(vSimsOut) - 1; m >= 0; m-- )
3276 fprintf( pFile, "%d", Abc_TtGetBit(Vec_WrdEntryP(vSimsOut, m), o) );
3277 fclose( pFile );
3278}
3279void Exa6_GenCount( word * pTruths, int nVars )
3280{
3281 int i, k;
3282 assert( nVars >= 3 && nVars <= 7 );
3283 for ( k = 0; k < 3; k++ )
3284 pTruths[k] = 0;
3285 for ( i = 0; i < (1 << nVars); i++ )
3286 {
3287 int n = Abc_TtCountOnes( (word)i );
3288 for ( k = 0; k < 3; k++ )
3289 if ( (n >> k) & 1 )
3290 Abc_TtSetBit( pTruths+k, i );
3291 }
3292}
3293void Exa6_GenProd( word * pTruths, int nVars )
3294{
3295 int i, j, k;
3296 nVars /= 2;
3297 assert( nVars >= 2 && nVars <= 3 );
3298 for ( k = 0; k < 2*nVars; k++ )
3299 pTruths[k] = 0;
3300 for ( i = 0; i < (1 << nVars); i++ )
3301 for ( j = 0; j < (1 << nVars); j++ )
3302 {
3303 int n = i * j;
3304 for ( k = 0; k < 2*nVars; k++ )
3305 if ( (n >> k) & 1 )
3306 Abc_TtSetBit( pTruths+k, (i << nVars) | j );
3307 }
3308}
3309
3321void Exa_ManExactSynthesis6_( Bmc_EsPar_t * pPars, char * pFileName )
3322{
3323 Vec_Wrd_t * vSimsDiv = NULL, * vSimsOut = NULL;
3324 word Entry, Truths[100] = { 0x96, 0xE8 };
3325// int i, nVars = 3, nOuts = 2;
3326// int i, nVars = 6, nOuts = 3;
3327 int i, nVars = 4, nOuts = 4, nDivs2, nOuts2;
3328// Exa6_GenCount( Truths, nVars );
3329 Exa6_GenProd( Truths, nVars );
3330 Exa6_WriteFile( pFileName, nVars, Truths, nOuts );
3331
3332 nVars = Exa6_ReadFile( pFileName, &vSimsDiv, &vSimsOut, &nDivs2, &nOuts2 );
3333
3334 Vec_WrdForEachEntry( vSimsDiv, Entry, i )
3335 Abc_TtPrintBits( &Entry, 1 + nVars );
3336 printf( "\n" );
3337 Vec_WrdForEachEntry( vSimsOut, Entry, i )
3338 Abc_TtPrintBits( &Entry, 1 << nOuts );
3339 printf( "\n" );
3340
3341 Vec_WrdFree( vSimsDiv );
3342 Vec_WrdFree( vSimsOut );
3343}
3344
3345
3346
3347
3359int Gia_ManDupMini_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
3360{
3361 if ( ~pObj->Value )
3362 return pObj->Value;
3363 assert( Gia_ObjIsAnd(pObj) );
3364 Gia_ManDupMini_rec( pNew, p, Gia_ObjFanin0(pObj) );
3365 Gia_ManDupMini_rec( pNew, p, Gia_ObjFanin1(pObj) );
3366 return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3367}
3368Gia_Man_t * Gia_ManDupMini( Gia_Man_t * p, Vec_Int_t * vIns, Vec_Int_t * vDivs, Vec_Int_t * vOuts, Mini_Aig_t * pMini )
3369{
3370 Gia_Man_t * pNew;
3371 Gia_Obj_t * pObj; int i, k;
3372 Vec_Int_t * vCopies = Vec_IntStartFull( Mini_AigNodeNum(pMini) );
3373 //int nPis = Mini_AigPiNum(pMini);
3374 Vec_IntWriteEntry( vCopies, 0, 0 );
3375 assert( Mini_AigPiNum(pMini) == Vec_IntSize(vIns)+Vec_IntSize(vDivs) );
3376 assert( Mini_AigPoNum(pMini) == Vec_IntSize(vOuts) );
3377 Gia_ManFillValue( p );
3378 pNew = Gia_ManStart( Gia_ManObjNum(p) );
3379 pNew->pName = Abc_UtilStrsav( p->pName );
3380 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
3381 Gia_ManConst0(p)->Value = 0;
3382 Gia_ManForEachCi( p, pObj, i )
3383 pObj->Value = Gia_ManAppendCi(pNew);
3384 Gia_ManForEachObjVec( vIns, p, pObj, i )
3385 Vec_IntWriteEntry( vCopies, 1+i, Gia_ManDupMini_rec(pNew, p, pObj) );
3386 Gia_ManForEachObjVec( vDivs, p, pObj, i )
3387 Vec_IntWriteEntry( vCopies, 1+Vec_IntSize(vIns)+i, Gia_ManDupMini_rec(pNew, p, pObj) );
3388 Mini_AigForEachAnd( pMini, k )
3389 {
3390 int iFaninLit0 = Mini_AigNodeFanin0( pMini, k );
3391 int iFaninLit1 = Mini_AigNodeFanin1( pMini, k );
3392 int iLit0 = Vec_IntEntry(vCopies, Mini_AigLit2Var(iFaninLit0)) ^ Mini_AigLitIsCompl(iFaninLit0);
3393 int iLit1 = Vec_IntEntry(vCopies, Mini_AigLit2Var(iFaninLit1)) ^ Mini_AigLitIsCompl(iFaninLit1);
3394 if ( iFaninLit0 < iFaninLit1 )
3395 Vec_IntWriteEntry( vCopies, k, Gia_ManAppendAnd(pNew, iLit0, iLit1) );
3396 else
3397 Vec_IntWriteEntry( vCopies, k, Gia_ManAppendXorReal(pNew, iLit0, iLit1) );
3398 }
3399 i = 0;
3400 Mini_AigForEachPo( pMini, k )
3401 {
3402 int iFaninLit0 = Mini_AigNodeFanin0( pMini, k );
3403 int iLit0 = Vec_IntEntry(vCopies, Mini_AigLit2Var(iFaninLit0)) ^ Mini_AigLitIsCompl(iFaninLit0);
3404 Gia_ManObj( p, Vec_IntEntry(vOuts, i++) )->Value = iLit0;
3405 }
3406 Gia_ManForEachCo( p, pObj, i )
3407 Gia_ManDupMini_rec( pNew, p, Gia_ObjFanin0(pObj) );
3408 Gia_ManForEachCo( p, pObj, i )
3409 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
3410 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
3411 Vec_IntFree( vCopies );
3412 return pNew;
3413}
3414
3415
3416
3417
3418
3419
3420typedef struct Exa6_Man_t_ Exa6_Man_t;
3421struct Exa6_Man_t_
3422{
3423 Vec_Wrd_t * vSimsIn; // input signatures (nWords = 1, nIns <= 64)
3424 Vec_Wrd_t * vSimsOut; // output signatures (nWords = 1, nOuts <= 6)
3425 int fVerbose;
3426 int nIns;
3427 int nDivs; // divisors (const + inputs + tfi + sidedivs)
3428 int nNodes;
3429 int nOuts;
3430 int nObjs;
3431 int VarMarks[MAJ_NOBJS][2][MAJ_NOBJS];
3432 int nCnfVars;
3433 int nCnfVars2;
3434 int nCnfClauses;
3435 FILE * pFile;
3436};
3437
3449int Exa6_ManMarkup( Exa6_Man_t * p )
3450{
3451 int i, k, j, nVars[3] = {1 + 3*p->nNodes, 0, 3*p->nNodes*Vec_WrdSize(p->vSimsIn)};
3452 assert( p->nObjs <= MAJ_NOBJS );
3453 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
3454 for ( k = 0; k < 2; k++ )
3455 for ( j = 1+!k; j < i-k; j++ )
3456 p->VarMarks[i][k][j] = nVars[0] + nVars[1]++;
3457 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
3458 for ( j = 0; j < p->nDivs + p->nNodes; j++ )
3459 p->VarMarks[i][0][j] = nVars[0] + nVars[1]++;
3460 if ( p->fVerbose )
3461 printf( "Variables: Function = %d. Structure = %d. Internal = %d. Total = %d.\n",
3462 nVars[0], nVars[1], nVars[2], nVars[0] + nVars[1] + nVars[2] );
3463 if ( 0 )
3464 {
3465 for ( j = 0; j < 2; j++ )
3466 {
3467 printf( " : " );
3468 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
3469 {
3470 for ( k = 0; k < 2; k++ )
3471 printf( "%3d ", j ? k : i );
3472 printf( " " );
3473 }
3474 printf( " " );
3475 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
3476 {
3477 printf( "%3d ", j ? 0 : i );
3478 printf( " " );
3479 }
3480 printf( "\n" );
3481 }
3482 for ( j = 0; j < 5 + p->nNodes*9 + p->nOuts*5; j++ )
3483 printf( "-" );
3484 printf( "\n" );
3485 for ( j = p->nObjs - 2; j >= 0; j-- )
3486 {
3487 if ( j > 0 && j <= p->nIns )
3488 printf( " %c : ", 'a'+j-1 );
3489 else if ( j > p->nIns && j < p->nDivs )
3490 printf( " %c : ", 'A'+j-1-p->nIns );
3491 else
3492 printf( "%2d : ", j );
3493 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
3494 {
3495 for ( k = 0; k < 2; k++ )
3496 printf( "%3d ", p->VarMarks[i][k][j] );
3497 printf( " " );
3498 }
3499 printf( " " );
3500 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
3501 {
3502 printf( "%3d ", p->VarMarks[i][0][j] );
3503 printf( " " );
3504 }
3505 printf( "\n" );
3506 }
3507 }
3508 return nVars[0] + nVars[1] + nVars[2];
3509}
3510Exa6_Man_t * Exa6_ManAlloc( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int fVerbose )
3511{
3512 Exa6_Man_t * p = ABC_CALLOC( Exa6_Man_t, 1 );
3513 assert( Vec_WrdSize(vSimsIn) == Vec_WrdSize(vSimsOut) );
3514 p->vSimsIn = vSimsIn;
3515 p->vSimsOut = vSimsOut;
3516 p->fVerbose = fVerbose;
3517 p->nIns = nIns;
3518 p->nDivs = nDivs;
3519 p->nNodes = nNodes;
3520 p->nOuts = nOuts;
3521 p->nObjs = p->nDivs + p->nNodes + p->nOuts;
3522 p->nCnfVars = Exa6_ManMarkup( p );
3523 p->nCnfVars2 = 0;
3524 assert( p->nObjs < 64 );
3525 return p;
3526}
3527void Exa6_ManFree( Exa6_Man_t * p )
3528{
3529 ABC_FREE( p );
3530}
3531
3532
3544static inline int Exa6_ManAddClause( Exa6_Man_t * p, int * pLits, int nLits )
3545{
3546 int i, k = 0;
3547 for ( i = 0; i < nLits; i++ )
3548 if ( pLits[i] == 1 )
3549 return 0;
3550 else if ( pLits[i] == 0 )
3551 continue;
3552 else if ( pLits[i] <= 2*(p->nCnfVars + p->nCnfVars2) )
3553 pLits[k++] = pLits[i];
3554 else assert( 0 );
3555 nLits = k;
3556 assert( nLits > 0 );
3557 if ( p->pFile )
3558 {
3559 p->nCnfClauses++;
3560 for ( i = 0; i < nLits; i++ )
3561 fprintf( p->pFile, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) );
3562 fprintf( p->pFile, "0\n" );
3563 }
3564 if ( 0 )
3565 {
3566 for ( i = 0; i < nLits; i++ )
3567 fprintf( stdout, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) );
3568 fprintf( stdout, "\n" );
3569 }
3570 return 1;
3571}
3572static inline int Exa6_ManAddClause4( Exa6_Man_t * p, int Lit0, int Lit1, int Lit2, int Lit3 )
3573{
3574 int pLits[4] = { Lit0, Lit1, Lit2, Lit3 };
3575 return Exa6_ManAddClause( p, pLits, 4 );
3576}
3577int Exa6_ManGenStart( Exa6_Man_t * p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans )
3578{
3579 int pLits[2*MAJ_NOBJS], i, j, k, n, m, nLits;
3580 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
3581 {
3582 int iVarStart = 1 + 3*(i - p->nDivs);//
3583 for ( k = 0; k < 2; k++ )
3584 {
3585 nLits = 0;
3586 for ( j = 0; j < p->nObjs; j++ )
3587 if ( p->VarMarks[i][k][j] )
3588 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
3589 assert( nLits > 0 );
3590 Exa6_ManAddClause( p, pLits, nLits );
3591 for ( n = 0; n < nLits; n++ )
3592 for ( m = n+1; m < nLits; m++ )
3593 Exa6_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
3594 if ( k == 1 )
3595 break;
3596 for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][0][j] )
3597 for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][1][n] )
3598 Exa6_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][j], 1), Abc_Var2Lit(p->VarMarks[i][1][n], 1), 0, 0 );
3599 }
3600 if ( fOrderNodes )
3601 for ( j = p->nDivs; j < i; j++ )
3602 for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
3603 for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
3604 Exa6_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][n], 1), Abc_Var2Lit(p->VarMarks[j][0][m], 1), 0, 0 );
3605 for ( j = p->nDivs; j < i; j++ )
3606 for ( k = 0; k < 2; k++ ) if ( p->VarMarks[i][k][j] )
3607 for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][!k][n] )
3608 for ( m = 0; m < 2; m++ ) if ( p->VarMarks[j][m][n] )
3609 Exa6_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][k][j], 1), Abc_Var2Lit(p->VarMarks[i][!k][n], 1), Abc_Var2Lit(p->VarMarks[j][m][n], 1), 0 );
3610 if ( fFancy )
3611 {
3612 nLits = 0;
3613 for ( k = 0; k < 5-fOnlyAnd; k++ )
3614 pLits[nLits++] = Abc_Var2Lit( iVarStart+k, 0 );
3615 Exa6_ManAddClause( p, pLits, nLits );
3616 for ( n = 0; n < nLits; n++ )
3617 for ( m = n+1; m < nLits; m++ )
3618 Exa6_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
3619 }
3620 else
3621 {
3622 for ( k = 0; k < 3; k++ )
3623 Exa6_ManAddClause4( p, Abc_Var2Lit(iVarStart, k==1), Abc_Var2Lit(iVarStart+1, k==2), Abc_Var2Lit(iVarStart+2, k!=0), 0);
3624 if ( fOnlyAnd )
3625 Exa6_ManAddClause4( p, Abc_Var2Lit(iVarStart, 1), Abc_Var2Lit(iVarStart+1, 1), Abc_Var2Lit(iVarStart+2, 0), 0);
3626 }
3627 }
3628 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
3629 {
3630 nLits = 0;
3631 for ( k = 0; k < 2; k++ )
3632 for ( j = i+1; j < p->nObjs; j++ )
3633 if ( p->VarMarks[j][k][i] )
3634 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[j][k][i], 0 );
3635 //Exa6_ManAddClause( p, pLits, nLits );
3636 if ( fUniqFans )
3637 for ( n = 0; n < nLits; n++ )
3638 for ( m = n+1; m < nLits; m++ )
3639 Exa6_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
3640 }
3641 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
3642 {
3643 nLits = 0;
3644 for ( j = 0; j < p->nDivs + p->nNodes; j++ ) if ( p->VarMarks[i][0][j] )
3645 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][0][j], 0 );
3646 Exa6_ManAddClause( p, pLits, nLits );
3647 for ( n = 0; n < nLits; n++ )
3648 for ( m = n+1; m < nLits; m++ )
3649 Exa6_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
3650 }
3651 return 1;
3652}
3653void Exa6_ManGenMint( Exa6_Man_t * p, int iMint, int fOnlyAnd, int fFancy )
3654{
3655 int iNodeVar = p->nCnfVars + 3*p->nNodes*(iMint - Vec_WrdSize(p->vSimsIn));
3656 int iOutMint = Abc_Tt6FirstBit( Vec_WrdEntry(p->vSimsOut, iMint) );
3657 int fOnlyOne = Abc_TtSuppOnlyOne( (int)Vec_WrdEntry(p->vSimsOut, iMint) );
3658 int i, k, n, j, VarVals[MAJ_NOBJS];
3659 int fAllOnes = Abc_TtCountOnes( Vec_WrdEntry(p->vSimsOut, iMint) ) == (1 << p->nOuts);
3660 if ( fAllOnes )
3661 return;
3662 assert( p->nObjs <= MAJ_NOBJS );
3663 assert( iMint < Vec_WrdSize(p->vSimsIn) );
3664 assert( p->nOuts <= 6 );
3665 for ( i = 0; i < p->nDivs; i++ )
3666 VarVals[i] = (Vec_WrdEntry(p->vSimsIn, iMint) >> i) & 1;
3667 for ( i = 0; i < p->nNodes; i++ )
3668 VarVals[p->nDivs + i] = Abc_Var2Lit(iNodeVar + 3*i + 2, 0);
3669 if ( fOnlyOne )
3670 {
3671 for ( i = 0; i < p->nOuts; i++ )
3672 VarVals[p->nDivs + p->nNodes + i] = (iOutMint >> i) & 1;
3673 }
3674 else
3675 {
3676 word t = Abc_Tt6Stretch( Vec_WrdEntry(p->vSimsOut, iMint), p->nOuts );
3677 int i, c, nCubes = 0, pCover[100], pLits[10];
3678 int iOutVar = p->nCnfVars + p->nCnfVars2; p->nCnfVars2 += p->nOuts;
3679 for ( i = 0; i < p->nOuts; i++ )
3680 VarVals[p->nDivs + p->nNodes + i] = Abc_Var2Lit(iOutVar + i, 0);
3681 assert( t );
3682 if ( ~t )
3683 {
3684 Abc_Tt6IsopCover( ~t, ~t, p->nOuts, pCover, &nCubes );
3685 for ( c = 0; c < nCubes; c++ )
3686 {
3687 int nLits = 0;
3688 for ( i = 0; i < p->nOuts; i++ )
3689 {
3690 int iLit = (pCover[c] >> (2*i)) & 3;
3691 if ( iLit == 1 || iLit == 2 )
3692 pLits[nLits++] = Abc_Var2Lit(iOutVar + i, iLit != 1);
3693 }
3694 Exa6_ManAddClause( p, pLits, nLits );
3695 }
3696 }
3697 }
3698 if ( 0 )
3699 {
3700 printf( "Adding minterm %d: ", iMint );
3701 for ( i = 0; i < p->nObjs; i++ )
3702 printf( " %d=%d", i, VarVals[i] );
3703 printf( "\n" );
3704 }
3705 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
3706 {
3707 int iVarStart = 1 + 3*(i - p->nDivs);//
3708 int iBaseVarI = iNodeVar + 3*(i - p->nDivs);
3709 for ( k = 0; k < 2; k++ )
3710 for ( j = 0; j < i; j++ ) if ( p->VarMarks[i][k][j] )
3711 for ( n = 0; n < 2; n++ )
3712 Exa6_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][k][j], 1), Abc_Var2Lit(iBaseVarI + k, n), Abc_LitNotCond(VarVals[j], !n), 0);
3713 for ( k = 0; k < 4; k++ )
3714 for ( n = 0; n < 2; n++ )
3715 Exa6_ManAddClause4( p, Abc_Var2Lit(iBaseVarI + 0, k&1), Abc_Var2Lit(iBaseVarI + 1, k>>1), Abc_Var2Lit(iBaseVarI + 2, !n), Abc_Var2Lit(k ? iVarStart + k-1 : 0, n));
3716 }
3717 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
3718 {
3719 for ( j = 0; j < p->nDivs + p->nNodes; j++ ) if ( p->VarMarks[i][0][j] )
3720 for ( n = 0; n < 2; n++ )
3721 Exa6_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][j], 1), Abc_LitNotCond(VarVals[j], n), Abc_LitNotCond(VarVals[i], !n), 0);
3722 }
3723}
3724void Exa6_ManGenCnf( Exa6_Man_t * p, char * pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans )
3725{
3726 int m;
3727 assert( p->pFile == NULL );
3728 p->pFile = fopen( pFileName, "wb" );
3729 fputs( "p cnf \n", p->pFile );
3730 Exa6_ManGenStart( p, fOnlyAnd, fFancy, fOrderNodes, fUniqFans );
3731 for ( m = 1; m < Vec_WrdSize(p->vSimsIn); m++ )
3732 Exa6_ManGenMint( p, m, fOnlyAnd, fFancy );
3733 rewind( p->pFile );
3734 fprintf( p->pFile, "p cnf %d %d", p->nCnfVars + p->nCnfVars2, p->nCnfClauses );
3735 fclose( p->pFile );
3736}
3737
3749static inline int Exa6_ManFindFanin( Exa6_Man_t * p, Vec_Int_t * vValues, int i, int k )
3750{
3751 int j, Count = 0, iVar = -1;
3752 for ( j = 0; j < p->nObjs; j++ )
3753 if ( p->VarMarks[i][k][j] && Vec_IntEntry(vValues, p->VarMarks[i][k][j]) )
3754 {
3755 iVar = j;
3756 Count++;
3757 }
3758 assert( Count == 1 );
3759 return iVar;
3760}
3761static inline void Exa6_ManPrintFanin( Exa6_Man_t * p, int iNode, int fComp )
3762{
3763 if ( iNode == 0 )
3764 printf( " %s", fComp ? "const1" : "const0" );
3765 else if ( iNode > 0 && iNode <= p->nIns )
3766 printf( " %s%c", fComp ? "~" : "", 'a'+iNode-1 );
3767 else if ( iNode > p->nIns && iNode < p->nDivs )
3768 printf( " %s%c", fComp ? "~" : "", 'A'+iNode-p->nIns-1 );
3769 else
3770 printf( " %s%d", fComp ? "~" : "", iNode );
3771}
3772void Exa6_ManPrintSolution( Exa6_Man_t * p, Vec_Int_t * vValues, int fFancy )
3773{
3774 int i, k;
3775 printf( "Circuit for %d-var function with %d divisors contains %d two-input gates:\n", p->nIns, p->nDivs, p->nNodes );
3776 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
3777 {
3778 int iVar = Exa6_ManFindFanin( p, vValues, i, 0 );
3779 printf( "%2d = ", i );
3780 Exa6_ManPrintFanin( p, iVar, 0 );
3781 printf( "\n" );
3782 }
3783 for ( i = p->nDivs + p->nNodes - 1; i >= p->nDivs; i-- )
3784 {
3785 int iVarStart = 1 + 3*(i - p->nDivs);//
3786 int Val1 = Vec_IntEntry(vValues, iVarStart);
3787 int Val2 = Vec_IntEntry(vValues, iVarStart+1);
3788 int Val3 = Vec_IntEntry(vValues, iVarStart+2);
3789 printf( "%2d = ", i );
3790 for ( k = 0; k < 2; k++ )
3791 {
3792 int iNode = Exa6_ManFindFanin( p, vValues, i, !k );
3793 int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3;
3794 Exa6_ManPrintFanin( p, iNode, fComp );
3795 if ( k ) break;
3796 printf( " %c", (Val1 && Val2) ? (Val3 ? '|' : '^') : '&' );
3797 }
3798 printf( "\n" );
3799 }
3800}
3801Mini_Aig_t * Exa6_ManMiniAig( Exa6_Man_t * p, Vec_Int_t * vValues, int fFancy )
3802{
3803 int i, k, Compl[MAJ_NOBJS] = {0};
3804 Mini_Aig_t * pMini = Mini_AigStartSupport( p->nDivs-1, p->nObjs );
3805 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
3806 {
3807 int iNodes[2] = {0};
3808 int iVarStart = 1 + 3*(i - p->nDivs);//
3809 int Val1 = Vec_IntEntry(vValues, iVarStart);
3810 int Val2 = Vec_IntEntry(vValues, iVarStart+1);
3811 int Val3 = Vec_IntEntry(vValues, iVarStart+2);
3812 Compl[i] = Val1 && Val2 && Val3;
3813 for ( k = 0; k < 2; k++ )
3814 {
3815 int iNode = Exa6_ManFindFanin( p, vValues, i, !k );
3816 int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3;
3817 iNodes[k] = Abc_Var2Lit(iNode, fComp ^ Compl[iNode]);
3818 }
3819 if ( Val1 && Val2 )
3820 {
3821 if ( Val3 )
3822 Mini_AigOr( pMini, iNodes[0], iNodes[1] );
3823 else
3824 Mini_AigXorSpecial( pMini, iNodes[0], iNodes[1] );
3825 }
3826 else
3827 Mini_AigAnd( pMini, iNodes[0], iNodes[1] );
3828 }
3829 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
3830 {
3831 int iVar = Exa6_ManFindFanin( p, vValues, i, 0 );
3832 Mini_AigCreatePo( pMini, Abc_Var2Lit(iVar, Compl[iVar]) );
3833 }
3834 assert( p->nObjs == Mini_AigNodeNum(pMini) );
3835 return pMini;
3836}
3837
3849Mini_Aig_t * Exa6_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose )
3850{
3851 Mini_Aig_t * pMini = NULL;
3852 abctime clkTotal = Abc_Clock();
3853 Vec_Int_t * vValues = NULL;
3854 int Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFF;
3855 char pFileNameIn[32]; sprintf( pFileNameIn, "_%05x_.cnf", Rand );
3856 char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand );
3857 Exa6_Man_t * p = Exa6_ManAlloc( vSimsIn, vSimsOut, nIns, 1+nIns+nDivs, nOuts, nNodes, fVerbose );
3858 Exa_ManIsNormalized( vSimsIn, vSimsOut );
3859 Exa6_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans );
3860 if ( fVerbose )
3861 printf( "Timeout = %d. OnlyAnd = %d. Fancy = %d. OrderNodes = %d. UniqueFans = %d. Verbose = %d.\n", TimeOut, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fVerbose );
3862 if ( fVerbose )
3863 printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", p->nCnfVars, p->nCnfClauses, pFileNameIn );
3864 vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, TimeOut, fVerbose );
3865 if ( vValues ) pMini = Exa6_ManMiniAig( p, vValues, fFancy );
3866 //if ( vValues ) Exa6_ManPrintSolution( p, vValues, fFancy );
3867 if ( vValues ) Exa_ManMiniPrint( pMini, p->nIns );
3868 if ( vValues && nIns <= 6 ) Exa_ManMiniVerify( pMini, vSimsIn, vSimsOut );
3869 Vec_IntFreeP( &vValues );
3870 Exa6_ManFree( p );
3871 unlink( pFileNameIn );
3872 Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
3873 return pMini;
3874}
3875Mini_Aig_t * Mini_AigDupCompl( Mini_Aig_t * p, int ComplIns, int ComplOuts )
3876{
3877 Mini_Aig_t * pNew = Mini_AigStartSupport( Mini_AigPiNum(p), Mini_AigNodeNum(p) );
3878 Vec_Int_t * vCopies = Vec_IntStartFull( Mini_AigNodeNum(p) ); int k, i = 0, o = 0;
3879 Vec_IntWriteEntry( vCopies, 0, 0 );
3880 Mini_AigForEachPi( p, k )
3881 Vec_IntWriteEntry( vCopies, k, Abc_Var2Lit(k, (ComplIns>>i++) & 1) );
3882 Mini_AigForEachAnd( p, k )
3883 {
3884 int iFaninLit0 = Mini_AigNodeFanin0( p, k );
3885 int iFaninLit1 = Mini_AigNodeFanin1( p, k );
3886 int iLit0 = Vec_IntEntry(vCopies, Mini_AigLit2Var(iFaninLit0)) ^ Mini_AigLitIsCompl(iFaninLit0);
3887 int iLit1 = Vec_IntEntry(vCopies, Mini_AigLit2Var(iFaninLit1)) ^ Mini_AigLitIsCompl(iFaninLit1);
3888 if ( iFaninLit0 < iFaninLit1 )
3889 Vec_IntWriteEntry( vCopies, k, Mini_AigAnd(pNew, iLit0, iLit1) );
3890 else
3891 Vec_IntWriteEntry( vCopies, k, Mini_AigXorSpecial(pNew, iLit0, iLit1) );
3892 }
3893 Mini_AigForEachPo( p, k )
3894 {
3895 int iFaninLit0 = Mini_AigNodeFanin0( p, k );
3896 int iLit0 = Vec_IntEntry(vCopies, Mini_AigLit2Var(iFaninLit0)) ^ Mini_AigLitIsCompl(iFaninLit0);
3897 Mini_AigCreatePo( pNew, iLit0 ^ ((ComplOuts >> o++) & 1) );
3898 }
3899 Vec_IntFree( vCopies );
3900 return pNew;
3901}
3902word Exa6_ManPolarMinterm( word Mint, int nOuts, int Polar )
3903{
3904 word MintNew = 0;
3905 int m, nMints = 1 << nOuts;
3906 for ( m = 0; m < nMints; m++ )
3907 if ( (Mint >> m) & 1 )
3908 MintNew |= (word)1 << (m ^ Polar);
3909 return MintNew;
3910}
3911int Exa6_ManFindPolar( word First, int nOuts )
3912{
3913 int i;
3914 for ( i = 0; i < (1 << nOuts); i++ )
3915 if ( Exa6_ManPolarMinterm(First, nOuts, i) & 1 )
3916 return i;
3917 return -1;
3918}
3919Vec_Wrd_t * Exa6_ManTransformOutputs( Vec_Wrd_t * vOuts, int nOuts )
3920{
3921 Vec_Wrd_t * vRes = Vec_WrdAlloc( Vec_WrdSize(vOuts) );
3922 int i, Polar = Exa6_ManFindPolar( Vec_WrdEntry(vOuts, 0), nOuts ); word Entry;
3923 Vec_WrdForEachEntry( vOuts, Entry, i )
3924 Vec_WrdPush( vRes, Exa6_ManPolarMinterm(Entry, nOuts, Polar) );
3925 return vRes;
3926}
3927Vec_Wrd_t * Exa6_ManTransformInputs( Vec_Wrd_t * vIns )
3928{
3929 Vec_Wrd_t * vRes = Vec_WrdAlloc( Vec_WrdSize(vIns) );
3930 int i; word Entry, Polar = Vec_WrdEntry( vIns, 0 );
3931 Vec_WrdForEachEntry( vIns, Entry, i )
3932 Vec_WrdPush( vRes, Entry ^ Polar );
3933 return vRes;
3934}
3935void Exa_ManExactPrint( Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut, int nDivs, int nOuts )
3936{
3937 word Entry; int i;
3938 Vec_WrdForEachEntry( vSimsDiv, Entry, i )
3939 Abc_TtPrintBits( &Entry, nDivs );
3940 printf( "\n" );
3941 Vec_WrdForEachEntry( vSimsOut, Entry, i )
3942 Abc_TtPrintBits( &Entry, 1 << nOuts );
3943 printf( "\n" );
3944}
3945Mini_Aig_t * Exa_ManExactSynthesis6Int( Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut, int nVars, int nDivs, int nOuts, int nNodes, int fOnlyAnd, int fVerbose, char * pFileName )
3946{
3947 Mini_Aig_t * pTemp, * pMini;
3948 Vec_Wrd_t * vSimsDiv2, * vSimsOut2;
3949 int DivCompl, OutCompl;
3950 if ( nVars == 0 ) return NULL;
3951 assert( nVars <= 8 );
3952 DivCompl = (int)Vec_WrdEntry(vSimsDiv, 0) >> 1;
3953 OutCompl = Exa6_ManFindPolar( Vec_WrdEntry(vSimsOut, 0), nOuts );
3954 if ( fVerbose )
3955 printf( "Inputs = %d. Divisors = %d. Outputs = %d. Nodes = %d. InP = %d. OutP = %d.\n",
3956 nVars, nDivs, nOuts, nNodes, DivCompl, OutCompl );
3957 vSimsDiv2 = Exa6_ManTransformInputs( vSimsDiv );
3958 vSimsOut2 = Exa6_ManTransformOutputs( vSimsOut, nOuts );
3959 pMini = Exa6_ManGenTest( vSimsDiv2, vSimsOut2, nVars, nDivs, nOuts, nNodes, 0, fOnlyAnd, 0, 0, 0, fVerbose );
3960 if ( pMini )
3961 {
3962 if ( DivCompl || OutCompl )
3963 {
3964 pMini = Mini_AigDupCompl( pTemp = pMini, DivCompl, OutCompl );
3965 Mini_AigStop( pTemp );
3966 }
3967 Mini_AigerWrite( pFileName ? Extra_FileNameGenericAppend(pFileName, "_twoexact.aig") : (char *)"exa6.aig", pMini, 1 );
3968 //if ( nVars <= 6 )
3969 // Exa_ManMiniVerify( pMini, vSimsDiv, vSimsOut );
3970 //printf( "\n" );
3971 //Mini_AigStop( pMini );
3972 }
3973 Vec_WrdFreeP( &vSimsDiv2 );
3974 Vec_WrdFreeP( &vSimsOut2 );
3975 return pMini;
3976}
3977void Exa_ManExactSynthesis6( Bmc_EsPar_t * pPars, char * pFileName )
3978{
3979 Mini_Aig_t * pMini = NULL;
3980 Vec_Wrd_t * vSimsDiv = NULL, * vSimsOut = NULL;
3981 int i, k, nDivs, nOuts, nVars = 0;
3982 if ( !strcmp(pFileName + strlen(pFileName) - 3, "rel") )
3983 nVars = Exa6_ReadFile( pFileName, &vSimsDiv, &vSimsOut, &nDivs, &nOuts );
3984 else if ( !strcmp(pFileName + strlen(pFileName) - 3, "pla") ) {
3985 Abc_RData_t * p = Abc_ReadPla( pFileName );
3986 Abc_RData_t * p2 = p ? Abc_RData2Rel( p ) : NULL;
3987 if ( !p || !p2 ) return;
3988 nDivs = 0;
3989 nOuts = p->nOuts;
3990 nVars = p->nIns;
3991 vSimsDiv = Vec_WrdStart( p2->nPats );
3992 for ( k = 0; k < p->nIns; k++ )
3993 for ( i = 0; i < p2->nPats; i++ )
3994 if ( Abc_RDataGetIn(p2, k, i) )
3995 Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(vSimsDiv, i), 1+k);
3996 vSimsOut = Vec_WrdStart( p2->nPats );
3997 for ( k = 0; k < (1 << p->nOuts); k++ )
3998 for ( i = 0; i < p2->nPats; i++ )
3999 if ( Abc_RDataGetOut(p2, k, i) )
4000 Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(vSimsOut, i), k);
4001 Abc_RDataStop( p );
4002 Abc_RDataStop( p2 );
4003 }
4004 else
4005 printf( "Unknown file extension in file \"%s\".\n", pFileName );
4006 if ( nVars == 0 )
4007 return;
4008 //Vec_WrdPrintBin( vSimsDiv, 1 );
4009 //Vec_WrdPrintBin( vSimsOut, 1 );
4010 Exa6_SortSims( vSimsDiv, vSimsOut );
4011 pMini = Exa_ManExactSynthesis6Int( vSimsDiv, vSimsOut, nVars, nDivs, nOuts, pPars->nNodes, pPars->fOnlyAnd, pPars->fVerbose, pFileName );
4012 Vec_WrdFreeP( &vSimsDiv );
4013 Vec_WrdFreeP( &vSimsOut );
4014 if ( pMini ) Mini_AigStop( pMini );
4015}
4016
4028static inline int Exa7_AddClause( FILE * pFile, int * pLits, int nLits )
4029{
4030 int i, k = 0;
4031 for ( i = 0; i < nLits; i++ ) {
4032 if ( pLits[i] == 1 )
4033 return 0;
4034 else if ( pLits[i] == 0 )
4035 continue;
4036 else
4037 pLits[k++] = pLits[i];
4038 }
4039 nLits = k;
4040 assert( nLits > 0 );
4041 if ( pFile )
4042 {
4043 for ( i = 0; i < nLits; i++ )
4044 fprintf( pFile, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) );
4045 fprintf( pFile, "0\n" );
4046 }
4047 if ( 0 )
4048 {
4049 for ( i = 0; i < nLits; i++ )
4050 fprintf( stdout, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i])-1 );
4051 fprintf( stdout, "\n" );
4052 }
4053 return 1;
4054}
4055static inline int Exa7_AddClause4( FILE * pFile, int Lit0, int Lit1, int Lit2, int Lit3 )
4056{
4057 int pLits[4] = { Lit0, Lit1, Lit2, Lit3 };
4058 return Exa7_AddClause( pFile, pLits, 4 );
4059}
4060int Exa7_GetVar( int n, int i, int j, int m )
4061{
4062 return 1 + n*n*m + n*i + j;
4063}
4064int Exa7_ManGenCnf( char * pFileName, word * pTruth, int nVars, int nNodes, int GateSize )
4065{
4066 int m, n, v, k, nV = nVars + nNodes, nMints = 1 << nVars, nClas = 0;
4067 int pVars[32] = {0}; assert( nVars + nNodes + 1 < 32 );
4068 FILE * pFile = fopen( pFileName, "wb" );
4069 fputs( "p cnf \n", pFile );
4070 for ( m = 0; m < nMints; m++ )
4071 {
4072 for ( v = 0; v < nVars; v++ )
4073 nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(Exa7_GetVar(nV, v, v, m), ((m >> v)&1)==0), 0, 0, 0 );
4074 nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(Exa7_GetVar(nV, nV-1, nV-1, m), ((pTruth[0] >> m)&1)==0), 0, 0, 0 );
4075 for ( n = nVars; n < nV; n++ )
4076 {
4077 int iValNode = Exa7_GetVar(nV, n, n, m);
4078 for ( v = 0; v < n; v++ )
4079 {
4080 int iParVar = Exa7_GetVar(nV, v, n, 0); // v < n
4081 int iFanVar = Exa7_GetVar(nV, n, v, m);
4082 int iValFan = Exa7_GetVar(nV, v, v, m);
4083 // iFanVar = ~iParVar | iValFan
4084 nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iFanVar, 1), Abc_Var2Lit(iParVar, 1), Abc_Var2Lit(iValFan, 0), 0 );
4085 nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iFanVar, 0), Abc_Var2Lit(iParVar, 0), 0, 0 );
4086 nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iFanVar, 0), Abc_Var2Lit(iValFan, 1), 0, 0 );
4087 // iParVar & ~iValFan => iValNode
4088 nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iParVar, 1), Abc_Var2Lit(iValFan, 0), Abc_Var2Lit(iValNode, 0), 0 );
4089 pVars[v] = Abc_Var2Lit(iFanVar, 1);
4090 }
4091 pVars[v] = Abc_Var2Lit(iValNode, 1);
4092 // (iFanVar0 & iFanVar1 & iFanVar2) => ~iValNode
4093 nClas += Exa7_AddClause( pFile, pVars, n+1 );
4094 }
4095 }
4096 for ( n = nVars; n < nV; n++ ) {
4097 for ( v = 0; v < n; v++ )
4098 pVars[v] = Abc_Var2Lit(Exa7_GetVar(nV, v, n, 0), 0); // v < n
4099 nClas += Exa7_AddClause( pFile, pVars, n );
4100 if ( GateSize ) {
4101 int Total = 1 << n, Limit = GateSize + 1;
4102 for ( m = 0; m < Total; m++ )
4103 {
4104 if ( Abc_TtCountOnes((word)m) != Limit )
4105 continue;
4106 for ( k = v = 0; v < n; v++ )
4107 if ( (m >> v) & 1 )
4108 pVars[k++] = Abc_Var2Lit(Exa7_GetVar(nV, v, n, 0), 1);
4109 assert( k == Limit );
4110 nClas += Exa7_AddClause( pFile, pVars, Limit );
4111 }
4112 }
4113 }
4114 rewind( pFile );
4115 fprintf( pFile, "p cnf %d %d", nMints * nV * nV, nClas );
4116 fclose( pFile );
4117 return nClas;
4118}
4119void Exa_ManDumpVerilog( Vec_Int_t * vValues, int nVars, int nNodes, int GateSize, word * pTruth )
4120{
4121 FILE * pFile;
4122 char Buffer[1000];
4123 char FileName[1100];
4124 int v, n, k, nV = nVars+nNodes;
4125 Extra_PrintHexadecimalString( Buffer, (unsigned *)pTruth, nVars );
4126 sprintf( FileName, "func%s_%d_%d.v", Buffer, GateSize, nNodes );
4127 pFile = fopen( FileName, "wb" );
4128 fprintf( pFile, "// Realization of the %d-input function %s using %d NAND gates:\n", nVars, Buffer, nNodes );
4129 fprintf( pFile, "module func%s_%d_%d ( input", Buffer, GateSize, nNodes );
4130 for ( v = 0; v < nVars; v++ )
4131 fprintf( pFile, " %c,", 'a'+v );
4132 fprintf( pFile, " output out );\n" );
4133 for ( n = nVars; n < nV; n++ ) {
4134 int nFans = 0;
4135 for ( v = 0; v < n; v++ )
4136 nFans += Vec_IntEntry(vValues, Exa7_GetVar(nV, v, n, 0));
4137 fprintf( pFile, " wire %c = ~(", 'a'+n );
4138 for ( k = v = 0; v < n; v++ )
4139 if ( Vec_IntEntry(vValues, Exa7_GetVar(nV, v, n, 0)) )
4140 fprintf( pFile, "%c%s", 'a'+v, ++k < nFans ? " & ":"" );
4141 fprintf( pFile, ");\n" );
4142 }
4143 fprintf( pFile, " assign out = %c;\n", 'a'+nV-1 );
4144 fprintf( pFile, "endmodule\n\n" );
4145 fclose( pFile );
4146 printf( "Solution was dumped into file \"%s\".\n", FileName );
4147}
4148void Exa_ManExactSynthesis7( Bmc_EsPar_t * pPars, int GateSize )
4149{
4150 abctime clkTotal = Abc_Clock();
4151 int v, n, nMints = 1 << pPars->nVars;
4152 int nV = pPars->nVars + pPars->nNodes;
4153 word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr );
4154 Vec_Int_t * vValues = NULL;
4155 int Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFF;
4156 char pFileNameIn[32]; sprintf( pFileNameIn, "_%05x_.cnf", Rand );
4157 char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand );
4158 int nClas = Exa7_ManGenCnf( pFileNameIn, pTruth, pPars->nVars, pPars->nNodes, GateSize );
4159 if ( pPars->fVerbose )
4160 printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", nMints * nV * nV, nClas, pFileNameIn );
4161 vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, pPars->RuntimeLim, pPars->fVerbose );
4162 if ( pPars->fVerbose && vValues ) {
4163 printf( " " );
4164 for ( n = 0; n < nV; n++ )
4165 printf( "%2d ", n );
4166 printf( "\n" );
4167 for ( n = pPars->nVars; n < nV; n++, printf("\n") ) {
4168 printf( "%2d : ", n );
4169 for ( v = 0; v < n; v++ )
4170 printf( " %c ", Vec_IntEntry(vValues, Exa7_GetVar(nV, v, n, 0)) ? '1':'.' ); // v < n
4171 }
4172 }
4173 if ( vValues )
4174 Exa_ManDumpVerilog( vValues, pPars->nVars, pPars->nNodes, GateSize, pTruth );
4175 Vec_IntFreeP( &vValues );
4176 unlink( pFileNameIn );
4177 Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
4178}
4179
4191void Exa_NpnCascadeTest()
4192{
4193 char Buffer[100];
4194 char Command[1000]; int i;
4195 FILE * pFile = fopen( "npn3.txt", "r" );
4196 for ( i = 0; i < 14; i++ )
4197// FILE * pFile = fopen( "npn4.txt", "r" );
4198// for ( i = 0; i < 222; i++ )
4199// FILE * pFile = fopen( "npn5.txt", "r" );
4200// for ( i = 0; i < 616126; i++ )
4201 {
4202 int Value = fscanf( pFile, "%s", Buffer );
4203 assert( Value == 1 );
4204 if ( i == 0 ) continue;
4205 if ( Buffer[strlen(Buffer)-1] == '\n' )
4206 Buffer[strlen(Buffer)-1] = '\0';
4207 if ( Buffer[strlen(Buffer)-1] == '\r' )
4208 Buffer[strlen(Buffer)-1] = '\0';
4209 sprintf( Command, "lutexact -I 3 -N 2 -K 2 -gvc %s", Buffer+2 );
4210 printf( "\nNPN class %6d : Command \"%s\":\n", i, Command );
4211 if ( Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ) )
4212 {
4213 fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
4214 return;
4215 }
4216 }
4217 fclose( pFile );
4218}
4219void Exa_NpnCascadeTest6()
4220{
4221 char Command[1000]; int i;
4222 Abc_Random(1);
4223 for ( i = 0; i < 10000; i++ )
4224 {
4225 word Truth = Abc_RandomW(0);
4226 sprintf( Command, "lutexact -I 6 -N 2 -K 5 -gvc %016lx", Truth );
4227 printf( "\nIter %4d : Command \"%s\":\n", i, Command );
4228 if ( Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ) )
4229 {
4230 fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
4231 return;
4232 }
4233 }
4234}
4235
4239
4240ABC_NAMESPACE_IMPL_END
4241
bmcg_sat_solver_conflictnum
int bmcg_sat_solver_conflictnum(bmcg_sat_solver *s)
Definition AbcGlucose.cpp:257
bmcg_sat_solver_set_runtime_limit
abctime bmcg_sat_solver_set_runtime_limit(bmcg_sat_solver *s, abctime Limit)
Definition AbcGlucose.cpp:230
bmcg_sat_solver_varnum
int bmcg_sat_solver_varnum(bmcg_sat_solver *s)
Definition AbcGlucose.cpp:245
bmcg_sat_solver_start
bmcg_sat_solver * bmcg_sat_solver_start()
MACRO DEFINITIONS ///.
Definition AbcGlucose.cpp:146
bmcg_sat_solver_solve
int bmcg_sat_solver_solve(bmcg_sat_solver *s, int *plits, int nlits)
Definition AbcGlucose.cpp:170
bmcg_sat_solver_addclause
int bmcg_sat_solver_addclause(bmcg_sat_solver *s, int *plits, int nlits)
Definition AbcGlucose.cpp:160
bmcg_sat_solver_read_cex_varvalue
int bmcg_sat_solver_read_cex_varvalue(bmcg_sat_solver *s, int ivar)
Definition AbcGlucose.cpp:220
bmcg_sat_solver_set_nvars
void bmcg_sat_solver_set_nvars(bmcg_sat_solver *s, int nvars)
Definition AbcGlucose.cpp:186
bmcg_sat_solver_clausenum
int bmcg_sat_solver_clausenum(bmcg_sat_solver *s)
Definition AbcGlucose.cpp:249
bmcg_sat_solver_stop
void bmcg_sat_solver_stop(bmcg_sat_solver *s)
Definition AbcGlucose.cpp:150
GLUCOSE_UNDEC
#define GLUCOSE_UNDEC
Definition AbcGlucose.h:36
GLUCOSE_UNSAT
#define GLUCOSE_UNSAT
INCLUDES ///.
Definition AbcGlucose.h:34
bmcg_sat_solver
void bmcg_sat_solver
Definition AbcGlucose.h:63
GLUCOSE_SAT
#define GLUCOSE_SAT
Definition AbcGlucose.h:35
nWords
int nWords
Definition abcNpn.c:127
Abc_RandomW
word Abc_RandomW(int fReset)
Definition utilSort.c:1022
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
Abc_Random
unsigned Abc_Random(int fReset)
Definition utilSort.c:1004
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Abc_FrameGetGlobalFrame
ABC_DLL Abc_Frame_t * Abc_FrameGetGlobalFrame()
Definition mainFrame.c:643
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
MAJ_NOBJS
#define MAJ_NOBJS
DECLARATIONS ///.
Definition bmcMaj2.c:33
Maj_ManValue
int Maj_ManValue(int iMint, int nVars)
FUNCTION DEFINITIONS ///.
Definition bmcMaj.c:80
Exa3_ManPrint
void Exa3_ManPrint(Exa3_Man_t *p, int i, int iMint, abctime clk)
Definition bmcMaj.c:1589
Exa4_ManMarkup
int Exa4_ManMarkup(Exa4_Man_t *p)
Definition bmcMaj.c:1917
Exa4_ManSolve
Vec_Int_t * Exa4_ManSolve(char *pFileNameIn, char *pFileNameOut, int TimeOut, int fVerbose)
Definition bmcMaj.c:1850
Exa5_ManMarkup
int Exa5_ManMarkup(Exa5_Man_t *p)
Definition bmcMaj.c:2505
Maj_ManFree
void Maj_ManFree(Maj_Man_t *p)
Definition bmcMaj.c:164
Abc_TtConvertEntry
word Abc_TtConvertEntry(word Res)
Definition bmcMaj.c:3027
Exa4_ManGenMint
void Exa4_ManGenMint(Exa4_Man_t *p, int iMint, int fOnlyAnd, int fFancy)
Definition bmcMaj.c:2142
Exa4_ManMiniAig
Mini_Aig_t * Exa4_ManMiniAig(Exa4_Man_t *p, Vec_Int_t *vValues, int fFancy)
Definition bmcMaj.c:2320
Exa6_ManMiniAig
Mini_Aig_t * Exa6_ManMiniAig(Exa6_Man_t *p, Vec_Int_t *vValues, int fFancy)
Definition bmcMaj.c:3801
Exa_ManTruthTables
Vec_Wrd_t * Exa_ManTruthTables(Exa_Man_t *p)
Definition bmcMaj.c:454
Exa6_GenCount
void Exa6_GenCount(word *pTruths, int nVars)
Definition bmcMaj.c:3279
Exa_ManDumpBlif
void Exa_ManDumpBlif(Exa_Man_t *p, int fCompl)
Definition bmcMaj.c:606
Exa_ManExactSynthesis7
void Exa_ManExactSynthesis7(Bmc_EsPar_t *pPars, int GateSize)
Definition bmcMaj.c:4148
Exa3_CountInputVars
Vec_Int_t * Exa3_CountInputVars(int nVars, Vec_Wec_t *p)
Definition bmcMaj.c:1068
Mini_AigWriteEntry
word Mini_AigWriteEntry(Mini_Aig_t *p)
Definition bmcMaj.c:3000
Exa6_ManTransformInputs
Vec_Wrd_t * Exa6_ManTransformInputs(Vec_Wrd_t *vIns)
Definition bmcMaj.c:3927
Maj_Man_t
struct Maj_Man_t_ Maj_Man_t
Definition bmcMaj.c:46
Exa6_ManFindPolar
int Exa6_ManFindPolar(word First, int nOuts)
Definition bmcMaj.c:3911
Exa6_ManPolarMinterm
word Exa6_ManPolarMinterm(word Mint, int nOuts, int Polar)
Definition bmcMaj.c:3902
Exa7_ManGenCnf
int Exa7_ManGenCnf(char *pFileName, word *pTruth, int nVars, int nNodes, int GateSize)
Definition bmcMaj.c:4064
Exa_ManExactPrint
void Exa_ManExactPrint(Vec_Wrd_t *vSimsDiv, Vec_Wrd_t *vSimsOut, int nDivs, int nOuts)
Definition bmcMaj.c:3935
Exa_ManExactSynthesis6_
void Exa_ManExactSynthesis6_(Bmc_EsPar_t *pPars, char *pFileName)
Definition bmcMaj.c:3321
Exa4_Man_t
struct Exa4_Man_t_ Exa4_Man_t
Definition bmcMaj.c:1889
Exa4_ManPrintSolution
void Exa4_ManPrintSolution(Exa4_Man_t *p, Vec_Int_t *vValues, int fFancy)
Definition bmcMaj.c:2271
Exa_ManExactSynthesis4_
void Exa_ManExactSynthesis4_(Bmc_EsPar_t *pPars)
Definition bmcMaj.c:2426
Exa_ManExactSynthesis6Int
Mini_Aig_t * Exa_ManExactSynthesis6Int(Vec_Wrd_t *vSimsDiv, Vec_Wrd_t *vSimsOut, int nVars, int nDivs, int nOuts, int nNodes, int fOnlyAnd, int fVerbose, char *pFileName)
Definition bmcMaj.c:3945
Exa5_ManAlloc
Exa5_Man_t * Exa5_ManAlloc(Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int fVerbose)
Definition bmcMaj.c:2568
Exa6_ManGenCnf
void Exa6_ManGenCnf(Exa6_Man_t *p, char *pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans)
Definition bmcMaj.c:3724
Exa6_ManPrintSolution
void Exa6_ManPrintSolution(Exa6_Man_t *p, Vec_Int_t *vValues, int fFancy)
Definition bmcMaj.c:3772
Exa4_ManGenCnf
void Exa4_ManGenCnf(Exa4_Man_t *p, char *pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard, char *pGuide)
Definition bmcMaj.c:2221
Exa6_ReadFile
int Exa6_ReadFile(char *pFileName, Vec_Wrd_t **pvSimsDiv, Vec_Wrd_t **pvSimsOut, int *pnDivs, int *pnOuts)
Definition bmcMaj.c:3164
Exa5_Man_t
struct Exa5_Man_t_ Exa5_Man_t
Definition bmcMaj.c:2475
Exa4_ManParse
Vec_Int_t * Exa4_ManParse(char *pFileName)
DECLARATIONS ///.
Definition bmcMaj.c:1812
Exa6_ManGenTest
Mini_Aig_t * Exa6_ManGenTest(Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose)
Definition bmcMaj.c:3849
Exa_NpnCascadeTest6
void Exa_NpnCascadeTest6()
Definition bmcMaj.c:4219
Exa_ManSolverSolve
int Exa_ManSolverSolve(Exa_Man_t *p)
Definition bmcMaj.c:749
Exa5_ManGenStart
int Exa5_ManGenStart(Exa5_Man_t *p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans)
Definition bmcMaj.c:2654
Exa4_ManGenTest
Mini_Aig_t * Exa4_ManGenTest(Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard, char *pGuide)
Definition bmcMaj.c:2395
Exa5_ManGenMint
void Exa5_ManGenMint(Exa5_Man_t *p, int iMint, int fOnlyAnd, int fFancy)
Definition bmcMaj.c:2729
Exa6_WriteFile
void Exa6_WriteFile(char *pFileName, int nVars, word *pTruths, int nTruths)
Definition bmcMaj.c:3242
Exa_ManMiniVerify
void Exa_ManMiniVerify(Mini_Aig_t *p, Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut)
Definition bmcMaj.c:1758
Exa3_ManExactSynthesisRand
void Exa3_ManExactSynthesisRand(Bmc_EsPar_t *pPars)
Definition bmcMaj.c:1655
Maj_ManTruthTables
Vec_Wrd_t * Maj_ManTruthTables(Maj_Man_t *p)
Definition bmcMaj.c:87
Exa_ManMarkup
int Exa_ManMarkup(Exa_Man_t *p)
Definition bmcMaj.c:462
Exa4_ManFree
void Exa4_ManFree(Exa4_Man_t *p)
Definition bmcMaj.c:1991
Mini_AigPrintArray
void Mini_AigPrintArray(FILE *pFile, Mini_Aig_t *p)
Definition bmcMaj.c:2988
Exa5_ManPrintSolution
void Exa5_ManPrintSolution(Exa5_Man_t *p, Vec_Int_t *vValues, int fFancy)
Definition bmcMaj.c:2815
Exa6_ManAlloc
Exa6_Man_t * Exa6_ManAlloc(Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int fVerbose)
Definition bmcMaj.c:3510
Exa3_Man_t
struct Exa3_Man_t_ Exa3_Man_t
Definition bmcMaj.c:994
Exa5_ManFree
void Exa5_ManFree(Exa5_Man_t *p)
Definition bmcMaj.c:2584
Exa5_ManGenCnf
void Exa5_ManGenCnf(Exa5_Man_t *p, char *pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans)
Definition bmcMaj.c:2767
Exa4_ManAlloc
Exa4_Man_t * Exa4_ManAlloc(Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int fVerbose)
Definition bmcMaj.c:1976
Exa_ManExactSynthesis6
void Exa_ManExactSynthesis6(Bmc_EsPar_t *pPars, char *pFileName)
Definition bmcMaj.c:3977
Exa6_SortSims
void Exa6_SortSims(Vec_Wrd_t *vSimsDiv, Vec_Wrd_t *vSimsOut)
Definition bmcMaj.c:3130
Exa6_ManGenStart
int Exa6_ManGenStart(Exa6_Man_t *p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans)
Definition bmcMaj.c:3577
Exa_ManAddCnfAdd
int Exa_ManAddCnfAdd(Exa_Man_t *p, int *pnAdded)
Definition bmcMaj.c:710
Exa6_GenProd
void Exa6_GenProd(word *pTruths, int nVars)
Definition bmcMaj.c:3293
Exa_Man_t
struct Exa_Man_t_ Exa_Man_t
Definition bmcMaj.c:421
Exa5_ManMiniAig
Mini_Aig_t * Exa5_ManMiniAig(Exa5_Man_t *p, Vec_Int_t *vValues)
Definition bmcMaj.c:2860
Exa5_ManGenTest
Mini_Aig_t * Exa5_ManGenTest(Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose)
Definition bmcMaj.c:2926
Exa_ManAlloc
Exa_Man_t * Exa_ManAlloc(Bmc_EsPar_t *pPars, word *pTruth)
Definition bmcMaj.c:502
Exa6_ManTransformOutputs
Vec_Wrd_t * Exa6_ManTransformOutputs(Vec_Wrd_t *vOuts, int nOuts)
Definition bmcMaj.c:3919
Maj_ManAddCnf
int Maj_ManAddCnf(Maj_Man_t *p, int iMint)
Definition bmcMaj.c:325
Exa_ManPrintSolution
void Exa_ManPrintSolution(Exa_Man_t *p, int fCompl)
Definition bmcMaj.c:659
Exa_ManAddCnf
int Exa_ManAddCnf(Exa_Man_t *p, int iMint)
Definition bmcMaj.c:885
Exa_ManIsNormalized
void Exa_ManIsNormalized(Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut)
Definition bmcMaj.c:1702
Exa_ManFree
void Exa_ManFree(Exa_Man_t *p)
Definition bmcMaj.c:527
Exa_ManExactSynthesis
void Exa_ManExactSynthesis(Bmc_EsPar_t *pPars)
Definition bmcMaj.c:940
Exa6_Man_t
struct Exa6_Man_t_ Exa6_Man_t
Definition bmcMaj.c:3420
Mini_AigDupCompl
Mini_Aig_t * Mini_AigDupCompl(Mini_Aig_t *p, int ComplIns, int ComplOuts)
Definition bmcMaj.c:3875
Exa6_WriteFile2
void Exa6_WriteFile2(char *pFileName, int nVars, int nDivs, int nOuts, Vec_Wrd_t *vSimsDiv, Vec_Wrd_t *vSimsOut)
Definition bmcMaj.c:3263
Exa_NpnCascadeTest
void Exa_NpnCascadeTest()
Definition bmcMaj.c:4191
Exa3_ChooseInputVars
Vec_Wec_t * Exa3_ChooseInputVars(int nVars, int nLuts, int nLutSize)
Definition bmcMaj.c:1077
Exa3_ChooseInputVars_int
Vec_Wec_t * Exa3_ChooseInputVars_int(int nVars, int nLuts, int nLutSize)
Definition bmcMaj.c:1055
Exa3_ManExactSynthesis
int Exa3_ManExactSynthesis(Bmc_EsPar_t *pPars)
Definition bmcMaj.c:1598
Exa6_ManMarkup
int Exa6_ManMarkup(Exa6_Man_t *p)
Definition bmcMaj.c:3449
Gia_ManDupMini
Gia_Man_t * Gia_ManDupMini(Gia_Man_t *p, Vec_Int_t *vIns, Vec_Int_t *vDivs, Vec_Int_t *vOuts, Mini_Aig_t *pMini)
Definition bmcMaj.c:3368
Exa7_GetVar
int Exa7_GetVar(int n, int i, int j, int m)
Definition bmcMaj.c:4060
Exa_ManDumpVerilog
void Exa_ManDumpVerilog(Vec_Int_t *vValues, int nVars, int nNodes, int GateSize, word *pTruth)
Definition bmcMaj.c:4119
Exa_ManExactSynthesis4Vars
void Exa_ManExactSynthesis4Vars()
Definition bmcMaj.c:3099
Maj_ManMarkup
int Maj_ManMarkup(Maj_Man_t *p)
Definition bmcMaj.c:100
MAJ_NOBJS
#define MAJ_NOBJS
DECLARATIONS ///.
Definition bmcMaj.c:44
Exa6_ManGenMint
void Exa6_ManGenMint(Exa6_Man_t *p, int iMint, int fOnlyAnd, int fFancy)
Definition bmcMaj.c:3653
Exa_ManAddCnfStart
int Exa_ManAddCnfStart(Exa_Man_t *p, int fOnlyAnd)
Definition bmcMaj.c:764
Exa_ManExactSynthesis5
void Exa_ManExactSynthesis5(Bmc_EsPar_t *pPars)
Definition bmcMaj.c:2953
Gia_ManDupMini_rec
int Gia_ManDupMini_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj)
Definition bmcMaj.c:3359
Maj_ManAlloc
Maj_Man_t * Maj_ManAlloc(int nVars, int nNodes, int fUseConst, int fUseLine)
Definition bmcMaj.c:147
Maj_ManPrintSolution
void Maj_ManPrintSolution(Maj_Man_t *p)
Definition bmcMaj.c:244
Maj_ManExactSynthesis
int Maj_ManExactSynthesis(int nVars, int nNodes, int fUseConst, int fUseLine, int fVerbose)
Definition bmcMaj.c:377
Exa_ManMiniPrint
void Exa_ManMiniPrint(Mini_Aig_t *p, int nIns)
Definition bmcMaj.c:1726
Exa_ManExactSynthesis4VarsOne
word Exa_ManExactSynthesis4VarsOne(int Index, int Truth, int nNodes)
Definition bmcMaj.c:3060
Exa4_ManGenStart
int Exa4_ManGenStart(Exa4_Man_t *p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard, char *pGuide)
Definition bmcMaj.c:2041
Exa_ManExactSynthesis4
void Exa_ManExactSynthesis4(Bmc_EsPar_t *pPars)
Definition bmcMaj.c:2449
Exa6_ManFree
void Exa6_ManFree(Exa6_Man_t *p)
Definition bmcMaj.c:3527
Maj_ManAddCnfStart
int Maj_ManAddCnfStart(Maj_Man_t *p)
Definition bmcMaj.c:278
Bmc_EsPar_t
typedefABC_NAMESPACE_HEADER_START struct Bmc_EsPar_t_ Bmc_EsPar_t
INCLUDES ///.
Definition bmc.h:47
Cmd_CommandExecute
ABC_DLL int Cmd_CommandExecute(Abc_Frame_t *pAbc, const char *sCommand)
Definition cmdApi.c:193
Pos
ush Pos
Definition deflate.h:88
p
Cube * p
Definition exorList.c:222
Var
int Var
Definition exorList.c:228
Extra_TimeStamp
char * Extra_TimeStamp()
Definition extraUtilFile.c:465
Extra_FileNameGenericAppend
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition extraUtilFile.c:192
Extra_PrintHexadecimalString
void Extra_PrintHexadecimalString(char *pString, unsigned Sign[], int nVars)
Definition extraUtilFile.c:611
Extra_BitMatrixTransposeP
ABC_NAMESPACE_IMPL_START void Extra_BitMatrixTransposeP(Vec_Wrd_t *vSimsIn, int nWordsIn, Vec_Wrd_t *vSimsOut, int nWordsOut)
DECLARATIONS ///.
Definition extraUtilMisc.c:2652
Gia_ManKSatGenLevels
Vec_Int_t * Gia_ManKSatGenLevels(char *pGuide, int nIns, int nNodes)
Definition giaSatLut.c:1686
Gia_RunKadical
Vec_Int_t * Gia_RunKadical(char *pFileNameIn, char *pFileNameOut, int Seed, int nBTLimit, int TimeOut, int fVerbose, int *pStatus)
Definition giaSatLut.c:1237
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition giaMan.c:764
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition giaUtil.c:369
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
Extra_PrintBinary
void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
Definition extraUtilFile.c:516
Abc_RData_t
typedefABC_NAMESPACE_HEADER_START struct Abc_RData_t_ Abc_RData_t
INCLUDES ///.
Definition ioResub.h:40
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Mini_Aig_t
struct Mini_Aig_t_ Mini_Aig_t
BASIC TYPES ///.
Definition miniaig.h:48
Mini_AigForEachPi
#define Mini_AigForEachPi(p, i)
Definition miniaig.h:138
Mini_AigForEachPo
#define Mini_AigForEachPo(p, i)
Definition miniaig.h:139
Mini_AigForEachAnd
#define Mini_AigForEachAnd(p, i)
Definition miniaig.h:140
Exa3_Man_t_
Definition bmcMaj.c:996
Exa3_Man_t_::nUsed
int nUsed[2]
Definition bmcMaj.c:1014
Exa3_Man_t_::vUsed2
Vec_Bit_t * vUsed2
Definition bmcMaj.c:1007
Exa3_Man_t_::pTruth
word * pTruth
Definition bmcMaj.c:1005
Exa3_Man_t_::vInVars
Vec_Wec_t * vInVars
Definition bmcMaj.c:1012
Exa3_Man_t_::vInfo
Vec_Wrd_t * vInfo
Definition bmcMaj.c:1006
Exa3_Man_t_::pSat
bmcg_sat_solver * pSat
Definition bmcMaj.c:1013
Exa3_Man_t_::vUsed3
Vec_Bit_t * vUsed3
Definition bmcMaj.c:1008
Exa3_Man_t_::nLutSize
int nLutSize
Definition bmcMaj.c:1000
Exa3_Man_t_::vOutLits
Vec_Wec_t * vOutLits
Definition bmcMaj.c:1011
Exa3_Man_t_::nWords
int nWords
Definition bmcMaj.c:1003
Exa3_Man_t_::nVars
int nVars
Definition bmcMaj.c:998
Exa3_Man_t_::VarMarks
int VarMarks[MAJ_NOBJS][6][MAJ_NOBJS]
Definition bmcMaj.c:1009
Exa3_Man_t_::nNodes
int nNodes
Definition bmcMaj.c:999
Exa3_Man_t_::VarVals
int VarVals[MAJ_NOBJS]
Definition bmcMaj.c:1010
Exa3_Man_t_::pPars
Bmc_EsPar_t * pPars
Definition bmcMaj.c:997
Exa3_Man_t_::nObjs
int nObjs
Definition bmcMaj.c:1002
Exa3_Man_t_::LutMask
int LutMask
Definition bmcMaj.c:1001
Exa3_Man_t_::iVar
int iVar
Definition bmcMaj.c:1004
Exa4_Man_t_
Definition bmcMaj.c:1891
Exa4_Man_t_::nIns
int nIns
Definition bmcMaj.c:1895
Exa4_Man_t_::nCnfClauses
int nCnfClauses
Definition bmcMaj.c:1902
Exa4_Man_t_::vSimsOut
Vec_Wrd_t * vSimsOut
Definition bmcMaj.c:1893
Exa4_Man_t_::nDivs
int nDivs
Definition bmcMaj.c:1896
Exa4_Man_t_::nOuts
int nOuts
Definition bmcMaj.c:1898
Exa4_Man_t_::nCnfVars
int nCnfVars
Definition bmcMaj.c:1901
Exa4_Man_t_::VarMarks
int VarMarks[MAJ_NOBJS][2][MAJ_NOBJS]
Definition bmcMaj.c:1900
Exa4_Man_t_::fVerbose
int fVerbose
Definition bmcMaj.c:1894
Exa4_Man_t_::nNodes
int nNodes
Definition bmcMaj.c:1897
Exa4_Man_t_::nObjs
int nObjs
Definition bmcMaj.c:1899
Exa4_Man_t_::vSimsIn
Vec_Wrd_t * vSimsIn
Definition bmcMaj.c:1892
Exa4_Man_t_::pFile
FILE * pFile
Definition bmcMaj.c:1903
Exa5_Man_t_
Definition bmcMaj.c:2477
Exa5_Man_t_::vSimsOut
Vec_Wrd_t * vSimsOut
Definition bmcMaj.c:2479
Exa5_Man_t_::nIns
int nIns
Definition bmcMaj.c:2481
Exa5_Man_t_::vFans
Vec_Int_t * vFans
Definition bmcMaj.c:2490
Exa5_Man_t_::nCnfClauses
int nCnfClauses
Definition bmcMaj.c:2488
Exa5_Man_t_::VarMarks
int VarMarks[MAJ_NOBJS][MAJ_NOBJS]
Definition bmcMaj.c:2486
Exa5_Man_t_::pFile
FILE * pFile
Definition bmcMaj.c:2489
Exa5_Man_t_::nOuts
int nOuts
Definition bmcMaj.c:2484
Exa5_Man_t_::nDivs
int nDivs
Definition bmcMaj.c:2482
Exa5_Man_t_::nCnfVars
int nCnfVars
Definition bmcMaj.c:2487
Exa5_Man_t_::nNodes
int nNodes
Definition bmcMaj.c:2483
Exa5_Man_t_::vSimsIn
Vec_Wrd_t * vSimsIn
Definition bmcMaj.c:2478
Exa5_Man_t_::fVerbose
int fVerbose
Definition bmcMaj.c:2480
Exa5_Man_t_::nObjs
int nObjs
Definition bmcMaj.c:2485
Exa6_Man_t_
Definition bmcMaj.c:3422
Exa6_Man_t_::nCnfVars2
int nCnfVars2
Definition bmcMaj.c:3433
Exa6_Man_t_::nOuts
int nOuts
Definition bmcMaj.c:3429
Exa6_Man_t_::fVerbose
int fVerbose
Definition bmcMaj.c:3425
Exa6_Man_t_::pFile
FILE * pFile
Definition bmcMaj.c:3435
Exa6_Man_t_::nNodes
int nNodes
Definition bmcMaj.c:3428
Exa6_Man_t_::nCnfVars
int nCnfVars
Definition bmcMaj.c:3432
Exa6_Man_t_::nDivs
int nDivs
Definition bmcMaj.c:3427
Exa6_Man_t_::vSimsIn
Vec_Wrd_t * vSimsIn
Definition bmcMaj.c:3423
Exa6_Man_t_::VarMarks
int VarMarks[MAJ_NOBJS][2][MAJ_NOBJS]
Definition bmcMaj.c:3431
Exa6_Man_t_::nObjs
int nObjs
Definition bmcMaj.c:3430
Exa6_Man_t_::nIns
int nIns
Definition bmcMaj.c:3426
Exa6_Man_t_::vSimsOut
Vec_Wrd_t * vSimsOut
Definition bmcMaj.c:3424
Exa6_Man_t_::nCnfClauses
int nCnfClauses
Definition bmcMaj.c:3434
Exa_Man_t_
Definition bmcMaj.c:423
Exa_Man_t_::pFile
FILE * pFile
Definition bmcMaj.c:436
Exa_Man_t_::pTruth
word * pTruth
Definition bmcMaj.c:430
Exa_Man_t_::nNodes
int nNodes
Definition bmcMaj.c:426
Exa_Man_t_::pPars
Bmc_EsPar_t * pPars
Definition bmcMaj.c:424
Exa_Man_t_::VarMarks
int VarMarks[MAJ_NOBJS][2][MAJ_NOBJS]
Definition bmcMaj.c:432
Exa_Man_t_::pSat
bmcg_sat_solver * pSat
Definition bmcMaj.c:435
Exa_Man_t_::nVars
int nVars
Definition bmcMaj.c:425
Exa_Man_t_::nCnfClauses
int nCnfClauses
Definition bmcMaj.c:437
Exa_Man_t_::vInfo
Vec_Wrd_t * vInfo
Definition bmcMaj.c:431
Exa_Man_t_::nObjs
int nObjs
Definition bmcMaj.c:427
Exa_Man_t_::VarVals
int VarVals[MAJ_NOBJS]
Definition bmcMaj.c:433
Exa_Man_t_::nWords
int nWords
Definition bmcMaj.c:428
Exa_Man_t_::iVar
int iVar
Definition bmcMaj.c:429
Exa_Man_t_::vOutLits
Vec_Wec_t * vOutLits
Definition bmcMaj.c:434
Gia_Man_t_::pSpec
char * pSpec
Definition gia.h:100
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Maj_Man_t_
Definition bmcMaj.c:48
Maj_Man_t_::vInfo
Vec_Wrd_t * vInfo
Definition bmcMaj.c:56
Maj_Man_t_::iVar
int iVar
Definition bmcMaj.c:53
Maj_Man_t_::nVars
int nVars
Definition bmcMaj.c:49
Maj_Man_t_::vOutLits
Vec_Wec_t * vOutLits
Definition bmcMaj.c:59
Maj_Man_t_::VarVals
int VarVals[MAJ_NOBJS+2]
Definition bmcMaj.c:58
Maj_Man_t_::nObjs
int nObjs
Definition bmcMaj.c:51
Maj_Man_t_::nWords
int nWords
Definition bmcMaj.c:52
Maj_Man_t_::fUseConst
int fUseConst
Definition bmcMaj.c:54
Maj_Man_t_::nNodes
int nNodes
Definition bmcMaj.c:50
Maj_Man_t_::fUseLine
int fUseLine
Definition bmcMaj.c:55
Maj_Man_t_::VarMarks
int VarMarks[MAJ_NOBJS][3][MAJ_NOBJS]
Definition bmcMaj.c:57
Maj_Man_t_::pSat
bmcg_sat_solver * pSat
Definition bmcMaj.c:60
MAJ_NOBJS
#define MAJ_NOBJS
Definition synthesisEngine.hpp:37
assert
#define assert(ex)
Definition util_old.h:213
strncmp
int strncmp()
strlen
int strlen()
system
int system()
strcmp
int strcmp()
sprintf
char * sprintf()
strtok
char * strtok()
rewind
VOID_HACK rewind()
Vec_Bit_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition vecBit.h:42
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryDoubleStart
#define Vec_IntForEachEntryDoubleStart(vVec, Entry1, Entry2, i, Start)
Definition vecInt.h:74
Vec_WecForEachLevel
#define Vec_WecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition vecWec.h:55
Vec_WecForEachLevelReverse
#define Vec_WecForEachLevelReverse(vGlob, vVec, i)
Definition vecWec.h:65
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42
Vec_WrdForEachEntry
#define Vec_WrdForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecWrd.h:54
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42