1 /**CFile****************************************************************
2
3 FileName [intContain.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Interpolation engine.]
8
9 Synopsis [Interpolant containment checking.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 24, 2008.]
16
17 Revision [$Id: intContain.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "intInt.h"
22 #include "proof/fra/fra.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 extern int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames );
31
32 ////////////////////////////////////////////////////////////////////////
33 /// FUNCTION DEFINITIONS ///
34 ////////////////////////////////////////////////////////////////////////
35
36 /**Function*************************************************************
37
38 Synopsis [Checks constainment of two interpolants.]
39
40 Description []
41
42 SideEffects []
43
44 SeeAlso []
45
46 ***********************************************************************/
Inter_ManCheckContainment(Aig_Man_t * pNew,Aig_Man_t * pOld)47 int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld )
48 {
49 Aig_Man_t * pMiter, * pAigTemp;
50 int RetValue;
51 pMiter = Aig_ManCreateMiter( pNew, pOld, 1 );
52 // pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 );
53 // Aig_ManStop( pAigTemp );
54 RetValue = Fra_FraigMiterStatus( pMiter );
55 if ( RetValue == -1 )
56 {
57 pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
58 RetValue = Fra_FraigMiterStatus( pAigTemp );
59 Aig_ManStop( pAigTemp );
60 // RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0, 0, 0 );
61 }
62 assert( RetValue != -1 );
63 Aig_ManStop( pMiter );
64 return RetValue;
65 }
66
67 /**Function*************************************************************
68
69 Synopsis [Checks constainment of two interpolants.]
70
71 Description []
72
73 SideEffects []
74
75 SeeAlso []
76
77 ***********************************************************************/
Inter_ManCheckEquivalence(Aig_Man_t * pNew,Aig_Man_t * pOld)78 int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld )
79 {
80 Aig_Man_t * pMiter, * pAigTemp;
81 int RetValue;
82 pMiter = Aig_ManCreateMiter( pNew, pOld, 0 );
83 // pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 );
84 // Aig_ManStop( pAigTemp );
85 RetValue = Fra_FraigMiterStatus( pMiter );
86 if ( RetValue == -1 )
87 {
88 pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
89 RetValue = Fra_FraigMiterStatus( pAigTemp );
90 Aig_ManStop( pAigTemp );
91 // RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0, 0, 0 );
92 }
93 assert( RetValue != -1 );
94 Aig_ManStop( pMiter );
95 return RetValue;
96 }
97
98
99 /**Function*************************************************************
100
101 Synopsis [Create timeframes of the manager for interpolation.]
102
103 Description [The resulting manager is combinational. The primary inputs
104 corresponding to register outputs are ordered first.]
105
106 SideEffects []
107
108 SeeAlso []
109
110 ***********************************************************************/
Inter_ManFramesLatches(Aig_Man_t * pAig,int nFrames,Vec_Ptr_t ** pvMapReg)111 Aig_Man_t * Inter_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t ** pvMapReg )
112 {
113 Aig_Man_t * pFrames;
114 Aig_Obj_t * pObj, * pObjLi, * pObjLo;
115 int i, f;
116 assert( Saig_ManRegNum(pAig) > 0 );
117 pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
118 // map the constant node
119 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
120 // create variables for register outputs
121 *pvMapReg = Vec_PtrAlloc( (nFrames+1) * Saig_ManRegNum(pAig) );
122 Saig_ManForEachLo( pAig, pObj, i )
123 {
124 pObj->pData = Aig_ObjCreateCi( pFrames );
125 Vec_PtrPush( *pvMapReg, pObj->pData );
126 }
127 // add timeframes
128 for ( f = 0; f < nFrames; f++ )
129 {
130 // create PI nodes for this frame
131 Saig_ManForEachPi( pAig, pObj, i )
132 pObj->pData = Aig_ObjCreateCi( pFrames );
133 // add internal nodes of this frame
134 Aig_ManForEachNode( pAig, pObj, i )
135 pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
136 // save register inputs
137 Saig_ManForEachLi( pAig, pObj, i )
138 pObj->pData = Aig_ObjChild0Copy(pObj);
139 // transfer to register outputs
140 Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
141 {
142 pObjLo->pData = pObjLi->pData;
143 Vec_PtrPush( *pvMapReg, pObjLo->pData );
144 }
145 }
146 return pFrames;
147 }
148
149 /**Function*************************************************************
150
151 Synopsis [Duplicates AIG while mapping PIs into the given array.]
152
153 Description []
154
155 SideEffects []
156
157 SeeAlso []
158
159 ***********************************************************************/
Inter_ManAppendCone(Aig_Man_t * pOld,Aig_Man_t * pNew,Aig_Obj_t ** ppNewPis,int fCompl)160 void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNewPis, int fCompl )
161 {
162 Aig_Obj_t * pObj;
163 int i;
164 assert( Aig_ManCoNum(pOld) == 1 );
165 // create the PIs
166 Aig_ManCleanData( pOld );
167 Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew);
168 Aig_ManForEachCi( pOld, pObj, i )
169 pObj->pData = ppNewPis[i];
170 // duplicate internal nodes
171 Aig_ManForEachNode( pOld, pObj, i )
172 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
173 // add one PO to new
174 pObj = Aig_ManCo( pOld, 0 );
175 Aig_ObjCreateCo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
176 }
177
178
179 /**Function*************************************************************
180
181 Synopsis [Checks constainment of two interpolants inductively.]
182
183 Description []
184
185 SideEffects []
186
187 SeeAlso []
188
189 ***********************************************************************/
Inter_ManCheckInductiveContainment(Aig_Man_t * pTrans,Aig_Man_t * pInter,int nSteps,int fBackward)190 int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward )
191 {
192 Aig_Man_t * pFrames;
193 Aig_Obj_t ** ppNodes;
194 Vec_Ptr_t * vMapRegs;
195 Cnf_Dat_t * pCnf;
196 sat_solver * pSat;
197 int f, nRegs, status;
198 nRegs = Saig_ManRegNum(pTrans);
199 assert( nRegs > 0 );
200 // generate the timeframes
201 pFrames = Inter_ManFramesLatches( pTrans, nSteps, &vMapRegs );
202 assert( Vec_PtrSize(vMapRegs) == (nSteps + 1) * nRegs );
203 // add main constraints to the timeframes
204 ppNodes = (Aig_Obj_t **)Vec_PtrArray(vMapRegs);
205 if ( !fBackward )
206 {
207 // forward inductive check: p -> p -> ... -> !p
208 for ( f = 0; f < nSteps; f++ )
209 Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 );
210 Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 1 );
211 }
212 else
213 {
214 // backward inductive check: p -> !p -> ... -> !p
215 Inter_ManAppendCone( pInter, pFrames, ppNodes + 0 * nRegs, 1 );
216 for ( f = 1; f <= nSteps; f++ )
217 Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 );
218 }
219 Vec_PtrFree( vMapRegs );
220 Aig_ManCleanup( pFrames );
221
222 // convert to CNF
223 pCnf = Cnf_Derive( pFrames, 0 );
224 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
225 // Cnf_DataFree( pCnf );
226 // Aig_ManStop( pFrames );
227
228 if ( pSat == NULL )
229 {
230 Cnf_DataFree( pCnf );
231 Aig_ManStop( pFrames );
232 return 1;
233 }
234
235 // solve the problem
236 status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
237
238 // Inter_ManCheckUniqueness( pTrans, pSat, pCnf, nSteps );
239
240 Cnf_DataFree( pCnf );
241 Aig_ManStop( pFrames );
242
243 sat_solver_delete( pSat );
244 return status == l_False;
245 }
246 ABC_NAMESPACE_IMPL_END
247
248 #include "proof/fra/fra.h"
249
250 ABC_NAMESPACE_IMPL_START
251
252
253 /**Function*************************************************************
254
255 Synopsis [Check if cex satisfies uniqueness constraints.]
256
257 Description []
258
259 SideEffects []
260
261 SeeAlso []
262
263 ***********************************************************************/
Inter_ManCheckUniqueness(Aig_Man_t * p,sat_solver * pSat,Cnf_Dat_t * pCnf,int nFrames)264 int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames )
265 {
266 extern int Fra_SmlNodesCompareInFrame( Fra_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1, int iFrame0, int iFrame1 );
267 extern void Fra_SmlAssignConst( Fra_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame );
268 extern void Fra_SmlSimulateOne( Fra_Sml_t * p );
269
270 Fra_Sml_t * pSml;
271 Vec_Int_t * vPis;
272 Aig_Obj_t * pObj, * pObj0;
273 int i, k, v, iBit, * pCounterEx;
274 int Counter;
275 if ( nFrames == 1 )
276 return 1;
277 // if ( pSat->model.size == 0 )
278
279 // possible consequences here!!!
280 assert( 0 );
281
282 if ( sat_solver_nvars(pSat) == 0 )
283 return 1;
284 // assert( Saig_ManPoNum(p) == 1 );
285 assert( Aig_ManRegNum(p) > 0 );
286 assert( Aig_ManRegNum(p) < Aig_ManCiNum(p) );
287
288 // get the counter-example
289 vPis = Vec_IntAlloc( 100 );
290 Aig_ManForEachCi( pCnf->pMan, pObj, k )
291 Vec_IntPush( vPis, pCnf->pVarNums[Aig_ObjId(pObj)] );
292 assert( Vec_IntSize(vPis) == Aig_ManRegNum(p) + nFrames * Saig_ManPiNum(p) );
293 pCounterEx = Sat_SolverGetModel( pSat, vPis->pArray, vPis->nSize );
294 Vec_IntFree( vPis );
295
296 // start a new sequential simulator
297 pSml = Fra_SmlStart( p, 0, nFrames, 1 );
298 // assign simulation info for the registers
299 iBit = 0;
300 Aig_ManForEachLoSeq( p, pObj, i )
301 Fra_SmlAssignConst( pSml, pObj, pCounterEx[iBit++], 0 );
302 // assign simulation info for the primary inputs
303 for ( i = 0; i < nFrames; i++ )
304 Aig_ManForEachPiSeq( p, pObj, k )
305 Fra_SmlAssignConst( pSml, pObj, pCounterEx[iBit++], i );
306 assert( iBit == Aig_ManCiNum(pCnf->pMan) );
307 // run simulation
308 Fra_SmlSimulateOne( pSml );
309
310 // check if the given output has failed
311 // RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManCo(pAig, 0) );
312 // assert( RetValue );
313
314 // check values at the internal nodes
315 Counter = 0;
316 for ( i = 0; i < nFrames; i++ )
317 for ( k = i+1; k < nFrames; k++ )
318 {
319 for ( v = 0; v < Aig_ManRegNum(p); v++ )
320 {
321 pObj0 = Aig_ManLo(p, v);
322 if ( !Fra_SmlNodesCompareInFrame( pSml, pObj0, pObj0, i, k ) )
323 break;
324 }
325 if ( v == Aig_ManRegNum(p) )
326 Counter++;
327 }
328 printf( "Uniquness does not hold in %d frames.\n", Counter );
329
330 Fra_SmlStop( pSml );
331 ABC_FREE( pCounterEx );
332 return 1;
333 }
334
335 ////////////////////////////////////////////////////////////////////////
336 /// END OF FILE ///
337 ////////////////////////////////////////////////////////////////////////
338
339
340 ABC_NAMESPACE_IMPL_END
341
342