1 /**CFile****************************************************************
2
3 FileName [bmcFx.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [SAT-based bounded model checking.]
8
9 Synopsis [INT-FX: Interpolation-based logic sharing extraction.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: bmcFx.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "bmc.h"
22 #include "misc/vec/vecWec.h"
23 #include "sat/cnf/cnf.h"
24 #include "sat/bsat/satStore.h"
25
26 ABC_NAMESPACE_IMPL_START
27
28
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32
33 ////////////////////////////////////////////////////////////////////////
34 /// FUNCTION DEFINITIONS ///
35 ////////////////////////////////////////////////////////////////////////
36
37 /**Function*************************************************************
38
39 Synopsis [Create hash table to hash divisors.]
40
41 Description []
42
43 SideEffects []
44
45 SeeAlso []
46
47 ***********************************************************************/
48 #define TAB_UNUSED 0x7FFF
49 typedef struct Tab_Obj_t_ Tab_Obj_t; // 16 bytes
50 struct Tab_Obj_t_
51 {
52 int Table;
53 int Next;
54 unsigned Cost : 17;
55 unsigned LitA : 15;
56 unsigned LitB : 15;
57 unsigned LitC : 15;
58 unsigned Func : 2;
59 };
60 typedef struct Tab_Tab_t_ Tab_Tab_t; // 16 bytes
61 struct Tab_Tab_t_
62 {
63 int SizeMask;
64 int nBins;
65 Tab_Obj_t * pBins;
66 };
Tab_TabAlloc(int LogSize)67 static inline Tab_Tab_t * Tab_TabAlloc( int LogSize )
68 {
69 Tab_Tab_t * p = ABC_CALLOC( Tab_Tab_t, 1 );
70 assert( LogSize >= 4 && LogSize <= 31 );
71 p->SizeMask = (1 << LogSize) - 1;
72 p->pBins = ABC_CALLOC( Tab_Obj_t, p->SizeMask + 1 );
73 p->nBins = 1;
74 return p;
75 }
Tab_TabFree(Tab_Tab_t * p)76 static inline void Tab_TabFree( Tab_Tab_t * p )
77 {
78 ABC_FREE( p->pBins );
79 ABC_FREE( p );
80 }
Tab_TabFindBest(Tab_Tab_t * p,int nDivs)81 static inline Vec_Int_t * Tab_TabFindBest( Tab_Tab_t * p, int nDivs )
82 {
83 char * pNames[5] = {"const1", "and", "xor", "mux", "none"};
84 int * pOrder, i;
85 Vec_Int_t * vDivs = Vec_IntAlloc( 100 );
86 Vec_Int_t * vCosts = Vec_IntAlloc( p->nBins );
87 Tab_Obj_t * pEnt, * pLimit = p->pBins + p->nBins;
88 for ( pEnt = p->pBins; pEnt < pLimit; pEnt++ )
89 Vec_IntPush( vCosts, -(int)pEnt->Cost );
90 pOrder = Abc_MergeSortCost( Vec_IntArray(vCosts), Vec_IntSize(vCosts) );
91 for ( i = 0; i < Vec_IntSize(vCosts); i++ )
92 {
93 pEnt = p->pBins + pOrder[i];
94 if ( i == nDivs || pEnt->Cost == 1 )
95 break;
96 printf( "Lit0 = %5d. Lit1 = %5d. Lit2 = %5d. Func = %s. Cost = %3d.\n",
97 pEnt->LitA, pEnt->LitB, pEnt->LitC, pNames[pEnt->Func], pEnt->Cost );
98 Vec_IntPushTwo( vDivs, pEnt->Func, pEnt->LitA );
99 Vec_IntPushTwo( vDivs, pEnt->LitB, pEnt->LitC );
100 }
101 Vec_IntFree( vCosts );
102 ABC_FREE( pOrder );
103 return vDivs;
104 }
Tab_Hash(int LitA,int LitB,int LitC,int Func,int Mask)105 static inline int Tab_Hash( int LitA, int LitB, int LitC, int Func, int Mask )
106 {
107 return (LitA * 50331653 + LitB * 100663319 + LitC * 201326611 + Func * 402653189) & Mask;
108 }
Tab_TabRehash(Tab_Tab_t * p)109 static inline void Tab_TabRehash( Tab_Tab_t * p )
110 {
111 Tab_Obj_t * pEnt, * pLimit, * pBin;
112 assert( p->nBins == p->SizeMask + 1 );
113 // realloc memory
114 p->pBins = ABC_REALLOC( Tab_Obj_t, p->pBins, 2 * (p->SizeMask + 1) );
115 memset( p->pBins + p->SizeMask + 1, 0, sizeof(Tab_Obj_t) * (p->SizeMask + 1) );
116 // clean entries
117 pLimit = p->pBins + p->SizeMask + 1;
118 for ( pEnt = p->pBins; pEnt < pLimit; pEnt++ )
119 pEnt->Table = pEnt->Next = 0;
120 // rehash entries
121 p->SizeMask = 2 * p->SizeMask + 1;
122 for ( pEnt = p->pBins + 1; pEnt < pLimit; pEnt++ )
123 {
124 pBin = p->pBins + Tab_Hash( pEnt->LitA, pEnt->LitB, pEnt->LitC, pEnt->Func, p->SizeMask );
125 pEnt->Next = pBin->Table;
126 pBin->Table = pEnt - p->pBins;
127 assert( !pEnt->Next || pEnt->Next != pBin->Table );
128 }
129 }
Tab_TabEntry(Tab_Tab_t * p,int i)130 static inline Tab_Obj_t * Tab_TabEntry( Tab_Tab_t * p, int i ) { return i ? p->pBins + i : NULL; }
Tab_TabHashAdd(Tab_Tab_t * p,int * pLits,int Func,int Cost)131 static inline int Tab_TabHashAdd( Tab_Tab_t * p, int * pLits, int Func, int Cost )
132 {
133 if ( p->nBins == p->SizeMask + 1 )
134 Tab_TabRehash( p );
135 assert( p->nBins < p->SizeMask + 1 );
136 {
137 Tab_Obj_t * pEnt, * pBin = p->pBins + Tab_Hash(pLits[0], pLits[1], pLits[2], Func, p->SizeMask);
138 for ( pEnt = Tab_TabEntry(p, pBin->Table); pEnt; pEnt = Tab_TabEntry(p, pEnt->Next) )
139 if ( (int)pEnt->LitA == pLits[0] && (int)pEnt->LitB == pLits[1] && (int)pEnt->LitC == pLits[2] && (int)pEnt->Func == Func )
140 { pEnt->Cost += Cost; return 1; }
141 pEnt = p->pBins + p->nBins;
142 pEnt->LitA = pLits[0];
143 pEnt->LitB = pLits[1];
144 pEnt->LitC = pLits[2];
145 pEnt->Func = Func;
146 pEnt->Cost = Cost;
147 pEnt->Next = pBin->Table;
148 pBin->Table = p->nBins++;
149 assert( !pEnt->Next || pEnt->Next != pBin->Table );
150 return 0;
151 }
152 }
153
154
155 /**Function*************************************************************
156
157 Synopsis [Input is four literals. Output is type, polarity and fanins.]
158
159 Description []
160
161 SideEffects []
162
163 SeeAlso []
164
165 ***********************************************************************/
166 // name types
167 typedef enum {
168 DIV_CST = 0, // 0: constant 1
169 DIV_AND, // 1: and (ordered fanins)
170 DIV_XOR, // 2: xor (ordered fanins)
171 DIV_MUX, // 3: mux (c, d1, d0)
172 DIV_NONE // 4: not used
173 } Div_Type_t;
174
Bmc_FxDivOr(int LitA,int LitB,int * pLits,int * pPhase)175 static inline Div_Type_t Bmc_FxDivOr( int LitA, int LitB, int * pLits, int * pPhase )
176 {
177 assert( LitA != LitB );
178 if ( Abc_Lit2Var(LitA) == Abc_Lit2Var(LitB) )
179 return DIV_CST;
180 if ( LitA > LitB )
181 ABC_SWAP( int, LitA, LitB );
182 pLits[0] = Abc_LitNot(LitA);
183 pLits[1] = Abc_LitNot(LitB);
184 *pPhase = 1;
185 return DIV_AND;
186 }
Bmc_FxDivXor(int LitA,int LitB,int * pLits,int * pPhase)187 static inline Div_Type_t Bmc_FxDivXor( int LitA, int LitB, int * pLits, int * pPhase )
188 {
189 assert( LitA != LitB );
190 *pPhase ^= Abc_LitIsCompl(LitA);
191 *pPhase ^= Abc_LitIsCompl(LitB);
192 pLits[0] = Abc_LitRegular(LitA);
193 pLits[1] = Abc_LitRegular(LitB);
194 return DIV_XOR;
195 }
Bmc_FxDivMux(int LitC,int LitCn,int LitT,int LitE,int * pLits,int * pPhase)196 static inline Div_Type_t Bmc_FxDivMux( int LitC, int LitCn, int LitT, int LitE, int * pLits, int * pPhase )
197 {
198 assert( LitC != LitCn );
199 assert( Abc_Lit2Var(LitC) == Abc_Lit2Var(LitCn) );
200 assert( Abc_Lit2Var(LitC) != Abc_Lit2Var(LitT) );
201 assert( Abc_Lit2Var(LitC) != Abc_Lit2Var(LitE) );
202 assert( Abc_Lit2Var(LitC) != Abc_Lit2Var(LitE) );
203 if ( Abc_LitIsCompl(LitC) )
204 {
205 LitC = Abc_LitRegular(LitC);
206 ABC_SWAP( int, LitT, LitE );
207 }
208 if ( Abc_LitIsCompl(LitT) )
209 {
210 *pPhase ^= 1;
211 LitT = Abc_LitNot(LitT);
212 LitE = Abc_LitNot(LitE);
213 }
214 pLits[0] = LitC;
215 pLits[1] = LitT;
216 pLits[2] = LitE;
217 return DIV_MUX;
218 }
Div_FindType(int LitA[2],int LitB[2],int * pLits,int * pPhase)219 static inline Div_Type_t Div_FindType( int LitA[2], int LitB[2], int * pLits, int * pPhase )
220 {
221 *pPhase = 0;
222 pLits[0] = pLits[1] = pLits[2] = TAB_UNUSED;
223 if ( LitA[0] == -1 && LitA[1] == -1 ) return DIV_CST;
224 if ( LitB[0] == -1 && LitB[1] == -1 ) return DIV_CST;
225 assert( LitA[0] >= 0 && LitB[0] >= 0 );
226 assert( LitA[0] != LitB[0] );
227 if ( LitA[1] == -1 && LitB[1] == -1 )
228 return Bmc_FxDivOr( LitA[0], LitB[0], pLits, pPhase );
229 assert( LitA[1] != LitB[1] );
230 if ( LitA[1] == -1 || LitB[1] == -1 )
231 {
232 if ( LitA[1] == -1 )
233 {
234 ABC_SWAP( int, LitA[0], LitB[0] );
235 ABC_SWAP( int, LitA[1], LitB[1] );
236 }
237 assert( LitA[0] >= 0 && LitA[1] >= 0 );
238 assert( LitB[0] >= 0 && LitB[1] == -1 );
239 if ( Abc_Lit2Var(LitB[0]) == Abc_Lit2Var(LitA[0]) )
240 return Bmc_FxDivOr( LitB[0], LitA[1], pLits, pPhase );
241 if ( Abc_Lit2Var(LitB[0]) == Abc_Lit2Var(LitA[1]) )
242 return Bmc_FxDivOr( LitB[0], LitA[0], pLits, pPhase );
243 return DIV_NONE;
244 }
245 if ( Abc_Lit2Var(LitA[0]) == Abc_Lit2Var(LitB[0]) && Abc_Lit2Var(LitA[1]) == Abc_Lit2Var(LitB[1]) )
246 return Bmc_FxDivXor( LitA[0], LitB[1], pLits, pPhase );
247 if ( Abc_Lit2Var(LitA[0]) == Abc_Lit2Var(LitB[0]) )
248 return Bmc_FxDivMux( LitA[0], LitB[0], LitA[1], LitB[1], pLits, pPhase );
249 if ( Abc_Lit2Var(LitA[0]) == Abc_Lit2Var(LitB[1]) )
250 return Bmc_FxDivMux( LitA[0], LitB[1], LitA[1], LitB[0], pLits, pPhase );
251 if ( Abc_Lit2Var(LitA[1]) == Abc_Lit2Var(LitB[0]) )
252 return Bmc_FxDivMux( LitA[1], LitB[0], LitA[0], LitB[1], pLits, pPhase );
253 if ( Abc_Lit2Var(LitA[1]) == Abc_Lit2Var(LitB[1]) )
254 return Bmc_FxDivMux( LitA[1], LitB[1], LitA[0], LitB[0], pLits, pPhase );
255 return DIV_NONE;
256 }
257
258 /**Function*************************************************************
259
260 Synopsis [Returns the number of shared variables, or -1 if failed.]
261
262 Description []
263
264 SideEffects []
265
266 SeeAlso []
267
268 ***********************************************************************/
Div_AddLit(int Lit,int pLits[2])269 static inline int Div_AddLit( int Lit, int pLits[2] )
270 {
271 if ( pLits[0] == -1 )
272 pLits[0] = Lit;
273 else if ( pLits[1] == -1 )
274 pLits[1] = Lit;
275 else return 1;
276 return 0;
277 }
Div_FindDiv(Vec_Int_t * vA,Vec_Int_t * vB,int pLitsA[2],int pLitsB[2])278 int Div_FindDiv( Vec_Int_t * vA, Vec_Int_t * vB, int pLitsA[2], int pLitsB[2] )
279 {
280 int Counter = 0;
281 int * pBegA = vA->pArray, * pEndA = vA->pArray + vA->nSize;
282 int * pBegB = vB->pArray, * pEndB = vB->pArray + vB->nSize;
283 pLitsA[0] = pLitsA[1] = pLitsB[0] = pLitsB[1] = -1;
284 while ( pBegA < pEndA && pBegB < pEndB )
285 {
286 if ( *pBegA == *pBegB )
287 pBegA++, pBegB++, Counter++;
288 else if ( *pBegA < *pBegB )
289 {
290 if ( Div_AddLit( *pBegA++, pLitsA ) )
291 return -1;
292 }
293 else
294 {
295 if ( Div_AddLit( *pBegB++, pLitsB ) )
296 return -1;
297 }
298 }
299 while ( pBegA < pEndA )
300 if ( Div_AddLit( *pBegA++, pLitsA ) )
301 return -1;
302 while ( pBegB < pEndB )
303 if ( Div_AddLit( *pBegB++, pLitsB ) )
304 return -1;
305 return Counter;
306 }
307
Div_CubePrintOne(Vec_Int_t * vCube,Vec_Str_t * vStr,int nVars)308 void Div_CubePrintOne( Vec_Int_t * vCube, Vec_Str_t * vStr, int nVars )
309 {
310 int i, Lit;
311 Vec_StrFill( vStr, nVars, '-' );
312 Vec_IntForEachEntry( vCube, Lit, i )
313 Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit) ? '0' : '1') );
314 printf( "%s\n", Vec_StrArray(vStr) );
315 }
Div_CubePrint(Vec_Wec_t * p,int nVars)316 void Div_CubePrint( Vec_Wec_t * p, int nVars )
317 {
318 Vec_Int_t * vCube; int i;
319 Vec_Str_t * vStr = Vec_StrStart( nVars + 1 );
320 Vec_WecForEachLevel( p, vCube, i )
321 Div_CubePrintOne( vCube, vStr, nVars );
322 Vec_StrFree( vStr );
323 }
324
Div_CubePairs(Vec_Wec_t * p,int nVars,int nDivs)325 Vec_Int_t * Div_CubePairs( Vec_Wec_t * p, int nVars, int nDivs )
326 {
327 int fVerbose = 0;
328 char * pNames[5] = {"const1", "and", "xor", "mux", "none"};
329 Vec_Int_t * vCube1, * vCube2, * vDivs;
330 int i1, i2, i, k, pLitsA[2], pLitsB[2], pLits[4], Type, Phase, nBase, Count = 0;
331 Vec_Str_t * vStr = Vec_StrStart( nVars + 1 );
332 Tab_Tab_t * pTab = Tab_TabAlloc( 5 );
333 Vec_WecForEachLevel( p, vCube1, i )
334 {
335 // add lit pairs
336 pLits[2] = TAB_UNUSED;
337 Vec_IntForEachEntry( vCube1, pLits[0], i1 )
338 Vec_IntForEachEntryStart( vCube1, pLits[1], i2, i1+1 )
339 {
340 Tab_TabHashAdd( pTab, pLits, DIV_AND, 1 );
341 }
342
343 Vec_WecForEachLevelStart( p, vCube2, k, i+1 )
344 {
345 nBase = Div_FindDiv( vCube1, vCube2, pLitsA, pLitsB );
346 if ( nBase == -1 )
347 continue;
348 Type = Div_FindType(pLitsA, pLitsB, pLits, &Phase);
349 if ( Type >= DIV_AND && Type <= DIV_MUX )
350 Tab_TabHashAdd( pTab, pLits, Type, nBase );
351
352 if ( fVerbose )
353 {
354 printf( "Pair %d:\n", Count++ );
355 Div_CubePrintOne( vCube1, vStr, nVars );
356 Div_CubePrintOne( vCube2, vStr, nVars );
357 printf( "Result = %d ", nBase );
358 assert( nBase > 0 );
359
360 printf( "Type = %s ", pNames[Type] );
361 printf( "LitA = %d ", pLits[0] );
362 printf( "LitB = %d ", pLits[1] );
363 printf( "LitC = %d ", pLits[2] );
364 printf( "Phase = %d ", Phase );
365 printf( "\n" );
366 }
367 }
368 }
369 // print the table
370 printf( "Divisors = %d.\n", pTab->nBins );
371 vDivs = Tab_TabFindBest( pTab, nDivs );
372 // cleanup
373 Vec_StrFree( vStr );
374 Tab_TabFree( pTab );
375 return vDivs;
376 }
377
378 /**Function*************************************************************
379
380 Synopsis [Solve the enumeration problem.]
381
382 Description []
383
384 SideEffects []
385
386 SeeAlso []
387
388 ***********************************************************************/
Bmc_FxSolve(sat_solver * pSat,int iOut,int iAuxVar,Vec_Int_t * vVars,int fDumpPla,int fVerbose,int * pCounter,Vec_Wec_t * vCubes)389 int Bmc_FxSolve( sat_solver * pSat, int iOut, int iAuxVar, Vec_Int_t * vVars, int fDumpPla, int fVerbose, int * pCounter, Vec_Wec_t * vCubes )
390 {
391 int nBTLimit = 1000000;
392 int fUseOrder = 1;
393 Vec_Int_t * vLevel = NULL;
394 Vec_Int_t * vLits = Vec_IntAlloc( Vec_IntSize(vVars) );
395 Vec_Int_t * vLits2 = Vec_IntAlloc( Vec_IntSize(vVars) );
396 Vec_Str_t * vCube = Vec_StrStart( Vec_IntSize(vVars)+1 );
397 int status, i, k, n, Lit, Lit2, iVar, nFinal, * pFinal, pLits[2], nIter = 0, RetValue = 0;
398 int Before, After, Total = 0, nLits = 0;
399 pLits[0] = Abc_Var2Lit( iOut + 1, 0 ); // F = 1
400 pLits[1] = Abc_Var2Lit( iAuxVar, 0 ); // iNewLit
401 if ( vCubes )
402 Vec_WecClear( vCubes );
403 if ( fDumpPla )
404 printf( ".i %d\n", Vec_IntSize(vVars) );
405 if ( fDumpPla )
406 printf( ".o %d\n", 1 );
407 while ( 1 )
408 {
409 // find onset minterm
410 status = sat_solver_solve( pSat, pLits, pLits + 2, nBTLimit, 0, 0, 0 );
411 if ( status == l_Undef )
412 { RetValue = -1; break; }
413 if ( status == l_False )
414 { RetValue = 1; break; }
415 assert( status == l_True );
416 // collect divisor literals
417 Vec_IntClear( vLits );
418 Vec_IntPush( vLits, Abc_LitNot(pLits[0]) ); // F = 0
419 // Vec_IntForEachEntryReverse( vVars, iVar, i )
420 Vec_IntForEachEntry( vVars, iVar, i )
421 Vec_IntPush( vLits, sat_solver_var_literal(pSat, iVar) );
422
423 if ( fUseOrder )
424 {
425 //////////////////////////////////////////////////////////////
426 // save these literals
427 Vec_IntClear( vLits2 );
428 Vec_IntAppend( vLits2, vLits );
429 Before = Vec_IntSize(vLits2);
430
431 // try removing literals from the cube
432 Vec_IntForEachEntry( vLits2, Lit2, k )
433 {
434 if ( Lit2 == Abc_LitNot(pLits[0]) )
435 continue;
436 Vec_IntClear( vLits );
437 Vec_IntForEachEntry( vLits2, Lit, n )
438 if ( Lit != -1 && Lit != Lit2 )
439 Vec_IntPush( vLits, Lit );
440 // call sat
441 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
442 if ( status == l_Undef )
443 assert( 0 );
444 if ( status == l_True ) // SAT
445 continue;
446 // Lit2 can be removed
447 Vec_IntWriteEntry( vLits2, k, -1 );
448 }
449
450 // make one final run
451 Vec_IntClear( vLits );
452 Vec_IntForEachEntry( vLits2, Lit2, k )
453 if ( Lit2 != -1 )
454 Vec_IntPush( vLits, Lit2 );
455 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
456 assert( status == l_False );
457
458 // get subset of literals
459 nFinal = sat_solver_final( pSat, &pFinal );
460 //////////////////////////////////////////////////////////////
461 }
462 else
463 {
464 ///////////////////////////////////////////////////////////////
465 // check against offset
466 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
467 if ( status == l_Undef )
468 { RetValue = -1; break; }
469 if ( status == l_True )
470 break;
471 assert( status == l_False );
472 // get subset of literals
473 nFinal = sat_solver_final( pSat, &pFinal );
474 Before = nFinal;
475 //printf( "Before %d. ", nFinal );
476
477 /*
478 // save these literals
479 Vec_IntClear( vLits );
480 for ( i = 0; i < nFinal; i++ )
481 Vec_IntPush( vLits, Abc_LitNot(pFinal[i]) );
482 Vec_IntReverseOrder( vLits );
483
484 // make one final run
485 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
486 assert( status == l_False );
487 nFinal = sat_solver_final( pSat, &pFinal );
488 */
489
490 // save these literals
491 Vec_IntClear( vLits2 );
492 for ( i = 0; i < nFinal; i++ )
493 Vec_IntPush( vLits2, Abc_LitNot(pFinal[i]) );
494 Vec_IntSort( vLits2, 1 );
495
496 // try removing literals from the cube
497 Vec_IntForEachEntry( vLits2, Lit2, k )
498 {
499 if ( Lit2 == Abc_LitNot(pLits[0]) )
500 continue;
501 Vec_IntClear( vLits );
502 Vec_IntForEachEntry( vLits2, Lit, n )
503 if ( Lit != -1 && Lit != Lit2 )
504 Vec_IntPush( vLits, Lit );
505 // call sat
506 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
507 if ( status == l_Undef )
508 assert( 0 );
509 if ( status == l_True ) // SAT
510 continue;
511 // Lit2 can be removed
512 Vec_IntWriteEntry( vLits2, k, -1 );
513 }
514
515 // make one final run
516 Vec_IntClear( vLits );
517 Vec_IntForEachEntry( vLits2, Lit2, k )
518 if ( Lit2 != -1 )
519 Vec_IntPush( vLits, Lit2 );
520 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
521 assert( status == l_False );
522
523 // put them back
524 nFinal = 0;
525 Vec_IntForEachEntry( vLits2, Lit2, k )
526 if ( Lit2 != -1 )
527 pFinal[nFinal++] = Abc_LitNot(Lit2);
528 /////////////////////////////////////////////////////////
529 }
530
531
532 //printf( "After %d. \n", nFinal );
533 After = nFinal;
534 Total += Before - After;
535
536 // get subset of literals
537 //nFinal = sat_solver_final( pSat, &pFinal );
538 // compute cube and add clause
539 Vec_IntClear( vLits );
540 Vec_IntPush( vLits, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
541 if ( fDumpPla )
542 Vec_StrFill( vCube, Vec_IntSize(vVars), '-' );
543 if ( vCubes )
544 vLevel = Vec_WecPushLevel( vCubes );
545 for ( i = 0; i < nFinal; i++ )
546 {
547 if ( pFinal[i] == pLits[0] )
548 continue;
549 Vec_IntPush( vLits, pFinal[i] );
550 iVar = Vec_IntFind( vVars, Abc_Lit2Var(pFinal[i]) );
551 assert( iVar >= 0 && iVar < Vec_IntSize(vVars) );
552 //printf( "%s%d ", Abc_LitIsCompl(pFinal[i]) ? "+":"-", iVar );
553 if ( fDumpPla )
554 Vec_StrWriteEntry( vCube, iVar, (char)(!Abc_LitIsCompl(pFinal[i]) ? '0' : '1') );
555 if ( vLevel )
556 Vec_IntPush( vLevel, Abc_Var2Lit(iVar, !Abc_LitIsCompl(pFinal[i])) );
557 }
558 if ( vCubes )
559 Vec_IntSort( vLevel, 0 );
560 if ( fDumpPla )
561 printf( "%s 1\n", Vec_StrArray(vCube) );
562 status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
563 assert( status );
564 nLits += Vec_IntSize(vLevel);
565 nIter++;
566 }
567 if ( fDumpPla )
568 printf( ".e\n" );
569 if ( fDumpPla )
570 printf( ".p %d\n\n", nIter );
571 if ( fVerbose )
572 printf( "Cubes = %d. Reduced = %d. Lits = %d\n", nIter, Total, nLits );
573 if ( pCounter )
574 *pCounter = nIter;
575 // assert( status == l_True );
576 Vec_IntFree( vLits );
577 Vec_IntFree( vLits2 );
578 Vec_StrFree( vCube );
579 return RetValue;
580 }
581
582 /**Function*************************************************************
583
584 Synopsis []
585
586 Description []
587
588 SideEffects []
589
590 SeeAlso []
591
592 ***********************************************************************/
Bmc_FxCompute(Gia_Man_t * p)593 int Bmc_FxCompute( Gia_Man_t * p )
594 {
595 // create dual-output circuit with on-set/off-set
596 extern Gia_Man_t * Gia_ManDupOnsetOffset( Gia_Man_t * p );
597 Gia_Man_t * p2 = Gia_ManDupOnsetOffset( p );
598 // create SAT solver
599 Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p2, 8, 0, 0, 0, 0 );
600 sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
601 // compute parameters
602 int nOuts = Gia_ManCoNum(p);
603 int nCiVars = Gia_ManCiNum(p), iCiVarBeg = pCnf->nVars - nCiVars;// - 1;
604 int o, i, n, RetValue, nCounter, iAuxVarStart = sat_solver_nvars( pSat );
605 int nCubes[2][2] = {{0}};
606 // create variables
607 Vec_Int_t * vVars = Vec_IntAlloc( nCiVars );
608 for ( n = 0; n < nCiVars; n++ )
609 Vec_IntPush( vVars, iCiVarBeg + n );
610 sat_solver_setnvars( pSat, iAuxVarStart + 4*nOuts );
611 // iterate through outputs
612 for ( o = 0; o < nOuts; o++ )
613 for ( i = 0; i < 2; i++ )
614 for ( n = 0; n < 2; n++ ) // 0=onset, 1=offset
615 // for ( n = 1; n >= 0; n-- ) // 0=onset, 1=offset
616 {
617 printf( "Out %3d %sset ", o, n ? "off" : " on" );
618 RetValue = Bmc_FxSolve( pSat, Abc_Var2Lit(o, n), iAuxVarStart + 2*i*nOuts + Abc_Var2Lit(o, n), vVars, 0, 0, &nCounter, NULL );
619 if ( RetValue == 0 )
620 printf( "Mismatch\n" );
621 if ( RetValue == -1 )
622 printf( "Timeout\n" );
623 nCubes[i][n] += nCounter;
624 }
625 // cleanup
626 Vec_IntFree( vVars );
627 sat_solver_delete( pSat );
628 Cnf_DataFree( pCnf );
629 Gia_ManStop( p2 );
630 printf( "Onset = %5d. Offset = %5d. Onset = %5d. Offset = %5d.\n", nCubes[0][0], nCubes[0][1], nCubes[1][0], nCubes[1][1] );
631 return 1;
632 }
633
634 /**Function*************************************************************
635
636 Synopsis []
637
638 Description []
639
640 SideEffects []
641
642 SeeAlso []
643
644 ***********************************************************************/
Bmc_FxAddClauses(sat_solver * pSat,Vec_Int_t * vDivs,int iCiVarBeg,int iVarStart)645 void Bmc_FxAddClauses( sat_solver * pSat, Vec_Int_t * vDivs, int iCiVarBeg, int iVarStart )
646 {
647 int i, Func, pLits[3], nDivs = Vec_IntSize(vDivs)/4;
648 assert( Vec_IntSize(vDivs) % 4 == 0 );
649 // create new var for each divisor
650 for ( i = 0; i < nDivs; i++ )
651 {
652 Func = Vec_IntEntry(vDivs, 4*i+0);
653 pLits[0] = Vec_IntEntry(vDivs, 4*i+1);
654 pLits[1] = Vec_IntEntry(vDivs, 4*i+2);
655 pLits[2] = Vec_IntEntry(vDivs, 4*i+3);
656 //printf( "Adding clause with vars %d %d -> %d\n", iCiVarBeg + Abc_Lit2Var(pLits[0]), iCiVarBeg + Abc_Lit2Var(pLits[1]), iVarStart + nDivs - 1 - i );
657 if ( Func == DIV_AND )
658 sat_solver_add_and( pSat,
659 iVarStart + nDivs - 1 - i, iCiVarBeg + Abc_Lit2Var(pLits[0]), iCiVarBeg + Abc_Lit2Var(pLits[1]),
660 Abc_LitIsCompl(pLits[0]), Abc_LitIsCompl(pLits[1]), 0 );
661 else if ( Func == DIV_XOR )
662 sat_solver_add_xor( pSat,
663 iVarStart + nDivs - 1 - i, iCiVarBeg + Abc_Lit2Var(pLits[0]), iCiVarBeg + Abc_Lit2Var(pLits[1]), 0 );
664 else if ( Func == DIV_MUX )
665 sat_solver_add_mux( pSat,
666 iVarStart + nDivs - 1 - i, iCiVarBeg + Abc_Lit2Var(pLits[0]), iCiVarBeg + Abc_Lit2Var(pLits[1]), iCiVarBeg + Abc_Lit2Var(pLits[2]),
667 Abc_LitIsCompl(pLits[0]), Abc_LitIsCompl(pLits[1]), Abc_LitIsCompl(pLits[2]), 0 );
668 else assert( 0 );
669 }
670 }
Bmc_FxComputeOne(Gia_Man_t * p,int nIterMax,int nDiv2Add)671 int Bmc_FxComputeOne( Gia_Man_t * p, int nIterMax, int nDiv2Add )
672 {
673 int Extra = 1000;
674 // create SAT solver
675 Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
676 sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
677 // compute parameters
678 int nCiVars = Gia_ManCiNum(p); // PI count
679 int iCiVarBeg = pCnf->nVars - nCiVars;//- 1; // first PI var
680 int iCiVarCur = iCiVarBeg + nCiVars; // current unused PI var
681 int n, Iter, RetValue;
682 // create variables
683 int iAuxVarStart = sat_solver_nvars(pSat) + Extra; // the aux var
684 sat_solver_setnvars( pSat, iAuxVarStart + 1 + nIterMax );
685 for ( Iter = 0; Iter < nIterMax; Iter++ )
686 {
687 Vec_Wec_t * vCubes = Vec_WecAlloc( 1000 );
688 // collect variables
689 Vec_Int_t * vVar2Sat = Vec_IntAlloc( iCiVarCur-iCiVarBeg ), * vDivs;
690 // for ( n = iCiVarCur - 1; n >= iCiVarBeg; n-- )
691 for ( n = iCiVarBeg; n < iCiVarCur; n++ )
692 Vec_IntPush( vVar2Sat, n );
693 // iterate through outputs
694 printf( "\nIteration %d (Aux = %d)\n", Iter, iAuxVarStart + Iter );
695 RetValue = Bmc_FxSolve( pSat, 0, iAuxVarStart + Iter, vVar2Sat, 1, 1, NULL, vCubes );
696 if ( RetValue == 0 )
697 printf( "Mismatch\n" );
698 if ( RetValue == -1 )
699 printf( "Timeout\n" );
700 // print cubes
701 //Div_CubePrint( vCubes, nCiVars );
702 vDivs = Div_CubePairs( vCubes, nCiVars, nDiv2Add );
703 Vec_WecFree( vCubes );
704 // add clauses and update variables
705 Bmc_FxAddClauses( pSat, vDivs, iCiVarBeg, iCiVarCur );
706 iCiVarCur += Vec_IntSize(vDivs)/4;
707 Vec_IntFree( vDivs );
708 // cleanup
709 assert( Vec_IntSize(vVar2Sat) <= nCiVars + Extra );
710 Vec_IntFree( vVar2Sat );
711 }
712 // cleanup
713 sat_solver_delete( pSat );
714 Cnf_DataFree( pCnf );
715 return 1;
716 }
717
718
719 ////////////////////////////////////////////////////////////////////////
720 /// END OF FILE ///
721 ////////////////////////////////////////////////////////////////////////
722
723
724 ABC_NAMESPACE_IMPL_END
725
726