ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
absGlaOld.c
Go to the documentation of this file.
1
20
21#include "sat/cnf/cnf.h"
22#include "sat/bsat/satSolver2.h"
23#include "base/main/main.h"
24#include "abs.h"
25#include "absRef.h"
26
27ABC_NAMESPACE_IMPL_START
28
32
33typedef struct Rfn_Obj_t_ Rfn_Obj_t; // refinement object
34struct Rfn_Obj_t_
35{
36 unsigned Value : 1; // value
37 unsigned fVisit : 1; // visited
38 unsigned fPPi : 1; // PPI
39 unsigned Prio : 16; // priority
40 unsigned Sign : 12; // traversal signature
41};
42
43typedef struct Gla_Obj_t_ Gla_Obj_t; // abstraction object
44struct Gla_Obj_t_
45{
46 int iGiaObj; // corresponding GIA obj
47 unsigned fAbs : 1; // belongs to abstraction
48 unsigned fCompl0 : 1; // compl bit of the first fanin
49 unsigned fConst : 1; // object attribute
50 unsigned fPi : 1; // object attribute
51 unsigned fPo : 1; // object attribute
52 unsigned fRo : 1; // object attribute
53 unsigned fRi : 1; // object attribute
54 unsigned fAnd : 1; // object attribute
55 unsigned fMark : 1; // nearby object
56 unsigned nFanins : 23; // fanin count
57 int Fanins[4]; // fanins
58 Vec_Int_t vFrames; // variables in each timeframe
59};
60
61typedef struct Gla_Man_t_ Gla_Man_t; // manager
62struct Gla_Man_t_
63{
64 // user data
65 Gia_Man_t * pGia0; // starting AIG manager
66 Gia_Man_t * pGia; // working AIG manager
67 Abs_Par_t * pPars; // parameters
68 // internal data
69 Vec_Int_t * vAbs; // abstracted objects
70 Gla_Obj_t * pObjRoot; // the primary output
71 Gla_Obj_t * pObjs; // objects
72 unsigned * pObj2Obj; // mapping of GIA obj into GLA obj
73 int nObjs; // the number of objects
74 int nAbsOld; // previous abstraction
75// int nAbsNew; // previous abstraction
76// int nLrnOld; // the number of bytes
77// int nLrnNew; // the number of bytes
78 // other data
79 int nCexes; // the number of counter-examples
80 int nObjAdded; // total number of objects added
81 int nSatVars; // the number of SAT variables
82 Cnf_Dat_t * pCnf; // CNF derived for the nodes
83 sat_solver2 * pSat; // incremental SAT solver
84 Vec_Int_t * vTemp; // temporary array
85 Vec_Int_t * vAddedNew; // temporary array
86 Vec_Int_t * vObjCounts; // object counters
87 Vec_Int_t * vCoreCounts; // counts how many times each object appears in the core
88 Vec_Int_t * vProofIds; // counts how many times each object appears in the core
89 int nProofIds; // proof ID counter
90 // refinement
91 Vec_Int_t * pvRefis; // vectors of each object
92 // refinement manager
93 Gia_Man_t * pGia2;
94 Rnm_Man_t * pRnm;
95 // statistics
96 abctime timeInit;
97 abctime timeSat;
98 abctime timeUnsat;
99 abctime timeCex;
100 abctime timeOther;
101};
102
103// declarations
104static Vec_Int_t * Gla_ManCollectPPis( Gla_Man_t * p, Vec_Int_t * vPis );
105static int Gla_ManCheckVar( Gla_Man_t * p, int iObj, int iFrame );
106static int Gla_ManGetVar( Gla_Man_t * p, int iObj, int iFrame );
107
108// object procedures
109static inline int Gla_ObjId( Gla_Man_t * p, Gla_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; }
110static inline Gla_Obj_t * Gla_ManObj( Gla_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; }
111static inline Gia_Obj_t * Gla_ManGiaObj( Gla_Man_t * p, Gla_Obj_t * pObj ) { return Gia_ManObj( p->pGia, pObj->iGiaObj ); }
112static inline int Gla_ObjSatValue( Gla_Man_t * p, int iGia, int f ) { return Gla_ManCheckVar(p, p->pObj2Obj[iGia], f) ? sat_solver2_var_value( p->pSat, Gla_ManGetVar(p, p->pObj2Obj[iGia], f) ) : 0; }
113
114static inline Rfn_Obj_t * Gla_ObjRef( Gla_Man_t * p, Gia_Obj_t * pObj, int f ) { return (Rfn_Obj_t *)Vec_IntGetEntryP( &(p->pvRefis[Gia_ObjId(p->pGia, pObj)]), f ); }
115static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) { *((int *)p) = 0; }
116
117
118// iterator through abstracted objects
119#define Gla_ManForEachObj( p, pObj ) \
120 for ( pObj = p->pObjs + 1; pObj < p->pObjs + p->nObjs; pObj++ )
121#define Gla_ManForEachObjAbs( p, pObj, i ) \
122 for ( i = 0; i < Vec_IntSize(p->vAbs) && ((pObj = Gla_ManObj(p, Vec_IntEntry(p->vAbs, i))),1); i++)
123#define Gla_ManForEachObjAbsVec( vVec, p, pObj, i ) \
124 for ( i = 0; i < Vec_IntSize(vVec) && ((pObj = Gla_ManObj(p, Vec_IntEntry(vVec, i))),1); i++)
125
126// iterator through fanins of an abstracted object
127#define Gla_ObjForEachFanin( p, pObj, pFanin, i ) \
128 for ( i = 0; (i < (int)pObj->nFanins) && ((pFanin = Gla_ManObj(p, pObj->Fanins[i])),1); i++ )
129
130// some lessons learned from debugging mismatches between GIA and mapped CNF
131// - inputs/output of AND-node may be PPIs (have SAT vars), but the node is not included in the abstraction
132// - some logic node can be a PPI of one LUT and an internal node of another LUT
133
137
149void Gia_GlaPrepareCexAndMap( Gla_Man_t * p, Abc_Cex_t ** ppCex, Vec_Int_t ** pvMap )
150{
151 Abc_Cex_t * pCex;
152 Vec_Int_t * vMap;
153 Gla_Obj_t * pObj, * pFanin;
154 Gia_Obj_t * pGiaObj;
155 int f, i, k;
156 // find PIs and PPIs
157 vMap = Vec_IntAlloc( 1000 );
158 Gla_ManForEachObjAbs( p, pObj, i )
159 {
160 assert( pObj->fConst || pObj->fRo || pObj->fAnd );
161 Gla_ObjForEachFanin( p, pObj, pFanin, k )
162 if ( !pFanin->fAbs )
163 Vec_IntPush( vMap, pFanin->iGiaObj );
164 }
165 Vec_IntUniqify( vMap );
166 // derive counter-example
167 pCex = Abc_CexAlloc( 0, Vec_IntSize(vMap), p->pPars->iFrame+1 );
168 pCex->iFrame = p->pPars->iFrame;
169 for ( f = 0; f <= p->pPars->iFrame; f++ )
170 Gia_ManForEachObjVec( vMap, p->pGia, pGiaObj, k )
171 if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pGiaObj), f ) )
172 Abc_InfoSetBit( pCex->pData, f * Vec_IntSize(vMap) + k );
173 *pvMap = vMap;
174 *ppCex = pCex;
175}
176
188Abc_Cex_t * Gla_ManDeriveCex( Gla_Man_t * p, Vec_Int_t * vPis )
189{
190 Abc_Cex_t * pCex;
191 Gia_Obj_t * pObj;
192 int i, f;
193 pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
194 pCex->iPo = 0;
195 pCex->iFrame = p->pPars->iFrame;
196 Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
197 {
198 if ( !Gia_ObjIsPi(p->pGia, pObj) )
199 continue;
200 assert( Gia_ObjIsPi(p->pGia, pObj) );
201 for ( f = 0; f <= pCex->iFrame; f++ )
202 if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
203 Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Gia_ObjCioId(pObj) );
204 }
205 return pCex;
206}
207
219void Gla_ManCollectInternal_rec( Gia_Man_t * p, Gia_Obj_t * pGiaObj, Vec_Int_t * vRoAnds )
220{
221 if ( Gia_ObjIsTravIdCurrent(p, pGiaObj) )
222 return;
223 Gia_ObjSetTravIdCurrent(p, pGiaObj);
224 assert( Gia_ObjIsAnd(pGiaObj) );
225 Gla_ManCollectInternal_rec( p, Gia_ObjFanin0(pGiaObj), vRoAnds );
226 Gla_ManCollectInternal_rec( p, Gia_ObjFanin1(pGiaObj), vRoAnds );
227 Vec_IntPush( vRoAnds, Gia_ObjId(p, pGiaObj) );
228}
229void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int_t * vCos, Vec_Int_t * vRoAnds )
230{
231 Gla_Obj_t * pObj, * pFanin;
232 Gia_Obj_t * pGiaObj;
233 int i, k;
234
235 // collect COs
236 Vec_IntPush( vCos, Gia_ObjId(p->pGia, Gia_ManPo(p->pGia, 0)) );
237 // collect fanins of abstracted objects
238 Gla_ManForEachObjAbs( p, pObj, i )
239 {
240 assert( pObj->fConst || pObj->fRo || pObj->fAnd );
241 if ( pObj->fRo )
242 {
243 pGiaObj = Gia_ObjRoToRi( p->pGia, Gia_ManObj(p->pGia, pObj->iGiaObj) );
244 Vec_IntPush( vCos, Gia_ObjId(p->pGia, pGiaObj) );
245 }
246 Gla_ObjForEachFanin( p, pObj, pFanin, k )
247 if ( !pFanin->fAbs )
248 Vec_IntPush( (pFanin->fPi ? vPis : vPPis), pFanin->iGiaObj );
249 }
250 Vec_IntUniqify( vPis );
251 Vec_IntUniqify( vPPis );
252 Vec_IntSort( vCos, 0 );
253 // sorting PIs/PPIs/COs leads to refinements that are more "well-aligned"...
254
255 // mark const/PIs/PPIs
256 Gia_ManIncrementTravId( p->pGia );
257 Gia_ObjSetTravIdCurrent( p->pGia, Gia_ManConst0(p->pGia) );
258 Gia_ManForEachObjVec( vPis, p->pGia, pGiaObj, i )
259 Gia_ObjSetTravIdCurrent( p->pGia, pGiaObj );
260 Gia_ManForEachObjVec( vPPis, p->pGia, pGiaObj, i )
261 Gia_ObjSetTravIdCurrent( p->pGia, pGiaObj );
262 // mark and add ROs first
263 Gia_ManForEachObjVec( vCos, p->pGia, pGiaObj, i )
264 {
265 if ( i == 0 ) continue;
266 pGiaObj = Gia_ObjRiToRo( p->pGia, pGiaObj );
267 Gia_ObjSetTravIdCurrent( p->pGia, pGiaObj );
268 Vec_IntPush( vRoAnds, Gia_ObjId(p->pGia, pGiaObj) );
269 }
270 // collect nodes between PIs/PPIs/ROs and COs
271 Gia_ManForEachObjVec( vCos, p->pGia, pGiaObj, i )
272 Gla_ManCollectInternal_rec( p->pGia, Gia_ObjFanin0(pGiaObj), vRoAnds );
273}
274
286void Gia_ManRefSetAndPropFanout_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect, int Sign )
287{
288 int i;//, Id = Gia_ObjId(p->pGia, pObj);
289 Rfn_Obj_t * pRef0, * pRef1, * pRef = Gla_ObjRef( p, pObj, f );
290 Gia_Obj_t * pFanout;
291 int k;
292 if ( (int)pRef->Sign != Sign )
293 return;
294 assert( pRef->fVisit == 0 );
295 pRef->fVisit = 1;
296 if ( pRef->fPPi )
297 {
298 assert( (int)pRef->Prio > 0 );
299 for ( i = p->pPars->iFrame; i >= 0; i-- )
300 if ( !Gla_ObjRef(p, pObj, i)->fVisit )
301 Gia_ManRefSetAndPropFanout_rec( p, pObj, i, vSelect, Sign );
302 Vec_IntPush( vSelect, Gia_ObjId(p->pGia, pObj) );
303 return;
304 }
305 if ( (Gia_ObjIsCo(pObj) && f == p->pPars->iFrame) || Gia_ObjIsPo(p->pGia, pObj) )
306 return;
307 if ( Gia_ObjIsRi(p->pGia, pObj) )
308 {
309 pFanout = Gia_ObjRiToRo(p->pGia, pObj);
310 if ( !Gla_ObjRef(p, pFanout, f+1)->fVisit )
311 Gia_ManRefSetAndPropFanout_rec( p, pFanout, f+1, vSelect, Sign );
312 return;
313 }
314 assert( Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) );
315 Gia_ObjForEachFanoutStatic( p->pGia, pObj, pFanout, k )
316 {
317// Rfn_Obj_t * pRefF = Gla_ObjRef(p, pFanout, f);
318 if ( Gla_ObjRef(p, pFanout, f)->fVisit )
319 continue;
320 if ( Gia_ObjIsCo(pFanout) )
321 {
322 Gia_ManRefSetAndPropFanout_rec( p, pFanout, f, vSelect, Sign );
323 continue;
324 }
325 assert( Gia_ObjIsAnd(pFanout) );
326 pRef0 = Gla_ObjRef( p, Gia_ObjFanin0(pFanout), f );
327 pRef1 = Gla_ObjRef( p, Gia_ObjFanin1(pFanout), f );
328 if ( ((pRef0->Value ^ Gia_ObjFaninC0(pFanout)) == 0 && pRef0->fVisit) ||
329 ((pRef1->Value ^ Gia_ObjFaninC1(pFanout)) == 0 && pRef1->fVisit) ||
330 ( ((pRef0->Value ^ Gia_ObjFaninC0(pFanout)) == 1 && pRef0->fVisit) &&
331 ((pRef1->Value ^ Gia_ObjFaninC1(pFanout)) == 1 && pRef1->fVisit) ) )
332 Gia_ManRefSetAndPropFanout_rec( p, pFanout, f, vSelect, Sign );
333 }
334}
335
347void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect, int Sign )
348{
349 int i;//, Id = Gia_ObjId(p->pGia, pObj);
350 Rfn_Obj_t * pRef = Gla_ObjRef( p, pObj, f );
351// assert( (int)pRef->Sign == Sign );
352 if ( pRef->fVisit )
353 return;
354 if ( p->pPars->fPropFanout )
355 Gia_ManRefSetAndPropFanout_rec( p, pObj, f, vSelect, Sign );
356 else
357 pRef->fVisit = 1;
358 if ( pRef->fPPi )
359 {
360 assert( (int)pRef->Prio > 0 );
361 if ( p->pPars->fPropFanout )
362 {
363 for ( i = p->pPars->iFrame; i >= 0; i-- )
364 if ( !Gla_ObjRef(p, pObj, i)->fVisit )
365 Gia_ManRefSetAndPropFanout_rec( p, pObj, i, vSelect, Sign );
366 }
367 else
368 {
369 Vec_IntPush( vSelect, Gia_ObjId(p->pGia, pObj) );
370 Vec_IntAddToEntry( p->vObjCounts, f, 1 );
371 }
372 return;
373 }
374 if ( Gia_ObjIsPi(p->pGia, pObj) || Gia_ObjIsConst0(pObj) )
375 return;
376 if ( Gia_ObjIsRo(p->pGia, pObj) )
377 {
378 if ( f > 0 )
379 Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj)), f-1, vSelect, Sign );
380 return;
381 }
382 if ( Gia_ObjIsAnd(pObj) )
383 {
384 Rfn_Obj_t * pRef0 = Gla_ObjRef( p, Gia_ObjFanin0(pObj), f );
385 Rfn_Obj_t * pRef1 = Gla_ObjRef( p, Gia_ObjFanin1(pObj), f );
386 if ( pRef->Value == 1 )
387 {
388 if ( pRef0->Prio > 0 )
389 Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vSelect, Sign );
390 if ( pRef1->Prio > 0 )
391 Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vSelect, Sign );
392 }
393 else // select one value
394 {
395 if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
396 {
397 if ( pRef0->Prio <= pRef1->Prio ) // choice
398 {
399 if ( pRef0->Prio > 0 )
400 Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vSelect, Sign );
401 }
402 else
403 {
404 if ( pRef1->Prio > 0 )
405 Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vSelect, Sign );
406 }
407 }
408 else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 )
409 {
410 if ( pRef0->Prio > 0 )
411 Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vSelect, Sign );
412 }
413 else if ( (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
414 {
415 if ( pRef1->Prio > 0 )
416 Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vSelect, Sign );
417 }
418 else assert( 0 );
419 }
420 }
421 else assert( 0 );
422}
423
424
436void Gla_ManVerifyUsingTerSim( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int_t * vRoAnds, Vec_Int_t * vCos, Vec_Int_t * vRes )
437{
438 Gia_Obj_t * pObj;
439 int i, f;
440// Gia_ManForEachObj( p->pGia, pObj, i )
441// assert( Gia_ObjTerSimGetC(pObj) );
442 for ( f = 0; f <= p->pPars->iFrame; f++ )
443 {
444 Gia_ObjTerSimSet0( Gia_ManConst0(p->pGia) );
445 Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
446 {
447 if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
448 Gia_ObjTerSimSet1( pObj );
449 else
450 Gia_ObjTerSimSet0( pObj );
451 }
452 Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
453 Gia_ObjTerSimSetX( pObj );
454 Gia_ManForEachObjVec( vRes, p->pGia, pObj, i )
455 if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
456 Gia_ObjTerSimSet1( pObj );
457 else
458 Gia_ObjTerSimSet0( pObj );
459
460 Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i )
461 {
462 if ( Gia_ObjIsAnd(pObj) )
463 Gia_ObjTerSimAnd( pObj );
464 else if ( f == 0 )
465 Gia_ObjTerSimSet0( pObj );
466 else
467 Gia_ObjTerSimRo( p->pGia, pObj );
468 }
469 Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
470 Gia_ObjTerSimCo( pObj );
471 }
472 pObj = Gia_ManPo( p->pGia, 0 );
473 if ( !Gia_ObjTerSimGet1(pObj) )
474 Abc_Print( 1, "\nRefinement verification has failed!!!\n" );
475 // clear
476 Gia_ObjTerSimSetC( Gia_ManConst0(p->pGia) );
477 Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
478 Gia_ObjTerSimSetC( pObj );
479 Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
480 Gia_ObjTerSimSetC( pObj );
481 Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i )
482 Gia_ObjTerSimSetC( pObj );
483 Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
484 Gia_ObjTerSimSetC( pObj );
485}
486
487
499Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
500{
501 Abc_Cex_t * pCex;
502 Vec_Int_t * vMap, * vVec;
503 Gia_Obj_t * pObj;
504 int i;
505 Gia_GlaPrepareCexAndMap( p, &pCex, &vMap );
506 vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, p->pPars->fNewRefine, 1 );
507 Abc_CexFree( pCex );
508 if ( Vec_IntSize(vVec) == 0 )
509 {
510 Vec_IntFree( vVec );
511 Abc_CexFreeP( &p->pGia->pCexSeq );
512 p->pGia->pCexSeq = Gla_ManDeriveCex( p, vMap );
513 Vec_IntFree( vMap );
514 return NULL;
515 }
516 Vec_IntFree( vMap );
517 // remap them into GLA objects
518 Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
519 Vec_IntWriteEntry( vVec, i, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] );
520 p->nObjAdded += Vec_IntSize(vVec);
521 return vVec;
522}
523
535Vec_Int_t * Gla_ManRefinement2( Gla_Man_t * p )
536{
537 int fVerify = 1;
538 static int Sign = 0;
539 Vec_Int_t * vPis, * vPPis, * vCos, * vRoAnds, * vSelect = NULL;
540 Rfn_Obj_t * pRef, * pRef0, * pRef1;
541 Gia_Obj_t * pObj;
542 int i, f;
543 Sign++;
544
545 // compute PIs and pseudo-PIs
546 vCos = Vec_IntAlloc( 1000 );
547 vPis = Vec_IntAlloc( 1000 );
548 vPPis = Vec_IntAlloc( 1000 );
549 vRoAnds = Vec_IntAlloc( 1000 );
550 Gla_ManCollect( p, vPis, vPPis, vCos, vRoAnds );
551
552/*
553 // check how many pseudo PIs have variables
554 Gla_ManForEachObjAbsVec( vPis, p, pGla, i )
555 {
556 Abc_Print( 1, " %5d : ", Gla_ObjId(p, pGla) );
557 for ( f = 0; f <= p->pPars->iFrame; f++ )
558 Abc_Print( 1, "%d", Gla_ManCheckVar(p, Gla_ObjId(p, pGla), f) );
559 Abc_Print( 1, "\n" );
560 }
561
562 // check how many pseudo PIs have variables
563 Gla_ManForEachObjAbsVec( vPPis, p, pGla, i )
564 {
565 Abc_Print( 1, "%5d : ", Gla_ObjId(p, pGla) );
566 for ( f = 0; f <= p->pPars->iFrame; f++ )
567 Abc_Print( 1, "%d", Gla_ManCheckVar(p, Gla_ObjId(p, pGla), f) );
568 Abc_Print( 1, "\n" );
569 }
570*/
571 // propagate values
572 for ( f = 0; f <= p->pPars->iFrame; f++ )
573 {
574 // constant
575 pRef = Gla_ObjRef( p, Gia_ManConst0(p->pGia), f ); Gla_ObjClearRef( pRef );
576 pRef->Value = 0;
577 pRef->Prio = 0;
578 pRef->Sign = Sign;
579 // primary input
580 Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
581 {
582// assert( f == p->pPars->iFrame || Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) );
583 pRef = Gla_ObjRef( p, pObj, f ); Gla_ObjClearRef( pRef );
584 pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f );
585 pRef->Prio = 0;
586 pRef->Sign = Sign;
587 assert( pRef->fVisit == 0 );
588 }
589 // primary input
590 Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
591 {
592// assert( f == p->pPars->iFrame || Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) );
593 assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
594 pRef = Gla_ObjRef( p, pObj, f ); Gla_ObjClearRef( pRef );
595 pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f );
596 pRef->Prio = i+1;
597 pRef->fPPi = 1;
598 pRef->Sign = Sign;
599 assert( pRef->fVisit == 0 );
600 }
601 // internal nodes
602 Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i )
603 {
604 assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
605 pRef = Gla_ObjRef( p, pObj, f ); Gla_ObjClearRef( pRef );
606 if ( Gia_ObjIsRo(p->pGia, pObj) )
607 {
608 if ( f == 0 )
609 {
610 pRef->Value = 0;
611 pRef->Prio = 0;
612 pRef->Sign = Sign;
613 }
614 else
615 {
616 pRef0 = Gla_ObjRef( p, Gia_ObjRoToRi(p->pGia, pObj), f-1 );
617 pRef->Value = pRef0->Value;
618 pRef->Prio = pRef0->Prio;
619 pRef->Sign = Sign;
620 }
621 continue;
622 }
623 assert( Gia_ObjIsAnd(pObj) );
624 pRef0 = Gla_ObjRef( p, Gia_ObjFanin0(pObj), f );
625 pRef1 = Gla_ObjRef( p, Gia_ObjFanin1(pObj), f );
626 pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj)) & (pRef1->Value ^ Gia_ObjFaninC1(pObj));
627
628 if ( p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] != ~0 &&
629 Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) &&
630 (int)pRef->Value != Gla_ObjSatValue(p, Gia_ObjId(p->pGia, pObj), f) )
631 {
632 Abc_Print( 1, "Object has value mismatch " );
633 Gia_ObjPrint( p->pGia, pObj );
634 }
635
636 if ( pRef->Value == 1 )
637 pRef->Prio = Abc_MaxInt( pRef0->Prio, pRef1->Prio );
638 else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
639 pRef->Prio = Abc_MinInt( pRef0->Prio, pRef1->Prio ); // choice
640 else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 )
641 pRef->Prio = pRef0->Prio;
642 else
643 pRef->Prio = pRef1->Prio;
644 assert( pRef->fVisit == 0 );
645 pRef->Sign = Sign;
646 }
647 // output nodes
648 Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
649 {
650 pRef = Gla_ObjRef( p, pObj, f ); Gla_ObjClearRef( pRef );
651 pRef0 = Gla_ObjRef( p, Gia_ObjFanin0(pObj), f );
652 pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj));
653 pRef->Prio = pRef0->Prio;
654 assert( pRef->fVisit == 0 );
655 pRef->Sign = Sign;
656 }
657 }
658
659 // make sure the output value is 1
660 pObj = Gia_ManPo( p->pGia, 0 );
661 pRef = Gla_ObjRef( p, pObj, p->pPars->iFrame );
662 if ( pRef->Value != 1 )
663 Abc_Print( 1, "\nCounter-example verification has failed!!!\n" );
664
665 // check the CEX
666 if ( pRef->Prio == 0 )
667 {
668 p->pGia->pCexSeq = Gla_ManDeriveCex( p, vPis );
669 Vec_IntFree( vPis );
670 Vec_IntFree( vPPis );
671 Vec_IntFree( vRoAnds );
672 Vec_IntFree( vCos );
673 return NULL;
674 }
675
676 // select objects
677 vSelect = Vec_IntAlloc( 100 );
678 Vec_IntFill( p->vObjCounts, p->pPars->iFrame+1, 0 );
679 Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), p->pPars->iFrame, vSelect, Sign );
680 Vec_IntUniqify( vSelect );
681
682/*
683 for ( f = 0; f < p->pPars->iFrame; f++ )
684 printf( "%2d", Vec_IntEntry(p->vObjCounts, f) );
685 printf( "\n" );
686*/
687 if ( fVerify )
688 Gla_ManVerifyUsingTerSim( p, vPis, vPPis, vRoAnds, vCos, vSelect );
689
690 // remap them into GLA objects
691 Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i )
692 Vec_IntWriteEntry( vSelect, i, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] );
693
694 Vec_IntFree( vPis );
695 Vec_IntFree( vPPis );
696 Vec_IntFree( vRoAnds );
697 Vec_IntFree( vCos );
698
699 p->nObjAdded += Vec_IntSize(vSelect);
700 return vSelect;
701}
702
703
715void Gla_ManCollectFanins( Gla_Man_t * p, Gla_Obj_t * pGla, int iObj, Vec_Int_t * vFanins )
716{
717 int i, nClauses, iFirstClause, * pLit;
718 nClauses = p->pCnf->pObj2Count[pGla->iGiaObj];
719 iFirstClause = p->pCnf->pObj2Clause[pGla->iGiaObj];
720 Vec_IntClear( vFanins );
721 for ( i = iFirstClause; i < iFirstClause + nClauses; i++ )
722 for ( pLit = p->pCnf->pClauses[i]; pLit < p->pCnf->pClauses[i+1]; pLit++ )
723 if ( lit_var(*pLit) != iObj )
724 Vec_IntPushUnique( vFanins, lit_var(*pLit) );
725 assert( Vec_IntSize( vFanins ) <= 4 );
726 Vec_IntSort( vFanins, 0 );
727}
728
729
741void Gia_ManDupMapped_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew )
742{
743 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
744 return;
745 Gia_ObjSetTravIdCurrent(p, pObj);
746 assert( Gia_ObjIsAnd(pObj) );
747 Gia_ManDupMapped_rec( p, Gia_ObjFanin0(pObj), pNew );
748 Gia_ManDupMapped_rec( p, Gia_ObjFanin1(pObj), pNew );
749 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
750 Vec_IntPush( pNew->vLutConfigs, Gia_ObjId(p, pObj) );
751}
752Gia_Man_t * Gia_ManDupMapped( Gia_Man_t * p, Vec_Int_t * vMapping )
753{
754 Gia_Man_t * pNew;
755 Gia_Obj_t * pObj, * pFanin;
756 int i, k, * pMapping, * pObj2Obj;
757 // start new manager
758 pNew = Gia_ManStart( Gia_ManObjNum(p) );
759 pNew->pName = Abc_UtilStrsav( p->pName );
760 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
761 // start mapping
762 Gia_ManFillValue( p );
763 pObj2Obj = ABC_FALLOC( int, Gia_ManObjNum(p) );
764 pObj2Obj[0] = 0;
765 // create reverse mapping and attach it to the node
766 pNew->vLutConfigs = Vec_IntAlloc( Gia_ManObjNum(p) * 4 / 3 );
767 Vec_IntPush( pNew->vLutConfigs, 0 );
768 Gia_ManForEachObj1( p, pObj, i )
769 {
770 if ( Gia_ObjIsAnd(pObj) )
771 {
772 int Offset = Vec_IntEntry(vMapping, Gia_ObjId(p, pObj));
773 if ( Offset == 0 )
774 continue;
775 pMapping = Vec_IntEntryP( vMapping, Offset );
776 Gia_ManIncrementTravId( p );
777 for ( k = 1; k <= 4; k++ )
778 {
779 if ( pMapping[k] == -1 )
780 continue;
781 pFanin = Gia_ManObj(p, pMapping[k]);
782 Gia_ObjSetTravIdCurrent( p, pFanin );
783 pFanin->Value = pObj2Obj[pMapping[k]];
784 assert( ~pFanin->Value );
785 }
786 assert( !Gia_ObjIsTravIdCurrent(p, pObj) );
787 assert( !~pObj->Value );
788 Gia_ManDupMapped_rec( p, pObj, pNew );
789 pObj2Obj[i] = pObj->Value;
790 assert( ~pObj->Value );
791 }
792 else if ( Gia_ObjIsCi(pObj) )
793 {
794 pObj2Obj[i] = Gia_ManAppendCi( pNew );
795 Vec_IntPush( pNew->vLutConfigs, i );
796 }
797 else if ( Gia_ObjIsCo(pObj) )
798 {
799 Gia_ObjFanin0(pObj)->Value = pObj2Obj[Gia_ObjFaninId0p(p, pObj)];
800 assert( ~Gia_ObjFanin0(pObj)->Value );
801 pObj2Obj[i] = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
802 Vec_IntPush( pNew->vLutConfigs, i );
803 }
804 }
805 assert( Vec_IntSize(pNew->vLutConfigs) == Gia_ManObjNum(pNew) );
806 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
807 // map original AIG into the new AIG
808 Gia_ManForEachObj( p, pObj, i )
809 pObj->Value = pObj2Obj[i];
810 ABC_FREE( pObj2Obj );
811 return pNew;
812}
813
825Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Abs_Par_t * pPars )
826{
827 Gla_Man_t * p;
828 Aig_Man_t * pAig;
829 Gia_Obj_t * pObj;
830 Gla_Obj_t * pGla;
831 Vec_Int_t * vMappingNew;
832 int i, k, Offset, * pMapping, * pLits, * pObj2Count, * pObj2Clause;
833
834 // start
835 p = ABC_CALLOC( Gla_Man_t, 1 );
836 p->pGia0 = pGia0;
837 p->pPars = pPars;
838 p->vAbs = Vec_IntAlloc( 100 );
839 p->vTemp = Vec_IntAlloc( 100 );
840 p->vAddedNew = Vec_IntAlloc( 100 );
841 p->vObjCounts = Vec_IntAlloc( 100 );
842
843 // internal data
844 pAig = Gia_ManToAigSimple( pGia0 );
845 p->pCnf = Cnf_DeriveOther( pAig, 1 );
846 Aig_ManStop( pAig );
847 // create working GIA
848 p->pGia = Gia_ManDupMapped( pGia0, p->pCnf->vMapping );
849 if ( pPars->fPropFanout )
850 Gia_ManStaticFanoutStart( p->pGia );
851
852 // derive new gate map
853 assert( pGia0->vGateClasses != 0 );
854 p->pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) );
855 p->vCoreCounts = Vec_IntStart( Gia_ManObjNum(p->pGia) );
856 p->vProofIds = Vec_IntAlloc(0);
857 // update p->pCnf->vMapping, p->pCnf->pObj2Count, p->pCnf->pObj2Clause
858 // (here are not updating p->pCnf->pVarNums because it is not needed)
859 vMappingNew = Vec_IntStart( Gia_ManObjNum(p->pGia) );
860 pObj2Count = ABC_FALLOC( int, Gia_ManObjNum(p->pGia) );
861 pObj2Clause = ABC_FALLOC( int, Gia_ManObjNum(p->pGia) );
862 Gia_ManForEachObj( pGia0, pObj, i )
863 {
864 // skip internal nodes not used in the mapping
865 if ( !~pObj->Value )
866 continue;
867 // replace positive literal by variable
868 assert( !Abc_LitIsCompl(pObj->Value) );
869 pObj->Value = Abc_Lit2Var(pObj->Value);
870 assert( (int)pObj->Value < Gia_ManObjNum(p->pGia) );
871 // update arrays
872 pObj2Count[pObj->Value] = p->pCnf->pObj2Count[i];
873 pObj2Clause[pObj->Value] = p->pCnf->pObj2Clause[i];
874 if ( Vec_IntEntry(pGia0->vGateClasses, i) )
875 Vec_IntWriteEntry( p->pGia->vGateClasses, pObj->Value, 1 );
876 // update mappings
877 Offset = Vec_IntEntry(p->pCnf->vMapping, i);
878 Vec_IntWriteEntry( vMappingNew, pObj->Value, Vec_IntSize(vMappingNew) );
879 pMapping = Vec_IntEntryP(p->pCnf->vMapping, Offset);
880 Vec_IntPush( vMappingNew, pMapping[0] );
881 for ( k = 1; k <= 4; k++ )
882 {
883 if ( pMapping[k] == -1 )
884 Vec_IntPush( vMappingNew, -1 );
885 else
886 {
887 assert( ~Gia_ManObj(pGia0, pMapping[k])->Value );
888 Vec_IntPush( vMappingNew, Gia_ManObj(pGia0, pMapping[k])->Value );
889 }
890 }
891 }
892 // update mapping after the offset (currently not being done because it is not used)
893 Vec_IntFree( p->pCnf->vMapping ); p->pCnf->vMapping = vMappingNew;
894 ABC_FREE( p->pCnf->pObj2Count ); p->pCnf->pObj2Count = pObj2Count;
895 ABC_FREE( p->pCnf->pObj2Clause ); p->pCnf->pObj2Clause = pObj2Clause;
896
897
898 // count the number of variables
899 p->nObjs = 1;
900 Gia_ManForEachObj( p->pGia, pObj, i )
901 if ( p->pCnf->pObj2Count[i] >= 0 )
902 pObj->Value = p->nObjs++;
903 else
904 pObj->Value = ~0;
905
906 // re-express CNF using new variable IDs
907 pLits = p->pCnf->pClauses[0];
908 for ( i = 0; i < p->pCnf->nLiterals; i++ )
909 {
910 // find the original AIG object
911 pObj = Gia_ManObj( pGia0, lit_var(pLits[i]) );
912 assert( ~pObj->Value );
913 // find the working AIG object
914 pObj = Gia_ManObj( p->pGia, pObj->Value );
915 assert( ~pObj->Value );
916 // express literal in terms of LUT variables
917 pLits[i] = toLitCond( pObj->Value, lit_sign(pLits[i]) );
918 }
919
920 // create objects
921 p->pObjs = ABC_CALLOC( Gla_Obj_t, p->nObjs );
922 p->pObj2Obj = ABC_FALLOC( unsigned, Gia_ManObjNum(p->pGia) );
923// p->pvRefis = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(p->pGia) );
924 Gia_ManForEachObj( p->pGia, pObj, i )
925 {
926 p->pObj2Obj[i] = pObj->Value;
927 if ( !~pObj->Value )
928 continue;
929 pGla = Gla_ManObj( p, pObj->Value );
930 pGla->iGiaObj = i;
931 pGla->fCompl0 = Gia_ObjFaninC0(pObj);
932 pGla->fConst = Gia_ObjIsConst0(pObj);
933 pGla->fPi = Gia_ObjIsPi(p->pGia, pObj);
934 pGla->fPo = Gia_ObjIsPo(p->pGia, pObj);
935 pGla->fRi = Gia_ObjIsRi(p->pGia, pObj);
936 pGla->fRo = Gia_ObjIsRo(p->pGia, pObj);
937 pGla->fAnd = Gia_ObjIsAnd(pObj);
938 if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) )
939 continue;
940 if ( Gia_ObjIsCo(pObj) )
941 {
942 pGla->nFanins = 1;
943 pGla->Fanins[0] = Gia_ObjFanin0(pObj)->Value;
944 continue;
945 }
946 if ( Gia_ObjIsAnd(pObj) )
947 {
948// Gla_ManCollectFanins( p, pGla, pObj->Value, p->vTemp );
949// pGla->nFanins = Vec_IntSize( p->vTemp );
950// memcpy( pGla->Fanins, Vec_IntArray(p->vTemp), sizeof(int) * Vec_IntSize(p->vTemp) );
951 Offset = Vec_IntEntry( p->pCnf->vMapping, i );
952 pMapping = Vec_IntEntryP( p->pCnf->vMapping, Offset );
953 pGla->nFanins = 0;
954 for ( k = 1; k <= 4; k++ )
955 if ( pMapping[k] != -1 )
956 pGla->Fanins[ pGla->nFanins++ ] = Gia_ManObj(p->pGia, pMapping[k])->Value;
957 continue;
958 }
959 assert( Gia_ObjIsRo(p->pGia, pObj) );
960 pGla->nFanins = 1;
961 pGla->Fanins[0] = Gia_ObjFanin0( Gia_ObjRoToRi(p->pGia, pObj) )->Value;
962 pGla->fCompl0 = Gia_ObjFaninC0( Gia_ObjRoToRi(p->pGia, pObj) );
963 }
964 p->pObjRoot = Gla_ManObj( p, Gia_ManPo(p->pGia, 0)->Value );
965 // abstraction
966 assert( p->pGia->vGateClasses != NULL );
967 Gla_ManForEachObj( p, pGla )
968 {
969 if ( Vec_IntEntry( p->pGia->vGateClasses, pGla->iGiaObj ) == 0 )
970 continue;
971 pGla->fAbs = 1;
972 Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) );
973 }
974 // other
975 p->pSat = sat_solver2_new();
976 if ( pPars->fUseFullProof )
977 p->pSat->pPrf1 = Vec_SetAlloc( 20 );
978// p->pSat->fVerbose = p->pPars->fVerbose;
979// sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax );
980 p->pSat->nLearntStart = p->pPars->nLearnedStart;
981 p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
982 p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
983 p->pSat->nLearntMax = p->pSat->nLearntStart;
984 p->nSatVars = 1;
985 // start the refinement manager
986// p->pGia2 = Gia_ManDup( p->pGia );
987 p->pRnm = Rnm_ManStart( p->pGia );
988 return p;
989}
990
1002Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia, Abs_Par_t * pPars )
1003{
1004 Gla_Man_t * p;
1005 Aig_Man_t * pAig;
1006 Gia_Obj_t * pObj;
1007 Gla_Obj_t * pGla;
1008 int i, * pLits;
1009 // start
1010 p = ABC_CALLOC( Gla_Man_t, 1 );
1011 p->pGia = pGia;
1012 p->pPars = pPars;
1013 p->vAbs = Vec_IntAlloc( 100 );
1014 p->vTemp = Vec_IntAlloc( 100 );
1015 p->vAddedNew = Vec_IntAlloc( 100 );
1016 // internal data
1017 pAig = Gia_ManToAigSimple( p->pGia );
1018 p->pCnf = Cnf_DeriveOther( pAig, 1 );
1019 Aig_ManStop( pAig );
1020 // count the number of variables
1021 p->nObjs = 1;
1022 Gia_ManForEachObj( p->pGia, pObj, i )
1023 if ( p->pCnf->pObj2Count[i] >= 0 )
1024 pObj->Value = p->nObjs++;
1025 else
1026 pObj->Value = ~0;
1027 // re-express CNF using new variable IDs
1028 pLits = p->pCnf->pClauses[0];
1029 for ( i = 0; i < p->pCnf->nLiterals; i++ )
1030 {
1031 pObj = Gia_ManObj( p->pGia, lit_var(pLits[i]) );
1032 assert( ~pObj->Value );
1033 pLits[i] = toLitCond( pObj->Value, lit_sign(pLits[i]) );
1034 }
1035 // create objects
1036 p->pObjs = ABC_CALLOC( Gla_Obj_t, p->nObjs );
1037 p->pObj2Obj = ABC_FALLOC( unsigned, Gia_ManObjNum(p->pGia) );
1038// p->pvRefis = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(p->pGia) );
1039 Gia_ManForEachObj( p->pGia, pObj, i )
1040 {
1041 p->pObj2Obj[i] = pObj->Value;
1042 if ( !~pObj->Value )
1043 continue;
1044 pGla = Gla_ManObj( p, pObj->Value );
1045 pGla->iGiaObj = i;
1046 pGla->fCompl0 = Gia_ObjFaninC0(pObj);
1047 pGla->fConst = Gia_ObjIsConst0(pObj);
1048 pGla->fPi = Gia_ObjIsPi(p->pGia, pObj);
1049 pGla->fPo = Gia_ObjIsPo(p->pGia, pObj);
1050 pGla->fRi = Gia_ObjIsRi(p->pGia, pObj);
1051 pGla->fRo = Gia_ObjIsRo(p->pGia, pObj);
1052 pGla->fAnd = Gia_ObjIsAnd(pObj);
1053 if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) )
1054 continue;
1055 if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) )
1056 {
1057 Gla_ManCollectFanins( p, pGla, pObj->Value, p->vTemp );
1058 pGla->nFanins = Vec_IntSize( p->vTemp );
1059 memcpy( pGla->Fanins, Vec_IntArray(p->vTemp), sizeof(int) * Vec_IntSize(p->vTemp) );
1060 continue;
1061 }
1062 assert( Gia_ObjIsRo(p->pGia, pObj) );
1063 pGla->nFanins = 1;
1064 pGla->Fanins[0] = Gia_ObjFanin0( Gia_ObjRoToRi(p->pGia, pObj) )->Value;
1065 pGla->fCompl0 = Gia_ObjFaninC0( Gia_ObjRoToRi(p->pGia, pObj) );
1066 }
1067 p->pObjRoot = Gla_ManObj( p, Gia_ManPo(p->pGia, 0)->Value );
1068 // abstraction
1069 assert( pGia->vGateClasses != NULL );
1070 Gla_ManForEachObj( p, pGla )
1071 {
1072 if ( Vec_IntEntry( pGia->vGateClasses, pGla->iGiaObj ) == 0 )
1073 continue;
1074 pGla->fAbs = 1;
1075 Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) );
1076 }
1077 // other
1078 p->pSat = sat_solver2_new();
1079 p->nSatVars = 1;
1080 return p;
1081}
1082
1094void Gla_ManStop( Gla_Man_t * p )
1095{
1096 Gla_Obj_t * pGla;
1097 int i;
1098
1099 if ( p->pPars->fVerbose )
1100 Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d Objs+ = %d\n",
1101 sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat),
1102 sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
1103
1104 // stop the refinement manager
1105// Gia_ManStopP( &p->pGia2 );
1106 Rnm_ManStop( p->pRnm, 0 );
1107
1108 if ( p->pvRefis )
1109 for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
1110 ABC_FREE( p->pvRefis[i].pArray );
1111 Gla_ManForEachObj( p, pGla )
1112 ABC_FREE( pGla->vFrames.pArray );
1113 Cnf_DataFree( p->pCnf );
1114 if ( p->pGia0 != NULL )
1115 Gia_ManStop( p->pGia );
1116// Gia_ManStaticFanoutStart( p->pGia0 );
1117 sat_solver2_delete( p->pSat );
1118 Vec_IntFreeP( &p->vObjCounts );
1119 Vec_IntFreeP( &p->vAddedNew );
1120 Vec_IntFreeP( &p->vCoreCounts );
1121 Vec_IntFreeP( &p->vProofIds );
1122 Vec_IntFreeP( &p->vTemp );
1123 Vec_IntFreeP( &p->vAbs );
1124 ABC_FREE( p->pvRefis );
1125 ABC_FREE( p->pObj2Obj );
1126 ABC_FREE( p->pObjs );
1127 ABC_FREE( p );
1128}
1129
1141int Gia_GlaAbsCount( Gla_Man_t * p, int fRo, int fAnd )
1142{
1143 Gla_Obj_t * pObj;
1144 int i, Counter = 0;
1145 if ( fRo )
1146 Gla_ManForEachObjAbs( p, pObj, i )
1147 Counter += (pObj->fRo && pObj->fAbs);
1148 else if ( fAnd )
1149 Gla_ManForEachObjAbs( p, pObj, i )
1150 Counter += (pObj->fAnd && pObj->fAbs);
1151 else
1152 Gla_ManForEachObjAbs( p, pObj, i )
1153 Counter += (pObj->fAbs);
1154 return Counter;
1155}
1156
1157
1169int Gla_ManTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vGla, int nUsageCount )
1170{
1171 int Value0, Value1;
1172 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
1173 return 1;
1174 Gia_ObjSetTravIdCurrent(p, pObj);
1175 if ( Gia_ObjIsCi(pObj) )
1176 return 0;
1177 assert( Gia_ObjIsAnd(pObj) );
1178 Value0 = Gla_ManTranslate_rec( p, Gia_ObjFanin0(pObj), vGla, nUsageCount );
1179 Value1 = Gla_ManTranslate_rec( p, Gia_ObjFanin1(pObj), vGla, nUsageCount );
1180 if ( Value0 || Value1 )
1181 Vec_IntAddToEntry( vGla, Gia_ObjId(p, pObj), nUsageCount );
1182 return Value0 || Value1;
1183}
1184Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p )
1185{
1186 Vec_Int_t * vGla, * vGla2;
1187 Gla_Obj_t * pObj, * pFanin;
1188 Gia_Obj_t * pGiaObj;
1189 int i, k, nUsageCount;
1190 vGla = Vec_IntStart( Gia_ManObjNum(p->pGia) );
1191 Gla_ManForEachObjAbs( p, pObj, i )
1192 {
1193 nUsageCount = Vec_IntEntry(p->vCoreCounts, pObj->iGiaObj);
1194 assert( nUsageCount >= 0 );
1195 if ( nUsageCount == 0 )
1196 nUsageCount++;
1197 pGiaObj = Gla_ManGiaObj( p, pObj );
1198 if ( Gia_ObjIsConst0(pGiaObj) || Gia_ObjIsRo(p->pGia, pGiaObj) )
1199 {
1200 Vec_IntWriteEntry( vGla, pObj->iGiaObj, nUsageCount );
1201 continue;
1202 }
1203 assert( Gia_ObjIsAnd(pGiaObj) );
1204 Gia_ManIncrementTravId( p->pGia );
1205 Gla_ObjForEachFanin( p, pObj, pFanin, k )
1206 Gia_ObjSetTravIdCurrent( p->pGia, Gla_ManGiaObj(p, pFanin) );
1207 Gla_ManTranslate_rec( p->pGia, pGiaObj, vGla, nUsageCount );
1208 }
1209 Vec_IntWriteEntry( vGla, 0, p->pPars->iFrame+1 );
1210 if ( p->pGia->vLutConfigs ) // use mapping from new to old
1211 {
1212 vGla2 = Vec_IntStart( Gia_ManObjNum(p->pGia0) );
1213 for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
1214 if ( Vec_IntEntry(vGla, i) )
1215 Vec_IntWriteEntry( vGla2, Vec_IntEntry(p->pGia->vLutConfigs, i), Vec_IntEntry(vGla, i) );
1216 Vec_IntFree( vGla );
1217 return vGla2;
1218 }
1219 return vGla;
1220}
1221
1222
1234Vec_Int_t * Gla_ManCollectPPis( Gla_Man_t * p, Vec_Int_t * vPis )
1235{
1236 Vec_Int_t * vPPis;
1237 Gla_Obj_t * pObj, * pFanin;
1238 int i, k;
1239 vPPis = Vec_IntAlloc( 1000 );
1240 if ( vPis )
1241 Vec_IntClear( vPis );
1242 Gla_ManForEachObjAbs( p, pObj, i )
1243 {
1244 assert( pObj->fConst || pObj->fRo || pObj->fAnd );
1245 Gla_ObjForEachFanin( p, pObj, pFanin, k )
1246 if ( !pFanin->fPi && !pFanin->fAbs )
1247 Vec_IntPush( vPPis, pObj->Fanins[k] );
1248 else if ( vPis && pFanin->fPi && !pFanin->fAbs )
1249 Vec_IntPush( vPis, pObj->Fanins[k] );
1250 }
1251 Vec_IntUniqify( vPPis );
1252 Vec_IntReverseOrder( vPPis );
1253 if ( vPis )
1254 Vec_IntUniqify( vPis );
1255 return vPPis;
1256}
1257int Gla_ManCountPPis( Gla_Man_t * p )
1258{
1259 Vec_Int_t * vPPis = Gla_ManCollectPPis( p, NULL );
1260 int RetValue = Vec_IntSize( vPPis );
1261 Vec_IntFree( vPPis );
1262 return RetValue;
1263}
1264void Gla_ManExplorePPis( Gla_Man_t * p, Vec_Int_t * vPPis )
1265{
1266 static int Round = 0;
1267 Gla_Obj_t * pObj, * pFanin;
1268 int i, j, k, Count;
1269 if ( (Round++ % 5) == 0 )
1270 return;
1271 j = 0;
1272 Gla_ManForEachObjAbsVec( vPPis, p, pObj, i )
1273 {
1274 assert( pObj->fAbs == 0 );
1275 Count = 0;
1276 Gla_ObjForEachFanin( p, pObj, pFanin, k )
1277 Count += pFanin->fAbs;
1278 if ( Count == 0 || ((Round & 1) && Count == 1) )
1279 continue;
1280 Vec_IntWriteEntry( vPPis, j++, Gla_ObjId(p, pObj) );
1281 }
1282// printf( "\n%d -> %d\n", Vec_IntSize(vPPis), j );
1283 Vec_IntShrink( vPPis, j );
1284}
1285
1286
1298int Gla_ManCheckVar( Gla_Man_t * p, int iObj, int iFrame )
1299{
1300 Gla_Obj_t * pGla = Gla_ManObj( p, iObj );
1301 int iVar = Vec_IntGetEntry( &pGla->vFrames, iFrame );
1302 assert( !pGla->fPo && !pGla->fRi );
1303 return (iVar > 0);
1304}
1305int Gla_ManGetVar( Gla_Man_t * p, int iObj, int iFrame )
1306{
1307 Gla_Obj_t * pGla = Gla_ManObj( p, iObj );
1308 int iVar = Vec_IntGetEntry( &pGla->vFrames, iFrame );
1309 assert( !pGla->fPo && !pGla->fRi );
1310 if ( iVar == 0 )
1311 {
1312 Vec_IntSetEntry( &pGla->vFrames, iFrame, (iVar = p->nSatVars++) );
1313 // remember the change
1314 Vec_IntPush( p->vAddedNew, iObj );
1315 Vec_IntPush( p->vAddedNew, iFrame );
1316 }
1317 return iVar;
1318}
1319void Gla_ManAddClauses( Gla_Man_t * p, int iObj, int iFrame, Vec_Int_t * vLits )
1320{
1321 Gla_Obj_t * pGlaObj = Gla_ManObj( p, iObj );
1322 int iVar, iVar1, iVar2;
1323 if ( pGlaObj->fConst )
1324 {
1325 iVar = Gla_ManGetVar( p, iObj, iFrame );
1326 sat_solver2_add_const( p->pSat, iVar, 1, 0, iObj );
1327 }
1328 else if ( pGlaObj->fRo )
1329 {
1330 assert( pGlaObj->nFanins == 1 );
1331 if ( iFrame == 0 )
1332 {
1333 iVar = Gla_ManGetVar( p, iObj, iFrame );
1334 sat_solver2_add_const( p->pSat, iVar, 1, 0, iObj );
1335 }
1336 else
1337 {
1338 iVar1 = Gla_ManGetVar( p, iObj, iFrame );
1339 iVar2 = Gla_ManGetVar( p, pGlaObj->Fanins[0], iFrame-1 );
1340 sat_solver2_add_buffer( p->pSat, iVar1, iVar2, pGlaObj->fCompl0, 0, iObj );
1341 }
1342 }
1343 else if ( pGlaObj->fAnd )
1344 {
1345 int i, RetValue, nClauses, iFirstClause, * pLit;
1346 nClauses = p->pCnf->pObj2Count[pGlaObj->iGiaObj];
1347 iFirstClause = p->pCnf->pObj2Clause[pGlaObj->iGiaObj];
1348 for ( i = iFirstClause; i < iFirstClause + nClauses; i++ )
1349 {
1350 Vec_IntClear( vLits );
1351 for ( pLit = p->pCnf->pClauses[i]; pLit < p->pCnf->pClauses[i+1]; pLit++ )
1352 {
1353 iVar = Gla_ManGetVar( p, lit_var(*pLit), iFrame );
1354 Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
1355 }
1356 RetValue = sat_solver2_addclause( p->pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits), iObj );
1357 }
1358 }
1359 else assert( 0 );
1360}
1361void Gia_GlaAddToCounters( Gla_Man_t * p, Vec_Int_t * vCore )
1362{
1363 Gla_Obj_t * pGla;
1364 int i;
1365 Gla_ManForEachObjAbsVec( vCore, p, pGla, i )
1366 Vec_IntAddToEntry( p->vCoreCounts, pGla->iGiaObj, 1 );
1367}
1368void Gia_GlaAddToAbs( Gla_Man_t * p, Vec_Int_t * vAbsAdd, int fCheck )
1369{
1370 Gla_Obj_t * pGla;
1371 int i, k = 0;
1372 Gla_ManForEachObjAbsVec( vAbsAdd, p, pGla, i )
1373 {
1374 if ( fCheck )
1375 {
1376 assert( pGla->fAbs == 0 );
1377 if ( p->pSat->pPrf2 )
1378 Vec_IntWriteEntry( p->vProofIds, Gla_ObjId(p, pGla), p->nProofIds++ );
1379 }
1380 if ( pGla->fAbs )
1381 continue;
1382 pGla->fAbs = 1;
1383 Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) );
1384 // filter clauses to remove those contained in the abstraction
1385 Vec_IntWriteEntry( vAbsAdd, k++, Gla_ObjId(p, pGla) );
1386 }
1387 Vec_IntShrink( vAbsAdd, k );
1388}
1389void Gia_GlaAddTimeFrame( Gla_Man_t * p, int f )
1390{
1391 Gla_Obj_t * pObj;
1392 int i;
1393 Gla_ManForEachObjAbs( p, pObj, i )
1394 Gla_ManAddClauses( p, Gla_ObjId(p, pObj), f, p->vTemp );
1395 sat_solver2_simplify( p->pSat );
1396}
1397void Gia_GlaAddOneSlice( Gla_Man_t * p, int fCur, Vec_Int_t * vCore )
1398{
1399 int f, i, iGlaObj;
1400 for ( f = fCur; f >= 0; f-- )
1401 Vec_IntForEachEntry( vCore, iGlaObj, i )
1402 Gla_ManAddClauses( p, iGlaObj, f, p->vTemp );
1403 sat_solver2_simplify( p->pSat );
1404}
1405void Gla_ManRollBack( Gla_Man_t * p )
1406{
1407 int i, iObj, iFrame;
1408 Vec_IntForEachEntryDouble( p->vAddedNew, iObj, iFrame, i )
1409 {
1410 assert( Vec_IntEntry( &Gla_ManObj(p, iObj)->vFrames, iFrame ) > 0 );
1411 Vec_IntWriteEntry( &Gla_ManObj(p, iObj)->vFrames, iFrame, 0 );
1412 }
1413 Vec_IntForEachEntryStart( p->vAbs, iObj, i, p->nAbsOld )
1414 {
1415 assert( Gla_ManObj( p, iObj )->fAbs == 1 );
1416 Gla_ManObj( p, iObj )->fAbs = 0;
1417 }
1418 Vec_IntShrink( p->vAbs, p->nAbsOld );
1419}
1420
1421
1422
1423
1424
1436int Gla_ManGetOutLit( Gla_Man_t * p, int f )
1437{
1438 Gla_Obj_t * pFanin = Gla_ManObj( p, p->pObjRoot->Fanins[0] );
1439 int iSat = Vec_IntEntry( &pFanin->vFrames, f );
1440 assert( iSat > 0 );
1441 if ( f == 0 && pFanin->fRo && !p->pObjRoot->fCompl0 )
1442 return -1;
1443 return Abc_Var2Lit( iSat, p->pObjRoot->fCompl0 );
1444}
1445Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls )
1446{
1447 Vec_Int_t * vCore = NULL;
1448 int nConfPrev = pSat->stats.conflicts;
1449 int RetValue, iLit = Gla_ManGetOutLit( p, f );
1450 abctime clk = Abc_Clock();
1451 if ( piRetValue )
1452 *piRetValue = 1;
1453 // consider special case when PO points to the flop
1454 // this leads to immediate conflict in the first timeframe
1455 if ( iLit == -1 )
1456 {
1457 vCore = Vec_IntAlloc( 1 );
1458 Vec_IntPush( vCore, p->pObjRoot->Fanins[0] );
1459 return vCore;
1460 }
1461 // solve the problem
1462 RetValue = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1463 if ( pnConfls )
1464 *pnConfls = (int)pSat->stats.conflicts - nConfPrev;
1465 if ( RetValue == l_Undef )
1466 {
1467 if ( piRetValue )
1468 *piRetValue = -1;
1469 return NULL;
1470 }
1471 if ( RetValue == l_True )
1472 {
1473 if ( piRetValue )
1474 *piRetValue = 0;
1475 return NULL;
1476 }
1477 if ( fVerbose )
1478 {
1479// Abc_Print( 1, "%6d", (int)pSat->stats.conflicts - nConfPrev );
1480// Abc_Print( 1, "UNSAT after %7d conflicts. ", pSat->stats.conflicts );
1481// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1482 }
1483 assert( RetValue == l_False );
1484 // derive the UNSAT core
1485 clk = Abc_Clock();
1486 vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
1487 if ( vCore )
1488 Vec_IntSort( vCore, 1 );
1489 if ( fVerbose )
1490 {
1491// Abc_Print( 1, "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
1492// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1493 }
1494 return vCore;
1495}
1496
1497
1509void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfls, int nCexes, abctime Time )
1510{
1511 if ( Abc_FrameIsBatchMode() && nCoreSize <= 0 )
1512 return;
1513 Abc_Print( 1, "%4d :", nFrames-1 );
1514 Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * Gia_GlaAbsCount(p, 0, 0) / (p->nObjs - Gia_ManPoNum(p->pGia) + Gia_ManCoNum(p->pGia) + 1)) );
1515 Abc_Print( 1, "%6d", Gia_GlaAbsCount(p, 0, 0) );
1516 Abc_Print( 1, "%5d", Gla_ManCountPPis(p) );
1517 Abc_Print( 1, "%5d", Gia_GlaAbsCount(p, 1, 0) );
1518 Abc_Print( 1, "%6d", Gia_GlaAbsCount(p, 0, 1) );
1519 Abc_Print( 1, "%8d", nConfls );
1520 if ( nCexes == 0 )
1521 Abc_Print( 1, "%5c", '-' );
1522 else
1523 Abc_Print( 1, "%5d", nCexes );
1524// Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) );
1525 Abc_PrintInt( sat_solver2_nvars(p->pSat) );
1526 Abc_PrintInt( sat_solver2_nclauses(p->pSat) );
1527 Abc_PrintInt( sat_solver2_nlearnts(p->pSat) );
1528// Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 );
1529 Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
1530 Abc_Print( 1, "%5.0f MB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<20) );
1531// Abc_PrintInt( p->nAbsNew );
1532// Abc_PrintInt( p->nLrnNew );
1533// Abc_Print( 1, "%4.1f MB", 4.0 * p->nLrnNew * Abc_BitWordNum(p->nAbsNew) / (1<<20) );
1534 Abc_Print( 1, "%s", (nCoreSize > 0 && nCexes > 0) ? "\n" : "\r" );
1535 fflush( stdout );
1536}
1537void Gla_ManReportMemory( Gla_Man_t * p )
1538{
1539 Gla_Obj_t * pGla;
1540 double memTot = 0;
1541 double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t);
1542 double memSat = sat_solver2_memory( p->pSat, 1 );
1543 double memPro = sat_solver2_memory_proof( p->pSat );
1544 double memMap = p->nObjs * sizeof(Gla_Obj_t) + Gia_ManObjNum(p->pGia) * sizeof(int);
1545 double memRef = Rnm_ManMemoryUsage( p->pRnm );
1546 double memOth = sizeof(Gla_Man_t);
1547 for ( pGla = p->pObjs; pGla < p->pObjs + p->nObjs; pGla++ )
1548 memMap += Vec_IntCap(&pGla->vFrames) * sizeof(int);
1549 memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
1550 memOth += Vec_IntCap(p->vTemp) * sizeof(int);
1551 memOth += Vec_IntCap(p->vAbs) * sizeof(int);
1552 memTot = memAig + memSat + memPro + memMap + memRef + memOth;
1553 ABC_PRMP( "Memory: AIG ", memAig, memTot );
1554 ABC_PRMP( "Memory: SAT ", memSat, memTot );
1555 ABC_PRMP( "Memory: Proof ", memPro, memTot );
1556 ABC_PRMP( "Memory: Map ", memMap, memTot );
1557 ABC_PRMP( "Memory: Refine ", memRef, memTot );
1558 ABC_PRMP( "Memory: Other ", memOth, memTot );
1559 ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
1560}
1561
1562
1574void Gia_GlaSendAbsracted( Gla_Man_t * p, int fVerbose )
1575{
1576 Gia_Man_t * pAbs;
1577 Vec_Int_t * vGateClasses;
1578 assert( Abc_FrameIsBridgeMode() );
1579// if ( fVerbose )
1580// Abc_Print( 1, "Sending abstracted model...\n" );
1581 // create abstraction (value of p->pGia is not used here)
1582 vGateClasses = Gla_ManTranslate( p );
1583 pAbs = Gia_ManDupAbsGates( p->pGia0, vGateClasses );
1584 Vec_IntFreeP( &vGateClasses );
1585 // send it out
1586 Gia_ManToBridgeAbsNetlist( stdout, pAbs, BRIDGE_ABS_NETLIST );
1587 Gia_ManStop( pAbs );
1588}
1589void Gia_GlaSendCancel( Gla_Man_t * p, int fVerbose )
1590{
1591 extern int Gia_ManToBridgeBadAbs( FILE * pFile );
1592 assert( Abc_FrameIsBridgeMode() );
1593// if ( fVerbose )
1594// Abc_Print( 1, "Cancelling previously sent model...\n" );
1595 Gia_ManToBridgeBadAbs( stdout );
1596}
1597
1609void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
1610{
1611 char * pFileNameDef = "glabs.aig";
1612 char * pFileName = p->pPars->pFileVabs ? p->pPars->pFileVabs : pFileNameDef;
1613 Gia_Man_t * pAbs;
1614 Vec_Int_t * vGateClasses;
1615 if ( fVerbose )
1616 Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
1617 // create abstraction
1618 vGateClasses = Gla_ManTranslate( p );
1619 pAbs = Gia_ManDupAbsGates( p->pGia0, vGateClasses );
1620 Vec_IntFreeP( &vGateClasses );
1621 // write into file
1622 Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
1623 Gia_ManStop( pAbs );
1624}
1625
1626
1638int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta )
1639{
1640 extern int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars );
1641 extern void Ga2_ManDumpStats( Gia_Man_t * pGia, Abs_Par_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN );
1642 Gla_Man_t * p;
1643 Vec_Int_t * vPPis, * vCore;//, * vCore2 = NULL;
1644 Abc_Cex_t * pCex = NULL;
1645 int f, i, iPrev, nConfls, Status, nVarsOld = 0, nCoreSize, fOneIsSent = 0, RetValue = -1;
1646 abctime clk2, clk = Abc_Clock();
1647 // preconditions
1648 assert( Gia_ManPoNum(pAig) == 1 );
1649 assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
1650 if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) )
1651 {
1652 if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) )
1653 {
1654 printf( "Sequential miter is trivially UNSAT.\n" );
1655 return 1;
1656 }
1657 ABC_FREE( pAig->pCexSeq );
1658 pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 );
1659 printf( "Sequential miter is trivially SAT.\n" );
1660 return 0;
1661 }
1662
1663 // compute intial abstraction
1664 if ( pAig->vGateClasses == NULL )
1665 {
1666 if ( fStartVta )
1667 {
1668 int nFramesMaxOld = pPars->nFramesMax;
1669 int nFramesStartOld = pPars->nFramesStart;
1670 int nTimeOutOld = pPars->nTimeOut;
1671 int nDumpOld = pPars->fDumpVabs;
1672 pPars->nFramesMax = pPars->nFramesStart;
1673 pPars->nFramesStart = Abc_MinInt( pPars->nFramesStart/2 + 1, 3 );
1674 pPars->nTimeOut = 20;
1675 pPars->fDumpVabs = 0;
1676 RetValue = Gia_VtaPerformInt( pAig, pPars );
1677 pPars->nFramesMax = nFramesMaxOld;
1678 pPars->nFramesStart = nFramesStartOld;
1679 pPars->nTimeOut = nTimeOutOld;
1680 pPars->fDumpVabs = nDumpOld;
1681 // create gate classes
1682 Vec_IntFreeP( &pAig->vGateClasses );
1683 if ( pAig->vObjClasses )
1684 pAig->vGateClasses = Gia_VtaConvertToGla( pAig, pAig->vObjClasses );
1685 Vec_IntFreeP( &pAig->vObjClasses );
1686 // return if VTA solve the problem if could not start
1687 if ( RetValue == 0 || pAig->vGateClasses == NULL )
1688 return RetValue;
1689 }
1690 else
1691 {
1692 pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
1693 Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
1694 Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)), 1 );
1695 }
1696 }
1697 // start the manager
1698 p = Gla_ManStart( pAig, pPars );
1699 p->timeInit = Abc_Clock() - clk;
1700 // set runtime limit
1701 if ( p->pPars->nTimeOut )
1702 sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
1703 // perform initial abstraction
1704 if ( p->pPars->fVerbose )
1705 {
1706 Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" );
1707 Abc_Print( 1, "FrameMax = %d ConfMax = %d Timeout = %d RatioMin = %d %%.\n",
1708 pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin );
1709 Abc_Print( 1, "LearnStart = %d LearnDelta = %d LearnRatio = %d %%.\n",
1710 pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce );
1711 Abc_Print( 1, " Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" );
1712 }
1713 for ( f = i = iPrev = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++, iPrev = i )
1714 {
1715 int nConflsBeg = sat_solver2_nconflicts(p->pSat);
1716 p->pPars->iFrame = f;
1717
1718 // load timeframe
1719 Gia_GlaAddTimeFrame( p, f );
1720
1721 // iterate as long as there are counter-examples
1722 for ( i = 0; ; i++ )
1723 {
1724 clk2 = Abc_Clock();
1725 vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
1726// assert( (vCore != NULL) == (Status == 1) );
1727 if ( Status == -1 || (p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit) ) // resource limit is reached
1728 {
1729 Prf_ManStopP( &p->pSat->pPrf2 );
1730// if ( Gia_ManRegNum(p->pGia) > 1 ) // for comb cases, return the abstraction
1731// Vec_IntShrink( p->vAbs, p->nAbsOld );
1732 goto finish;
1733 }
1734 if ( Status == 1 )
1735 {
1736 Prf_ManStopP( &p->pSat->pPrf2 );
1737 p->timeUnsat += Abc_Clock() - clk2;
1738 break;
1739 }
1740 p->timeSat += Abc_Clock() - clk2;
1741 assert( Status == 0 );
1742 p->nCexes++;
1743
1744 // cancel old one if it was sent
1745 if ( Abc_FrameIsBridgeMode() && fOneIsSent )
1746 {
1747 Gia_GlaSendCancel( p, pPars->fVerbose );
1748 fOneIsSent = 0;
1749 }
1750
1751 // perform the refinement
1752 clk2 = Abc_Clock();
1753 if ( pPars->fAddLayer )
1754 {
1755 vPPis = Gla_ManCollectPPis( p, NULL );
1756// Gla_ManExplorePPis( p, vPPis );
1757 }
1758 else
1759 {
1760 vPPis = Gla_ManRefinement( p );
1761 if ( vPPis == NULL )
1762 {
1763 Prf_ManStopP( &p->pSat->pPrf2 );
1764 pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
1765 break;
1766 }
1767 }
1768 assert( pCex == NULL );
1769
1770 // start proof logging
1771 if ( i == 0 )
1772 {
1773 // create bookmark to be used for rollback
1774 sat_solver2_bookmark( p->pSat );
1775 Vec_IntClear( p->vAddedNew );
1776 p->nAbsOld = Vec_IntSize( p->vAbs );
1777 nVarsOld = p->nSatVars;
1778// p->nLrnOld = sat_solver2_nlearnts( p->pSat );
1779// p->nAbsNew = 0;
1780// p->nLrnNew = 0;
1781
1782 // start incremental proof manager
1783 assert( p->pSat->pPrf2 == NULL );
1784 if ( p->pSat->pPrf1 == NULL )
1785 p->pSat->pPrf2 = Prf_ManAlloc();
1786 if ( p->pSat->pPrf2 )
1787 {
1788 p->nProofIds = 0;
1789 Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
1790 Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vPPis) );
1791 }
1792 }
1793 else
1794 {
1795 // resize the proof logger
1796 if ( p->pSat->pPrf2 )
1797 Prf_ManGrow( p->pSat->pPrf2, p->nProofIds + Vec_IntSize(vPPis) );
1798 }
1799
1800 Gia_GlaAddToAbs( p, vPPis, 1 );
1801 Gia_GlaAddOneSlice( p, f, vPPis );
1802 Vec_IntFree( vPPis );
1803
1804 // print the result (do not count it towards change)
1805 if ( p->pPars->fVerbose )
1806 Gla_ManAbsPrintFrame( p, -1, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk );
1807 }
1808 if ( pCex != NULL )
1809 break;
1810 assert( Status == 1 );
1811
1812 // valid core is obtained
1813 nCoreSize = 1;
1814 if ( vCore )
1815 {
1816 nCoreSize += Vec_IntSize( vCore );
1817 Gia_GlaAddToCounters( p, vCore );
1818 }
1819 if ( i == 0 )
1820 {
1821 p->pPars->nFramesNoChange++;
1822 Vec_IntFreeP( &vCore );
1823 }
1824 else
1825 {
1826 p->pPars->nFramesNoChange = 0;
1827// p->nAbsNew = Vec_IntSize( p->vAbs ) - p->nAbsOld;
1828// p->nLrnNew = Abc_AbsInt( sat_solver2_nlearnts( p->pSat ) - p->nLrnOld );
1829 // update the SAT solver
1830 sat_solver2_rollback( p->pSat );
1831 // update storage
1832 Gla_ManRollBack( p );
1833 p->nSatVars = nVarsOld;
1834 // load this timeframe
1835 Gia_GlaAddToAbs( p, vCore, 0 );
1836 Gia_GlaAddOneSlice( p, f, vCore );
1837 Vec_IntFree( vCore );
1838 // run SAT solver
1839 clk2 = Abc_Clock();
1840 vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
1841 p->timeUnsat += Abc_Clock() - clk2;
1842// assert( (vCore != NULL) == (Status == 1) );
1843 Vec_IntFreeP( &vCore );
1844 if ( Status == -1 ) // resource limit is reached
1845 break;
1846 if ( Status == 0 )
1847 {
1848 assert( 0 );
1849 // Vta_ManSatVerify( p );
1850 // make sure, there was no initial abstraction (otherwise, it was invalid)
1851 assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart );
1852 // pCex = Vga_ManDeriveCex( p );
1853 break;
1854 }
1855 }
1856 // print the result
1857 if ( p->pPars->fVerbose )
1858 Gla_ManAbsPrintFrame( p, nCoreSize, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk );
1859
1860 if ( f > 2 && iPrev > 0 && i == 0 ) // change has happened
1861 {
1862 if ( Abc_FrameIsBridgeMode() )
1863 {
1864 // cancel old one if it was sent
1865 if ( fOneIsSent )
1866 Gia_GlaSendCancel( p, pPars->fVerbose );
1867 // send new one
1868 Gia_GlaSendAbsracted( p, pPars->fVerbose );
1869 fOneIsSent = 1;
1870 }
1871
1872 // dump the model into file
1873 if ( p->pPars->fDumpVabs )
1874 {
1875 char Command[1000];
1876 Abc_FrameSetStatus( -1 );
1877 Abc_FrameSetCex( NULL );
1878 Abc_FrameSetNFrames( f+1 );
1879 sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status") );
1880 Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
1881 Gia_GlaDumpAbsracted( p, pPars->fVerbose );
1882 }
1883 }
1884
1885 // check if the number of objects is below limit
1886 if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 )
1887 {
1888 Status = -1;
1889 break;
1890 }
1891 }
1892finish:
1893 // analize the results
1894 if ( pCex == NULL )
1895 {
1896 if ( p->pPars->fVerbose && Status == -1 )
1897 printf( "\n" );
1898// if ( pAig->vGateClasses != NULL )
1899// Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
1900 Vec_IntFreeP( &pAig->vGateClasses );
1901 pAig->vGateClasses = Gla_ManTranslate( p );
1902 if ( Status == -1 )
1903 {
1904 if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit )
1905 Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange );
1906 else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
1907 Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, f, p->pPars->nFramesNoChange );
1908 else if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 )
1909 Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f );
1910 else
1911 Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f );
1912 }
1913 else
1914 {
1915 p->pPars->iFrame++;
1916 Abc_Print( 1, "GLA completed %d frames with a %d-stable abstraction. ", f, p->pPars->nFramesNoChange );
1917 }
1918 }
1919 else
1920 {
1921 if ( p->pPars->fVerbose )
1922 printf( "\n" );
1923 ABC_FREE( pAig->pCexSeq );
1924 pAig->pCexSeq = pCex;
1925 if ( !Gia_ManVerifyCex( pAig, pCex, 0 ) )
1926 Abc_Print( 1, " Gia_ManPerformGlaOld(): CEX verification has failed!\n" );
1927 Abc_Print( 1, "Counter-example detected in frame %d. ", f );
1928 p->pPars->iFrame = pCex->iFrame - 1;
1929 Vec_IntFreeP( &pAig->vGateClasses );
1930 RetValue = 0;
1931 }
1932 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1933 if ( p->pPars->fVerbose )
1934 {
1935 p->timeOther = (Abc_Clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit;
1936 ABC_PRTP( "Runtime: Initializing", p->timeInit, Abc_Clock() - clk );
1937 ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, Abc_Clock() - clk );
1938 ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, Abc_Clock() - clk );
1939 ABC_PRTP( "Runtime: Refinement ", p->timeCex, Abc_Clock() - clk );
1940 ABC_PRTP( "Runtime: Other ", p->timeOther, Abc_Clock() - clk );
1941 ABC_PRTP( "Runtime: TOTAL ", Abc_Clock() - clk, Abc_Clock() - clk );
1942 Gla_ManReportMemory( p );
1943 }
1944// Ga2_ManDumpStats( pAig, p->pPars, p->pSat, p->pPars->iFrame, 1 );
1945 Gla_ManStop( p );
1946 fflush( stdout );
1947 return RetValue;
1948}
1949
1953
1954
1955ABC_NAMESPACE_IMPL_END
1956
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_FALLOC
#define ABC_FALLOC(type, num)
Definition abc_global.h:266
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition abc_global.h:258
Gia_ManToBridgeAbsNetlist
int Gia_ManToBridgeAbsNetlist(FILE *pFile, void *p, int pkg_type)
Definition utilBridge.c:192
ABC_PRMP
#define ABC_PRMP(a, f, F)
Definition abc_global.h:262
BRIDGE_ABS_NETLIST
#define BRIDGE_ABS_NETLIST
Definition abc_global.h:387
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Abc_FrameGetGlobalFrame
ABC_DLL Abc_Frame_t * Abc_FrameGetGlobalFrame()
Definition mainFrame.c:643
Gia_GlaAbsCount
int Gia_GlaAbsCount(Gla_Man_t *p, int fRo, int fAnd)
Definition absGlaOld.c:1141
Gia_ManDupMapped
Gia_Man_t * Gia_ManDupMapped(Gia_Man_t *p, Vec_Int_t *vMapping)
Definition absGlaOld.c:752
Gia_GlaSendAbsracted
void Gia_GlaSendAbsracted(Gla_Man_t *p, int fVerbose)
Definition absGlaOld.c:1574
Gla_ManRefSelect_rec
void Gla_ManRefSelect_rec(Gla_Man_t *p, Gia_Obj_t *pObj, int f, Vec_Int_t *vSelect, int Sign)
Definition absGlaOld.c:347
Gia_GlaAddToCounters
void Gia_GlaAddToCounters(Gla_Man_t *p, Vec_Int_t *vCore)
Definition absGlaOld.c:1361
Gla_ManGetOutLit
int Gla_ManGetOutLit(Gla_Man_t *p, int f)
Definition absGlaOld.c:1436
Gla_ManReportMemory
void Gla_ManReportMemory(Gla_Man_t *p)
Definition absGlaOld.c:1537
Gia_GlaPrepareCexAndMap
void Gia_GlaPrepareCexAndMap(Gla_Man_t *p, Abc_Cex_t **ppCex, Vec_Int_t **pvMap)
FUNCTION DEFINITIONS ///.
Definition absGlaOld.c:149
Gla_ManCollectFanins
void Gla_ManCollectFanins(Gla_Man_t *p, Gla_Obj_t *pGla, int iObj, Vec_Int_t *vFanins)
Definition absGlaOld.c:715
Gla_ManAddClauses
void Gla_ManAddClauses(Gla_Man_t *p, int iObj, int iFrame, Vec_Int_t *vLits)
Definition absGlaOld.c:1319
Gia_GlaSendCancel
void Gia_GlaSendCancel(Gla_Man_t *p, int fVerbose)
Definition absGlaOld.c:1589
Gia_ManRefSetAndPropFanout_rec
void Gia_ManRefSetAndPropFanout_rec(Gla_Man_t *p, Gia_Obj_t *pObj, int f, Vec_Int_t *vSelect, int Sign)
Definition absGlaOld.c:286
Rfn_Obj_t
typedefABC_NAMESPACE_IMPL_START struct Rfn_Obj_t_ Rfn_Obj_t
DECLARATIONS ///.
Definition absGlaOld.c:33
Gla_ManStop
void Gla_ManStop(Gla_Man_t *p)
Definition absGlaOld.c:1094
Gla_ManForEachObjAbsVec
#define Gla_ManForEachObjAbsVec(vVec, p, pObj, i)
Definition absGlaOld.c:123
Gia_GlaAddTimeFrame
void Gia_GlaAddTimeFrame(Gla_Man_t *p, int f)
Definition absGlaOld.c:1389
Gia_GlaAddOneSlice
void Gia_GlaAddOneSlice(Gla_Man_t *p, int fCur, Vec_Int_t *vCore)
Definition absGlaOld.c:1397
Gla_ManVerifyUsingTerSim
void Gla_ManVerifyUsingTerSim(Gla_Man_t *p, Vec_Int_t *vPis, Vec_Int_t *vPPis, Vec_Int_t *vRoAnds, Vec_Int_t *vCos, Vec_Int_t *vRes)
Definition absGlaOld.c:436
Gla_ManRefinement2
Vec_Int_t * Gla_ManRefinement2(Gla_Man_t *p)
Definition absGlaOld.c:535
Gia_GlaDumpAbsracted
void Gia_GlaDumpAbsracted(Gla_Man_t *p, int fVerbose)
Definition absGlaOld.c:1609
Gia_GlaAddToAbs
void Gia_GlaAddToAbs(Gla_Man_t *p, Vec_Int_t *vAbsAdd, int fCheck)
Definition absGlaOld.c:1368
Gla_Obj_t
struct Gla_Obj_t_ Gla_Obj_t
Definition absGlaOld.c:43
Gia_ManPerformGlaOld
int Gia_ManPerformGlaOld(Gia_Man_t *pAig, Abs_Par_t *pPars, int fStartVta)
Definition absGlaOld.c:1638
Gla_ManCountPPis
int Gla_ManCountPPis(Gla_Man_t *p)
Definition absGlaOld.c:1257
Gla_ManForEachObjAbs
#define Gla_ManForEachObjAbs(p, pObj, i)
Definition absGlaOld.c:121
Gla_ManTranslate
Vec_Int_t * Gla_ManTranslate(Gla_Man_t *p)
Definition absGlaOld.c:1184
Gla_ManStart2
Gla_Man_t * Gla_ManStart2(Gia_Man_t *pGia, Abs_Par_t *pPars)
Definition absGlaOld.c:1002
Gla_ManStart
Gla_Man_t * Gla_ManStart(Gia_Man_t *pGia0, Abs_Par_t *pPars)
Definition absGlaOld.c:825
Gla_ManRefinement
Vec_Int_t * Gla_ManRefinement(Gla_Man_t *p)
Definition absGlaOld.c:499
Gla_ManRollBack
void Gla_ManRollBack(Gla_Man_t *p)
Definition absGlaOld.c:1405
Gla_ManExplorePPis
void Gla_ManExplorePPis(Gla_Man_t *p, Vec_Int_t *vPPis)
Definition absGlaOld.c:1264
Gla_Man_t
struct Gla_Man_t_ Gla_Man_t
Definition absGlaOld.c:61
Gla_ManCollect
void Gla_ManCollect(Gla_Man_t *p, Vec_Int_t *vPis, Vec_Int_t *vPPis, Vec_Int_t *vCos, Vec_Int_t *vRoAnds)
Definition absGlaOld.c:229
Gla_ManDeriveCex
Abc_Cex_t * Gla_ManDeriveCex(Gla_Man_t *p, Vec_Int_t *vPis)
Definition absGlaOld.c:188
Gla_ManCollectInternal_rec
void Gla_ManCollectInternal_rec(Gia_Man_t *p, Gia_Obj_t *pGiaObj, Vec_Int_t *vRoAnds)
Definition absGlaOld.c:219
Gla_ObjForEachFanin
#define Gla_ObjForEachFanin(p, pObj, pFanin, i)
Definition absGlaOld.c:127
Gla_ManForEachObj
#define Gla_ManForEachObj(p, pObj)
Definition absGlaOld.c:119
Gla_ManAbsPrintFrame
void Gla_ManAbsPrintFrame(Gla_Man_t *p, int nCoreSize, int nFrames, int nConfls, int nCexes, abctime Time)
Definition absGlaOld.c:1509
Gla_ManUnsatCore
Vec_Int_t * Gla_ManUnsatCore(Gla_Man_t *p, int f, sat_solver2 *pSat, int nConfMax, int fVerbose, int *piRetValue, int *pnConfls)
Definition absGlaOld.c:1445
Gia_ManDupMapped_rec
void Gia_ManDupMapped_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Gia_Man_t *pNew)
Definition absGlaOld.c:741
Gla_ManTranslate_rec
int Gla_ManTranslate_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vGla, int nUsageCount)
Definition absGlaOld.c:1169
Ga2_ManDumpStats
void Ga2_ManDumpStats(Gia_Man_t *pGia, Abs_Par_t *pPars, sat_solver2 *pSat, int iFrame, int fUseN)
Definition absGla.c:410
Rnm_ManStop
void Rnm_ManStop(Rnm_Man_t *p, int fProfile)
Definition absRef.c:285
Rnm_ManMemoryUsage
double Rnm_ManMemoryUsage(Rnm_Man_t *p)
Definition absRef.c:317
Rnm_ManRefine
Vec_Int_t * Rnm_ManRefine(Rnm_Man_t *p, Abc_Cex_t *pCex, Vec_Int_t *vMap, int fPropFanout, int fNewRefinement, int fVerbose)
Definition absRef.c:673
Rnm_ManStart
Rnm_Man_t * Rnm_ManStart(Gia_Man_t *pGia)
FUNCTION DEFINITIONS ///.
Definition absRef.c:264
Rnm_Man_t
struct Rnm_Man_t_ Rnm_Man_t
Definition absRef.h:55
Gia_VtaPerformInt
int Gia_VtaPerformInt(Gia_Man_t *pAig, Abs_Par_t *pPars)
Definition absVta.c:1492
Gia_ManDupAbsGates
Gia_Man_t * Gia_ManDupAbsGates(Gia_Man_t *p, Vec_Int_t *vGateClasses)
Definition absDup.c:220
Gia_VtaConvertToGla
Vec_Int_t * Gia_VtaConvertToGla(Gia_Man_t *p, Vec_Int_t *vVta)
Definition absUtil.c:78
Abs_Par_t
typedefABC_NAMESPACE_HEADER_START struct Abs_Par_t_ Abs_Par_t
INCLUDES ///.
Definition abs.h:46
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Abc_FrameSetNFrames
ABC_DLL void Abc_FrameSetNFrames(int nFrames)
Definition mainFrame.c:100
Abc_FrameSetStatus
ABC_DLL void Abc_FrameSetStatus(int Status)
Definition mainFrame.c:101
Abc_FrameSetCex
ABC_DLL void Abc_FrameSetCex(Abc_Cex_t *pCex)
Definition mainFrame.c:99
Abc_FrameIsBridgeMode
ABC_DLL int Abc_FrameIsBridgeMode()
Definition mainFrame.c:113
Abc_FrameIsBatchMode
ABC_DLL int Abc_FrameIsBatchMode()
Definition mainFrame.c:110
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
l_True
#define l_True
Definition bmcBmcS.c:35
l_Undef
#define l_Undef
Definition bmcBmcS.c:34
l_False
#define l_False
Definition bmcBmcS.c:36
Cmd_CommandExecute
ABC_DLL int Cmd_CommandExecute(Abc_Frame_t *pAbc, const char *sCommand)
Definition cmdApi.c:193
Cnf_DeriveOther
Cnf_Dat_t * Cnf_DeriveOther(Aig_Man_t *pAig, int fSkipTtMin)
Definition cnfCore.c:219
Cnf_Dat_t
struct Cnf_Dat_t_ Cnf_Dat_t
Definition cnf.h:52
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition cnfMan.c:207
p
Cube * p
Definition exorList.c:222
Extra_FileNameGenericAppend
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition extraUtilFile.c:192
Gia_ManToAigSimple
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition giaAig.c:408
Gia_ObjForEachFanoutStatic
#define Gia_ObjForEachFanoutStatic(p, pObj, pFanout, i)
Definition gia.h:1125
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ManStaticFanoutStart
void Gia_ManStaticFanoutStart(Gia_Man_t *p)
Definition giaFanout.c:238
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition giaMan.c:764
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ObjPrint
void Gia_ObjPrint(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition giaUtil.c:1456
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition giaUtil.c:369
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManForEachObj1
#define Gia_ManForEachObj1(p, pObj, i)
Definition gia.h:1192
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
Gia_ManVerifyCex
int Gia_ManVerifyCex(Gia_Man_t *pAig, Abc_Cex_t *p, int fDualOut)
DECLARATIONS ///.
Definition giaCex.c:48
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine)
Definition giaAiger.c:1595
sat_solver2_memory_proof
double sat_solver2_memory_proof(sat_solver2 *s)
Definition satSolver2.c:1733
sat_solver2_delete
void sat_solver2_delete(sat_solver2 *s)
Definition satSolver2.c:1225
sat_solver2_memory
double sat_solver2_memory(sat_solver2 *s, int fAll)
Definition satSolver2.c:1692
sat_solver2_simplify
int sat_solver2_simplify(sat_solver2 *s)
Definition satSolver2.c:996
sat_solver2_new
sat_solver2 * sat_solver2_new(void)
Definition satSolver2.c:1109
sat_solver2_rollback
void sat_solver2_rollback(sat_solver2 *s)
Definition satSolver2.c:1586
sat_solver2_solve
int sat_solver2_solve(sat_solver2 *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition satSolver2.c:1835
Sat_ProofCore
void * Sat_ProofCore(sat_solver2 *s)
Definition satSolver2.c:1985
sat_solver2_addclause
int sat_solver2_addclause(sat_solver2 *s, lit *begin, lit *end, int Id)
Definition satSolver2.c:1287
sat_solver2
struct sat_solver2_t sat_solver2
Definition satSolver2.h:44
Gia_Man_t_::pSpec
char * pSpec
Definition gia.h:100
Gia_Man_t_::vLutConfigs
Vec_Int_t * vLutConfigs
Definition gia.h:144
Gia_Man_t_::vObjClasses
Vec_Int_t * vObjClasses
Definition gia.h:158
Gia_Man_t_::vGateClasses
Vec_Int_t * vGateClasses
Definition gia.h:157
Gia_Man_t_::pCexSeq
Abc_Cex_t * pCexSeq
Definition gia.h:150
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Gla_Man_t_
Definition absGlaOld.c:63
Gla_Man_t_::pGia2
Gia_Man_t * pGia2
Definition absGlaOld.c:93
Gla_Man_t_::vCoreCounts
Vec_Int_t * vCoreCounts
Definition absGlaOld.c:87
Gla_Man_t_::nObjAdded
int nObjAdded
Definition absGlaOld.c:80
Gla_Man_t_::pvRefis
Vec_Int_t * pvRefis
Definition absGlaOld.c:91
Gla_Man_t_::pSat
sat_solver2 * pSat
Definition absGlaOld.c:83
Gla_Man_t_::pPars
Abs_Par_t * pPars
Definition absGlaOld.c:67
Gla_Man_t_::timeInit
abctime timeInit
Definition absGlaOld.c:96
Gla_Man_t_::vAbs
Vec_Int_t * vAbs
Definition absGlaOld.c:69
Gla_Man_t_::pObjs
Gla_Obj_t * pObjs
Definition absGlaOld.c:71
Gla_Man_t_::pObj2Obj
unsigned * pObj2Obj
Definition absGlaOld.c:72
Gla_Man_t_::pGia0
Gia_Man_t * pGia0
Definition absGlaOld.c:65
Gla_Man_t_::timeUnsat
abctime timeUnsat
Definition absGlaOld.c:98
Gla_Man_t_::timeSat
abctime timeSat
Definition absGlaOld.c:97
Gla_Man_t_::nSatVars
int nSatVars
Definition absGlaOld.c:81
Gla_Man_t_::vProofIds
Vec_Int_t * vProofIds
Definition absGlaOld.c:88
Gla_Man_t_::pObjRoot
Gla_Obj_t * pObjRoot
Definition absGlaOld.c:70
Gla_Man_t_::vTemp
Vec_Int_t * vTemp
Definition absGlaOld.c:84
Gla_Man_t_::nAbsOld
int nAbsOld
Definition absGlaOld.c:74
Gla_Man_t_::nCexes
int nCexes
Definition absGlaOld.c:79
Gla_Man_t_::pCnf
Cnf_Dat_t * pCnf
Definition absGlaOld.c:82
Gla_Man_t_::pRnm
Rnm_Man_t * pRnm
Definition absGlaOld.c:94
Gla_Man_t_::timeCex
abctime timeCex
Definition absGlaOld.c:99
Gla_Man_t_::pGia
Gia_Man_t * pGia
Definition absGlaOld.c:66
Gla_Man_t_::vObjCounts
Vec_Int_t * vObjCounts
Definition absGlaOld.c:86
Gla_Man_t_::nObjs
int nObjs
Definition absGlaOld.c:73
Gla_Man_t_::vAddedNew
Vec_Int_t * vAddedNew
Definition absGlaOld.c:85
Gla_Man_t_::nProofIds
int nProofIds
Definition absGlaOld.c:89
Gla_Man_t_::timeOther
abctime timeOther
Definition absGlaOld.c:100
Gla_Obj_t_
Definition absGlaOld.c:45
Gla_Obj_t_::Fanins
int Fanins[4]
Definition absGlaOld.c:57
Gla_Obj_t_::fAbs
unsigned fAbs
Definition absGlaOld.c:47
Gla_Obj_t_::fAnd
unsigned fAnd
Definition absGlaOld.c:54
Gla_Obj_t_::fRi
unsigned fRi
Definition absGlaOld.c:53
Gla_Obj_t_::fPo
unsigned fPo
Definition absGlaOld.c:51
Gla_Obj_t_::fConst
unsigned fConst
Definition absGlaOld.c:49
Gla_Obj_t_::fPi
unsigned fPi
Definition absGlaOld.c:50
Gla_Obj_t_::nFanins
unsigned nFanins
Definition absGlaOld.c:56
Gla_Obj_t_::fRo
unsigned fRo
Definition absGlaOld.c:52
Gla_Obj_t_::vFrames
Vec_Int_t vFrames
Definition absGlaOld.c:58
Gla_Obj_t_::iGiaObj
int iGiaObj
Definition absGlaOld.c:46
Gla_Obj_t_::fMark
unsigned fMark
Definition absGlaOld.c:55
Gla_Obj_t_::fCompl0
unsigned fCompl0
Definition absGlaOld.c:48
Rfn_Obj_t_
Definition absGlaOld.c:35
Rfn_Obj_t_::Prio
unsigned Prio
Definition absGlaOld.c:39
Rfn_Obj_t_::fVisit
unsigned fVisit
Definition absGlaOld.c:37
Rfn_Obj_t_::Sign
unsigned Sign
Definition absGlaOld.c:40
Rfn_Obj_t_::fPPi
unsigned fPPi
Definition absGlaOld.c:38
Rfn_Obj_t_::Value
unsigned Value
Definition absGlaOld.c:36
sat_solver2_t::stats
stats_t stats
Definition satSolver2.h:172
stats_t::conflicts
ABC_INT64_T conflicts
Definition satVec.h:156
Gia_ManToBridgeBadAbs
int Gia_ManToBridgeBadAbs(FILE *pFile)
Definition utilBridge.c:202
Abc_CexFreeP
void Abc_CexFreeP(Abc_Cex_t **p)
Definition utilCex.c:361
Abc_CexMakeTriv
Abc_Cex_t * Abc_CexMakeTriv(int nRegs, int nTruePis, int nTruePos, int iFrameOut)
Definition utilCex.c:85
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition utilCex.c:382
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition utilCex.c:51
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
assert
#define assert(ex)
Definition util_old.h:213
memcpy
char * memcpy()
sprintf
char * sprintf()
Vec_IntForEachEntryDouble
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition vecInt.h:72
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56