ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
ifSat.c
Go to the documentation of this file.
1
20
21#include "if.h"
22#include "sat/bsat/satSolver.h"
23
24ABC_NAMESPACE_IMPL_START
25
29
33
45void * 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}
64void * 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}
86void If_ManSatUnbuild( void * p )
87{
88 if ( p )
89 sat_solver_delete( (sat_solver *)p );
90}
91
103static 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}
119word 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
151int 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
263unsigned 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}
477unsigned 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
495void 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}
522void 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
545
546
547ABC_NAMESPACE_IMPL_END
548
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
nTotal
int nTotal
DECLARATIONS ///.
Definition cutTruth.c:37
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
sat_solver
#define sat_solver
Definition cecSatG2.c:34
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
Dau_DsdToTruth
word * Dau_DsdToTruth(char *p, int nVars)
Definition dauDsd.c:609
Dau_DecPrintSet
void Dau_DecPrintSet(unsigned set, int nVars, int fNewLine)
Definition dauNonDsd.c:390
Dau_DsdPrintFromTruth
void Dau_DsdPrintFromTruth(word *pTruth, int nVarsInit)
Definition dauDsd.c:1968
Dau_DecSortSet
void Dau_DecSortSet(unsigned set, int nVars, int *pnUnique, int *pnShared, int *pnFree)
Definition dauNonDsd.c:371
p
Cube * p
Definition exorList.c:222
If_ManSatBuildXY
ABC_NAMESPACE_IMPL_START void * If_ManSatBuildXY(int nLutSize)
DECLARATIONS ///.
Definition ifSat.c:45
If_ManSat6Truth
word If_ManSat6Truth(word uBound, word uFree, int *pBSet, int nBSet, int *pSSet, int nSSet, int *pFSet, int nFSet)
Definition ifSat.c:119
If_ManSatCheckXYall
unsigned If_ManSatCheckXYall(void *pSat, int nLutSize, word *pTruth, int nVars, Vec_Int_t *vLits)
Definition ifSat.c:477
If_ManSatTest3
void If_ManSatTest3()
Definition ifSat.c:522
If_ManSatCheckXYall_int
unsigned If_ManSatCheckXYall_int(void *pSat, int nLutSize, word *pTruth, int nVars, Vec_Int_t *vLits)
Definition ifSat.c:263
If_ManSatCheckXY
int If_ManSatCheckXY(void *pSat, int nLutSize, word *pTruth, int nVars, unsigned uSet, word *pTBound, word *pTFree, Vec_Int_t *vLits)
Definition ifSat.c:151
If_ManSatUnbuild
void If_ManSatUnbuild(void *p)
Definition ifSat.c:86
If_ManSatBuildXYZ
void * If_ManSatBuildXYZ(int nLutSize)
Definition ifSat.c:64
If_ManSatTest2
void If_ManSatTest2()
Definition ifSat.c:495
IF_MAX_FUNC_LUTSIZE
#define IF_MAX_FUNC_LUTSIZE
Definition if.h:55
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
sat_solver_new
sat_solver * sat_solver_new(void)
Definition satSolver.c:1137
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition satSolver.c:1272
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
assert
#define assert(ex)
Definition util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54