ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
sbdSat.c
Go to the documentation of this file.
1
20
21#include "sbdInt.h"
22#include "misc/util/utilTruth.h"
23
24ABC_NAMESPACE_IMPL_START
25
26
30
31#define MAX_M 8 // max inputs
32#define MAX_N 30 // max nodes
33#define MAX_K 6 // max lutsize
34#define MAX_D 8 // max delays
35
39
40// new AIG manager
41typedef struct Sbd_Pro_t_ Sbd_Pro_t;
42struct Sbd_Pro_t_
43{
44 int nLuts; // LUT count
45 int nSize; // LUT size
46 int nDivs; // divisor count
47 int nVars; // intermediate variables (nLuts * nSize)
48 int nPars; // total parameter count (nLuts * (1 << nSize) + nLuts * nSize * nDivs)
49 int pPars1[SBD_LUTS_MAX][1<<SBD_SIZE_MAX]; // lut parameters
50 int pPars2[SBD_LUTS_MAX][SBD_SIZE_MAX][SBD_DIV_MAX]; // topo parameters
51 int pVars[SBD_LUTS_MAX][SBD_SIZE_MAX+1]; // internal variables
52 int pDivs[SBD_DIV_MAX]; // divisor variables (external)
53};
54
66Vec_Int_t * Sbd_ProblemSetup( Sbd_Pro_t * p, int nLuts, int nSize, int nDivs )
67{
68 Vec_Int_t * vCnf = Vec_IntAlloc( 1000 );
69 int i, k, d, v, n, iVar = 0;
70 assert( nLuts >= 1 && nLuts <= 2 );
71 memset( p, 0, sizeof(Sbd_Pro_t) );
72 p->nLuts = nLuts;
73 p->nSize = nSize;
74 p->nDivs = nDivs;
75 p->nVars = nLuts * nSize;
76 p->nPars = nLuts * (1 << nSize) + nLuts * nSize * nDivs;
77 // set parameters
78 for ( i = 0; i < nLuts; i++ )
79 for ( k = 0; k < (1 << nSize); k++ )
80 p->pPars1[i][k] = iVar++;
81 for ( i = 0; i < nLuts; i++ )
82 for ( k = 0; k < nSize; k++ )
83 for ( d = 0; d < nDivs; d++ )
84 p->pPars2[i][k][d] = iVar++;
85 // set intermediate variables
86 for ( i = 0; i < nLuts; i++ )
87 for ( k = 0; k < nSize; k++ )
88 p->pVars[i][k] = iVar++;
89 // set top variables
90 for ( i = 1; i < nLuts; i++ )
91 p->pVars[i][nSize] = p->pVars[i-1][0];
92 // set divisor variables
93 for ( d = 0; d < nDivs; d++ )
94 p->pDivs[d] = iVar++;
95 assert( iVar == p->nPars + p->nVars + p->nDivs );
96
97 // input compatiblity clauses
98 for ( i = 0; i < nLuts; i++ )
99 for ( k = (i > 0); k < nSize; k++ )
100 for ( d = 0; d < nDivs; d++ )
101 for ( n = 0; n < nDivs; n++ )
102 {
103 if ( n < d )
104 {
105 Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
106 Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][n], 0) );
107 Vec_IntPush( vCnf, -1 );
108 }
109 else if ( k < nSize-1 )
110 {
111 Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
112 Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k+1][n], 0) );
113 Vec_IntPush( vCnf, -1 );
114 }
115 }
116
117 // create LUT clauses
118 for ( i = 0; i < nLuts; i++ )
119 for ( k = 0; k < (1 << nSize); k++ )
120 for ( n = 0; n < 2; n++ )
121 {
122 for ( v = 0; v < nSize; v++ )
123 Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][v], (k >> v) & 1) );
124 Vec_IntPush( vCnf, Abc_Var2Lit(p->pVars[i][nSize], n) );
125 Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], !n) );
126 Vec_IntPush( vCnf, -1 );
127 }
128
129 // create input clauses
130 for ( i = 0; i < nLuts; i++ )
131 for ( k = (i > 0); k < nSize; k++ )
132 for ( d = 0; d < nDivs; d++ )
133 for ( n = 0; n < 2; n++ )
134 {
135 Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
136 Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], n) );
137 Vec_IntPush( vCnf, Abc_Var2Lit(p->pDivs[d], !n) );
138 Vec_IntPush( vCnf, -1 );
139 }
140
141 return vCnf;
142}
143// add clauses to the don't-care computation solver
144void Sbd_ProblemLoad1( Sbd_Pro_t * p, Vec_Int_t * vCnf, int iStartVar, int * pDivVars, int iTopVar, sat_solver * pSat )
145{
146 int pLits[8], nLits, i, k, iLit, RetValue;
147 int ThisTopVar = p->pVars[0][p->nSize];
148 int FirstDivVar = p->nPars + p->nVars;
149 // add clauses
150 for ( i = 0; i < Vec_IntSize(vCnf); i++ )
151 {
152 assert( Vec_IntEntry(vCnf, i) != -1 );
153 for ( k = i+1; k < Vec_IntSize(vCnf); k++ )
154 if ( Vec_IntEntry(vCnf, i) == -1 )
155 break;
156 nLits = 0;
157 Vec_IntForEachEntryStartStop( vCnf, iLit, i, i, k ) {
158 if ( Abc_Lit2Var(iLit) == ThisTopVar )
159 pLits[nLits++] = Abc_Var2Lit( ThisTopVar, Abc_LitIsCompl(iLit) );
160 else if ( Abc_Lit2Var(iLit) >= FirstDivVar )
161 pLits[nLits++] = Abc_Var2Lit( pDivVars[Abc_Lit2Var(iLit)-FirstDivVar], Abc_LitIsCompl(iLit) );
162 else
163 pLits[nLits++] = iLit + 2 * iStartVar;
164 }
165 assert( nLits <= 8 );
166 RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits );
167 assert( RetValue );
168 }
169}
170// add clauses to the functionality evaluation solver
171void Sbd_ProblemLoad2( Sbd_Pro_t * p, Vec_Wec_t * vCnf, int iStartVar, int * pDivVarValues, int iTopVarValue, sat_solver * pSat )
172{
173 Vec_Int_t * vLevel;
174 int pLits[8], nLits, i, k, iLit, RetValue;
175 int ThisTopVar = p->pVars[0][p->nSize];
176 int FirstDivVar = p->nPars + p->nVars;
177 int FirstIntVar = p->nPars;
178 // add clauses
179 Vec_WecForEachLevel( vCnf, vLevel, i )
180 {
181 nLits = 0;
182 Vec_IntForEachEntry( vLevel, iLit, k ) {
183 if ( Abc_Lit2Var(iLit) == ThisTopVar )
184 {
185 if ( Abc_LitIsCompl(iLit) == iTopVarValue )
186 break;
187 continue;
188 }
189 else if ( Abc_Lit2Var(iLit) >= FirstDivVar )
190 {
191 if ( Abc_LitIsCompl(iLit) == pDivVarValues[Abc_Lit2Var(iLit)-FirstDivVar] )
192 break;
193 continue;
194 }
195 else if ( Abc_Lit2Var(iLit) >= FirstIntVar )
196 pLits[nLits++] = iLit + 2 * iStartVar;
197 else
198 pLits[nLits++] = iLit;
199 }
200 if ( k < Vec_IntSize(vLevel) )
201 continue;
202 assert( nLits <= 8 );
203 RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits );
204 assert( RetValue );
205 }
206}
207
208
220sat_solver * Sbd_SolverTopo( int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K], int pVars2[MAX_M+MAX_N][MAX_D], int pDelays[], int Req, int * pnVars ) // inputs, nodes, lutsize
221{
222 sat_solver * pSat = NULL;
223 Vec_Int_t * vTemp = Vec_IntAlloc(100);
224 // assign vars
225 int RetValue, n, i, j, j2, k, k2, d, Count, nVars = 0;
226 for ( n = 0; n < N; n++ )
227 for ( i = 0; i < M+N; i++ )
228 for ( k = 0; k < K; k++ )
229 pVars[n][i][k] = -1;
230 for ( n = 0; n < N; n++ )
231 for ( i = 0; i < M+n; i++ )
232 for ( k = 0; k < K; k++ )
233 pVars[n][i][k] = nVars++;
234 printf( "Number of topo vars = %d.\n", nVars );
235 *pnVars = nVars;
236 // add constraints
237 pSat = sat_solver_new();
238 sat_solver_setnvars( pSat, nVars );
239 // each node is used
240 for ( i = 0; i < M+N-1; i++ )
241 {
242 Vec_IntClear( vTemp );
243 for ( n = 0; n < N; n++ )
244 for ( k = 0; k < K; k++ )
245 if ( pVars[n][i][k] >= 0 )
246 Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][k], 0) );
247 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
248 assert( RetValue );
249 }
250 printf( "Added %d node connectivity constraints.\n", i );
251 // each fanin of each node is connected exactly once
252 Count = 0;
253 for ( n = 0; n < N; n++ )
254 for ( k = 0; k < K; k++ )
255 {
256 // connected
257 Vec_IntClear( vTemp );
258 for ( i = 0; i < M+n; i++ )
259 Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][k], 0) );
260 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
261 assert( RetValue );
262 // exactly once
263 for ( i = 0; i < M+n; i++ )
264 for ( j = i+1; j < M+n; j++ )
265 {
266 Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][k], 1), Abc_Var2Lit(pVars[n][j][k], 1) );
267 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
268 assert( RetValue );
269 Count++;
270 }
271 }
272 printf( "Added %d fanin connectivity constraints.\n", Count );
273 // node fanins are unique
274 Count = 0;
275 for ( n = 0; n < N; n++ )
276 for ( i = 0; i < M+n; i++ )
277 for ( k = 0; k < K; k++ )
278 for ( j = i; j < M+n; j++ )
279 for ( k2 = k+1; k2 < K; k2++ )
280 {
281 Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][k], 1), Abc_Var2Lit(pVars[n][j][k2], 1) );
282 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
283 assert( RetValue );
284 Count++;
285 }
286 printf( "Added %d fanin exclusivity constraints.\n", Count );
287 // nodes are ordered
288 Count = 0;
289 for ( n = 1; n < N; n++ )
290 for ( i = 0; i < M+n-1; i++ )
291 {
292 // first of n cannot be smaller than first of n-1 (but can be equal)
293 for ( j = i+1; j < M+n-1; j++ )
294 {
295 Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][0], 1), Abc_Var2Lit(pVars[n-1][j][0], 1) );
296 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
297 assert( RetValue );
298 Count++;
299 }
300 // if first nodes of n and n-1 are equal, second nodes are ordered
301 Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][0], 1), Abc_Var2Lit(pVars[n-1][i][0], 1) );
302 for ( j = 0; j < i; j++ )
303 for ( j2 = j+1; j2 < i; j2++ )
304 {
305 Vec_IntPushTwo( vTemp, Abc_Var2Lit(pVars[n][j][1], 1), Abc_Var2Lit(pVars[n-1][j2][1], 1) );
306 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
307 assert( RetValue );
308 Vec_IntShrink( vTemp, 2 );
309 Count++;
310 }
311 }
312 printf( "Added %d node ordering constraints.\n", Count );
313 // exclude fanins of two-input nodes
314 Count = 0;
315 if ( K == 2 )
316 for ( n = 1; n < N; n++ )
317 for ( i = M; i < M+n; i++ )
318 for ( j = 0; j < i; j++ )
319 for ( k = 0; k < K; k++ )
320 {
321 Vec_IntClear( vTemp );
322 Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][0], 1) );
323 Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][j][1], 1) );
324 Vec_IntPush( vTemp, Abc_Var2Lit(pVars[i-M][j][k], 1) );
325 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
326 assert( RetValue );
327 Count++;
328 }
329 printf( "Added %d two-node non-triviality constraints.\n", Count );
330
331
332 // assign delay vars
333 assert( Req < MAX_D-1 );
334 for ( i = 0; i < M+N; i++ )
335 for ( d = 0; d < MAX_D; d++ )
336 pVars2[i][d] = nVars++;
337 printf( "Number of total vars = %d.\n", nVars );
338 // set input delays
339 for ( i = 0; i < M; i++ )
340 {
341 assert( pDelays[i] < MAX_D-2 );
342 Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars2[i][pDelays[i]], 0) );
343 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
344 assert( RetValue );
345 }
346 // set output delay
347 for ( k = Req; k < MAX_D; k++ )
348 {
349 Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars2[M+N-1][Req+1], 1) );
350 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
351 assert( RetValue );
352 }
353 // set internal nodes
354 for ( n = 0; n < N; n++ )
355 for ( i = 0; i < M+n; i++ )
356 for ( k = 0; k < K; k++ )
357 for ( d = 0; d < MAX_D-1; d++ )
358 {
359 Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars[n][i][k], 1) );
360 Vec_IntPush( vTemp, Abc_Var2Lit(pVars2[i][d], 1) );
361 Vec_IntPush( vTemp, Abc_Var2Lit(pVars2[M+n][d+1], 0) );
362 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
363 assert( RetValue );
364 }
365
366
367 Vec_IntFree( vTemp );
368 return pSat;
369}
370void Sbd_SolverTopoPrint( sat_solver * pSat, int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K] )
371{
372 int n, i, k;
373 printf( "Solution:\n" );
374 printf( " | " );
375 for ( n = 0; n < N; n++ )
376 printf( "%2d ", M+n );
377 printf( "\n" );
378 for ( i = M+N-2; i >= 0; i-- )
379 {
380 printf( "%2d %c | ", i, i < M ? 'i' : ' ' );
381 for ( n = 0; n < N; n++ )
382 {
383 for ( k = K-1; k >= 0; k-- )
384 if ( pVars[n][i][k] == -1 )
385 printf( " " );
386 else
387 printf( "%c", sat_solver_var_value(pSat, pVars[n][i][k]) ? '*' : '.' );
388 printf( " " );
389 }
390 printf( "\n" );
391 }
392}
393void Sbd_SolverTopoTest()
394{
395 int M = 8; // 6; // inputs
396 int N = 3; // 16; // nodes
397 int K = 4; // 2; // lutsize
398 int status, v, nVars, nIter, nSols = 0;
399 int pVars[MAX_N][MAX_M+MAX_N][MAX_K]; // 20 x 32 x 6 = 3840
400 int pVars2[MAX_M+MAX_N][MAX_D]; // 20 x 32 x 6 = 3840
401 int pDelays[MAX_M] = {1,0,0,0,1};
402 abctime clk = Abc_Clock();
403 Vec_Int_t * vLits = Vec_IntAlloc(100);
404 sat_solver * pSat = Sbd_SolverTopo( M, N, K, pVars, pVars2, pDelays, 2, &nVars );
405 for ( nIter = 0; nIter < 1000000; nIter++ )
406 {
407 // find onset minterm
408 status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
409 if ( status == l_Undef )
410 break;
411 if ( status == l_False )
412 break;
413 assert( status == l_True );
414 nSols++;
415 // print solution
416 if ( nIter < 5 )
417 Sbd_SolverTopoPrint( pSat, M, N, K, pVars );
418 // remember variable values
419 Vec_IntClear( vLits );
420 for ( v = 0; v < nVars; v++ )
421 if ( sat_solver_var_value(pSat, v) )
422 Vec_IntPush( vLits, Abc_Var2Lit(v, 1) );
423 // add breaking clause
424 status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
425 if ( status == 0 )
426 break;
427 //if ( nIter == 5 )
428 // break;
429 }
430 sat_solver_delete( pSat );
431 Vec_IntFree( vLits );
432 printf( "Found %d solutions. ", nSols );
433 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
434}
435
436
437
449void Sbd_SolverSynth( int M, int N, int K, int pLuts[MAX_N][MAX_K] )
450{
451 int Used[MAX_M+MAX_N] = {0};
452 int nUnused = M;
453 int n, iFan0, iFan1;
454 srand( time(NULL) );
455 for ( n = 0; nUnused < N - n; n++ )
456 {
457 iFan0 = iFan1 = 0;
458 while ( (iFan0 = rand() % (M + n)) == (iFan1 = rand() % (M + n)) )
459 ;
460 pLuts[n][0] = iFan0;
461 pLuts[n][1] = iFan1;
462 if ( Used[iFan0] == 0 )
463 {
464 Used[iFan0] = 1;
465 nUnused--;
466 }
467 if ( Used[iFan1] == 0 )
468 {
469 Used[iFan1] = 1;
470 nUnused--;
471 }
472 nUnused++;
473 }
474 if ( nUnused == N - n )
475 {
476 // undo the first one
477 for ( iFan0 = 0; iFan0 < M+n; iFan0++ )
478 if ( Used[iFan0] )
479 {
480 Used[iFan0] = 0;
481 nUnused++;
482 break;
483 }
484
485 }
486 assert( nUnused == N - n + 1 );
487 for ( ; n < N; n++ )
488 {
489 for ( iFan0 = 0; iFan0 < M+n; iFan0++ )
490 if ( Used[iFan0] == 0 )
491 {
492 Used[iFan0] = 1;
493 break;
494 }
495 assert( iFan0 < M+n );
496 for ( iFan1 = 0; iFan1 < M+n; iFan1++ )
497 if ( Used[iFan1] == 0 )
498 {
499 Used[iFan1] = 1;
500 break;
501 }
502 assert( iFan1 < M+n );
503 pLuts[n][0] = iFan0;
504 pLuts[n][1] = iFan1;
505 }
506
507 printf( "{\n" );
508 for ( n = 0; n < N; n++ )
509 printf( " {%d, %d}%s // %d\n", pLuts[n][0], pLuts[n][1], n==N-1 ? "" :",", M+n );
510 printf( "};\n" );
511}
512
513
525word Sbd_SolverTruth( int M, int N, int K, int pLuts[MAX_N][MAX_K], int pValues[MAX_N*((1<<MAX_K)-1)] )
526{
527 int i, k, v, nLutPars = (1 << K) - 1;
528 word Truths[MAX_M+MAX_N];
529 assert( M <= 6 && N <= MAX_N );
530 for ( i = 0; i < M; i++ )
531 Truths[i] = s_Truths6[i];
532 for ( i = 0; i < N; i++ )
533 {
534 word Truth = 0, Mint;
535 for ( k = 1; k <= nLutPars; k++ )
536 {
537 if ( !pValues[i*nLutPars+k-1] )
538 continue;
539 Mint = ~(word)0;
540 for ( v = 0; v < K; v++ )
541 Mint &= ((k >> v) & 1) ? Truths[pLuts[i][v]] : ~Truths[pLuts[i][v]];
542 Truth |= Mint;
543 }
544 Truths[M+i] = Truth;
545 }
546 return Truths[M+N-1];
547}
548word * Sbd_SolverTruthWord( int M, int N, int K, int pLuts[MAX_N][MAX_K], int pValues[MAX_N*((1<<MAX_K)-1)], word * pTruthsElem, int fCompl )
549{
550 int i, k, v, nLutPars = (1 << K) - 1;
551 int nWords = Abc_TtWordNum( M );
552 word * pRes = pTruthsElem + (M+N-1)*nWords;
553 assert( M <= MAX_M && N <= MAX_N );
554 for ( i = 0; i < N; i++ )
555 {
556 word * pMint, * pTruth = pTruthsElem + (M+i)*nWords;
557 Abc_TtClear( pTruth, nWords );
558 for ( k = 1; k <= nLutPars; k++ )
559 {
560 if ( !pValues[i*nLutPars+k-1] )
561 continue;
562 pMint = pTruthsElem + (M+N)*nWords;
563 Abc_TtFill( pMint, nWords );
564 for ( v = 0; v < K; v++ )
565 {
566 word * pFanin = pTruthsElem + pLuts[i][v]*nWords;
567 Abc_TtAndSharp( pMint, pMint, pFanin, nWords, ((k >> v) & 1) == 0 );
568 }
569 Abc_TtOr( pTruth, pTruth, pMint, nWords );
570 }
571 }
572 if ( fCompl )
573 Abc_TtNot( pRes, nWords );
574 return pRes;
575}
576
577
589int Sbd_SolverFunc( int M, int N, int K, int pLuts[MAX_N][MAX_K], word * pTruthInit, int * pValues )
590{
591 int fVerbose = 0;
592 abctime clk = Abc_Clock();
593 abctime clk2, clkOther = 0;
594 sat_solver * pSat = NULL;
595 int nWords = Abc_TtWordNum(M);
596 int pLits[MAX_K+2], pLits2[MAX_K+2], nLits;
597 int nLutPars = (1 << K) - 1, nVars = N * nLutPars;
598 int i, k, m, status, iMint, Iter, fCompl = (int)(pTruthInit[0] & 1);
599 // create truth tables
600 word * pTruthNew, * pTruths = ABC_ALLOC( word, Abc_TtWordNum(MAX_N) * (MAX_M + MAX_N + 1) );
601 Abc_TtElemInit2( pTruths, M );
602 // create solver
603 pSat = sat_solver_new();
604 sat_solver_setnvars( pSat, nVars );
605 printf( "Number of parameters %d x %d = %d.\n", N, nLutPars, nVars );
606 // start with the last minterm
607// iMint = (1 << M) - 1;
608 iMint = 1;
609 for ( Iter = 0; Iter < (1 << M); Iter++ )
610 {
611 // assign the first intermediate variable
612 int nVarStart = sat_solver_nvars(pSat);
613 sat_solver_setnvars( pSat, nVarStart + N - 1 );
614 // add clauses for nodes
615 //if ( fVerbose )
616 printf( "Iter %3d : Mint = %3d. Conflicts =%8d.\n", Iter, iMint, sat_solver_nconflicts(pSat) );
617 for ( i = 0; i < N; i++ )
618 for ( m = 0; m <= nLutPars; m++ )
619 {
620 if ( fVerbose )
621 printf( "i = %d. m = %d.\n", i, m );
622 // selector variables
623 nLits = 0;
624 for ( k = 0; k < K; k++ )
625 {
626 if ( pLuts[i][k] >= M )
627 {
628 assert( pLuts[i][k] - M < N - 1 );
629 pLits[nLits] = pLits2[nLits] = Abc_Var2Lit( nVarStart + pLuts[i][k] - M, (m >> k) & 1 );
630 nLits++;
631 }
632 else if ( ((iMint >> pLuts[i][k]) & 1) != ((m >> k) & 1) )
633 break;
634 }
635 if ( k < K )
636 continue;
637 // add parameter
638 if ( m )
639 {
640 pLits[nLits] = Abc_Var2Lit( i*nLutPars + m-1, 1 );
641 pLits2[nLits] = Abc_Var2Lit( i*nLutPars + m-1, 0 );
642 nLits++;
643 }
644 // node variable
645 if ( i != N - 1 )
646 {
647 pLits[nLits] = Abc_Var2Lit( nVarStart + i, 0 );
648 pLits2[nLits] = Abc_Var2Lit( nVarStart + i, 1 );
649 nLits++;
650 }
651 // add clauses
652 if ( i != N - 1 || Abc_TtGetBit(pTruthInit, iMint) != fCompl )
653 {
654 status = sat_solver_addclause( pSat, pLits2, pLits2 + nLits );
655 if ( status == 0 )
656 {
657 fCompl = -1;
658 goto finish;
659 }
660 }
661 if ( (i != N - 1 || Abc_TtGetBit(pTruthInit, iMint) == fCompl) && m > 0 )
662 {
663 status = sat_solver_addclause( pSat, pLits, pLits + nLits );
664 if ( status == 0 )
665 {
666 fCompl = -1;
667 goto finish;
668 }
669 }
670 }
671
672 // run SAT solver
673 status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
674 if ( status == l_Undef )
675 break;
676 if ( status == l_False )
677 {
678 fCompl = -1;
679 goto finish;
680 }
681 assert( status == l_True );
682
683 // collect values
684 for ( i = 0; i < nVars; i++ )
685 pValues[i] = sat_solver_var_value(pSat, i);
686
687 clk2 = Abc_Clock();
688 pTruthNew = Sbd_SolverTruthWord( M, N, K, pLuts, pValues, pTruths, fCompl );
689 clkOther += Abc_Clock() - clk2;
690
691 if ( fVerbose )
692 {
693 for ( i = 0; i < nVars; i++ )
694 printf( "%d=%d ", i, pValues[i] );
695 printf( " " );
696 for ( i = nVars; i < sat_solver_nvars(pSat); i++ )
697 printf( "%d=%d ", i, sat_solver_var_value(pSat, i) );
698 printf( "\n" );
699 Extra_PrintBinary( stdout, (unsigned *)pTruthInit, (1 << M) ); printf( "\n" );
700 Extra_PrintBinary( stdout, (unsigned *)pTruthNew, (1 << M) ); printf( "\n" );
701 }
702 if ( Abc_TtEqual(pTruthInit, pTruthNew, nWords) )
703 break;
704
705 // get new minterm
706 iMint = Abc_TtFindFirstDiffBit( pTruthInit, pTruthNew, M );
707 }
708finish:
709 printf( "Finished after %d iterations and %d conflicts. ", Iter, sat_solver_nconflicts(pSat) );
710 sat_solver_delete( pSat );
711 ABC_FREE( pTruths );
712 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
713 Abc_PrintTime( 1, "Time", clkOther );
714 return fCompl;
715}
716void Sbd_SolverFuncTest()
717{
718// int M = 4; // 6; // inputs
719// int N = 3; // 16; // nodes
720// int K = 2; // 2; // lutsize
721// word Truth = ~((word)3 << 8);
722// int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9} };
723
724/*
725 int M = 6; // 6; // inputs
726 int N = 19; // 16; // nodes
727 int K = 2; // 2; // lutsize
728 word pTruth[4] = { ABC_CONST(0x9ef7a8d9c7193a0f), 0, 0, 0 };
729 int pLuts[MAX_N][MAX_K] = {
730 {3, 5}, {1, 6}, {0, 5}, {8, 2}, {7, 9},
731 {0, 1}, {2, 11}, {5, 12}, {3, 13}, {1, 14},
732 {10, 15}, {11, 2}, {3, 17}, {9, 18}, {0, 13},
733 {20, 7}, {19, 21}, {4, 16}, {23, 22}
734 };
735*/
736
737/*
738 int M = 6; // 6; // inputs
739 int N = 5; // 16; // nodes
740 int K = 4; // 2; // lutsize
741 word Truth = ABC_CONST(0x9ef7a8d9c7193a0f);
742 int pLuts[MAX_N][MAX_K] = {
743 {0, 1, 2, 3}, // 6
744 {1, 2, 3, 4}, // 7
745 {2, 3, 4, 5}, // 8
746 {0, 1, 4, 5}, // 9
747 {6, 7, 8, 9} // 10
748 };
749*/
750
751/*
752 int M = 8; // 6; // inputs
753 int N = 7; // 16; // nodes
754 int K = 2; // 2; // lutsize
755// word pTruth[4] = { 0, 0, 0, ABC_CONST(0x8000000000000000) };
756// word pTruth[4] = { ABC_CONST(0x0000000000000001), 0, 0, 0 };
757 word pTruth[4] = { 0, 0, 0, ABC_CONST(0x0000000000020000) };
758 int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9}, {10,11}, {12,13} };
759*/
760
761 int M = 8; // 6; // inputs
762 int N = 7; // 16; // nodes
763 int K = 2; // 2; // lutsize
764 word pTruth[4] = { ABC_CONST(0x0000080000020000), ABC_CONST(0x0000000000020000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000020000) };
765 int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9}, {10,11}, {12,13} };
766
767 int pValues[MAX_N*((1<<MAX_K)-1)];
768 int Res, i, k, nLutPars = (1 << K) - 1;
769
770 //Sbd_SolverSynth( M, N, K, pLuts );
771
772 Res = Sbd_SolverFunc( M, N, K, pLuts, pTruth, pValues );
773 if ( Res == -1 )
774 {
775 printf( "Solution does not exist.\n" );
776 return;
777 }
778 printf( "Result (compl = %d):\n", Res );
779 for ( i = 0; i < N; i++ )
780 {
781 for ( k = nLutPars-1; k >= 0; k-- )
782 printf( "%d", pValues[i*nLutPars+k] );
783 printf( "0\n" );
784 }
785}
786
790
791
792ABC_NAMESPACE_IMPL_END
793
nWords
int nWords
Definition abcNpn.c:127
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition abc_global.h:240
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
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
l_True
#define l_True
Definition bmcBmcS.c:35
l_Undef
#define l_Undef
Definition bmcBmcS.c:34
l_False
#define l_False
Definition bmcBmcS.c:36
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
sat_solver
#define sat_solver
Definition cecSatG2.c:34
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
p
Cube * p
Definition exorList.c:222
Extra_PrintBinary
void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
Definition extraUtilFile.c:516
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
M
word M(word f1, word f2, int n)
Definition kitPerm.c:240
sat_solver_new
sat_solver * sat_solver_new(void)
Definition satSolver.c:1137
sat_solver_nconflicts
int sat_solver_nconflicts(sat_solver *s)
Definition satSolver.c:2381
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition satSolver.c:1272
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition satSolver.c:2369
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
SBD_SIZE_MAX
#define SBD_SIZE_MAX
Definition sbdInt.h:56
SBD_DIV_MAX
#define SBD_DIV_MAX
Definition sbdInt.h:57
SBD_LUTS_MAX
#define SBD_LUTS_MAX
Definition sbdInt.h:55
Sbd_ProblemLoad1
void Sbd_ProblemLoad1(Sbd_Pro_t *p, Vec_Int_t *vCnf, int iStartVar, int *pDivVars, int iTopVar, sat_solver *pSat)
Definition sbdSat.c:144
Sbd_SolverTopoTest
void Sbd_SolverTopoTest()
Definition sbdSat.c:393
MAX_N
#define MAX_N
Definition sbdSat.c:32
Sbd_SolverTopoPrint
void Sbd_SolverTopoPrint(sat_solver *pSat, int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K])
Definition sbdSat.c:370
Sbd_SolverTruthWord
word * Sbd_SolverTruthWord(int M, int N, int K, int pLuts[MAX_N][MAX_K], int pValues[MAX_N *((1<< MAX_K) -1)], word *pTruthsElem, int fCompl)
Definition sbdSat.c:548
Sbd_SolverFuncTest
void Sbd_SolverFuncTest()
Definition sbdSat.c:716
Sbd_SolverTopo
sat_solver * Sbd_SolverTopo(int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K], int pVars2[MAX_M+MAX_N][MAX_D], int pDelays[], int Req, int *pnVars)
Definition sbdSat.c:220
Sbd_SolverFunc
int Sbd_SolverFunc(int M, int N, int K, int pLuts[MAX_N][MAX_K], word *pTruthInit, int *pValues)
Definition sbdSat.c:589
Sbd_SolverSynth
void Sbd_SolverSynth(int M, int N, int K, int pLuts[MAX_N][MAX_K])
Definition sbdSat.c:449
Sbd_SolverTruth
word Sbd_SolverTruth(int M, int N, int K, int pLuts[MAX_N][MAX_K], int pValues[MAX_N *((1<< MAX_K) -1)])
Definition sbdSat.c:525
MAX_M
#define MAX_M
DECLARATIONS ///.
Definition sbdSat.c:31
Sbd_Pro_t
struct Sbd_Pro_t_ Sbd_Pro_t
FUNCTION DEFINITIONS ///.
Definition sbdSat.c:41
Sbd_ProblemLoad2
void Sbd_ProblemLoad2(Sbd_Pro_t *p, Vec_Wec_t *vCnf, int iStartVar, int *pDivVarValues, int iTopVarValue, sat_solver *pSat)
Definition sbdSat.c:171
MAX_K
#define MAX_K
Definition sbdSat.c:33
Sbd_ProblemSetup
Vec_Int_t * Sbd_ProblemSetup(Sbd_Pro_t *p, int nLuts, int nSize, int nDivs)
Definition sbdSat.c:66
MAX_D
#define MAX_D
Definition sbdSat.c:34
Sbd_Pro_t_
Definition sbdSat.c:43
Sbd_Pro_t_::pPars2
int pPars2[SBD_LUTS_MAX][SBD_SIZE_MAX][SBD_DIV_MAX]
Definition sbdSat.c:50
Sbd_Pro_t_::pDivs
int pDivs[SBD_DIV_MAX]
Definition sbdSat.c:52
Sbd_Pro_t_::nVars
int nVars
Definition sbdSat.c:47
Sbd_Pro_t_::pVars
int pVars[SBD_LUTS_MAX][SBD_SIZE_MAX+1]
Definition sbdSat.c:51
Sbd_Pro_t_::pPars1
int pPars1[SBD_LUTS_MAX][1<< SBD_SIZE_MAX]
Definition sbdSat.c:49
Sbd_Pro_t_::nLuts
int nLuts
Definition sbdSat.c:44
Sbd_Pro_t_::nDivs
int nDivs
Definition sbdSat.c:46
Sbd_Pro_t_::nSize
int nSize
Definition sbdSat.c:45
Sbd_Pro_t_::nPars
int nPars
Definition sbdSat.c:48
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryStartStop
#define Vec_IntForEachEntryStartStop(vVec, Entry, i, Start, Stop)
Definition vecInt.h:60
Vec_WecForEachLevel
#define Vec_WecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition vecWec.h:55
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42