1 /**CFile****************************************************************
2
3 FileName [intM114p.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Interpolation engine.]
8
9 Synopsis [Intepolation using interfaced to MiniSat-1.14p.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 24, 2008.]
16
17 Revision [$Id: intM114p.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "intInt.h"
22 #include "sat/psat/m114p.h"
23
24 #ifdef ABC_USE_LIBRARIES
25
26 ABC_NAMESPACE_IMPL_START
27
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31
32 ////////////////////////////////////////////////////////////////////////
33 /// FUNCTION DEFINITIONS ///
34 ////////////////////////////////////////////////////////////////////////
35
36 /**Function*************************************************************
37
38 Synopsis [Returns the SAT solver for one interpolation run.]
39
40 Description [pInter is the previous interpolant. pAig is one time frame.
41 pFrames is the unrolled time frames.]
42
43 SideEffects []
44
45 SeeAlso []
46
47 ***********************************************************************/
Inter_ManDeriveSatSolverM114p(Aig_Man_t * pInter,Cnf_Dat_t * pCnfInter,Aig_Man_t * pAig,Cnf_Dat_t * pCnfAig,Aig_Man_t * pFrames,Cnf_Dat_t * pCnfFrames,Vec_Int_t ** pvMapRoots,Vec_Int_t ** pvMapVars)48 M114p_Solver_t Inter_ManDeriveSatSolverM114p(
49 Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter,
50 Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig,
51 Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames,
52 Vec_Int_t ** pvMapRoots, Vec_Int_t ** pvMapVars )
53 {
54 M114p_Solver_t pSat;
55 Aig_Obj_t * pObj, * pObj2;
56 int i, Lits[2];
57
58 // sanity checks
59 assert( Aig_ManRegNum(pInter) == 0 );
60 assert( Aig_ManRegNum(pAig) > 0 );
61 assert( Aig_ManRegNum(pFrames) == 0 );
62 assert( Aig_ManCoNum(pInter) == 1 );
63 assert( Aig_ManCoNum(pFrames) == 1 );
64 assert( Aig_ManCiNum(pInter) == Aig_ManRegNum(pAig) );
65 // assert( (Aig_ManCiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
66
67 // prepare CNFs
68 Cnf_DataLift( pCnfAig, pCnfFrames->nVars );
69 Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars );
70
71 *pvMapRoots = Vec_IntAlloc( 10000 );
72 *pvMapVars = Vec_IntAlloc( 0 );
73 Vec_IntFill( *pvMapVars, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars, -1 );
74 for ( i = 0; i < pCnfFrames->nVars; i++ )
75 Vec_IntWriteEntry( *pvMapVars, i, -2 );
76
77 // start the solver
78 pSat = M114p_SolverNew( 1 );
79 M114p_SolverSetVarNum( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars );
80
81 // add clauses of A
82 // interpolant
83 for ( i = 0; i < pCnfInter->nClauses; i++ )
84 {
85 Vec_IntPush( *pvMapRoots, 0 );
86 if ( !M114p_SolverAddClause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) )
87 assert( 0 );
88 }
89 // connector clauses
90 Aig_ManForEachCi( pInter, pObj, i )
91 {
92 pObj2 = Saig_ManLo( pAig, i );
93 Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
94 Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
95 Vec_IntPush( *pvMapRoots, 0 );
96 if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
97 assert( 0 );
98 Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
99 Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
100 Vec_IntPush( *pvMapRoots, 0 );
101 if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
102 assert( 0 );
103 }
104 // one timeframe
105 for ( i = 0; i < pCnfAig->nClauses; i++ )
106 {
107 Vec_IntPush( *pvMapRoots, 0 );
108 if ( !M114p_SolverAddClause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) )
109 assert( 0 );
110 }
111 // connector clauses
112 Aig_ManForEachCi( pFrames, pObj, i )
113 {
114 if ( i == Aig_ManRegNum(pAig) )
115 break;
116 // Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
117 Vec_IntWriteEntry( *pvMapVars, pCnfFrames->pVarNums[pObj->Id], i );
118
119 pObj2 = Saig_ManLi( pAig, i );
120 Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
121 Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
122 Vec_IntPush( *pvMapRoots, 0 );
123 if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
124 assert( 0 );
125 Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
126 Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
127 Vec_IntPush( *pvMapRoots, 0 );
128 if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
129 assert( 0 );
130 }
131 // add clauses of B
132 for ( i = 0; i < pCnfFrames->nClauses; i++ )
133 {
134 Vec_IntPush( *pvMapRoots, 1 );
135 if ( !M114p_SolverAddClause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )
136 {
137 // assert( 0 );
138 break;
139 }
140 }
141 // return clauses to the original state
142 Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
143 Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
144 return pSat;
145 }
146
147
148 /**Function*************************************************************
149
150 Synopsis [Performs one resolution step.]
151
152 Description []
153
154 SideEffects []
155
156 SeeAlso []
157
158 ***********************************************************************/
Inter_ManResolveM114p(Vec_Int_t * vResolvent,int * pLits,int nLits,int iVar)159 int Inter_ManResolveM114p( Vec_Int_t * vResolvent, int * pLits, int nLits, int iVar )
160 {
161 int i, k, iLit = -1, fFound = 0;
162 // find the variable in the clause
163 for ( i = 0; i < vResolvent->nSize; i++ )
164 if ( lit_var(vResolvent->pArray[i]) == iVar )
165 {
166 iLit = vResolvent->pArray[i];
167 vResolvent->pArray[i] = vResolvent->pArray[--vResolvent->nSize];
168 break;
169 }
170 assert( iLit != -1 );
171 // add other variables
172 for ( i = 0; i < nLits; i++ )
173 {
174 if ( lit_var(pLits[i]) == iVar )
175 {
176 assert( iLit == lit_neg(pLits[i]) );
177 fFound = 1;
178 continue;
179 }
180 // check if this literal appears
181 for ( k = 0; k < vResolvent->nSize; k++ )
182 if ( vResolvent->pArray[k] == pLits[i] )
183 break;
184 if ( k < vResolvent->nSize )
185 continue;
186 // add this literal
187 Vec_IntPush( vResolvent, pLits[i] );
188 }
189 assert( fFound );
190 return 1;
191 }
192
193 /**Function*************************************************************
194
195 Synopsis [Computes interpolant using MiniSat-1.14p.]
196
197 Description [Assumes that the solver returned UNSAT and proof
198 logging was enabled. Array vMapRoots maps number of each root clause
199 into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
200 solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
201 where <num> is the var's 0-based number in the ordering of C variables.]
202
203 SideEffects []
204
205 SeeAlso []
206
207 ***********************************************************************/
Inter_ManInterpolateM114pPudlak(M114p_Solver_t s,Vec_Int_t * vMapRoots,Vec_Int_t * vMapVars)208 Aig_Man_t * Inter_ManInterpolateM114pPudlak( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
209 {
210 Aig_Man_t * p;
211 Aig_Obj_t * pInter, * pInter2, * pVar;
212 Vec_Ptr_t * vInters;
213 Vec_Int_t * vLiterals, * vClauses, * vResolvent;
214 int * pLitsNext, nLitsNext, nOffset, iLit;
215 int * pLits, * pClauses, * pVars;
216 int nLits, nVars, i, k, v, iVar;
217 assert( M114p_SolverProofIsReady(s) );
218 vInters = Vec_PtrAlloc( 1000 );
219
220 vLiterals = Vec_IntAlloc( 10000 );
221 vClauses = Vec_IntAlloc( 1000 );
222 vResolvent = Vec_IntAlloc( 100 );
223
224 // create elementary variables
225 p = Aig_ManStart( 10000 );
226 Vec_IntForEachEntry( vMapVars, iVar, i )
227 if ( iVar >= 0 )
228 Aig_IthVar(p, iVar);
229 // process root clauses
230 M114p_SolverForEachRoot( s, &pLits, nLits, i )
231 {
232 if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
233 pInter = Aig_ManConst1(p);
234 else // clause of A
235 pInter = Aig_ManConst0(p);
236 Vec_PtrPush( vInters, pInter );
237
238 // save the root clause
239 Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
240 Vec_IntPush( vLiterals, nLits );
241 for ( v = 0; v < nLits; v++ )
242 Vec_IntPush( vLiterals, pLits[v] );
243 }
244 assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
245
246 // process learned clauses
247 M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
248 {
249 pInter = Vec_PtrEntry( vInters, pClauses[0] );
250
251 // initialize the resolvent
252 nOffset = Vec_IntEntry( vClauses, pClauses[0] );
253 nLitsNext = Vec_IntEntry( vLiterals, nOffset );
254 pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
255 Vec_IntClear( vResolvent );
256 for ( v = 0; v < nLitsNext; v++ )
257 Vec_IntPush( vResolvent, pLitsNext[v] );
258
259 for ( k = 0; k < nVars; k++ )
260 {
261 iVar = Vec_IntEntry( vMapVars, pVars[k] );
262 pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
263
264 // resolve it with the next clause
265 nOffset = Vec_IntEntry( vClauses, pClauses[k+1] );
266 nLitsNext = Vec_IntEntry( vLiterals, nOffset );
267 pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
268 Inter_ManResolveM114p( vResolvent, pLitsNext, nLitsNext, pVars[k] );
269
270 if ( iVar == -1 ) // var of A
271 pInter = Aig_Or( p, pInter, pInter2 );
272 else if ( iVar == -2 ) // var of B
273 pInter = Aig_And( p, pInter, pInter2 );
274 else // var of C
275 {
276 // check polarity of the pivot variable in the clause
277 for ( v = 0; v < nLitsNext; v++ )
278 if ( lit_var(pLitsNext[v]) == pVars[k] )
279 break;
280 assert( v < nLitsNext );
281 pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLitsNext[v]) );
282 pInter = Aig_Mux( p, pVar, pInter, pInter2 );
283 }
284 }
285 Vec_PtrPush( vInters, pInter );
286
287 // store the resulting clause
288 Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
289 Vec_IntPush( vLiterals, Vec_IntSize(vResolvent) );
290 Vec_IntForEachEntry( vResolvent, iLit, v )
291 Vec_IntPush( vLiterals, iLit );
292 }
293 assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
294 assert( Vec_IntSize(vResolvent) == 0 ); // the empty clause
295 Vec_PtrFree( vInters );
296 Vec_IntFree( vLiterals );
297 Vec_IntFree( vClauses );
298 Vec_IntFree( vResolvent );
299 Aig_ObjCreateCo( p, pInter );
300 Aig_ManCleanup( p );
301 return p;
302 }
303
304
305 /**Function*************************************************************
306
307 Synopsis [Computes interpolant using MiniSat-1.14p.]
308
309 Description [Assumes that the solver returned UNSAT and proof
310 logging was enabled. Array vMapRoots maps number of each root clause
311 into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
312 solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
313 where <num> is the var's 0-based number in the ordering of C variables.]
314
315 SideEffects []
316
317 SeeAlso []
318
319 ***********************************************************************/
Inter_ManpInterpolateM114(M114p_Solver_t s,Vec_Int_t * vMapRoots,Vec_Int_t * vMapVars)320 Aig_Man_t * Inter_ManpInterpolateM114( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
321 {
322 Aig_Man_t * p;
323 Aig_Obj_t * pInter, * pInter2, * pVar;
324 Vec_Ptr_t * vInters;
325 int * pLits, * pClauses, * pVars;
326 int nLits, nVars, i, k, iVar;
327 int nClauses;
328
329 nClauses = M114p_SolverProofClauseNum(s);
330
331 assert( M114p_SolverProofIsReady(s) );
332
333 vInters = Vec_PtrAlloc( 1000 );
334 // process root clauses
335 p = Aig_ManStart( 10000 );
336 M114p_SolverForEachRoot( s, &pLits, nLits, i )
337 {
338 if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
339 pInter = Aig_ManConst1(p);
340 else // clause of A
341 {
342 pInter = Aig_ManConst0(p);
343 for ( k = 0; k < nLits; k++ )
344 {
345 iVar = Vec_IntEntry( vMapVars, lit_var(pLits[k]) );
346 if ( iVar < 0 ) // var of A or B
347 continue;
348 // this is a variable of C
349 pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLits[k]) );
350 pInter = Aig_Or( p, pInter, pVar );
351 }
352 }
353 Vec_PtrPush( vInters, pInter );
354 }
355 // assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
356
357 // process learned clauses
358 M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
359 {
360 pInter = Vec_PtrEntry( vInters, pClauses[0] );
361 for ( k = 0; k < nVars; k++ )
362 {
363 iVar = Vec_IntEntry( vMapVars, pVars[k] );
364 pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
365 if ( iVar == -1 ) // var of A
366 pInter = Aig_Or( p, pInter, pInter2 );
367 else // var of B or C
368 pInter = Aig_And( p, pInter, pInter2 );
369 }
370 Vec_PtrPush( vInters, pInter );
371 }
372
373 assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
374 Vec_PtrFree( vInters );
375 Aig_ObjCreateCo( p, pInter );
376 Aig_ManCleanup( p );
377 assert( Aig_ManCheck(p) );
378 return p;
379 }
380
381
382 /**Function*************************************************************
383
384 Synopsis [Performs one SAT run with interpolation.]
385
386 Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
387
388 SideEffects []
389
390 SeeAlso []
391
392 ***********************************************************************/
Inter_ManPerformOneStepM114p(Inter_Man_t * p,int fUsePudlak,int fUseOther)393 int Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther )
394 {
395 M114p_Solver_t pSat;
396 Vec_Int_t * vMapRoots, * vMapVars;
397 clock_t clk;
398 int status, RetValue;
399 assert( p->pInterNew == NULL );
400 // derive the SAT solver
401 pSat = Inter_ManDeriveSatSolverM114p( p->pInter, p->pCnfInter,
402 p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames,
403 &vMapRoots, &vMapVars );
404 // solve the problem
405 clk = clock();
406 status = M114p_SolverSolve( pSat, NULL, NULL, 0 );
407 p->nConfCur = M114p_SolverGetConflictNum( pSat );
408 p->timeSat += clock() - clk;
409 if ( status == 0 )
410 {
411 RetValue = 1;
412 // Inter_ManpInterpolateM114Report( pSat, vMapRoots, vMapVars );
413
414 clk = clock();
415 if ( fUsePudlak )
416 p->pInterNew = Inter_ManInterpolateM114pPudlak( pSat, vMapRoots, vMapVars );
417 else
418 p->pInterNew = Inter_ManpInterpolateM114( pSat, vMapRoots, vMapVars );
419 p->timeInt += clock() - clk;
420 }
421 else if ( status == 1 )
422 {
423 RetValue = 0;
424 }
425 else
426 {
427 RetValue = -1;
428 }
429 M114p_SolverDelete( pSat );
430 Vec_IntFree( vMapRoots );
431 Vec_IntFree( vMapVars );
432 return RetValue;
433 }
434
435 ////////////////////////////////////////////////////////////////////////
436 /// END OF FILE ///
437 ////////////////////////////////////////////////////////////////////////
438
439 ABC_NAMESPACE_IMPL_END
440
441 #endif
442
443
444