1 /**CFile****************************************************************
2
3 FileName [mfsInter.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [The good old minimization with complete don't-cares.]
8
9 Synopsis [Procedures for computing resub function by interpolation.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: mfsInter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "mfsInt.h"
22 #include "bool/kit/kit.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34
35 /**Function*************************************************************
36
37 Synopsis [Adds constraints for the two-input AND-gate.]
38
39 Description []
40
41 SideEffects []
42
43 SeeAlso []
44
45 ***********************************************************************/
Abc_MfsSatAddXor(sat_solver * pSat,int iVarA,int iVarB,int iVarC)46 int Abc_MfsSatAddXor( sat_solver * pSat, int iVarA, int iVarB, int iVarC )
47 {
48 lit Lits[3];
49
50 Lits[0] = toLitCond( iVarA, 1 );
51 Lits[1] = toLitCond( iVarB, 1 );
52 Lits[2] = toLitCond( iVarC, 1 );
53 if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
54 return 0;
55
56 Lits[0] = toLitCond( iVarA, 1 );
57 Lits[1] = toLitCond( iVarB, 0 );
58 Lits[2] = toLitCond( iVarC, 0 );
59 if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
60 return 0;
61
62 Lits[0] = toLitCond( iVarA, 0 );
63 Lits[1] = toLitCond( iVarB, 1 );
64 Lits[2] = toLitCond( iVarC, 0 );
65 if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
66 return 0;
67
68 Lits[0] = toLitCond( iVarA, 0 );
69 Lits[1] = toLitCond( iVarB, 0 );
70 Lits[2] = toLitCond( iVarC, 1 );
71 if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
72 return 0;
73
74 return 1;
75 }
76
77 /**Function*************************************************************
78
79 Synopsis [Creates miter for checking resubsitution.]
80
81 Description []
82
83 SideEffects []
84
85 SeeAlso []
86
87 ***********************************************************************/
Abc_MfsCreateSolverResub(Mfs_Man_t * p,int * pCands,int nCands,int fInvert)88 sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, int fInvert )
89 {
90 sat_solver * pSat;
91 Aig_Obj_t * pObjPo;
92 int Lits[2], status, iVar, i, c;
93
94 // get the literal for the output of F
95 pObjPo = Aig_ManCo( p->pAigWin, Aig_ManCoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) - 1 );
96 Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], fInvert );
97
98 // collect the outputs of the divisors
99 Vec_IntClear( p->vProjVarsCnf );
100 Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vCos, pObjPo, i, Aig_ManCoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) )
101 {
102 assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
103 Vec_IntPush( p->vProjVarsCnf, p->pCnf->pVarNums[pObjPo->Id] );
104 }
105 assert( Vec_IntSize(p->vProjVarsCnf) == Vec_PtrSize(p->vDivs) );
106
107 // start the solver
108 pSat = sat_solver_new();
109 sat_solver_setnvars( pSat, 2 * p->pCnf->nVars + Vec_PtrSize(p->vDivs) );
110 if ( pCands )
111 sat_solver_store_alloc( pSat );
112
113 // load the first copy of the clauses
114 for ( i = 0; i < p->pCnf->nClauses; i++ )
115 {
116 if ( !sat_solver_addclause( pSat, p->pCnf->pClauses[i], p->pCnf->pClauses[i+1] ) )
117 {
118 sat_solver_delete( pSat );
119 return NULL;
120 }
121 }
122 // add the clause for the first output of F
123 if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
124 {
125 sat_solver_delete( pSat );
126 return NULL;
127 }
128
129 // add one-hotness constraints
130 if ( p->pPars->fOneHotness )
131 {
132 p->pSat = pSat;
133 if ( !Abc_NtkAddOneHotness( p ) )
134 return NULL;
135 p->pSat = NULL;
136 }
137
138 // bookmark the clauses of A
139 if ( pCands )
140 sat_solver_store_mark_clauses_a( pSat );
141
142 // transform the literals
143 for ( i = 0; i < p->pCnf->nLiterals; i++ )
144 p->pCnf->pClauses[0][i] += 2 * p->pCnf->nVars;
145 // load the second copy of the clauses
146 for ( i = 0; i < p->pCnf->nClauses; i++ )
147 {
148 if ( !sat_solver_addclause( pSat, p->pCnf->pClauses[i], p->pCnf->pClauses[i+1] ) )
149 {
150 sat_solver_delete( pSat );
151 return NULL;
152 }
153 }
154 // add one-hotness constraints
155 if ( p->pPars->fOneHotness )
156 {
157 p->pSat = pSat;
158 if ( !Abc_NtkAddOneHotness( p ) )
159 return NULL;
160 p->pSat = NULL;
161 }
162 // transform the literals
163 for ( i = 0; i < p->pCnf->nLiterals; i++ )
164 p->pCnf->pClauses[0][i] -= 2 * p->pCnf->nVars;
165 // add the clause for the second output of F
166 Lits[0] = 2 * p->pCnf->nVars + lit_neg( Lits[0] );
167 if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
168 {
169 sat_solver_delete( pSat );
170 return NULL;
171 }
172
173 if ( pCands )
174 {
175 // add relevant clauses for EXOR gates
176 for ( c = 0; c < nCands; c++ )
177 {
178 // get the variable number of this divisor
179 i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
180 // get the corresponding SAT variable
181 iVar = Vec_IntEntry( p->vProjVarsCnf, i );
182 // add the corresponding EXOR gate
183 if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
184 {
185 sat_solver_delete( pSat );
186 return NULL;
187 }
188 // add the corresponding clause
189 if ( !sat_solver_addclause( pSat, pCands + c, pCands + c + 1 ) )
190 {
191 sat_solver_delete( pSat );
192 return NULL;
193 }
194 }
195 // bookmark the roots
196 sat_solver_store_mark_roots( pSat );
197 }
198 else
199 {
200 // add the clauses for the EXOR gates - and remember their outputs
201 Vec_IntClear( p->vProjVarsSat );
202 Vec_IntForEachEntry( p->vProjVarsCnf, iVar, i )
203 {
204 if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
205 {
206 sat_solver_delete( pSat );
207 return NULL;
208 }
209 Vec_IntPush( p->vProjVarsSat, 2 * p->pCnf->nVars + i );
210 }
211 assert( Vec_IntSize(p->vProjVarsCnf) == Vec_IntSize(p->vProjVarsSat) );
212 // simplify the solver
213 status = sat_solver_simplify(pSat);
214 if ( status == 0 )
215 {
216 // printf( "Abc_MfsCreateSolverResub(): SAT solver construction has failed. Skipping node.\n" );
217 sat_solver_delete( pSat );
218 return NULL;
219 }
220 }
221 return pSat;
222 }
223
224 /**Function*************************************************************
225
226 Synopsis [Performs interpolation.]
227
228 Description [Derives the new function of the node.]
229
230 SideEffects []
231
232 SeeAlso []
233
234 ***********************************************************************/
Abc_NtkMfsInterplateTruth(Mfs_Man_t * p,int * pCands,int nCands,int fInvert)235 unsigned * Abc_NtkMfsInterplateTruth( Mfs_Man_t * p, int * pCands, int nCands, int fInvert )
236 {
237 sat_solver * pSat;
238 Sto_Man_t * pCnf = NULL;
239 unsigned * puTruth;
240 int nFanins, status;
241 int c, i, * pGloVars;
242
243 // derive the SAT solver for interpolation
244 pSat = Abc_MfsCreateSolverResub( p, pCands, nCands, fInvert );
245
246 // solve the problem
247 status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
248 if ( status != l_False )
249 {
250 p->nTimeOuts++;
251 return NULL;
252 }
253 // get the learned clauses
254 pCnf = (Sto_Man_t *)sat_solver_store_release( pSat );
255 sat_solver_delete( pSat );
256
257 // set the global variables
258 pGloVars = Int_ManSetGlobalVars( p->pMan, nCands );
259 for ( c = 0; c < nCands; c++ )
260 {
261 // get the variable number of this divisor
262 i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
263 // get the corresponding SAT variable
264 pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i );
265 }
266
267 // derive the interpolant
268 nFanins = Int_ManInterpolate( p->pMan, pCnf, 0, &puTruth );
269 Sto_ManFree( pCnf );
270 assert( nFanins == nCands );
271 return puTruth;
272 }
273
274 /**Function*************************************************************
275
276 Synopsis [Performs interpolation.]
277
278 Description [Derives the new function of the node.]
279
280 SideEffects []
281
282 SeeAlso []
283
284 ***********************************************************************/
Abc_NtkMfsInterplateEval(Mfs_Man_t * p,int * pCands,int nCands)285 int Abc_NtkMfsInterplateEval( Mfs_Man_t * p, int * pCands, int nCands )
286 {
287 unsigned * pTruth, uTruth0[2], uTruth1[2];
288 int nCounter;
289 pTruth = Abc_NtkMfsInterplateTruth( p, pCands, nCands, 0 );
290 if ( nCands == 6 )
291 {
292 uTruth1[0] = pTruth[0];
293 uTruth1[1] = pTruth[1];
294 }
295 else
296 {
297 uTruth1[0] = pTruth[0];
298 uTruth1[1] = pTruth[0];
299 }
300 pTruth = Abc_NtkMfsInterplateTruth( p, pCands, nCands, 1 );
301 if ( nCands == 6 )
302 {
303 uTruth0[0] = ~pTruth[0];
304 uTruth0[1] = ~pTruth[1];
305 }
306 else
307 {
308 uTruth0[0] = ~pTruth[0];
309 uTruth0[1] = ~pTruth[0];
310 }
311 nCounter = Extra_WordCountOnes( uTruth0[0] ^ uTruth1[0] );
312 nCounter += Extra_WordCountOnes( uTruth0[1] ^ uTruth1[1] );
313 // printf( "%d ", nCounter );
314 return nCounter;
315 }
316
317
318 /**Function*************************************************************
319
320 Synopsis [Performs interpolation.]
321
322 Description [Derives the new function of the node.]
323
324 SideEffects []
325
326 SeeAlso []
327
328 ***********************************************************************/
Abc_NtkMfsInterplate(Mfs_Man_t * p,int * pCands,int nCands)329 Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
330 {
331 extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
332 int fDumpFile = 0;
333 char FileName[32];
334 sat_solver * pSat;
335 Sto_Man_t * pCnf = NULL;
336 unsigned * puTruth;
337 Kit_Graph_t * pGraph;
338 Hop_Obj_t * pFunc;
339 int nFanins, status;
340 int c, i, * pGloVars;
341 // abctime clk = Abc_Clock();
342 // p->nDcMints += Abc_NtkMfsInterplateEval( p, pCands, nCands );
343
344 // derive the SAT solver for interpolation
345 pSat = Abc_MfsCreateSolverResub( p, pCands, nCands, 0 );
346
347 // dump CNF file (remember to uncomment two-lit clases in clause_create_new() in 'satSolver.c')
348 if ( fDumpFile )
349 {
350 static int Counter = 0;
351 sprintf( FileName, "cnf\\pj1_if6_mfs%03d.cnf", Counter++ );
352 Sat_SolverWriteDimacs( pSat, FileName, NULL, NULL, 1 );
353 }
354
355 // solve the problem
356 status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
357 if ( fDumpFile )
358 printf( "File %s has UNSAT problem with %d conflicts.\n", FileName, (int)pSat->stats.conflicts );
359 if ( status != l_False )
360 {
361 p->nTimeOuts++;
362 return NULL;
363 }
364 //printf( "%d\n", pSat->stats.conflicts );
365 // ABC_PRT( "S", Abc_Clock() - clk );
366 // get the learned clauses
367 pCnf = (Sto_Man_t *)sat_solver_store_release( pSat );
368 sat_solver_delete( pSat );
369
370 // set the global variables
371 pGloVars = Int_ManSetGlobalVars( p->pMan, nCands );
372 for ( c = 0; c < nCands; c++ )
373 {
374 // get the variable number of this divisor
375 i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
376 // get the corresponding SAT variable
377 pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i );
378 }
379
380 // derive the interpolant
381 nFanins = Int_ManInterpolate( p->pMan, pCnf, 0, &puTruth );
382 Sto_ManFree( pCnf );
383 assert( nFanins == nCands );
384
385 // transform interpolant into AIG
386 pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
387 pFunc = Kit_GraphToHop( (Hop_Man_t *)p->pNtk->pManFunc, pGraph );
388 Kit_GraphFree( pGraph );
389 return pFunc;
390 }
391
392 ////////////////////////////////////////////////////////////////////////
393 /// END OF FILE ///
394 ////////////////////////////////////////////////////////////////////////
395
396
397 ABC_NAMESPACE_IMPL_END
398
399