1 /**CFile****************************************************************
2
3 FileName [cecSat.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Combinational equivalence checking.]
8
9 Synopsis [Detection of structural isomorphism.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: cecSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "aig/gia/gia.h"
22 #include "misc/util/utilTruth.h"
23 #include "sat/satoko/satoko.h"
24 #include "cec.h"
25
26 ABC_NAMESPACE_IMPL_START
27
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31
32 // sweeping manager
33 typedef struct Cec2_Par_t_ Cec2_Par_t;
34 struct Cec2_Par_t_
35 {
36 int nSimWords; // simulation words
37 int nSimRounds; // simulation rounds
38 int nItersMax; // max number of iterations
39 int nConfLimit; // SAT solver conflict limit
40 int fIsMiter; // this is a miter
41 int fUseCones; // use logic cones
42 int fVeryVerbose; // verbose stats
43 int fVerbose; // verbose stats
44 };
45
46 // SAT solving manager
47 typedef struct Cec2_Man_t_ Cec2_Man_t;
48 struct Cec2_Man_t_
49 {
50 Cec2_Par_t * pPars; // parameters
51 Gia_Man_t * pAig; // user's AIG
52 Gia_Man_t * pNew; // internal AIG
53 // SAT solving
54 satoko_t * pSat; // SAT solver
55 Vec_Ptr_t * vFrontier; // CNF construction
56 Vec_Ptr_t * vFanins; // CNF construction
57 Vec_Wrd_t * vSims; // CI simulation info
58 Vec_Int_t * vNodesNew; // nodes
59 Vec_Int_t * vSatVars; // nodes
60 Vec_Int_t * vObjSatPairs; // nodes
61 Vec_Int_t * vCexTriples; // nodes
62 // statistics
63 int nPatterns;
64 int nSatSat;
65 int nSatUnsat;
66 int nSatUndec;
67 abctime timeSatSat;
68 abctime timeSatUnsat;
69 abctime timeSatUndec;
70 abctime timeSim;
71 abctime timeRefine;
72 abctime timeExtra;
73 abctime timeStart;
74 };
75
Cec2_ObjSatId(Gia_Man_t * p,Gia_Obj_t * pObj)76 static inline int Cec2_ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjCopy2Array(p, Gia_ObjId(p, pObj)); }
Cec2_ObjSetSatId(Gia_Man_t * p,Gia_Obj_t * pObj,int Num)77 static inline int Cec2_ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num ) { assert(Cec2_ObjSatId(p, pObj) == -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), Num); return Num; }
Cec2_ObjCleanSatId(Gia_Man_t * p,Gia_Obj_t * pObj)78 static inline void Cec2_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(Cec2_ObjSatId(p, pObj) != -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), -1); }
79
80 ////////////////////////////////////////////////////////////////////////
81 /// FUNCTION DEFINITIONS ///
82 ////////////////////////////////////////////////////////////////////////
83
84 /**Function*************************************************************
85
86 Synopsis [Sets parameter defaults.]
87
88 Description []
89
90 SideEffects []
91
92 SeeAlso []
93
94 ***********************************************************************/
Cec2_SetDefaultParams(Cec2_Par_t * p)95 void Cec2_SetDefaultParams( Cec2_Par_t * p )
96 {
97 memset( p, 0, sizeof(Cec2_Par_t) );
98 p->nSimWords = 12; // simulation words
99 p->nSimRounds = 4; // simulation rounds
100 p->nItersMax = 10; // max number of iterations
101 p->nConfLimit = 1000; // conflict limit at a node
102 p->fIsMiter = 0; // this is a miter
103 p->fUseCones = 1; // use logic cones
104 p->fVeryVerbose = 0; // verbose stats
105 p->fVerbose = 0; // verbose stats
106 }
107
108 /**Function*************************************************************
109
110 Synopsis [Adds clauses to the solver.]
111
112 Description []
113
114 SideEffects []
115
116 SeeAlso []
117
118 ***********************************************************************/
Cec2_AddClausesMux(Gia_Man_t * p,Gia_Obj_t * pNode,satoko_t * pSat)119 void Cec2_AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, satoko_t * pSat )
120 {
121 int fPolarFlip = 0;
122 Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
123 int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
124
125 assert( !Gia_IsComplement( pNode ) );
126 assert( pNode->fMark0 );
127 // get nodes (I = if, T = then, E = else)
128 pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
129 // get the variable numbers
130 VarF = Cec2_ObjSatId(p, pNode);
131 VarI = Cec2_ObjSatId(p, pNodeI);
132 VarT = Cec2_ObjSatId(p, Gia_Regular(pNodeT));
133 VarE = Cec2_ObjSatId(p, Gia_Regular(pNodeE));
134 // get the complementation flags
135 fCompT = Gia_IsComplement(pNodeT);
136 fCompE = Gia_IsComplement(pNodeE);
137
138 // f = ITE(i, t, e)
139
140 // i' + t' + f
141 // i' + t + f'
142 // i + e' + f
143 // i + e + f'
144
145 // create four clauses
146 pLits[0] = Abc_Var2Lit(VarI, 1);
147 pLits[1] = Abc_Var2Lit(VarT, 1^fCompT);
148 pLits[2] = Abc_Var2Lit(VarF, 0);
149 if ( fPolarFlip )
150 {
151 if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
152 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
153 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
154 }
155 RetValue = satoko_add_clause( pSat, pLits, 3 );
156 assert( RetValue );
157 pLits[0] = Abc_Var2Lit(VarI, 1);
158 pLits[1] = Abc_Var2Lit(VarT, 0^fCompT);
159 pLits[2] = Abc_Var2Lit(VarF, 1);
160 if ( fPolarFlip )
161 {
162 if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
163 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
164 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
165 }
166 RetValue = satoko_add_clause( pSat, pLits, 3 );
167 assert( RetValue );
168 pLits[0] = Abc_Var2Lit(VarI, 0);
169 pLits[1] = Abc_Var2Lit(VarE, 1^fCompE);
170 pLits[2] = Abc_Var2Lit(VarF, 0);
171 if ( fPolarFlip )
172 {
173 if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
174 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
175 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
176 }
177 RetValue = satoko_add_clause( pSat, pLits, 3 );
178 assert( RetValue );
179 pLits[0] = Abc_Var2Lit(VarI, 0);
180 pLits[1] = Abc_Var2Lit(VarE, 0^fCompE);
181 pLits[2] = Abc_Var2Lit(VarF, 1);
182 if ( fPolarFlip )
183 {
184 if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
185 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
186 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
187 }
188 RetValue = satoko_add_clause( pSat, pLits, 3 );
189 assert( RetValue );
190
191 // two additional clauses
192 // t' & e' -> f'
193 // t & e -> f
194
195 // t + e + f'
196 // t' + e' + f
197
198 if ( VarT == VarE )
199 {
200 // assert( fCompT == !fCompE );
201 return;
202 }
203
204 pLits[0] = Abc_Var2Lit(VarT, 0^fCompT);
205 pLits[1] = Abc_Var2Lit(VarE, 0^fCompE);
206 pLits[2] = Abc_Var2Lit(VarF, 1);
207 if ( fPolarFlip )
208 {
209 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
210 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
211 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
212 }
213 RetValue = satoko_add_clause( pSat, pLits, 3 );
214 assert( RetValue );
215 pLits[0] = Abc_Var2Lit(VarT, 1^fCompT);
216 pLits[1] = Abc_Var2Lit(VarE, 1^fCompE);
217 pLits[2] = Abc_Var2Lit(VarF, 0);
218 if ( fPolarFlip )
219 {
220 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
221 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
222 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
223 }
224 RetValue = satoko_add_clause( pSat, pLits, 3 );
225 assert( RetValue );
226 }
Cec2_AddClausesSuper(Gia_Man_t * p,Gia_Obj_t * pNode,Vec_Ptr_t * vSuper,satoko_t * pSat)227 void Cec2_AddClausesSuper( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper, satoko_t * pSat )
228 {
229 int fPolarFlip = 0;
230 Gia_Obj_t * pFanin;
231 int * pLits, nLits, RetValue, i;
232 assert( !Gia_IsComplement(pNode) );
233 assert( Gia_ObjIsAnd( pNode ) );
234 // create storage for literals
235 nLits = Vec_PtrSize(vSuper) + 1;
236 pLits = ABC_ALLOC( int, nLits );
237 // suppose AND-gate is A & B = C
238 // add !A => !C or A + !C
239 Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
240 {
241 pLits[0] = Abc_Var2Lit(Cec2_ObjSatId(p, Gia_Regular(pFanin)), Gia_IsComplement(pFanin));
242 pLits[1] = Abc_Var2Lit(Cec2_ObjSatId(p, pNode), 1);
243 if ( fPolarFlip )
244 {
245 if ( Gia_Regular(pFanin)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
246 if ( pNode->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
247 }
248 RetValue = satoko_add_clause( pSat, pLits, 2 );
249 assert( RetValue );
250 }
251 // add A & B => C or !A + !B + C
252 Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
253 {
254 pLits[i] = Abc_Var2Lit(Cec2_ObjSatId(p, Gia_Regular(pFanin)), !Gia_IsComplement(pFanin));
255 if ( fPolarFlip )
256 {
257 if ( Gia_Regular(pFanin)->fPhase ) pLits[i] = Abc_LitNot( pLits[i] );
258 }
259 }
260 pLits[nLits-1] = Abc_Var2Lit(Cec2_ObjSatId(p, pNode), 0);
261 if ( fPolarFlip )
262 {
263 if ( pNode->fPhase ) pLits[nLits-1] = Abc_LitNot( pLits[nLits-1] );
264 }
265 RetValue = satoko_add_clause( pSat, pLits, nLits );
266 assert( RetValue );
267 ABC_FREE( pLits );
268 }
269
270 /**Function*************************************************************
271
272 Synopsis [Adds clauses and returns CNF variable of the node.]
273
274 Description []
275
276 SideEffects []
277
278 SeeAlso []
279
280 ***********************************************************************/
Cec2_CollectSuper_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Ptr_t * vSuper,int fFirst,int fUseMuxes)281 void Cec2_CollectSuper_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
282 {
283 // if the new node is complemented or a PI, another gate begins
284 if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) ||
285 (!fFirst && (p->pRefs ? Gia_ObjRefNum(p, pObj) : Gia_ObjValue(pObj)) > 1) ||
286 (fUseMuxes && pObj->fMark0) )
287 {
288 Vec_PtrPushUnique( vSuper, pObj );
289 return;
290 }
291 // go through the branches
292 Cec2_CollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes );
293 Cec2_CollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes );
294 }
Cec2_CollectSuper(Gia_Man_t * p,Gia_Obj_t * pObj,int fUseMuxes,Vec_Ptr_t * vSuper)295 void Cec2_CollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
296 {
297 assert( !Gia_IsComplement(pObj) );
298 assert( !Gia_ObjIsCi(pObj) );
299 Vec_PtrClear( vSuper );
300 Cec2_CollectSuper_rec( p, pObj, vSuper, 1, fUseMuxes );
301 }
Cec2_ObjAddToFrontier(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Ptr_t * vFrontier,satoko_t * pSat)302 void Cec2_ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier, satoko_t * pSat )
303 {
304 int iVar;
305 assert( !Gia_IsComplement(pObj) );
306 assert( !Gia_ObjIsConst0(pObj) );
307 if ( Cec2_ObjSatId(p, pObj) >= 0 )
308 return;
309 assert( Cec2_ObjSatId(p, pObj) == -1 );
310 iVar = satoko_add_variable(pSat, 0);
311 if ( p->vVar2Obj )
312 {
313 assert( Vec_IntSize(p->vVar2Obj) == iVar );
314 Vec_IntPush( p->vVar2Obj, Gia_ObjId(p, pObj) );
315 }
316 Cec2_ObjSetSatId( p, pObj, iVar );
317 if ( Gia_ObjIsAnd(pObj) )
318 Vec_PtrPush( vFrontier, pObj );
319 }
Gia_ObjGetCnfVar(Gia_Man_t * pGia,int iObj,Vec_Ptr_t * vFrontier,Vec_Ptr_t * vFanins,satoko_t * pSat)320 int Gia_ObjGetCnfVar( Gia_Man_t * pGia, int iObj, Vec_Ptr_t * vFrontier, Vec_Ptr_t * vFanins, satoko_t * pSat )
321 {
322 Gia_Obj_t * pNode, * pFanin;
323 Gia_Obj_t * pObj = Gia_ManObj(pGia, iObj);
324 int i, k, fUseMuxes = 1;
325 if ( Vec_IntSize(&pGia->vCopies2) < Gia_ManObjNum(pGia) )
326 Vec_IntFillExtra( &pGia->vCopies2, Gia_ManObjNum(pGia), -1 );
327 // quit if CNF is ready
328 if ( Cec2_ObjSatId(pGia,pObj) >= 0 )
329 return Cec2_ObjSatId(pGia,pObj);
330 assert( iObj > 0 );
331 if ( Gia_ObjIsCi(pObj) )
332 {
333 int iVar = satoko_add_variable(pSat, 0);
334 if ( pGia->vVar2Obj )
335 {
336 assert( Vec_IntSize(pGia->vVar2Obj) == iVar );
337 Vec_IntPush( pGia->vVar2Obj, iObj );
338 }
339 return Cec2_ObjSetSatId( pGia, pObj, iVar );
340 }
341 assert( Gia_ObjIsAnd(pObj) );
342 // start the frontier
343 Vec_PtrClear( vFrontier );
344 Cec2_ObjAddToFrontier( pGia, pObj, vFrontier, pSat );
345 // explore nodes in the frontier
346 Vec_PtrForEachEntry( Gia_Obj_t *, vFrontier, pNode, i )
347 {
348 // create the supergate
349 assert( Cec2_ObjSatId(pGia,pNode) >= 0 );
350 if ( fUseMuxes && pNode->fMark0 )
351 {
352 Vec_PtrClear( vFanins );
353 Vec_PtrPushUnique( vFanins, Gia_ObjFanin0( Gia_ObjFanin0(pNode) ) );
354 Vec_PtrPushUnique( vFanins, Gia_ObjFanin0( Gia_ObjFanin1(pNode) ) );
355 Vec_PtrPushUnique( vFanins, Gia_ObjFanin1( Gia_ObjFanin0(pNode) ) );
356 Vec_PtrPushUnique( vFanins, Gia_ObjFanin1( Gia_ObjFanin1(pNode) ) );
357 Vec_PtrForEachEntry( Gia_Obj_t *, vFanins, pFanin, k )
358 Cec2_ObjAddToFrontier( pGia, Gia_Regular(pFanin), vFrontier, pSat );
359 Cec2_AddClausesMux( pGia, pNode, pSat );
360 }
361 else
362 {
363 Cec2_CollectSuper( pGia, pNode, fUseMuxes, vFanins );
364 Vec_PtrForEachEntry( Gia_Obj_t *, vFanins, pFanin, k )
365 Cec2_ObjAddToFrontier( pGia, Gia_Regular(pFanin), vFrontier, pSat );
366 Cec2_AddClausesSuper( pGia, pNode, vFanins, pSat );
367 //printf( "%d ", Vec_PtrSize(vFanins) );
368 }
369 assert( Vec_PtrSize(vFanins) > 1 );
370 }
371 return Cec2_ObjSatId(pGia,pObj);
372 }
Cec2_ObjGetCnfVar(Cec2_Man_t * p,int iObj)373 int Cec2_ObjGetCnfVar( Cec2_Man_t * p, int iObj )
374 {
375 return Gia_ObjGetCnfVar( p->pNew, iObj, p->vFrontier, p->vFanins, p->pSat );
376 }
377
378
379 /**Function*************************************************************
380
381 Synopsis [Internal simulation APIs.]
382
383 Description []
384
385 SideEffects []
386
387 SeeAlso []
388
389 ***********************************************************************/
Cec2_ObjSim(Gia_Man_t * p,int iObj)390 static inline word * Cec2_ObjSim( Gia_Man_t * p, int iObj )
391 {
392 return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj );
393 }
Cec2_ObjSimSetInputBit(Gia_Man_t * p,int iObj,int Bit)394 static inline void Cec2_ObjSimSetInputBit( Gia_Man_t * p, int iObj, int Bit )
395 {
396 word * pSim = Cec2_ObjSim( p, iObj );
397 if ( Abc_InfoHasBit( (unsigned*)pSim, p->iPatsPi ) != Bit )
398 Abc_InfoXorBit( (unsigned*)pSim, p->iPatsPi );
399 }
Cec2_ObjSimRo(Gia_Man_t * p,int iObj)400 static inline void Cec2_ObjSimRo( Gia_Man_t * p, int iObj )
401 {
402 int w;
403 word * pSimRo = Cec2_ObjSim( p, iObj );
404 word * pSimRi = Cec2_ObjSim( p, Gia_ObjRoToRiId(p, iObj) );
405 for ( w = 0; w < p->nSimWords; w++ )
406 pSimRo[w] = pSimRi[w];
407 }
Cec2_ObjSimCo(Gia_Man_t * p,int iObj)408 static inline void Cec2_ObjSimCo( Gia_Man_t * p, int iObj )
409 {
410 int w;
411 Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
412 word * pSimCo = Cec2_ObjSim( p, iObj );
413 word * pSimDri = Cec2_ObjSim( p, Gia_ObjFaninId0(pObj, iObj) );
414 if ( Gia_ObjFaninC0(pObj) )
415 for ( w = 0; w < p->nSimWords; w++ )
416 pSimCo[w] = ~pSimDri[w];
417 else
418 for ( w = 0; w < p->nSimWords; w++ )
419 pSimCo[w] = pSimDri[w];
420 }
Cec2_ObjSimAnd(Gia_Man_t * p,int iObj)421 static inline void Cec2_ObjSimAnd( Gia_Man_t * p, int iObj )
422 {
423 int w;
424 Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
425 word * pSim = Cec2_ObjSim( p, iObj );
426 word * pSim0 = Cec2_ObjSim( p, Gia_ObjFaninId0(pObj, iObj) );
427 word * pSim1 = Cec2_ObjSim( p, Gia_ObjFaninId1(pObj, iObj) );
428 if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
429 for ( w = 0; w < p->nSimWords; w++ )
430 pSim[w] = ~pSim0[w] & ~pSim1[w];
431 else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) )
432 for ( w = 0; w < p->nSimWords; w++ )
433 pSim[w] = ~pSim0[w] & pSim1[w];
434 else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
435 for ( w = 0; w < p->nSimWords; w++ )
436 pSim[w] = pSim0[w] & ~pSim1[w];
437 else
438 for ( w = 0; w < p->nSimWords; w++ )
439 pSim[w] = pSim0[w] & pSim1[w];
440 }
Cec2_ObjSimEqual(Gia_Man_t * p,int iObj0,int iObj1)441 static inline int Cec2_ObjSimEqual( Gia_Man_t * p, int iObj0, int iObj1 )
442 {
443 int w;
444 word * pSim0 = Cec2_ObjSim( p, iObj0 );
445 word * pSim1 = Cec2_ObjSim( p, iObj1 );
446 if ( (pSim0[0] & 1) == (pSim1[0] & 1) )
447 {
448 for ( w = 0; w < p->nSimWords; w++ )
449 if ( pSim0[w] != pSim1[w] )
450 return 0;
451 return 1;
452 }
453 else
454 {
455 for ( w = 0; w < p->nSimWords; w++ )
456 if ( pSim0[w] != ~pSim1[w] )
457 return 0;
458 return 1;
459 }
460 }
Cec2_ObjSimCi(Gia_Man_t * p,int iObj)461 static inline void Cec2_ObjSimCi( Gia_Man_t * p, int iObj )
462 {
463 int w;
464 word * pSim = Cec2_ObjSim( p, iObj );
465 for ( w = 0; w < p->nSimWords; w++ )
466 pSim[w] = Gia_ManRandomW( 0 );
467 pSim[0] <<= 1;
468 }
Cec2_ManSimulateCis(Gia_Man_t * p)469 void Cec2_ManSimulateCis( Gia_Man_t * p )
470 {
471 int i, Id;
472 Gia_ManForEachCiId( p, Id, i )
473 Cec2_ObjSimCi( p, Id );
474 p->iPatsPi = 0;
475 }
Cec2_ManDeriveCex(Gia_Man_t * p,int iOut,int iPat)476 Abc_Cex_t * Cec2_ManDeriveCex( Gia_Man_t * p, int iOut, int iPat )
477 {
478 Abc_Cex_t * pCex;
479 int i, Id;
480 pCex = Abc_CexAlloc( 0, Gia_ManCiNum(p), 1 );
481 pCex->iPo = iOut;
482 if ( iPat == -1 )
483 return pCex;
484 Gia_ManForEachCiId( p, Id, i )
485 if ( Abc_InfoHasBit((unsigned *)Cec2_ObjSim(p, Id), iPat) )
486 Abc_InfoSetBit( pCex->pData, i );
487 return pCex;
488 }
Cec2_ManSimulateCos(Gia_Man_t * p)489 int Cec2_ManSimulateCos( Gia_Man_t * p )
490 {
491 int i, Id;
492 // check outputs and generate CEX if they fail
493 Gia_ManForEachCoId( p, Id, i )
494 {
495 Cec2_ObjSimCo( p, Id );
496 if ( Cec2_ObjSimEqual(p, Id, 0) )
497 continue;
498 p->pCexSeq = Cec2_ManDeriveCex( p, i, Abc_TtFindFirstBit2(Cec2_ObjSim(p, Id), p->nSimWords) );
499 return 0;
500 }
501 return 1;
502 }
Cec2_ManSaveCis(Gia_Man_t * p)503 void Cec2_ManSaveCis( Gia_Man_t * p )
504 {
505 int w, i, Id;
506 assert( p->vSimsPi != NULL );
507 for ( w = 0; w < p->nSimWords; w++ )
508 Gia_ManForEachCiId( p, Id, i )
509 Vec_WrdPush( p->vSimsPi, Cec2_ObjSim(p, Id)[w] );
510 }
Cec2_ManSimulate(Gia_Man_t * p,Vec_Int_t * vTriples,Cec2_Man_t * pMan)511 int Cec2_ManSimulate( Gia_Man_t * p, Vec_Int_t * vTriples, Cec2_Man_t * pMan )
512 {
513 extern void Cec2_ManSimClassRefineOne( Gia_Man_t * p, int iRepr );
514 abctime clk = Abc_Clock();
515 Gia_Obj_t * pObj;
516 int i, iRepr, iObj, Entry, Count = 0;
517 //Cec2_ManSaveCis( p );
518 Gia_ManForEachAnd( p, pObj, i )
519 Cec2_ObjSimAnd( p, i );
520 pMan->timeSim += Abc_Clock() - clk;
521 if ( p->pReprs == NULL )
522 return 0;
523 if ( vTriples )
524 {
525 Vec_IntForEachEntryTriple( vTriples, iRepr, iObj, Entry, i )
526 {
527 word * pSim0 = Cec2_ObjSim( p, iRepr );
528 word * pSim1 = Cec2_ObjSim( p, iObj );
529 int iPat = Abc_Lit2Var(Entry);
530 int fPhase = Abc_LitIsCompl(Entry);
531 if ( (fPhase ^ Abc_InfoHasBit((unsigned *)pSim0, iPat)) == Abc_InfoHasBit((unsigned *)pSim1, iPat) )
532 Count++;
533 }
534 }
535 clk = Abc_Clock();
536 Gia_ManForEachClass0( p, i )
537 Cec2_ManSimClassRefineOne( p, i );
538 pMan->timeRefine += Abc_Clock() - clk;
539 return Count;
540 }
Cec2_ManSimAlloc(Gia_Man_t * p,int nWords)541 void Cec2_ManSimAlloc( Gia_Man_t * p, int nWords )
542 {
543 Vec_WrdFreeP( &p->vSims );
544 Vec_WrdFreeP( &p->vSimsPi );
545 p->vSims = Vec_WrdStart( Gia_ManObjNum(p) * nWords );
546 p->vSimsPi = Vec_WrdAlloc( Gia_ManCiNum(p) * nWords * 4 ); // storage for CI patterns
547 p->nSimWords = nWords;
548 }
549
550
551 /**Function*************************************************************
552
553 Synopsis [Computes hash key of the simulation info.]
554
555 Description []
556
557 SideEffects []
558
559 SeeAlso []
560
561 ***********************************************************************/
Cec2_ManSimHashKey(word * pSim,int nSims,int nTableSize)562 int Cec2_ManSimHashKey( word * pSim, int nSims, int nTableSize )
563 {
564 static int s_Primes[16] = {
565 1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177,
566 4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
567 unsigned uHash = 0, * pSimU = (unsigned *)pSim;
568 int i, nSimsU = 2 * nSims;
569 if ( pSimU[0] & 1 )
570 for ( i = 0; i < nSimsU; i++ )
571 uHash ^= ~pSimU[i] * s_Primes[i & 0xf];
572 else
573 for ( i = 0; i < nSimsU; i++ )
574 uHash ^= pSimU[i] * s_Primes[i & 0xf];
575 return (int)(uHash % nTableSize);
576
577 }
578
579 /**Function*************************************************************
580
581 Synopsis [Creating initial equivalence classes.]
582
583 Description []
584
585 SideEffects []
586
587 SeeAlso []
588
589 ***********************************************************************/
Cec2_ManSimClassRefineOne(Gia_Man_t * p,int iRepr)590 void Cec2_ManSimClassRefineOne( Gia_Man_t * p, int iRepr )
591 {
592 int iObj, iPrev = iRepr, iPrev2, iRepr2;
593 Gia_ClassForEachObj1( p, iRepr, iRepr2 )
594 if ( Cec2_ObjSimEqual(p, iRepr, iRepr2) )
595 iPrev = iRepr2;
596 else
597 break;
598 if ( iRepr2 <= 0 ) // no refinement
599 return;
600 // relink remaining nodes of the class
601 // nodes that are equal to iRepr, remain in the class of iRepr
602 // nodes that are not equal to iRepr, move to the class of iRepr2
603 Gia_ObjSetRepr( p, iRepr2, GIA_VOID );
604 iPrev2 = iRepr2;
605 for ( iObj = Gia_ObjNext(p, iRepr2); iObj > 0; iObj = Gia_ObjNext(p, iObj) )
606 {
607 if ( Cec2_ObjSimEqual(p, iRepr, iObj) ) // remains with iRepr
608 {
609 Gia_ObjSetNext( p, iPrev, iObj );
610 iPrev = iObj;
611 }
612 else // moves to iRepr2
613 {
614 Gia_ObjSetRepr( p, iObj, iRepr2 );
615 Gia_ObjSetNext( p, iPrev2, iObj );
616 iPrev2 = iObj;
617 }
618 }
619 Gia_ObjSetNext( p, iPrev, -1 );
620 Gia_ObjSetNext( p, iPrev2, -1 );
621 }
Cec2_ManCreateClasses(Gia_Man_t * p,Cec2_Man_t * pMan)622 void Cec2_ManCreateClasses( Gia_Man_t * p, Cec2_Man_t * pMan )
623 {
624 abctime clk;
625 Gia_Obj_t * pObj;
626 int nWords = p->nSimWords;
627 int * pTable, nTableSize, i, Key;
628 // allocate representation
629 ABC_FREE( p->pReprs );
630 ABC_FREE( p->pNexts );
631 p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
632 p->pNexts = ABC_FALLOC( int, Gia_ManObjNum(p) );
633 // hash each node by its simulation info
634 nTableSize = Abc_PrimeCudd( Gia_ManObjNum(p) );
635 pTable = ABC_FALLOC( int, nTableSize );
636 Gia_ManForEachObj( p, pObj, i )
637 {
638 p->pReprs[i].iRepr = GIA_VOID;
639 if ( Gia_ObjIsCo(pObj) )
640 continue;
641 Key = Cec2_ManSimHashKey( Cec2_ObjSim(p, i), nWords, nTableSize );
642 assert( Key >= 0 && Key < nTableSize );
643 if ( pTable[Key] == -1 )
644 pTable[Key] = i;
645 else
646 Gia_ObjSetRepr( p, i, pTable[Key] );
647 }
648 // create classes
649 for ( i = Gia_ManObjNum(p) - 1; i >= 0; i-- )
650 {
651 int iRepr = Gia_ObjRepr(p, i);
652 if ( iRepr == GIA_VOID )
653 continue;
654 Gia_ObjSetNext( p, i, Gia_ObjNext(p, iRepr) );
655 Gia_ObjSetNext( p, iRepr, i );
656 }
657 ABC_FREE( pTable );
658 clk = Abc_Clock();
659 Gia_ManForEachClass0( p, i )
660 Cec2_ManSimClassRefineOne( p, i );
661 pMan->timeRefine += Abc_Clock() - clk;
662 }
663
664
665 /**Function*************************************************************
666
667 Synopsis []
668
669 Description []
670
671 SideEffects []
672
673 SeeAlso []
674
675 ***********************************************************************/
Cec2_ManCreate(Gia_Man_t * pAig,Cec2_Par_t * pPars)676 Cec2_Man_t * Cec2_ManCreate( Gia_Man_t * pAig, Cec2_Par_t * pPars )
677 {
678 Cec2_Man_t * p;
679 Gia_Obj_t * pObj; int i;
680 satoko_opts_t Pars;
681 //assert( Gia_ManRegNum(pAig) == 0 );
682 p = ABC_CALLOC( Cec2_Man_t, 1 );
683 memset( p, 0, sizeof(Cec2_Man_t) );
684 p->timeStart = Abc_Clock();
685 p->pPars = pPars;
686 p->pAig = pAig;
687 // create new manager
688 p->pNew = Gia_ManStart( Gia_ManObjNum(pAig) );
689 Gia_ManFillValue( pAig );
690 Gia_ManConst0(pAig)->Value = 0;
691 Gia_ManForEachCi( pAig, pObj, i )
692 pObj->Value = Gia_ManAppendCi( p->pNew );
693 Gia_ManHashAlloc( p->pNew );
694 Vec_IntFill( &p->pNew->vCopies2, Gia_ManObjNum(p->pNew), -1 );
695 // SAT solving
696 memset( &Pars, 0, sizeof(satoko_opts_t) );
697 p->pSat = satoko_create();
698 p->vFrontier = Vec_PtrAlloc( 1000 );
699 p->vFanins = Vec_PtrAlloc( 100 );
700 p->vNodesNew = Vec_IntAlloc( 100 );
701 p->vSatVars = Vec_IntAlloc( 100 );
702 p->vObjSatPairs = Vec_IntAlloc( 100 );
703 p->vCexTriples = Vec_IntAlloc( 100 );
704 Pars.conf_limit = pPars->nConfLimit;
705 satoko_configure(p->pSat, &Pars);
706 // remember pointer to the solver in the AIG manager
707 pAig->pData = p->pSat;
708 return p;
709 }
Cec2_ManDestroy(Cec2_Man_t * p)710 void Cec2_ManDestroy( Cec2_Man_t * p )
711 {
712 if ( p->pPars->fVerbose )
713 {
714 abctime timeTotal = Abc_Clock() - p->timeStart;
715 abctime timeSat = p->timeSatSat + p->timeSatUnsat + p->timeSatUndec;
716 abctime timeOther = timeTotal - timeSat - p->timeSim - p->timeRefine - p->timeExtra;
717 // Abc_Print( 1, "%d\n", p->Num );
718 ABC_PRTP( "SAT solving", timeSat, timeTotal );
719 ABC_PRTP( " sat ", p->timeSatSat, timeTotal );
720 ABC_PRTP( " unsat ", p->timeSatUnsat, timeTotal );
721 ABC_PRTP( " fail ", p->timeSatUndec, timeTotal );
722 ABC_PRTP( "Simulation ", p->timeSim, timeTotal );
723 ABC_PRTP( "Refinement ", p->timeRefine, timeTotal );
724 ABC_PRTP( "Rollback ", p->timeExtra, timeTotal );
725 ABC_PRTP( "Other ", timeOther, timeTotal );
726 ABC_PRTP( "TOTAL ", timeTotal, timeTotal );
727 fflush( stdout );
728 }
729
730 Vec_WrdFreeP( &p->pAig->vSims );
731 //Vec_WrdFreeP( &p->pAig->vSimsPi );
732 Gia_ManCleanMark01( p->pAig );
733 satoko_destroy( p->pSat );
734 Gia_ManStopP( &p->pNew );
735 Vec_PtrFreeP( &p->vFrontier );
736 Vec_PtrFreeP( &p->vFanins );
737 Vec_IntFreeP( &p->vNodesNew );
738 Vec_IntFreeP( &p->vSatVars );
739 Vec_IntFreeP( &p->vObjSatPairs );
740 Vec_IntFreeP( &p->vCexTriples );
741 ABC_FREE( p );
742 }
743
744
745 /**Function*************************************************************
746
747 Synopsis [Verify counter-example.]
748
749 Description []
750
751 SideEffects []
752
753 SeeAlso []
754
755 ***********************************************************************/
Cec2_ManVerify_rec(Gia_Man_t * p,int iObj,satoko_t * pSat)756 int Cec2_ManVerify_rec( Gia_Man_t * p, int iObj, satoko_t * pSat )
757 {
758 int Value0, Value1;
759 Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
760 if ( iObj == 0 ) return 0;
761 if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
762 return pObj->fMark1;
763 Gia_ObjSetTravIdCurrentId(p, iObj);
764 if ( Gia_ObjIsCi(pObj) )
765 return pObj->fMark1 = satoko_var_polarity(pSat, Cec2_ObjSatId(p, pObj)) == SATOKO_LIT_TRUE;
766 assert( Gia_ObjIsAnd(pObj) );
767 Value0 = Cec2_ManVerify_rec( p, Gia_ObjFaninId0(pObj, iObj), pSat ) ^ Gia_ObjFaninC0(pObj);
768 Value1 = Cec2_ManVerify_rec( p, Gia_ObjFaninId1(pObj, iObj), pSat ) ^ Gia_ObjFaninC1(pObj);
769 return pObj->fMark1 = Value0 & Value1;
770 }
Cec2_ManVerify(Gia_Man_t * p,int iObj0,int iObj1,int fPhase,satoko_t * pSat)771 void Cec2_ManVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase, satoko_t * pSat )
772 {
773 int Value0, Value1;
774 Gia_ManIncrementTravId( p );
775 Value0 = Cec2_ManVerify_rec( p, iObj0, pSat );
776 Value1 = Cec2_ManVerify_rec( p, iObj1, pSat );
777 if ( (Value0 ^ Value1) == fPhase )
778 printf( "CEX verification FAILED for obj %d and obj %d.\n", iObj0, iObj1 );
779 // else
780 // printf( "CEX verification succeeded for obj %d and obj %d.\n", iObj0, iObj1 );;
781 }
782
783 /**Function*************************************************************
784
785 Synopsis [Internal simulation APIs.]
786
787 Description []
788
789 SideEffects []
790
791 SeeAlso []
792
793 ***********************************************************************/
Cec2_ManCollect_rec(Cec2_Man_t * p,int iObj)794 void Cec2_ManCollect_rec( Cec2_Man_t * p, int iObj )
795 {
796 Gia_Obj_t * pObj;
797 if ( Gia_ObjIsTravIdCurrentId(p->pNew, iObj) )
798 return;
799 Gia_ObjSetTravIdCurrentId(p->pNew, iObj);
800 pObj = Gia_ManObj( p->pNew, iObj );
801 if ( Cec2_ObjSatId(p->pNew, pObj) >= 0 )
802 {
803 Vec_IntPush( p->vNodesNew, iObj );
804 Vec_IntPush( p->vSatVars, Cec2_ObjSatId(p->pNew, pObj) );
805 }
806 if ( !iObj )
807 return;
808 if ( Gia_ObjIsAnd(pObj) )
809 {
810 Cec2_ManCollect_rec( p, Gia_ObjFaninId0(pObj, iObj) );
811 Cec2_ManCollect_rec( p, Gia_ObjFaninId1(pObj, iObj) );
812 }
813 else
814 {
815 assert( Cec2_ObjSatId(p->pNew, pObj) >= 0 );
816 Vec_IntPushTwo( p->vObjSatPairs, Gia_ManCiIdToId(p->pAig, Gia_ObjCioId(pObj)), Cec2_ObjSatId(p->pNew, pObj) ); // SAT var
817 }
818 }
Cec2_ManSolveTwo(Cec2_Man_t * p,int iObj0,int iObj1,int fPhase)819 int Cec2_ManSolveTwo( Cec2_Man_t * p, int iObj0, int iObj1, int fPhase )
820 {
821 Gia_Obj_t * pObj;
822 int status, i, iVar0, iVar1;
823 if (iObj1 < iObj0)
824 iObj1 ^= iObj0, iObj0 ^= iObj1, iObj1 ^= iObj0;
825 assert( iObj0 < iObj1 );
826 assert( p->pPars->fUseCones || satoko_varnum(p->pSat) == 0 );
827 if ( !iObj0 && Cec2_ObjSatId(p->pNew, Gia_ManConst0(p->pNew)) == -1 )
828 Cec2_ObjSetSatId( p->pNew, Gia_ManConst0(p->pNew), satoko_add_variable(p->pSat, 0) );
829 iVar0 = Cec2_ObjGetCnfVar( p, iObj0 );
830 iVar1 = Cec2_ObjGetCnfVar( p, iObj1 );
831 // collect inputs and internal nodes
832 Vec_IntClear( p->vNodesNew );
833 Vec_IntClear( p->vSatVars );
834 Vec_IntClear( p->vObjSatPairs );
835 Gia_ManIncrementTravId( p->pNew );
836 Cec2_ManCollect_rec( p, iObj0 );
837 Cec2_ManCollect_rec( p, iObj1 );
838 // solve direct
839 if ( p->pPars->fUseCones ) satoko_mark_cone( p->pSat, Vec_IntArray(p->vSatVars), Vec_IntSize(p->vSatVars) );
840 satoko_assump_push( p->pSat, Abc_Var2Lit(iVar0, 1) );
841 satoko_assump_push( p->pSat, Abc_Var2Lit(iVar1, fPhase) );
842 status = satoko_solve( p->pSat );
843 satoko_assump_pop( p->pSat );
844 satoko_assump_pop( p->pSat );
845 if ( status == SATOKO_UNSAT && iObj0 > 0 )
846 {
847 // solve reverse
848 satoko_assump_push( p->pSat, Abc_Var2Lit(iVar0, 0) );
849 satoko_assump_push( p->pSat, Abc_Var2Lit(iVar1, !fPhase) );
850 status = satoko_solve( p->pSat );
851 satoko_assump_pop( p->pSat );
852 satoko_assump_pop( p->pSat );
853 }
854 if ( p->pPars->fUseCones ) satoko_unmark_cone( p->pSat, Vec_IntArray(p->vSatVars), Vec_IntSize(p->vSatVars) );
855 //if ( status == SATOKO_SAT )
856 // Cec2_ManVerify( p->pNew, iObj0, iObj1, fPhase, p->pSat );
857 if ( p->pPars->fUseCones )
858 return status;
859 Gia_ManForEachObjVec( p->vNodesNew, p->pNew, pObj, i )
860 Cec2_ObjCleanSatId( p->pNew, pObj );
861 return status;
862 }
863
Cec2_ManSweepNode(Cec2_Man_t * p,int iObj)864 int Cec2_ManSweepNode( Cec2_Man_t * p, int iObj )
865 {
866 abctime clk = Abc_Clock();
867 int i, IdAig, IdSat, status, RetValue = 1;
868 Gia_Obj_t * pObj = Gia_ManObj( p->pAig, iObj );
869 Gia_Obj_t * pRepr = Gia_ObjReprObj( p->pAig, iObj );
870 int fCompl = Abc_LitIsCompl(pObj->Value) ^ Abc_LitIsCompl(pRepr->Value) ^ pObj->fPhase ^ pRepr->fPhase;
871 status = Cec2_ManSolveTwo( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl );
872 if ( status == SATOKO_SAT )
873 {
874 p->nSatSat++;
875 p->nPatterns++;
876 p->pAig->iPatsPi = (p->pAig->iPatsPi == 64 * p->pAig->nSimWords - 1) ? 1 : p->pAig->iPatsPi + 1;
877 assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords );
878 Vec_IntForEachEntryDouble( p->vObjSatPairs, IdAig, IdSat, i )
879 Cec2_ObjSimSetInputBit( p->pAig, IdAig, satoko_var_polarity(p->pSat, IdSat) == SATOKO_LIT_TRUE );
880 p->timeSatSat += Abc_Clock() - clk;
881 RetValue = 0;
882 }
883 else if ( status == SATOKO_UNSAT )
884 {
885 p->nSatUnsat++;
886 pObj->Value = Abc_LitNotCond( pRepr->Value, fCompl );
887 Gia_ObjSetProved( p->pAig, iObj );
888 p->timeSatUnsat += Abc_Clock() - clk;
889 RetValue = 1;
890 }
891 else
892 {
893 p->nSatUndec++;
894 assert( status == SATOKO_UNDEC );
895 Gia_ObjSetFailed( p->pAig, iObj );
896 p->timeSatUndec += Abc_Clock() - clk;
897 RetValue = 2;
898 }
899 if ( p->pPars->fUseCones )
900 return RetValue;
901 clk = Abc_Clock();
902 satoko_rollback( p->pSat );
903 p->timeExtra += Abc_Clock() - clk;
904 satoko_stats(p->pSat)->n_conflicts = 0;
905 return RetValue;
906 }
Cec2_ManPrintStats(Gia_Man_t * p,Cec2_Par_t * pPars,Cec2_Man_t * pMan)907 void Cec2_ManPrintStats( Gia_Man_t * p, Cec2_Par_t * pPars, Cec2_Man_t * pMan )
908 {
909 if ( !pPars->fVerbose )
910 return;
911 printf( "S =%5d ", pMan ? pMan->nSatSat : 0 );
912 printf( "U =%5d ", pMan ? pMan->nSatUnsat : 0 );
913 printf( "F =%5d ", pMan ? pMan->nSatUndec : 0 );
914 Gia_ManEquivPrintClasses( p, pPars->fVeryVerbose, 0 );
915 }
Cec2_ManPerformSweeping(Gia_Man_t * p,Cec2_Par_t * pPars,Gia_Man_t ** ppNew)916 int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppNew )
917 {
918 Cec2_Man_t * pMan = Cec2_ManCreate( p, pPars );
919 Gia_Obj_t * pObj, * pRepr, * pObjNew;
920 int i, Iter, fDisproved = 1;
921
922 // check if any output trivially fails under all-0 pattern
923 Gia_ManRandomW( 1 );
924 Gia_ManSetPhase( p );
925 if ( pPars->fIsMiter )
926 {
927 Gia_ManForEachCo( p, pObj, i )
928 if ( pObj->fPhase )
929 {
930 p->pCexSeq = Cec2_ManDeriveCex( p, i, -1 );
931 goto finalize;
932 }
933 }
934
935 // simulate one round and create classes
936 Cec2_ManSimAlloc( p, pPars->nSimWords );
937 Cec2_ManSimulateCis( p );
938 Cec2_ManSimulate( p, NULL, pMan );
939 if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected
940 goto finalize;
941 Cec2_ManCreateClasses( p, pMan );
942 Cec2_ManPrintStats( p, pPars, pMan );
943
944 // perform additinal simulation
945 for ( i = 0; i < pPars->nSimRounds; i++ )
946 {
947 Cec2_ManSimulateCis( p );
948 Cec2_ManSimulate( p, NULL, pMan );
949 if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected
950 goto finalize;
951 Cec2_ManPrintStats( p, pPars, pMan );
952 }
953 // perform sweeping
954 //pMan = Cec2_ManCreate( p, pPars );
955 for ( Iter = 0; fDisproved && Iter < pPars->nItersMax; Iter++ )
956 {
957 fDisproved = 0;
958 pMan->nPatterns = 0;
959 Cec2_ManSimulateCis( p );
960 Vec_IntClear( pMan->vCexTriples );
961 Gia_ManForEachAnd( p, pObj, i )
962 {
963 if ( ~pObj->Value || Gia_ObjFailed(p, i) ) // skip swept nodes and failed nodes
964 continue;
965 if ( !~Gia_ObjFanin0(pObj)->Value || !~Gia_ObjFanin1(pObj)->Value ) // skip fanouts of non-swept nodes
966 continue;
967 assert( !Gia_ObjProved(p, i) && !Gia_ObjFailed(p, i) );
968 // duplicate the node
969 pObj->Value = Gia_ManHashAnd( pMan->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
970 if ( Vec_IntSize(&pMan->pNew->vCopies2) == Abc_Lit2Var(pObj->Value) )
971 {
972 pObjNew = Gia_ManObj( pMan->pNew, Abc_Lit2Var(pObj->Value) );
973 pObjNew->fMark0 = Gia_ObjIsMuxType( pObjNew );
974 Gia_ObjSetPhase( pMan->pNew, pObjNew );
975 Vec_IntPush( &pMan->pNew->vCopies2, -1 );
976 }
977 assert( Vec_IntSize(&pMan->pNew->vCopies2) == Gia_ManObjNum(pMan->pNew) );
978 pRepr = Gia_ObjReprObj( p, i );
979 if ( pRepr == NULL || !~pRepr->Value )
980 continue;
981 if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) )
982 {
983 assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) );
984 Gia_ObjSetProved( p, i );
985 continue;
986 }
987 if ( Cec2_ManSweepNode(pMan, i) )
988 {
989 if ( Gia_ObjProved(p, i) )
990 pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase );
991 continue;
992 }
993 pObj->Value = ~0;
994 Vec_IntPushThree( pMan->vCexTriples, Gia_ObjId(p, pRepr), i, Abc_Var2Lit(p->iPatsPi, pObj->fPhase ^ pRepr->fPhase) );
995 fDisproved = 1;
996 }
997 if ( fDisproved )
998 {
999 int Fails = Cec2_ManSimulate( p, pMan->vCexTriples, pMan );
1000 if ( Fails && pPars->fVerbose )
1001 printf( "Failed to resimulate %d times with pattern = %d (total = %d).\n", Fails, pMan->nPatterns, pPars->nSimWords * 64 );
1002 if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected
1003 break;
1004 }
1005 Cec2_ManPrintStats( p, pPars, pMan );
1006 }
1007 // finish the AIG, if it is not finished
1008 if ( ppNew )
1009 {
1010 Gia_ManForEachAnd( p, pObj, i )
1011 if ( !~pObj->Value )
1012 pObj->Value = Gia_ManHashAnd( pMan->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1013 Gia_ManForEachCo( p, pObj, i )
1014 pObj->Value = Gia_ManAppendCo( pMan->pNew, Gia_ObjFanin0Copy(pObj) );
1015 *ppNew = Gia_ManCleanup( pMan->pNew );
1016 (*ppNew)->pName = Abc_UtilStrsav( p->pName );
1017 (*ppNew)->pSpec = Abc_UtilStrsav( p->pSpec );
1018 }
1019 finalize:
1020 Cec2_ManDestroy( pMan );
1021 //Gia_ManEquivPrintClasses( p, 1, 0 );
1022 return p->pCexSeq ? 0 : 1;
1023 }
Cec2_ManSimulateTest(Gia_Man_t * p,Cec_ParFra_t * pPars0)1024 Gia_Man_t * Cec2_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars0 )
1025 {
1026 Gia_Man_t * pNew = NULL;
1027 //abctime clk = Abc_Clock();
1028 Cec2_Par_t Pars, * pPars = &Pars;
1029 Cec2_SetDefaultParams( pPars );
1030 // set resource limits
1031 // pPars->nSimWords = pPars0->nWords; // simulation words
1032 // pPars->nSimRounds = pPars0->nRounds; // simulation rounds
1033 // pPars->nItersMax = pPars0->nItersMax; // max number of iterations
1034 pPars->nConfLimit = pPars0->nBTLimit; // conflict limit at a node
1035 pPars->fUseCones = pPars0->fUseCones;
1036 pPars->fVerbose = pPars0->fVerbose;
1037 // Gia_ManComputeGiaEquivs( p, 100000, 0 );
1038 // Gia_ManEquivPrintClasses( p, 1, 0 );
1039 Cec2_ManPerformSweeping( p, pPars, &pNew );
1040 //Abc_PrintTime( 1, "SAT sweeping time", Abc_Clock() - clk );
1041 return pNew;
1042 }
1043
1044 ////////////////////////////////////////////////////////////////////////
1045 /// END OF FILE ///
1046 ////////////////////////////////////////////////////////////////////////
1047
1048
1049 ABC_NAMESPACE_IMPL_END
1050
1051