1 /**CFile****************************************************************
2
3 FileName [ifSat.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [FPGA mapping based on priority cuts.]
8
9 Synopsis [SAT-based evaluation.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - November 21, 2006.]
16
17 Revision [$Id: ifSat.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "if.h"
22 #include "sat/bsat/satSolver.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis [Builds SAT instance for the given structure.]
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
If_ManSatBuildXY(int nLutSize)45 void * If_ManSatBuildXY( int nLutSize )
46 {
47 int nMintsL = (1 << nLutSize);
48 int nMintsF = (1 << (2 * nLutSize - 1));
49 int nVars = 2 * nMintsL + nMintsF;
50 int iVarP0 = 0; // LUT0 parameters (total nMintsL)
51 int iVarP1 = nMintsL; // LUT1 parameters (total nMintsL)
52 int m,iVarM = 2 * nMintsL; // MUX vars (total nMintsF)
53 sat_solver * p = sat_solver_new();
54 sat_solver_setnvars( p, nVars );
55 for ( m = 0; m < nMintsF; m++ )
56 sat_solver_add_mux( p,
57 iVarM + m,
58 iVarP0 + m % nMintsL,
59 iVarP1 + 2 * (m / nMintsL) + 1,
60 iVarP1 + 2 * (m / nMintsL),
61 0, 0, 0, 0 );
62 return p;
63 }
If_ManSatBuildXYZ(int nLutSize)64 void * If_ManSatBuildXYZ( int nLutSize )
65 {
66 int nMintsL = (1 << nLutSize);
67 int nMintsF = (1 << (3 * nLutSize - 2));
68 int nVars = 3 * nMintsL + nMintsF;
69 int iVarP0 = 0; // LUT0 parameters (total nMintsL)
70 int iVarP1 = nMintsL; // LUT1 parameters (total nMintsL)
71 int iVarP2 = 2 * nMintsL; // LUT2 parameters (total nMintsL)
72 int m,iVarM = 3 * nMintsL; // MUX vars (total nMintsF)
73 sat_solver * p = sat_solver_new();
74 sat_solver_setnvars( p, nVars );
75 for ( m = 0; m < nMintsF; m++ )
76 sat_solver_add_mux41( p,
77 iVarM + m,
78 iVarP0 + m % nMintsL,
79 iVarP1 + (m >> nLutSize) % nMintsL,
80 iVarP2 + 4 * (m >> (2 * nLutSize)) + 0,
81 iVarP2 + 4 * (m >> (2 * nLutSize)) + 1,
82 iVarP2 + 4 * (m >> (2 * nLutSize)) + 2,
83 iVarP2 + 4 * (m >> (2 * nLutSize)) + 3 );
84 return p;
85 }
If_ManSatUnbuild(void * p)86 void If_ManSatUnbuild( void * p )
87 {
88 if ( p )
89 sat_solver_delete( (sat_solver *)p );
90 }
91
92 /**Function*************************************************************
93
94 Synopsis [Verification for 6-input function.]
95
96 Description []
97
98 SideEffects []
99
100 SeeAlso []
101
102 ***********************************************************************/
If_ManSat6ComposeLut4(int t,word f[4],int k)103 static word If_ManSat6ComposeLut4( int t, word f[4], int k )
104 {
105 int m, v, nMints = (1 << k);
106 word c, r = 0;
107 assert( k <= 4 );
108 for ( m = 0; m < nMints; m++ )
109 {
110 if ( !((t >> m) & 1) )
111 continue;
112 c = ~(word)0;
113 for ( v = 0; v < k; v++ )
114 c &= ((m >> v) & 1) ? f[v] : ~f[v];
115 r |= c;
116 }
117 return r;
118 }
If_ManSat6Truth(word uBound,word uFree,int * pBSet,int nBSet,int * pSSet,int nSSet,int * pFSet,int nFSet)119 word If_ManSat6Truth( word uBound, word uFree, int * pBSet, int nBSet, int * pSSet, int nSSet, int * pFSet, int nFSet )
120 {
121 word r, q, f[4];
122 int i, k = 0;
123 // bound set vars
124 for ( i = 0; i < nSSet; i++ )
125 f[k++] = s_Truths6[pSSet[i]];
126 for ( i = 0; i < nBSet; i++ )
127 f[k++] = s_Truths6[pBSet[i]];
128 q = If_ManSat6ComposeLut4( (int)(uBound & 0xffff), f, k );
129 // free set vars
130 k = 0;
131 f[k++] = q;
132 for ( i = 0; i < nSSet; i++ )
133 f[k++] = s_Truths6[pSSet[i]];
134 for ( i = 0; i < nFSet; i++ )
135 f[k++] = s_Truths6[pFSet[i]];
136 r = If_ManSat6ComposeLut4( (int)(uFree & 0xffff), f, k );
137 return r;
138 }
139
140 /**Function*************************************************************
141
142 Synopsis [Returns config string for the given truth table.]
143
144 Description []
145
146 SideEffects []
147
148 SeeAlso []
149
150 ***********************************************************************/
If_ManSatCheckXY(void * pSat,int nLutSize,word * pTruth,int nVars,unsigned uSet,word * pTBound,word * pTFree,Vec_Int_t * vLits)151 int If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits )
152 {
153 sat_solver * p = (sat_solver *)pSat;
154 int iBSet, nBSet = 0, pBSet[IF_MAX_FUNC_LUTSIZE];
155 int iSSet, nSSet = 0, pSSet[IF_MAX_FUNC_LUTSIZE];
156 int iFSet, nFSet = 0, pFSet[IF_MAX_FUNC_LUTSIZE];
157 int nMintsL = (1 << nLutSize);
158 int nMintsF = (1 << (2 * nLutSize - 1));
159 int v, Value, m, mNew, nMintsFNew, nMintsLNew;
160 word Res;
161 // collect variable sets
162 Dau_DecSortSet( uSet, nVars, &nBSet, &nSSet, &nFSet );
163 assert( nBSet + nSSet + nFSet == nVars );
164 // check variable bounds
165 assert( nSSet + nBSet <= nLutSize );
166 assert( nLutSize + nSSet + nFSet <= 2*nLutSize - 1 );
167 nMintsFNew = (1 << (nLutSize + nSSet + nFSet));
168 // remap minterms
169 Vec_IntFill( vLits, nMintsF, -1 );
170 for ( m = 0; m < (1 << nVars); m++ )
171 {
172 mNew = iBSet = iSSet = iFSet = 0;
173 for ( v = 0; v < nVars; v++ )
174 {
175 Value = ((uSet >> (v << 1)) & 3);
176 if ( Value == 0 ) // FS
177 {
178 if ( ((m >> v) & 1) )
179 mNew |= 1 << (nLutSize + nSSet + iFSet), pFSet[iFSet] = v;
180 iFSet++;
181 }
182 else if ( Value == 1 ) // BS
183 {
184 if ( ((m >> v) & 1) )
185 mNew |= 1 << (nSSet + iBSet), pBSet[iBSet] = v;
186 iBSet++;
187 }
188 else if ( Value == 3 ) // SS
189 {
190 if ( ((m >> v) & 1) )
191 {
192 mNew |= 1 << iSSet;
193 mNew |= 1 << (nLutSize + iSSet);
194 pSSet[iSSet] = v;
195 }
196 iSSet++;
197 }
198 else assert( Value == 0 );
199 }
200 assert( iBSet == nBSet && iFSet == nFSet );
201 assert( Vec_IntEntry(vLits, mNew) == -1 );
202 Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) );
203 }
204 // find assumptions
205 v = 0;
206 Vec_IntForEachEntry( vLits, Value, m )
207 {
208 // printf( "%d", (Value >= 0) ? Value : 2 );
209 if ( Value >= 0 )
210 Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(2 * nMintsL + m, !Value) );
211 }
212 Vec_IntShrink( vLits, v );
213 // printf( " %d\n", Vec_IntSize(vLits) );
214 // run SAT solver
215 Value = sat_solver_solve( p, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
216 if ( Value != l_True )
217 return 0;
218 if ( pTBound && pTFree )
219 {
220 // collect config
221 assert( nSSet + nBSet <= nLutSize );
222 *pTBound = 0;
223 nMintsLNew = (1 << (nSSet + nBSet));
224 for ( m = 0; m < nMintsLNew; m++ )
225 if ( sat_solver_var_value(p, m) )
226 Abc_TtSetBit( pTBound, m );
227 *pTBound = Abc_Tt6Stretch( *pTBound, nSSet + nBSet );
228 // collect configs
229 assert( nSSet + nFSet + 1 <= nLutSize );
230 *pTFree = 0;
231 nMintsLNew = (1 << (1 + nSSet + nFSet));
232 for ( m = 0; m < nMintsLNew; m++ )
233 if ( sat_solver_var_value(p, nMintsL+m) )
234 Abc_TtSetBit( pTFree, m );
235 *pTFree = Abc_Tt6Stretch( *pTFree, 1 + nSSet + nFSet );
236 if ( nVars != 6 || nLutSize != 4 )
237 return 1;
238 // verify the result
239 Res = If_ManSat6Truth( *pTBound, *pTFree, pBSet, nBSet, pSSet, nSSet, pFSet, nFSet );
240 if ( pTruth[0] != Res )
241 {
242 Dau_DsdPrintFromTruth( pTruth, nVars );
243 Dau_DsdPrintFromTruth( &Res, nVars );
244 Dau_DsdPrintFromTruth( pTBound, nSSet+nBSet );
245 Dau_DsdPrintFromTruth( pTFree, nSSet+nFSet+1 );
246 printf( "Verification failed!\n" );
247 }
248 }
249 return 1;
250 }
251
252 /**Function*************************************************************
253
254 Synopsis [Returns config string for the given truth table.]
255
256 Description []
257
258 SideEffects []
259
260 SeeAlso []
261
262 ***********************************************************************/
If_ManSatCheckXYall_int(void * pSat,int nLutSize,word * pTruth,int nVars,Vec_Int_t * vLits)263 unsigned If_ManSatCheckXYall_int( void * pSat, int nLutSize, word * pTruth, int nVars, Vec_Int_t * vLits )
264 {
265 unsigned uSet = 0;
266 int nTotal = 2 * nLutSize - 1;
267 int nShared = nTotal - nVars;
268 int i[6], s[4];
269 assert( nLutSize >= 2 && nLutSize <= 6 );
270 assert( nLutSize < nVars && nVars <= nTotal );
271 assert( nShared >= 0 && nShared < nLutSize - 1 );
272 if ( nLutSize == 2 )
273 {
274 assert( nShared == 0 );
275 for ( i[0] = 0; i[0] < nVars; i[0]++ )
276 for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
277 {
278 uSet = (1 << (2*i[0])) | (1 << (2*i[1]));
279 if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
280 return uSet;
281 }
282 }
283 else if ( nLutSize == 3 )
284 {
285 for ( i[0] = 0; i[0] < nVars; i[0]++ )
286 for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
287 for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
288 {
289 uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2]));
290 if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
291 return uSet;
292 }
293 if ( nShared < 1 )
294 return 0;
295 for ( i[0] = 0; i[0] < nVars; i[0]++ )
296 for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
297 for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
298 {
299 uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2]));
300 for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
301 if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])), NULL, NULL, vLits) )
302 return uSet | (3 << (2*i[s[0]]));
303 }
304 }
305 else if ( nLutSize == 4 )
306 {
307 for ( i[0] = 0; i[0] < nVars; i[0]++ )
308 for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
309 for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
310 for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
311 {
312 uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3]));
313 if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
314 return uSet;
315 }
316 if ( nShared < 1 )
317 return 0;
318 for ( i[0] = 0; i[0] < nVars; i[0]++ )
319 for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
320 for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
321 for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
322 {
323 uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3]));
324 for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
325 if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])), NULL, NULL, vLits) )
326 return uSet | (3 << (2*i[s[0]]));
327 }
328 if ( nShared < 2 )
329 return 0;
330 for ( i[0] = 0; i[0] < nVars; i[0]++ )
331 for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
332 for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
333 for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
334 {
335 uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3]));
336 {
337 for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
338 for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
339 if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])), NULL, NULL, vLits) )
340 return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]]));
341 }
342 }
343 }
344 else if ( nLutSize == 5 )
345 {
346 for ( i[0] = 0; i[0] < nVars; i[0]++ )
347 for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
348 for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
349 for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
350 for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
351 {
352 uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4]));
353 if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
354 return uSet;
355 }
356 if ( nShared < 1 )
357 return 0;
358 for ( i[0] = 0; i[0] < nVars; i[0]++ )
359 for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
360 for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
361 for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
362 for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
363 {
364 uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4]));
365 for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
366 if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])), NULL, NULL, vLits) )
367 return uSet | (3 << (2*i[s[0]]));
368 }
369 if ( nShared < 2 )
370 return 0;
371 for ( i[0] = 0; i[0] < nVars; i[0]++ )
372 for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
373 for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
374 for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
375 for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
376 {
377 uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4]));
378 for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
379 for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
380 if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])), NULL, NULL, vLits) )
381 return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]]));
382 }
383 if ( nShared < 3 )
384 return 0;
385 for ( i[0] = 0; i[0] < nVars; i[0]++ )
386 for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
387 for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
388 for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
389 for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
390 {
391 uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4]));
392 for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
393 for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
394 for ( s[2] = s[1]+1; s[2] < nLutSize; s[2]++ )
395 if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]])), NULL, NULL, vLits) )
396 return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]]));
397 }
398 }
399 else if ( nLutSize == 6 )
400 {
401 for ( i[0] = 0; i[0] < nVars; i[0]++ )
402 for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
403 for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
404 for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
405 for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
406 for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
407 {
408 uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
409 if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
410 return uSet;
411 }
412 if ( nShared < 1 )
413 return 0;
414 for ( i[0] = 0; i[0] < nVars; i[0]++ )
415 for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
416 for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
417 for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
418 for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
419 for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
420 {
421 uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
422 for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
423 if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])), NULL, NULL, vLits) )
424 return uSet | (3 << (2*i[s[0]]));
425 }
426 if ( nShared < 2 )
427 return 0;
428 for ( i[0] = 0; i[0] < nVars; i[0]++ )
429 for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
430 for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
431 for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
432 for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
433 for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
434 {
435 uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
436 for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
437 for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
438 if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])), NULL, NULL, vLits) )
439 return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]]));
440 }
441 if ( nShared < 3 )
442 return 0;
443 for ( i[0] = 0; i[0] < nVars; i[0]++ )
444 for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
445 for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
446 for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
447 for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
448 for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
449 {
450 uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
451 for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
452 for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
453 for ( s[2] = s[1]+1; s[2] < nLutSize; s[2]++ )
454 if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]])), NULL, NULL, vLits) )
455 return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]]));
456 }
457 if ( nShared < 4 )
458 return 0;
459 for ( i[0] = 0; i[0] < nVars; i[0]++ )
460 for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
461 for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
462 for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
463 for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
464 for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
465 {
466 uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
467 for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
468 for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
469 for ( s[2] = s[1]+1; s[2] < nLutSize; s[2]++ )
470 for ( s[3] = s[1]+1; s[3] < nLutSize; s[3]++ )
471 if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]])) | (3 << (2*i[s[3]])), NULL, NULL, vLits) )
472 return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]])) | (3 << (2*i[s[3]]));
473 }
474 }
475 return 0;
476 }
If_ManSatCheckXYall(void * pSat,int nLutSize,word * pTruth,int nVars,Vec_Int_t * vLits)477 unsigned If_ManSatCheckXYall( void * pSat, int nLutSize, word * pTruth, int nVars, Vec_Int_t * vLits )
478 {
479 unsigned uSet = If_ManSatCheckXYall_int( pSat, nLutSize, pTruth, nVars, vLits );
480 // Dau_DecPrintSet( uSet, nVars, 1 );
481 return uSet;
482 }
483
484 /**Function*************************************************************
485
486 Synopsis [Test procedure.]
487
488 Description []
489
490 SideEffects []
491
492 SeeAlso []
493
494 ***********************************************************************/
If_ManSatTest2()495 void If_ManSatTest2()
496 {
497 int nVars = 6;
498 int nLutSize = 4;
499 sat_solver * p = (sat_solver *)If_ManSatBuildXY( nLutSize );
500 // char * pDsd = "(abcdefg)";
501 // char * pDsd = "([a!bc]d!e)";
502 char * pDsd = "0123456789ABCDEF{abcdef}";
503 word * pTruth = Dau_DsdToTruth( pDsd, nVars );
504 word uBound, uFree;
505 Vec_Int_t * vLits = Vec_IntAlloc( 100 );
506 // unsigned uSet = (1 << 0) | (1 << 2) | (1 << 4) | (1 << 6);
507 // unsigned uSet = (3 << 0) | (1 << 2) | (1 << 8) | (1 << 4);
508 unsigned uSet = (1 << 0) | (3 << 2) | (1 << 4) | (1 << 6);
509 int RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
510 assert( RetValue );
511
512 // Abc_TtPrintBinary( pTruth, nVars );
513 // Abc_TtPrintBinary( &uBound, nLutSize );
514 // Abc_TtPrintBinary( &uFree, nLutSize );
515
516 Dau_DsdPrintFromTruth( pTruth, nVars );
517 Dau_DsdPrintFromTruth( &uBound, nLutSize );
518 Dau_DsdPrintFromTruth( &uFree, nLutSize );
519 sat_solver_delete(p);
520 Vec_IntFree( vLits );
521 }
If_ManSatTest3()522 void If_ManSatTest3()
523 {
524 int nVars = 6;
525 int nLutSize = 4;
526 sat_solver * p = (sat_solver *)If_ManSatBuildXY( nLutSize );
527 // char * pDsd = "(abcdefg)";
528 // char * pDsd = "([a!bc]d!e)";
529 char * pDsd = "0123456789ABCDEF{abcdef}";
530 word * pTruth = Dau_DsdToTruth( pDsd, nVars );
531 Vec_Int_t * vLits = Vec_IntAlloc( 100 );
532 // unsigned uSet = (1 << 0) | (1 << 2) | (1 << 4) | (1 << 6);
533 // unsigned uSet = (3 << 0) | (1 << 2) | (1 << 8) | (1 << 4);
534 unsigned uSet = (1 << 0) | (3 << 2) | (1 << 4) | (1 << 6);
535 uSet = If_ManSatCheckXYall( p, nLutSize, pTruth, nVars, vLits );
536 Dau_DecPrintSet( uSet, nVars, 1 );
537
538 sat_solver_delete(p);
539 Vec_IntFree( vLits );
540 }
541
542 ////////////////////////////////////////////////////////////////////////
543 /// END OF FILE ///
544 ////////////////////////////////////////////////////////////////////////
545
546
547 ABC_NAMESPACE_IMPL_END
548
549