1 /**CFile****************************************************************
2 
3   FileName    [bmcMaj2.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [SAT-based bounded model checking.]
8 
9   Synopsis    [Exact synthesis with majority gates.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - October 1, 2017.]
16 
17   Revision    [$Id: bmcMaj.c,v 1.00 2017/10/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "bmc.h"
22 #include "misc/extra/extra.h"
23 #include "misc/util/utilTruth.h"
24 #include "sat/cnf/cnf.h"
25 #include "sat/bsat/satStore.h"
26 
27 ABC_NAMESPACE_IMPL_START
28 
29 ////////////////////////////////////////////////////////////////////////
30 ///                        DECLARATIONS                              ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 #define MAJ_NOBJS  32 // Const0 + Const1 + nVars + nNodes
34 
35 typedef struct Maj_Man_t_ Maj_Man_t;
36 struct Maj_Man_t_
37 {
38     int               nVars;     // inputs
39     int               nNodes;    // internal nodes
40     int               nObjs;     // total objects (2 consts, nVars inputs, nNodes internal nodes)
41     int               nWords;    // the truth table size in 64-bit words
42     int               iVar;      // the next available SAT variable
43     int               fUseConst; // use constant fanins
44     int               fUseLine;  // use cascade topology
45     int               fUseRand;  // use random topology
46     int               nRands;    // number of random connections
47     int               fVerbose;  // verbose flag
48     Vec_Wrd_t *       vInfo;     // Const0 + Const1 + nVars + nNodes + Maj(nVars)
49     int               VarMarks[MAJ_NOBJS][3][MAJ_NOBJS]; // variable marks
50     int               VarVals[MAJ_NOBJS+2]; // values of the first 2 + nVars variables
51     Vec_Wec_t *       vOutLits;  // output vars
52     sat_solver *      pSat;      // SAT solver
53 };
54 
Maj_ManTruth(Maj_Man_t * p,int v)55 static inline word *  Maj_ManTruth( Maj_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); }
56 
57 ////////////////////////////////////////////////////////////////////////
58 ///                     FUNCTION DEFINITIONS                         ///
59 ////////////////////////////////////////////////////////////////////////
60 
61 /**Function*************************************************************
62 
63   Synopsis    []
64 
65   Description []
66 
67   SideEffects []
68 
69   SeeAlso     []
70 
71 ***********************************************************************/
Maj_ManValue(int iMint,int nVars)72 static int Maj_ManValue( int iMint, int nVars )
73 {
74     int k, Count = 0;
75     for ( k = 0; k < nVars; k++ )
76         Count += (iMint >> k) & 1;
77     return (int)(Count > nVars/2);
78 }
Maj_ManTruthTables(Maj_Man_t * p)79 static Vec_Wrd_t * Maj_ManTruthTables( Maj_Man_t * p )
80 {
81     Vec_Wrd_t * vInfo = p->vInfo = Vec_WrdStart( p->nWords * (p->nObjs + 1) );
82     int i, nMints = Abc_MaxInt( 64, 1 << p->nVars );
83     Abc_TtFill( Maj_ManTruth(p, 1), p->nWords );
84     for ( i = 0; i < p->nVars; i++ )
85         Abc_TtIthVar( Maj_ManTruth(p, i+2), i, p->nVars );
86     for ( i = 0; i < nMints; i++ )
87         if ( Maj_ManValue(i, p->nVars) )
88             Abc_TtSetBit( Maj_ManTruth(p, p->nObjs), i );
89     //Dau_DsdPrintFromTruth( Maj_ManTruth(p, p->nObjs), p->nVars );
90     return vInfo;
91 }
Maj_ManConnect(int VarCons[MAJ_NOBJS][3],int nVars,int nObjs,int nRands,int fVerbose)92 static void Maj_ManConnect( int VarCons[MAJ_NOBJS][3], int nVars, int nObjs, int nRands, int fVerbose )
93 {
94     int i, v, r, x;
95     srand(clock());
96     for ( i = nObjs-2; i >= nVars + 2; i-- )
97     {
98         while ( 1 )
99         {
100             int Index = 1 + (rand() % (nObjs-1-i));
101             for ( v = 2; v >= 0; v-- )
102 //            for ( v = 0; v < 3; v++ )
103                 if ( VarCons[i+Index][v] == 0 )
104                 {
105                     VarCons[i+Index][v] = i;
106                     if ( fVerbose )
107                     printf( "%d -> %d  ", i, i+Index );
108                     break;
109                 }
110             if ( v >= 0 )
111                 break;
112         }
113     }
114     for ( r = 0; r < nRands; r++ )
115     {
116         i = nVars+2 + (rand() % ((nObjs-1)-(nVars+2)));
117         for ( x = 0; x < 100; x++ )
118         {
119             int Index = 1 + (rand() % (nObjs-1-i));
120             for ( v = 2; v >= 0; v-- )
121 //            for ( v = 0; v < 3; v++ )
122             {
123                 if ( VarCons[i+Index][v] == i )
124                 {
125                     v = -1;
126                     break;
127                 }
128                 if ( VarCons[i+Index][v] == 0 )
129                 {
130                     VarCons[i+Index][v] = i;
131                     if ( fVerbose )
132                     printf( "+%d -> %d  ", i, i+Index );
133                     break;
134                 }
135             }
136             if ( v >= 0 )
137                 break;
138         }
139         if ( x == 100 )
140             r--;
141     }
142     if ( fVerbose )
143     printf( "\n" );
144 }
Maj_ManConnect2(int VarCons[MAJ_NOBJS][3],int nVars,int nObjs,int nRands)145 static void Maj_ManConnect2( int VarCons[MAJ_NOBJS][3], int nVars, int nObjs, int nRands )
146 {
147     VarCons[8+2][2]  = 7+2;
148     VarCons[10+2][2] = 9+2;
149     VarCons[11+2][2] = 7+2;
150     VarCons[11+2][1] = 8+2;
151     VarCons[12+2][2] = 9+2;
152     VarCons[12+2][1] = 10+2;
153     VarCons[13+2][2] = 11+2;
154     VarCons[13+2][1] = 12+2;
155 }
Maj_ManMarkup(Maj_Man_t * p)156 static int Maj_ManMarkup( Maj_Man_t * p )
157 {
158     int VarCons[MAJ_NOBJS][3] = {{0}};
159     int i, k, j, m;
160     p->iVar = 1;
161     assert( p->nObjs <= MAJ_NOBJS );
162     // create connections
163     if ( p->fUseRand )
164         Maj_ManConnect( VarCons, p->nVars, p->nObjs, p->nRands, p->fVerbose );
165     // make exception for the first node
166     i = p->nVars + 2;
167     for ( k = 0; k < 3; k++ )
168     {
169         j = 4-k;
170         Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
171         p->VarMarks[i][k][j] = p->iVar++;
172     }
173     // assign variables for other nodes
174     for ( i = p->nVars + 3; i < p->nObjs; i++ )
175     {
176         for ( k = 0; k < 3; k++ )
177         {
178             if ( p->fUseLine && k == 0 )
179             {
180                 j = i-1;
181                 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
182                 p->VarMarks[i][k][j] = p->iVar++;
183                 continue;
184             }
185             if ( p->fUseRand && VarCons[i][k] > 0 )
186             {
187                 j = VarCons[i][k];
188                 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
189                 p->VarMarks[i][k][j] = p->iVar++;
190                 continue;
191             }
192 
193             for ( j = (p->fUseConst && k == 2) ? 0 : 2; j < (p->fUseRand ? p->nVars+2-k : i-k); j++ )
194             {
195                 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
196                 p->VarMarks[i][k][j] = p->iVar++;
197             }
198         }
199     }
200     printf( "The number of parameter variables = %d.\n", p->iVar );
201     if ( !p->fVerbose )
202         return p->iVar;
203     // printout
204     printf( "     " );
205     for ( i = p->nVars + 2; i < p->nObjs; i++ )
206         printf( "   Node %2d    ", i  );
207     printf( "\n" );
208     for ( m = 0; m < p->nObjs; m++ )
209     {
210         printf( "%2d : ", m );
211         for ( i = p->nVars + 2; i < p->nObjs; i++ )
212         {
213             for ( j = 0; j < p->nObjs; j++ )
214             {
215                 if ( j != m )
216                     continue;
217                 for ( k = 0; k < 3; k++ )
218                     if ( p->VarMarks[i][k][j] )
219                         printf( "%3d ", p->VarMarks[i][k][j] );
220                     else
221                         printf( "%3c ", '.' );
222                 printf( "  " );
223             }
224         }
225         printf( "\n" );
226     }
227     return p->iVar;
228 }
Maj_ManAlloc(int nVars,int nNodes,int fUseConst,int fUseLine,int fUseRand,int nRands,int fVerbose)229 static Maj_Man_t * Maj_ManAlloc( int nVars, int nNodes, int fUseConst, int fUseLine, int fUseRand, int nRands, int fVerbose )
230 {
231     Maj_Man_t * p = ABC_CALLOC( Maj_Man_t, 1 );
232     p->nVars      = nVars;
233     p->nNodes     = nNodes;
234     p->nObjs      = 2 + nVars + nNodes;
235     p->fUseConst  = fUseConst;
236     p->fUseLine   = fUseLine;
237     p->fUseRand   = fUseRand;
238     p->fVerbose   = fVerbose;
239     p->nRands     = nRands;
240     p->nWords     = Abc_TtWordNum(nVars);
241     p->vOutLits   = Vec_WecStart( p->nObjs );
242     p->iVar       = Maj_ManMarkup( p );
243     p->VarVals[1] = 1;
244     p->vInfo      = Maj_ManTruthTables( p );
245     p->pSat       = sat_solver_new();
246     sat_solver_setnvars( p->pSat, p->iVar );
247     return p;
248 }
Maj_ManFree(Maj_Man_t * p)249 static void Maj_ManFree( Maj_Man_t * p )
250 {
251     sat_solver_delete( p->pSat );
252     Vec_WrdFree( p->vInfo );
253     Vec_WecFree( p->vOutLits );
254     ABC_FREE( p );
255 }
256 
257 
258 /**Function*************************************************************
259 
260   Synopsis    []
261 
262   Description []
263 
264   SideEffects []
265 
266   SeeAlso     []
267 
268 ***********************************************************************/
Maj_ManFindFanin(Maj_Man_t * p,int i,int k)269 static inline int Maj_ManFindFanin( Maj_Man_t * p, int i, int k )
270 {
271     int j, Count = 0, iVar = -1;
272     for ( j = 0; j < p->nObjs; j++ )
273         if ( p->VarMarks[i][k][j] && sat_solver_var_value(p->pSat, p->VarMarks[i][k][j]) )
274         {
275             iVar = j;
276             Count++;
277         }
278     assert( Count == 1 );
279     return iVar;
280 }
Maj_ManEval(Maj_Man_t * p)281 static inline int Maj_ManEval( Maj_Man_t * p )
282 {
283     int fUseMiddle = 1;
284     static int Flag = 0;
285     int i, k, iMint; word * pFanins[3];
286     for ( i = p->nVars + 2; i < p->nObjs; i++ )
287     {
288         for ( k = 0; k < 3; k++ )
289             pFanins[k] = Maj_ManTruth( p, Maj_ManFindFanin(p, i, k) );
290         Abc_TtMaj( Maj_ManTruth(p, i), pFanins[0], pFanins[1], pFanins[2], p->nWords );
291     }
292     if ( fUseMiddle )
293     {
294         iMint = -1;
295         for ( i = 0; i < (1 << p->nVars); i++ )
296         {
297             int nOnes = Abc_TtBitCount16(i);
298             if ( nOnes < p->nVars/2 || nOnes > p->nVars/2+1 )
299                 continue;
300             if ( Abc_TtGetBit(Maj_ManTruth(p, p->nObjs), i) == Abc_TtGetBit(Maj_ManTruth(p, p->nObjs-1), i) )
301                 continue;
302             iMint = i;
303             break;
304         }
305     }
306     else
307     {
308         if ( Flag && p->nVars >= 6 )
309             iMint = Abc_TtFindLastDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
310         else
311             iMint = Abc_TtFindFirstDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
312     }
313     //Flag ^= 1;
314     assert( iMint < (1 << p->nVars) );
315     return iMint;
316 }
317 
318 /**Function*************************************************************
319 
320   Synopsis    []
321 
322   Description []
323 
324   SideEffects []
325 
326   SeeAlso     []
327 
328 ***********************************************************************/
Maj_ManPrintSolution(Maj_Man_t * p)329 static void Maj_ManPrintSolution( Maj_Man_t * p )
330 {
331     int i, k, iVar;
332     printf( "Realization of %d-input majority using %d MAJ3 gates:\n", p->nVars, p->nNodes );
333 //    for ( i = p->nVars + 2; i < p->nObjs; i++ )
334     for ( i = p->nObjs - 1; i >= p->nVars + 2; i-- )
335     {
336         printf( "%02d = MAJ(", i-2 );
337         for ( k = 2; k >= 0; k-- )
338         {
339             iVar = Maj_ManFindFanin( p, i, k );
340             if ( iVar >= 2 && iVar < p->nVars + 2 )
341                 printf( " %c", 'a'+iVar-2 );
342             else if ( iVar < 2 )
343                 printf( " %d", iVar );
344             else
345                 printf( " %02d", iVar-2 );
346         }
347         printf( " )\n" );
348     }
349 }
350 
351 
352 /**Function*************************************************************
353 
354   Synopsis    []
355 
356   Description []
357 
358   SideEffects []
359 
360   SeeAlso     []
361 
362 ***********************************************************************/
Maj_ManAddCnfStart(Maj_Man_t * p)363 static int Maj_ManAddCnfStart( Maj_Man_t * p )
364 {
365     int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m;
366     // input constraints
367     for ( i = p->nVars + 2; i < p->nObjs; i++ )
368     {
369         for ( k = 0; k < 3; k++ )
370         {
371             int nLits = 0;
372             for ( j = 0; j < p->nObjs; j++ )
373                 if ( p->VarMarks[i][k][j] )
374                     pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
375             assert( nLits > 0 );
376             // input uniqueness
377             if ( !sat_solver_addclause( p->pSat, pLits, pLits+nLits ) )
378                 return 0;
379             for ( n = 0;   n < nLits; n++ )
380             for ( m = n+1; m < nLits; m++ )
381             {
382                 pLits2[0] = Abc_LitNot(pLits[n]);
383                 pLits2[1] = Abc_LitNot(pLits[m]);
384                 if ( !sat_solver_addclause( p->pSat, pLits2, pLits2+2 ) )
385                     return 0;
386             }
387             if ( k == 2 || p->VarMarks[i][k][2] == 0 || p->VarMarks[i][k+1][2] == 0 )
388                 continue;
389             // symmetry breaking
390             for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
391             for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] )
392             {
393                 pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
394                 pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 );
395                 if ( !sat_solver_addclause( p->pSat, pLits2, pLits2+2 ) )
396                     return 0;
397             }
398         }
399     }
400     // outputs should be used
401     for ( i = 2; i < p->nObjs - 1; i++ )
402     {
403         Vec_Int_t * vArray = Vec_WecEntry(p->vOutLits, i);
404         assert( Vec_IntSize(vArray) > 0 );
405         if ( !sat_solver_addclause( p->pSat, Vec_IntArray(vArray), Vec_IntLimit(vArray) ) )
406             return 0;
407     }
408     return 1;
409 }
Maj_ManAddCnf(Maj_Man_t * p,int iMint)410 static int Maj_ManAddCnf( Maj_Man_t * p, int iMint )
411 {
412     // save minterm values
413     int i, k, n, j, Value = Maj_ManValue(iMint, p->nVars);
414     for ( i = 0; i < p->nVars; i++ )
415         p->VarVals[i+2] = (iMint >> i) & 1;
416     sat_solver_setnvars( p->pSat, p->iVar + 4*p->nNodes );
417     //printf( "Adding clauses for minterm %d.\n", iMint );
418     for ( i = p->nVars + 2; i < p->nObjs; i++ )
419     {
420         // fanin connectivity
421         int iBaseSatVarI = p->iVar + 4*(i - p->nVars - 2);
422         for ( k = 0; k < 3; k++ )
423         {
424             for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
425             {
426                 int iBaseSatVarJ = p->iVar + 4*(j - p->nVars - 2);
427                 for ( n = 0; n < 2; n++ )
428                 {
429                     int pLits[3], nLits = 0;
430                     pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
431                     pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + k, n );
432                     if ( j >= p->nVars + 2 )
433                         pLits[nLits++] = Abc_Var2Lit( iBaseSatVarJ + 3, !n );
434                     else if ( p->VarVals[j] == n )
435                         continue;
436                     if ( !sat_solver_addclause( p->pSat, pLits, pLits+nLits ) )
437                         return 0;
438                 }
439             }
440         }
441         // node functionality
442         for ( n = 0; n < 2; n++ )
443         {
444             if ( i == p->nObjs - 1 && n == Value )
445                 continue;
446             for ( k = 0; k < 3; k++ )
447             {
448                 int pLits[3], nLits = 0;
449                 if ( k != 0 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 0, n );
450                 if ( k != 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 1, n );
451                 if ( k != 2 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 2, n );
452                 if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 3, !n );
453                 assert( nLits <= 3 );
454                 if ( !sat_solver_addclause( p->pSat, pLits, pLits+nLits ) )
455                     return 0;
456             }
457         }
458     }
459     p->iVar += 4*p->nNodes;
460     return 1;
461 }
Maj_ManExactSynthesis2(int nVars,int nNodes,int fUseConst,int fUseLine,int fUseRand,int nRands,int fVerbose)462 int Maj_ManExactSynthesis2( int nVars, int nNodes, int fUseConst, int fUseLine, int fUseRand, int nRands, int fVerbose )
463 {
464     int i, iMint = 0;
465     abctime clkTotal = Abc_Clock();
466     Maj_Man_t * p = Maj_ManAlloc( nVars, nNodes, fUseConst, fUseLine, fUseRand, nRands, fVerbose );
467     int status = Maj_ManAddCnfStart( p );
468     assert( status );
469     if ( fVerbose )
470     printf( "Running exact synthesis for %d-input majority with %d MAJ3 gates...\n", p->nVars, p->nNodes );
471     for ( i = 0; iMint != -1; i++ )
472     {
473         abctime clk = Abc_Clock();
474         if ( !Maj_ManAddCnf( p, iMint ) )
475         {
476             printf( "The problem has no solution after %2d iterations.  ", i+1 );
477             break;
478         }
479         status = sat_solver_solve( p->pSat, NULL, NULL, 0, 0, 0, 0 );
480         if ( fVerbose )
481         {
482             printf( "Iter %3d : ", i );
483             Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
484             printf( "  Var =%5d  ", p->iVar );
485             printf( "Cla =%6d  ", sat_solver_nclauses(p->pSat) );
486             printf( "Conf =%9d  ", sat_solver_nconflicts(p->pSat) );
487             Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
488         }
489         if ( status == l_False )
490         {
491             printf( "The problem has no solution after %2d iterations.  ", i+1 );
492             break;
493         }
494         iMint = Maj_ManEval( p );
495     }
496     if ( iMint == -1 )
497         Maj_ManPrintSolution( p );
498     Maj_ManFree( p );
499     Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
500     return iMint == -1;
501 }
502 
Maj_ManExactSynthesisTest()503 int Maj_ManExactSynthesisTest()
504 {
505 //    while ( !Maj_ManExactSynthesis2( 5, 4, 0, 0, 1, 1, 0 ) );
506 //    while ( !Maj_ManExactSynthesis2( 7, 7, 0, 0, 1, 2, 0 ) );
507     while ( !Maj_ManExactSynthesis2( 9, 10, 0, 0, 1, 3, 0 ) );
508     return 1;
509 }
510 
511 
512 
513 
514 
515 
516 typedef struct Exa_Man_t_ Exa_Man_t;
517 struct Exa_Man_t_
518 {
519     Bmc_EsPar_t *     pPars;     // parameters
520     int               nVars;     // inputs
521     int               nNodes;    // internal nodes
522     int               nObjs;     // total objects (nVars inputs + nNodes internal nodes)
523     int               nWords;    // the truth table size in 64-bit words
524     int               iVar;      // the next available SAT variable
525     word *            pTruth;    // truth table
526     Vec_Wrd_t *       vInfo;     // nVars + nNodes + 1
527     int               VarMarks[MAJ_NOBJS][2][MAJ_NOBJS]; // variable marks
528     int               VarVals[MAJ_NOBJS]; // values of the first nVars variables
529     Vec_Wec_t *       vOutLits;  // output vars
530     sat_solver *      pSat;      // SAT solver
531 };
532 
Exa_ManTruth(Exa_Man_t * p,int v)533 static inline word *  Exa_ManTruth( Exa_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); }
534 
535 
536 /**Function*************************************************************
537 
538   Synopsis    []
539 
540   Description []
541 
542   SideEffects []
543 
544   SeeAlso     []
545 
546 ***********************************************************************/
Exa_ManTruthTables(Exa_Man_t * p)547 static Vec_Wrd_t * Exa_ManTruthTables( Exa_Man_t * p )
548 {
549     Vec_Wrd_t * vInfo = p->vInfo = Vec_WrdStart( p->nWords * (p->nObjs+1) ); int i;
550     for ( i = 0; i < p->nVars; i++ )
551         Abc_TtIthVar( Exa_ManTruth(p, i), i, p->nVars );
552     //Dau_DsdPrintFromTruth( Exa_ManTruth(p, p->nObjs), p->nVars );
553     return vInfo;
554 }
Exa_ManMarkup(Exa_Man_t * p)555 static int Exa_ManMarkup( Exa_Man_t * p )
556 {
557     int i, k, j;
558     assert( p->nObjs <= MAJ_NOBJS );
559     // assign functionality
560     p->iVar = 1 + p->nNodes * 3;
561     // assign connectivity variables
562     for ( i = p->nVars; i < p->nObjs; i++ )
563     {
564         for ( k = 0; k < 2; k++ )
565         {
566             if ( p->pPars->fFewerVars && i == p->nObjs - 1 && k == 0 )
567             {
568                 j = p->nObjs - 2;
569                 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
570                 p->VarMarks[i][k][j] = p->iVar++;
571                 continue;
572             }
573             for ( j = p->pPars->fFewerVars ? 1 - k : 0; j < i - k; j++ )
574             {
575                 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
576                 p->VarMarks[i][k][j] = p->iVar++;
577             }
578         }
579     }
580     printf( "The number of parameter variables = %d.\n", p->iVar );
581     return p->iVar;
582     // printout
583     for ( i = p->nVars; i < p->nObjs; i++ )
584     {
585         printf( "Node %d\n", i );
586         for ( j = 0; j < p->nObjs; j++ )
587         {
588             for ( k = 0; k < 2; k++ )
589                 printf( "%3d ", p->VarMarks[i][k][j] );
590             printf( "\n" );
591         }
592     }
593     return p->iVar;
594 }
Exa_ManAlloc(Bmc_EsPar_t * pPars,word * pTruth)595 static Exa_Man_t * Exa_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
596 {
597     Exa_Man_t * p = ABC_CALLOC( Exa_Man_t, 1 );
598     p->pPars      = pPars;
599     p->nVars      = pPars->nVars;
600     p->nNodes     = pPars->nNodes;
601     p->nObjs      = pPars->nVars + pPars->nNodes;
602     p->nWords     = Abc_TtWordNum(pPars->nVars);
603     p->pTruth     = pTruth;
604     p->vOutLits   = Vec_WecStart( p->nObjs );
605     p->iVar       = Exa_ManMarkup( p );
606     p->vInfo      = Exa_ManTruthTables( p );
607     p->pSat       = sat_solver_new();
608     sat_solver_setnvars( p->pSat, p->iVar );
609     return p;
610 }
Exa_ManFree(Exa_Man_t * p)611 static void Exa_ManFree( Exa_Man_t * p )
612 {
613     sat_solver_delete( p->pSat );
614     Vec_WrdFree( p->vInfo );
615     Vec_WecFree( p->vOutLits );
616     ABC_FREE( p );
617 }
618 
619 
620 /**Function*************************************************************
621 
622   Synopsis    []
623 
624   Description []
625 
626   SideEffects []
627 
628   SeeAlso     []
629 
630 ***********************************************************************/
Exa_ManFindFanin(Exa_Man_t * p,int i,int k)631 static inline int Exa_ManFindFanin( Exa_Man_t * p, int i, int k )
632 {
633     int j, Count = 0, iVar = -1;
634     for ( j = 0; j < p->nObjs; j++ )
635         if ( p->VarMarks[i][k][j] && sat_solver_var_value(p->pSat, p->VarMarks[i][k][j]) )
636         {
637             iVar = j;
638             Count++;
639         }
640     assert( Count == 1 );
641     return iVar;
642 }
Exa_ManEval(Exa_Man_t * p)643 static inline int Exa_ManEval( Exa_Man_t * p )
644 {
645     static int Flag = 0;
646     int i, k, iMint; word * pFanins[2];
647     for ( i = p->nVars; i < p->nObjs; i++ )
648     {
649         int iVarStart = 1 + 3*(i - p->nVars);
650         for ( k = 0; k < 2; k++ )
651             pFanins[k] = Exa_ManTruth( p, Exa_ManFindFanin(p, i, k) );
652         Abc_TtConst0( Exa_ManTruth(p, i), p->nWords );
653         for ( k = 1; k < 4; k++ )
654         {
655             if ( !sat_solver_var_value(p->pSat, iVarStart+k-1) )
656                 continue;
657             Abc_TtAndCompl( Exa_ManTruth(p, p->nObjs), pFanins[0], !(k&1), pFanins[1], !(k>>1), p->nWords );
658             Abc_TtOr( Exa_ManTruth(p, i), Exa_ManTruth(p, i), Exa_ManTruth(p, p->nObjs), p->nWords );
659         }
660     }
661     if ( Flag && p->nVars >= 6 )
662         iMint = Abc_TtFindLastDiffBit( Exa_ManTruth(p, p->nObjs-1), p->pTruth, p->nVars );
663     else
664         iMint = Abc_TtFindFirstDiffBit( Exa_ManTruth(p, p->nObjs-1), p->pTruth, p->nVars );
665     //Flag ^= 1;
666     assert( iMint < (1 << p->nVars) );
667     return iMint;
668 }
669 
670 /**Function*************************************************************
671 
672   Synopsis    []
673 
674   Description []
675 
676   SideEffects []
677 
678   SeeAlso     []
679 
680 ***********************************************************************/
Exa_ManPrintSolution(Exa_Man_t * p,int fCompl)681 static void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl )
682 {
683     int i, k, iVar;
684     printf( "Realization of given %d-input function using %d two-input gates:\n", p->nVars, p->nNodes );
685 //    for ( i = p->nVars + 2; i < p->nObjs; i++ )
686     for ( i = p->nObjs - 1; i >= p->nVars; i-- )
687     {
688         int iVarStart = 1 + 3*(i - p->nVars);
689         int Val1 = sat_solver_var_value(p->pSat, iVarStart);
690         int Val2 = sat_solver_var_value(p->pSat, iVarStart+1);
691         int Val3 = sat_solver_var_value(p->pSat, iVarStart+2);
692         if ( i == p->nObjs - 1 && fCompl )
693             printf( "%02d = 4\'b%d%d%d1(", i, !Val3, !Val2, !Val1 );
694         else
695             printf( "%02d = 4\'b%d%d%d0(", i, Val3, Val2, Val1 );
696         for ( k = 1; k >= 0; k-- )
697         {
698             iVar = Exa_ManFindFanin( p, i, k );
699             if ( iVar >= 0 && iVar < p->nVars )
700                 printf( " %c", 'a'+iVar );
701             else
702                 printf( " %02d", iVar );
703         }
704         printf( " )\n" );
705     }
706 }
707 
708 
709 /**Function*************************************************************
710 
711   Synopsis    []
712 
713   Description []
714 
715   SideEffects []
716 
717   SeeAlso     []
718 
719 ***********************************************************************/
Exa_ManAddCnfStart(Exa_Man_t * p,int fOnlyAnd)720 static int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
721 {
722     int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m;
723     // input constraints
724     for ( i = p->nVars; i < p->nObjs; i++ )
725     {
726         int iVarStart = 1 + 3*(i - p->nVars);
727         for ( k = 0; k < 2; k++ )
728         {
729             int nLits = 0;
730             for ( j = 0; j < p->nObjs; j++ )
731                 if ( p->VarMarks[i][k][j] )
732                     pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
733             assert( nLits > 0 );
734             // input uniqueness
735             if ( !sat_solver_addclause( p->pSat, pLits, pLits+nLits ) )
736                 return 0;
737             for ( n = 0;   n < nLits; n++ )
738             for ( m = n+1; m < nLits; m++ )
739             {
740                 pLits2[0] = Abc_LitNot(pLits[n]);
741                 pLits2[1] = Abc_LitNot(pLits[m]);
742                 if ( !sat_solver_addclause( p->pSat, pLits2, pLits2+2 ) )
743                     return 0;
744             }
745             if ( k == 1 )
746                 break;
747             // symmetry breaking
748             for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
749             for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] )
750             {
751                 pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
752                 pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 );
753                 if ( !sat_solver_addclause( p->pSat, pLits2, pLits2+2 ) )
754                     return 0;
755             }
756         }
757 #ifdef USE_NODE_ORDER
758         // node ordering
759         for ( j = p->nVars; j < i; j++ )
760         for ( n = 0;   n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
761         for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
762         {
763             pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 );
764             pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 );
765             if ( !sat_solver_addclause( p->pSat, pLits2, pLits2+2 ) )
766                 return 0;
767         }
768 #endif
769         // two input functions
770         for ( k = 0; k < 3; k++ )
771         {
772             pLits[0] = Abc_Var2Lit( iVarStart,   k==1 );
773             pLits[1] = Abc_Var2Lit( iVarStart+1, k==2 );
774             pLits[2] = Abc_Var2Lit( iVarStart+2, k!=0 );
775             if ( !sat_solver_addclause( p->pSat, pLits, pLits+3 ) )
776                 return 0;
777         }
778         if ( fOnlyAnd )
779         {
780             pLits[0] = Abc_Var2Lit( iVarStart,   1 );
781             pLits[1] = Abc_Var2Lit( iVarStart+1, 1 );
782             pLits[2] = Abc_Var2Lit( iVarStart+2, 0 );
783             if ( !sat_solver_addclause( p->pSat, pLits, pLits+3 ) )
784                 return 0;
785         }
786     }
787     // outputs should be used
788     for ( i = 0; i < p->nObjs - 1; i++ )
789     {
790         Vec_Int_t * vArray = Vec_WecEntry(p->vOutLits, i);
791         assert( Vec_IntSize(vArray) > 0 );
792         if ( !sat_solver_addclause( p->pSat, Vec_IntArray(vArray), Vec_IntLimit(vArray) ) )
793             return 0;
794     }
795     return 1;
796 }
Exa_ManAddCnf(Exa_Man_t * p,int iMint)797 static int Exa_ManAddCnf( Exa_Man_t * p, int iMint )
798 {
799     // save minterm values
800     int i, k, n, j, Value = Abc_TtGetBit(p->pTruth, iMint);
801     for ( i = 0; i < p->nVars; i++ )
802         p->VarVals[i] = (iMint >> i) & 1;
803     sat_solver_setnvars( p->pSat, p->iVar + 3*p->nNodes );
804     //printf( "Adding clauses for minterm %d with value %d.\n", iMint, Value );
805     for ( i = p->nVars; i < p->nObjs; i++ )
806     {
807         // fanin connectivity
808         int iVarStart = 1 + 3*(i - p->nVars);
809         int iBaseSatVarI = p->iVar + 3*(i - p->nVars);
810         for ( k = 0; k < 2; k++ )
811         {
812             for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
813             {
814                 int iBaseSatVarJ = p->iVar + 3*(j - p->nVars);
815                 for ( n = 0; n < 2; n++ )
816                 {
817                     int pLits[3], nLits = 0;
818                     pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
819                     pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + k, n );
820                     if ( j >= p->nVars )
821                         pLits[nLits++] = Abc_Var2Lit( iBaseSatVarJ + 2, !n );
822                     else if ( p->VarVals[j] == n )
823                         continue;
824                     if ( !sat_solver_addclause( p->pSat, pLits, pLits+nLits ) )
825                         return 0;
826                 }
827             }
828         }
829         // node functionality
830         for ( n = 0; n < 2; n++ )
831         {
832             if ( i == p->nObjs - 1 && n == Value )
833                 continue;
834             for ( k = 0; k < 4; k++ )
835             {
836                 int pLits[4], nLits = 0;
837                 if ( k == 0 && n == 1 )
838                     continue;
839                 pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 0, (k&1)  );
840                 pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 1, (k>>1) );
841                 if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 2, !n );
842                 if ( k > 0 )             pLits[nLits++] = Abc_Var2Lit( iVarStart +  k-1,  n );
843                 assert( nLits <= 4 );
844                 if ( !sat_solver_addclause( p->pSat, pLits, pLits+nLits ) )
845                     return 0;
846             }
847         }
848     }
849     p->iVar += 3*p->nNodes;
850     return 1;
851 }
Exa_ManExactSynthesis2(Bmc_EsPar_t * pPars)852 void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars )
853 {
854     int i, status, iMint = 1;
855     abctime clkTotal = Abc_Clock();
856     Exa_Man_t * p; int fCompl = 0;
857     word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr );
858     assert( pPars->nVars <= 10 );
859     p = Exa_ManAlloc( pPars, pTruth );
860     if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); }
861     status = Exa_ManAddCnfStart( p, pPars->fOnlyAnd );
862     assert( status );
863     printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes );
864     for ( i = 0; iMint != -1; i++ )
865     {
866         abctime clk = Abc_Clock();
867         if ( !Exa_ManAddCnf( p, iMint ) )
868             break;
869         status = sat_solver_solve( p->pSat, NULL, NULL, 0, 0, 0, 0 );
870         if ( pPars->fVerbose )
871         {
872             printf( "Iter %3d : ", i );
873             Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
874             printf( "  Var =%5d  ", p->iVar );
875             printf( "Cla =%6d  ", sat_solver_nclauses(p->pSat) );
876             printf( "Conf =%9d  ", sat_solver_nconflicts(p->pSat) );
877             Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
878         }
879         if ( status == l_False )
880         {
881             printf( "The problem has no solution.\n" );
882             break;
883         }
884         iMint = Exa_ManEval( p );
885     }
886     if ( iMint == -1 )
887         Exa_ManPrintSolution( p, fCompl );
888     Exa_ManFree( p );
889     Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
890 }
891 
892 
893 
894 
895 
896 
897 typedef struct Exa3_Man_t_ Exa3_Man_t;
898 struct Exa3_Man_t_
899 {
900     Bmc_EsPar_t *     pPars;     // parameters
901     int               nVars;     // inputs
902     int               nNodes;    // internal nodes
903     int               nLutSize;  // lut size
904     int               LutMask;   // lut mask
905     int               nObjs;     // total objects (nVars inputs + nNodes internal nodes)
906     int               nWords;    // the truth table size in 64-bit words
907     int               iVar;      // the next available SAT variable
908     word *            pTruth;    // truth table
909     Vec_Wrd_t *       vInfo;     // nVars + nNodes + 1
910     int               VarMarks[MAJ_NOBJS][6][MAJ_NOBJS]; // variable marks
911     int               VarVals[MAJ_NOBJS]; // values of the first nVars variables
912     Vec_Wec_t *       vOutLits;  // output vars
913     sat_solver *      pSat;      // SAT solver
914 };
915 
Exa3_ManTruth(Exa3_Man_t * p,int v)916 static inline word *  Exa3_ManTruth( Exa3_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); }
917 
918 
919 /**Function*************************************************************
920 
921   Synopsis    []
922 
923   Description []
924 
925   SideEffects []
926 
927   SeeAlso     []
928 
929 ***********************************************************************/
Exa3_ManTruthTables(Exa3_Man_t * p)930 static Vec_Wrd_t * Exa3_ManTruthTables( Exa3_Man_t * p )
931 {
932     Vec_Wrd_t * vInfo = p->vInfo = Vec_WrdStart( p->nWords * (p->nObjs+1) ); int i;
933     for ( i = 0; i < p->nVars; i++ )
934         Abc_TtIthVar( Exa3_ManTruth(p, i), i, p->nVars );
935     //Dau_DsdPrintFromTruth( Exa3_ManTruth(p, p->nObjs), p->nVars );
936     return vInfo;
937 }
Exa3_ManMarkup(Exa3_Man_t * p)938 static int Exa3_ManMarkup( Exa3_Man_t * p )
939 {
940     int i, k, j;
941     assert( p->nObjs <= MAJ_NOBJS );
942     // assign functionality variables
943     p->iVar = 1 + p->LutMask * p->nNodes;
944     // assign connectivity variables
945     for ( i = p->nVars; i < p->nObjs; i++ )
946     {
947         for ( k = 0; k < p->nLutSize; k++ )
948         {
949             if ( p->pPars->fFewerVars && i == p->nObjs - 1 && k == 0 )
950             {
951                 j = p->nObjs - 2;
952                 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
953                 p->VarMarks[i][k][j] = p->iVar++;
954                 continue;
955             }
956             for ( j = p->pPars->fFewerVars ? p->nLutSize - 1 - k : 0; j < i - k; j++ )
957             {
958                 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
959                 p->VarMarks[i][k][j] = p->iVar++;
960             }
961         }
962     }
963     printf( "The number of parameter variables = %d.\n", p->iVar );
964     return p->iVar;
965     // printout
966 //    for ( i = p->nVars; i < p->nObjs; i++ )
967     for ( i = p->nObjs - 1; i >= p->nVars; i-- )
968     {
969         printf( "       Node %2d\n", i );
970         for ( j = 0; j < p->nObjs; j++ )
971         {
972             printf( "Fanin %2d : ", j );
973             for ( k = 0; k < p->nLutSize; k++ )
974                 printf( "%3d ", p->VarMarks[i][k][j] );
975             printf( "\n" );
976         }
977     }
978     return p->iVar;
979 }
Exa3_ManInitPolarityFindVar(Exa3_Man_t * p,int i,int k,int * pIndex)980 static int Exa3_ManInitPolarityFindVar( Exa3_Man_t * p, int i, int k, int * pIndex )
981 {
982     int iVar;
983     do {
984         iVar = p->VarMarks[i][k][*pIndex];
985         *pIndex = (*pIndex + 1) % p->nVars;
986     } while ( iVar <= 0 );
987     //intf( "Setting var %d.\n", iVar );
988     return iVar;
989 }
Exa3_ManInitPolarity(Exa3_Man_t * p)990 static void Exa3_ManInitPolarity( Exa3_Man_t * p )
991 {
992     int i, k, iVar, nInputs = 0;
993     for ( i = p->nVars; i < p->nObjs; i++ )
994     {
995         // create AND-gate
996         int iVarStart = 1 + p->LutMask*(i - p->nVars);
997         iVar = iVarStart + p->LutMask-1;
998         p->pSat->polarity[iVar] = 1;
999         //printf( "Setting var %d.\n", iVar );
1000     }
1001     for ( i = p->nVars; i < p->nObjs; i++ )
1002     {
1003         // connect first fanin to previous
1004         if ( i == p->nVars )
1005         {
1006             for ( k = p->nLutSize - 1; k >= 0; k-- )
1007             {
1008                 iVar = Exa3_ManInitPolarityFindVar( p, i, k, &nInputs );
1009                 p->pSat->polarity[iVar] = 1;
1010             }
1011         }
1012         else
1013         {
1014             for ( k = p->nLutSize - 1; k > 0; k-- )
1015             {
1016                 iVar = Exa3_ManInitPolarityFindVar( p, i, k, &nInputs );
1017                 p->pSat->polarity[iVar] = 1;
1018             }
1019             iVar = p->VarMarks[i][0][i-1];
1020             if ( iVar <= 0 ) printf( "Variable mapping error.\n" ), fflush(stdout);
1021             assert( iVar > 0 );
1022             p->pSat->polarity[iVar] = 1;
1023             //intf( "Setting var %d.\n", iVar );
1024         }
1025         //intf( "\n" );
1026     }
1027 }
Exa3_ManAlloc(Bmc_EsPar_t * pPars,word * pTruth)1028 static Exa3_Man_t * Exa3_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
1029 {
1030     Exa3_Man_t * p = ABC_CALLOC( Exa3_Man_t, 1 );
1031     p->pPars      = pPars;
1032     p->nVars      = pPars->nVars;
1033     p->nNodes     = pPars->nNodes;
1034     p->nLutSize   = pPars->nLutSize;
1035     p->LutMask    = (1 << pPars->nLutSize) - 1;
1036     p->nObjs      = pPars->nVars + pPars->nNodes;
1037     p->nWords     = Abc_TtWordNum(pPars->nVars);
1038     p->pTruth     = pTruth;
1039     p->vOutLits   = Vec_WecStart( p->nObjs );
1040     p->iVar       = Exa3_ManMarkup( p );
1041     p->vInfo      = Exa3_ManTruthTables( p );
1042     p->pSat       = sat_solver_new();
1043     sat_solver_setnvars( p->pSat, p->iVar );
1044     //Exa3_ManInitPolarity( p );
1045     return p;
1046 }
Exa3_ManFree(Exa3_Man_t * p)1047 static void Exa3_ManFree( Exa3_Man_t * p )
1048 {
1049     sat_solver_delete( p->pSat );
1050     Vec_WrdFree( p->vInfo );
1051     Vec_WecFree( p->vOutLits );
1052     ABC_FREE( p );
1053 }
1054 
1055 
1056 /**Function*************************************************************
1057 
1058   Synopsis    []
1059 
1060   Description []
1061 
1062   SideEffects []
1063 
1064   SeeAlso     []
1065 
1066 ***********************************************************************/
Exa3_ManFindFanin(Exa3_Man_t * p,int i,int k)1067 static inline int Exa3_ManFindFanin( Exa3_Man_t * p, int i, int k )
1068 {
1069     int j, Count = 0, iVar = -1;
1070     for ( j = 0; j < p->nObjs; j++ )
1071         if ( p->VarMarks[i][k][j] && sat_solver_var_value(p->pSat, p->VarMarks[i][k][j]) )
1072         {
1073             iVar = j;
1074             Count++;
1075         }
1076     assert( Count == 1 );
1077     return iVar;
1078 }
Exa3_ManEval(Exa3_Man_t * p)1079 static inline int Exa3_ManEval( Exa3_Man_t * p )
1080 {
1081     static int Flag = 0;
1082     int i, k, j, iMint; word * pFanins[6];
1083     for ( i = p->nVars; i < p->nObjs; i++ )
1084     {
1085         int iVarStart = 1 + p->LutMask*(i - p->nVars);
1086         for ( k = 0; k < p->nLutSize; k++ )
1087             pFanins[k] = Exa3_ManTruth( p, Exa3_ManFindFanin(p, i, k) );
1088         Abc_TtConst0( Exa3_ManTruth(p, i),        p->nWords );
1089         for ( k = 1; k <= p->LutMask; k++ )
1090         {
1091             if ( !sat_solver_var_value(p->pSat, iVarStart+k-1) )
1092                 continue;
1093 //            Abc_TtAndCompl( Exa3_ManTruth(p, p->nObjs), pFanins[0], !(k&1), pFanins[1], !(k>>1), p->nWords );
1094             Abc_TtConst1( Exa3_ManTruth(p, p->nObjs), p->nWords );
1095             for ( j = 0; j < p->nLutSize; j++ )
1096                 Abc_TtAndCompl( Exa3_ManTruth(p, p->nObjs), Exa3_ManTruth(p, p->nObjs), 0, pFanins[j], !((k >> j) & 1), p->nWords );
1097             Abc_TtOr( Exa3_ManTruth(p, i), Exa3_ManTruth(p, i), Exa3_ManTruth(p, p->nObjs), p->nWords );
1098         }
1099     }
1100     if ( Flag && p->nVars >= 6 )
1101         iMint = Abc_TtFindLastDiffBit( Exa3_ManTruth(p, p->nObjs-1), p->pTruth, p->nVars );
1102     else
1103         iMint = Abc_TtFindFirstDiffBit( Exa3_ManTruth(p, p->nObjs-1), p->pTruth, p->nVars );
1104     //Flag ^= 1;
1105     assert( iMint < (1 << p->nVars) );
1106     return iMint;
1107 }
1108 
1109 /**Function*************************************************************
1110 
1111   Synopsis    []
1112 
1113   Description []
1114 
1115   SideEffects []
1116 
1117   SeeAlso     []
1118 
1119 ***********************************************************************/
Exa3_ManPrintSolution(Exa3_Man_t * p,int fCompl)1120 static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl )
1121 {
1122     int i, k, iVar;
1123     printf( "Realization of given %d-input function using %d %d-input LUTs:\n", p->nVars, p->nNodes, p->nLutSize );
1124     for ( i = p->nObjs - 1; i >= p->nVars; i-- )
1125     {
1126         int Val, iVarStart = 1 + p->LutMask*(i - p->nVars);
1127 
1128 //        int Val1 = sat_solver_var_value(p->pSat, iVarStart);
1129 //        int Val2 = sat_solver_var_value(p->pSat, iVarStart+1);
1130 //        int Val3 = sat_solver_var_value(p->pSat, iVarStart+2);
1131 //        if ( i == p->nObjs - 1 && fCompl )
1132 //            printf( "%02d = 4\'b%d%d%d1(", i, !Val3, !Val2, !Val1 );
1133 //        else
1134 //            printf( "%02d = 4\'b%d%d%d0(", i, Val3, Val2, Val1 );
1135 
1136         printf( "%02d = %d\'b", i, 1 << p->nLutSize );
1137         for ( k = p->LutMask - 1; k >= 0; k-- )
1138         {
1139             Val = sat_solver_var_value(p->pSat, iVarStart+k);
1140             if ( i == p->nObjs - 1 && fCompl )
1141                 printf( "%d", !Val );
1142             else
1143                 printf( "%d", Val );
1144         }
1145         if ( i == p->nObjs - 1 && fCompl )
1146             printf( "1(" );
1147         else
1148             printf( "0(" );
1149 
1150         for ( k = p->nLutSize - 1; k >= 0; k-- )
1151         {
1152             iVar = Exa3_ManFindFanin( p, i, k );
1153             if ( iVar >= 0 && iVar < p->nVars )
1154                 printf( " %c", 'a'+iVar );
1155             else
1156                 printf( " %02d", iVar );
1157         }
1158         printf( " )\n" );
1159     }
1160 }
1161 
1162 
1163 /**Function*************************************************************
1164 
1165   Synopsis    []
1166 
1167   Description []
1168 
1169   SideEffects []
1170 
1171   SeeAlso     []
1172 
1173 ***********************************************************************/
Exa3_ManAddCnfStart(Exa3_Man_t * p,int fOnlyAnd)1174 static int Exa3_ManAddCnfStart( Exa3_Man_t * p, int fOnlyAnd )
1175 {
1176     int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m;
1177     // input constraints
1178     for ( i = p->nVars; i < p->nObjs; i++ )
1179     {
1180         int iVarStart = 1 + p->LutMask*(i - p->nVars);
1181         for ( k = 0; k < p->nLutSize; k++ )
1182         {
1183             int nLits = 0;
1184             for ( j = 0; j < p->nObjs; j++ )
1185                 if ( p->VarMarks[i][k][j] )
1186                     pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
1187             assert( nLits > 0 );
1188             // input uniqueness
1189             if ( !sat_solver_addclause( p->pSat, pLits, pLits+nLits ) )
1190                 return 0;
1191             for ( n = 0;   n < nLits; n++ )
1192             for ( m = n+1; m < nLits; m++ )
1193             {
1194                 pLits2[0] = Abc_LitNot(pLits[n]);
1195                 pLits2[1] = Abc_LitNot(pLits[m]);
1196                 if ( !sat_solver_addclause( p->pSat, pLits2, pLits2+2 ) )
1197                     return 0;
1198             }
1199             if ( k == p->nLutSize - 1 )
1200                 break;
1201             // symmetry breaking
1202             for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
1203             for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] )
1204             {
1205                 pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
1206                 pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 );
1207                 if ( !sat_solver_addclause( p->pSat, pLits2, pLits2+2 ) )
1208                     return 0;
1209             }
1210         }
1211         //printf( "Node %d:\n", i );
1212         //sat_solver_flip_print_clause( p->pSat );
1213 #ifdef USE_NODE_ORDER
1214         // node ordering
1215         for ( j = p->nVars; j < i; j++ )
1216         for ( n = 0;   n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
1217         for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
1218         {
1219             pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 );
1220             pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 );
1221             if ( !sat_solver_addclause( p->pSat, pLits2, pLits2+2 ) )
1222                 return 0;
1223         }
1224 #endif
1225         if ( p->nLutSize != 2 )
1226             continue;
1227         // two-input functions
1228         for ( k = 0; k < 3; k++ )
1229         {
1230             pLits[0] = Abc_Var2Lit( iVarStart,   k==1 );
1231             pLits[1] = Abc_Var2Lit( iVarStart+1, k==2 );
1232             pLits[2] = Abc_Var2Lit( iVarStart+2, k!=0 );
1233             if ( !sat_solver_addclause( p->pSat, pLits, pLits+3 ) )
1234                 return 0;
1235         }
1236         if ( fOnlyAnd )
1237         {
1238             pLits[0] = Abc_Var2Lit( iVarStart,   1 );
1239             pLits[1] = Abc_Var2Lit( iVarStart+1, 1 );
1240             pLits[2] = Abc_Var2Lit( iVarStart+2, 0 );
1241             if ( !sat_solver_addclause( p->pSat, pLits, pLits+3 ) )
1242                 return 0;
1243         }
1244     }
1245     // outputs should be used
1246     for ( i = 0; i < p->nObjs - 1; i++ )
1247     {
1248         Vec_Int_t * vArray = Vec_WecEntry(p->vOutLits, i);
1249         assert( Vec_IntSize(vArray) > 0 );
1250         if ( !sat_solver_addclause( p->pSat, Vec_IntArray(vArray), Vec_IntLimit(vArray) ) )
1251             return 0;
1252     }
1253     return 1;
1254 }
Exa3_ManAddCnf(Exa3_Man_t * p,int iMint)1255 static int Exa3_ManAddCnf( Exa3_Man_t * p, int iMint )
1256 {
1257     // save minterm values
1258     int i, k, n, j, Value = Abc_TtGetBit(p->pTruth, iMint);
1259     for ( i = 0; i < p->nVars; i++ )
1260         p->VarVals[i] = (iMint >> i) & 1;
1261     sat_solver_setnvars( p->pSat, p->iVar + (p->nLutSize+1)*p->nNodes );
1262     //printf( "Adding clauses for minterm %d with value %d.\n", iMint, Value );
1263     for ( i = p->nVars; i < p->nObjs; i++ )
1264     {
1265         // fanin connectivity
1266         int iVarStart = 1 + p->LutMask*(i - p->nVars);
1267         int iBaseSatVarI = p->iVar + (p->nLutSize+1)*(i - p->nVars);
1268         for ( k = 0; k < p->nLutSize; k++ )
1269         {
1270             for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
1271             {
1272                 int iBaseSatVarJ = p->iVar + (p->nLutSize+1)*(j - p->nVars);
1273                 for ( n = 0; n < 2; n++ )
1274                 {
1275                     int pLits[3], nLits = 0;
1276                     pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
1277                     pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + k, n );
1278                     if ( j >= p->nVars )
1279                         pLits[nLits++] = Abc_Var2Lit( iBaseSatVarJ + p->nLutSize, !n );
1280                     else if ( p->VarVals[j] == n )
1281                         continue;
1282                     if ( !sat_solver_addclause( p->pSat, pLits, pLits+nLits ) )
1283                         return 0;
1284                 }
1285             }
1286         }
1287         // node functionality
1288         for ( n = 0; n < 2; n++ )
1289         {
1290             if ( i == p->nObjs - 1 && n == Value )
1291                 continue;
1292             for ( k = 0; k <= p->LutMask; k++ )
1293             {
1294                 int pLits[8], nLits = 0;
1295                 if ( k == 0 && n == 1 )
1296                     continue;
1297                 //pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 0, (k&1)  );
1298                 //pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 1, (k>>1) );
1299                 //if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 2, !n );
1300                 for ( j = 0; j < p->nLutSize; j++ )
1301                     pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + j, (k >> j) & 1 );
1302                 if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + j, !n );
1303                 if ( k > 0 )             pLits[nLits++] = Abc_Var2Lit( iVarStart +  k-1,  n );
1304                 assert( nLits <= p->nLutSize+2 );
1305                 if ( !sat_solver_addclause( p->pSat, pLits, pLits+nLits ) )
1306                     return 0;
1307             }
1308         }
1309     }
1310     p->iVar += (p->nLutSize+1)*p->nNodes;
1311     return 1;
1312 }
Exa3_ManExactSynthesis2(Bmc_EsPar_t * pPars)1313 void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars )
1314 {
1315     int i, status, iMint = 1;
1316     abctime clkTotal = Abc_Clock();
1317     Exa3_Man_t * p; int fCompl = 0;
1318     word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr );
1319     assert( pPars->nVars <= 10 );
1320     assert( pPars->nLutSize <= 6 );
1321     p = Exa3_ManAlloc( pPars, pTruth );
1322     if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); }
1323     status = Exa3_ManAddCnfStart( p, pPars->fOnlyAnd );
1324     assert( status );
1325     printf( "Running exact synthesis for %d-input function with %d %d-input LUTs...\n", p->nVars, p->nNodes, p->nLutSize );
1326     for ( i = 0; iMint != -1; i++ )
1327     {
1328         abctime clk = Abc_Clock();
1329         if ( !Exa3_ManAddCnf( p, iMint ) )
1330             break;
1331         status = sat_solver_solve( p->pSat, NULL, NULL, 0, 0, 0, 0 );
1332         if ( pPars->fVerbose )
1333         {
1334             printf( "Iter %3d : ", i );
1335             Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
1336             printf( "  Var =%5d  ", p->iVar );
1337             printf( "Cla =%6d  ", sat_solver_nclauses(p->pSat) );
1338             printf( "Conf =%9d  ", sat_solver_nconflicts(p->pSat) );
1339             Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1340         }
1341         if ( status == l_False )
1342         {
1343             printf( "The problem has no solution.\n" );
1344             break;
1345         }
1346         iMint = Exa3_ManEval( p );
1347     }
1348     if ( iMint == -1 )
1349         Exa3_ManPrintSolution( p, fCompl );
1350     Exa3_ManFree( p );
1351     Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
1352 }
1353 
1354 
1355 ////////////////////////////////////////////////////////////////////////
1356 ///                       END OF FILE                                ///
1357 ////////////////////////////////////////////////////////////////////////
1358 
1359 
1360 ABC_NAMESPACE_IMPL_END
1361 
1362