1 /**CFile****************************************************************
2
3 FileName [intM114.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Interpolation engine.]
8
9 Synopsis [Intepolation using ABC's proof generator added to MiniSat-1.14c.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 24, 2008.]
16
17 Revision [$Id: intM114.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "intInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis [Returns the SAT solver for one interpolation run.]
37
38 Description [pInter is the previous interpolant. pAig is one time frame.
39 pFrames is the unrolled time frames.]
40
41 SideEffects []
42
43 SeeAlso []
44
45 ***********************************************************************/
Inter_ManDeriveSatSolver(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 * vVarsAB,int fUseBackward)46 sat_solver * Inter_ManDeriveSatSolver(
47 Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter,
48 Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig,
49 Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames,
50 Vec_Int_t * vVarsAB, int fUseBackward )
51 {
52 sat_solver * pSat;
53 Aig_Obj_t * pObj, * pObj2;
54 int i, Lits[2];
55
56 //Aig_ManDumpBlif( pInter, "out_inter.blif", NULL, NULL );
57 //Aig_ManDumpBlif( pAig, "out_aig.blif", NULL, NULL );
58 //Aig_ManDumpBlif( pFrames, "out_frames.blif", NULL, NULL );
59
60 // sanity checks
61 assert( Aig_ManRegNum(pInter) == 0 );
62 assert( Aig_ManRegNum(pAig) > 0 );
63 assert( Aig_ManRegNum(pFrames) == 0 );
64 assert( Aig_ManCoNum(pInter) == 1 );
65 assert( Aig_ManCoNum(pFrames) == fUseBackward? Saig_ManRegNum(pAig) : 1 );
66 assert( fUseBackward || Aig_ManCiNum(pInter) == Aig_ManRegNum(pAig) );
67 // assert( (Aig_ManCiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
68
69 // prepare CNFs
70 Cnf_DataLift( pCnfAig, pCnfFrames->nVars );
71 Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars );
72
73 // start the solver
74 pSat = sat_solver_new();
75 sat_solver_store_alloc( pSat );
76 sat_solver_setnvars( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars );
77
78 // add clauses of A
79 // interpolant
80 for ( i = 0; i < pCnfInter->nClauses; i++ )
81 {
82 if ( !sat_solver_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) )
83 {
84 sat_solver_delete( pSat );
85 // return clauses to the original state
86 Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
87 Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
88 return NULL;
89 }
90 }
91 // connector clauses
92 if ( fUseBackward )
93 {
94 Saig_ManForEachLi( pAig, pObj2, i )
95 {
96 if ( Saig_ManRegNum(pAig) == Aig_ManCiNum(pInter) )
97 pObj = Aig_ManCi( pInter, i );
98 else
99 {
100 assert( Aig_ManCiNum(pAig) == Aig_ManCiNum(pInter) );
101 pObj = Aig_ManCi( pInter, Aig_ManCiNum(pAig)-Saig_ManRegNum(pAig) + i );
102 }
103
104 Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
105 Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
106 if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
107 assert( 0 );
108 Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
109 Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
110 if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
111 assert( 0 );
112 }
113 }
114 else
115 {
116 Aig_ManForEachCi( pInter, pObj, i )
117 {
118 pObj2 = Saig_ManLo( pAig, i );
119
120 Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
121 Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
122 if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
123 assert( 0 );
124 Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
125 Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
126 if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
127 assert( 0 );
128 }
129 }
130 // one timeframe
131 for ( i = 0; i < pCnfAig->nClauses; i++ )
132 {
133 if ( !sat_solver_addclause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) )
134 assert( 0 );
135 }
136 // connector clauses
137 Vec_IntClear( vVarsAB );
138 if ( fUseBackward )
139 {
140 Aig_ManForEachCo( pFrames, pObj, i )
141 {
142 assert( pCnfFrames->pVarNums[pObj->Id] >= 0 );
143 Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
144
145 pObj2 = Saig_ManLo( pAig, i );
146 Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
147 Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
148 if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
149 assert( 0 );
150 Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
151 Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
152 if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
153 assert( 0 );
154 }
155 }
156 else
157 {
158 Aig_ManForEachCi( pFrames, pObj, i )
159 {
160 if ( i == Aig_ManRegNum(pAig) )
161 break;
162 Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
163
164 pObj2 = Saig_ManLi( pAig, i );
165 Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
166 Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
167 if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
168 assert( 0 );
169 Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
170 Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
171 if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
172 assert( 0 );
173 }
174 }
175 // add clauses of B
176 sat_solver_store_mark_clauses_a( pSat );
177 for ( i = 0; i < pCnfFrames->nClauses; i++ )
178 {
179 if ( !sat_solver_addclause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )
180 {
181 pSat->fSolved = 1;
182 break;
183 }
184 }
185 sat_solver_store_mark_roots( pSat );
186 // return clauses to the original state
187 Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
188 Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
189 return pSat;
190 }
191
192 /**Function*************************************************************
193
194 Synopsis [Performs one SAT run with interpolation.]
195
196 Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
197
198 SideEffects []
199
200 SeeAlso []
201
202 ***********************************************************************/
Inter_ManPerformOneStep(Inter_Man_t * p,int fUseBias,int fUseBackward,abctime nTimeNewOut)203 int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, abctime nTimeNewOut )
204 {
205 sat_solver * pSat;
206 void * pSatCnf = NULL;
207 Inta_Man_t * pManInterA;
208 // Intb_Man_t * pManInterB;
209 int * pGlobalVars;
210 int status, RetValue;
211 int i, Var;
212 abctime clk;
213 // assert( p->pInterNew == NULL );
214
215 // derive the SAT solver
216 pSat = Inter_ManDeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB, fUseBackward );
217 if ( pSat == NULL )
218 {
219 p->pInterNew = NULL;
220 return 1;
221 }
222
223 // set runtime limit
224 if ( nTimeNewOut )
225 sat_solver_set_runtime_limit( pSat, nTimeNewOut );
226
227 // collect global variables
228 pGlobalVars = ABC_CALLOC( int, sat_solver_nvars(pSat) );
229 Vec_IntForEachEntry( p->vVarsAB, Var, i )
230 pGlobalVars[Var] = 1;
231 pSat->pGlobalVars = fUseBias? pGlobalVars : NULL;
232
233 // solve the problem
234 clk = Abc_Clock();
235 status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)p->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
236 p->nConfCur = pSat->stats.conflicts;
237 p->timeSat += Abc_Clock() - clk;
238
239 pSat->pGlobalVars = NULL;
240 ABC_FREE( pGlobalVars );
241 if ( status == l_False )
242 {
243 pSatCnf = sat_solver_store_release( pSat );
244 RetValue = 1;
245 }
246 else if ( status == l_True )
247 {
248 RetValue = 0;
249 }
250 else
251 {
252 RetValue = -1;
253 }
254 sat_solver_delete( pSat );
255 if ( pSatCnf == NULL )
256 return RetValue;
257
258 // create the resulting manager
259 clk = Abc_Clock();
260 /*
261 if ( !fUseIp )
262 {
263 pManInterA = Inta_ManAlloc();
264 p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
265 Inta_ManFree( pManInterA );
266 }
267 else
268 {
269 Aig_Man_t * pInterNew2;
270 int RetValue;
271
272 pManInterA = Inta_ManAlloc();
273 p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
274 // Inter_ManVerifyInterpolant1( pManInterA, pSatCnf, p->pInterNew );
275 Inta_ManFree( pManInterA );
276
277 pManInterB = Intb_ManAlloc();
278 pInterNew2 = Intb_ManInterpolate( pManInterB, pSatCnf, p->vVarsAB, 0 );
279 Inter_ManVerifyInterpolant2( pManInterB, pSatCnf, pInterNew2 );
280 Intb_ManFree( pManInterB );
281
282 // check relationship
283 RetValue = Inter_ManCheckEquivalence( pInterNew2, p->pInterNew );
284 if ( RetValue )
285 printf( "Equivalence \"Ip == Im\" holds\n" );
286 else
287 {
288 // printf( "Equivalence \"Ip == Im\" does not hold\n" );
289 RetValue = Inter_ManCheckContainment( pInterNew2, p->pInterNew );
290 if ( RetValue )
291 printf( "Containment \"Ip -> Im\" holds\n" );
292 else
293 printf( "Containment \"Ip -> Im\" does not hold\n" );
294
295 RetValue = Inter_ManCheckContainment( p->pInterNew, pInterNew2 );
296 if ( RetValue )
297 printf( "Containment \"Im -> Ip\" holds\n" );
298 else
299 printf( "Containment \"Im -> Ip\" does not hold\n" );
300 }
301
302 Aig_ManStop( pInterNew2 );
303 }
304 */
305
306 pManInterA = Inta_ManAlloc();
307 p->pInterNew = (Aig_Man_t *)Inta_ManInterpolate( pManInterA, (Sto_Man_t *)pSatCnf, nTimeNewOut, p->vVarsAB, 0 );
308 Inta_ManFree( pManInterA );
309
310 p->timeInt += Abc_Clock() - clk;
311 Sto_ManFree( (Sto_Man_t *)pSatCnf );
312 if ( p->pInterNew == NULL )
313 RetValue = -1;
314 return RetValue;
315 }
316
317 ////////////////////////////////////////////////////////////////////////
318 /// END OF FILE ///
319 ////////////////////////////////////////////////////////////////////////
320
321
322 ABC_NAMESPACE_IMPL_END
323
324