abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
absGlaOld.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [absGla.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Abstraction package.]
8 
9  Synopsis [Gate-level abstraction.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: absGla.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
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 
27 ABC_NAMESPACE_IMPL_START
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 typedef struct Rfn_Obj_t_ Rfn_Obj_t; // refinement object
34 struct 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 
43 typedef struct Gla_Obj_t_ Gla_Obj_t; // abstraction object
44 struct 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 
61 typedef struct Gla_Man_t_ Gla_Man_t; // manager
62 struct 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
104 static Vec_Int_t * Gla_ManCollectPPis( Gla_Man_t * p, Vec_Int_t * vPis );
105 static int Gla_ManCheckVar( Gla_Man_t * p, int iObj, int iFrame );
106 static int Gla_ManGetVar( Gla_Man_t * p, int iObj, int iFrame );
107 
108 // object procedures
109 static 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; }
110 static inline Gla_Obj_t * Gla_ManObj( Gla_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; }
111 static inline Gia_Obj_t * Gla_ManGiaObj( Gla_Man_t * p, Gla_Obj_t * pObj ) { return Gia_ManObj( p->pGia, pObj->iGiaObj ); }
112 static 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 
114 static 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 ); }
115 static 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 
134 ////////////////////////////////////////////////////////////////////////
135 /// FUNCTION DEFINITIONS ///
136 ////////////////////////////////////////////////////////////////////////
137 
138 /**Function*************************************************************
139 
140  Synopsis [Prepares CEX and vMap for refinement.]
141 
142  Description []
143 
144  SideEffects []
145 
146  SeeAlso []
147 
148 ***********************************************************************/
149 void 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 
177 /**Function*************************************************************
178 
179  Synopsis [Derives counter-example using current assignments.]
180 
181  Description []
182 
183  SideEffects []
184 
185  SeeAlso []
186 
187 ***********************************************************************/
188 Abc_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 
208 /**Function*************************************************************
209 
210  Synopsis [Collects GIA abstraction objects.]
211 
212  Description []
213 
214  SideEffects []
215 
216  SeeAlso []
217 
218 ***********************************************************************/
219 void 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 }
229 void 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 
275 /**Function*************************************************************
276 
277  Synopsis [Drive implications of the given node towards primary outputs.]
278 
279  Description []
280 
281  SideEffects []
282 
283  SeeAlso []
284 
285 ***********************************************************************/
286 void 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 
336 /**Function*************************************************************
337 
338  Synopsis [Selects assignments to be refined.]
339 
340  Description []
341 
342  SideEffects []
343 
344  SeeAlso []
345 
346 ***********************************************************************/
347 void 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 
425 /**Function*************************************************************
426 
427  Synopsis [Performs refinement.]
428 
429  Description []
430 
431  SideEffects []
432 
433  SeeAlso []
434 
435 ***********************************************************************/
436 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 )
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 
488 /**Function*************************************************************
489 
490  Synopsis [Performs refinement.]
491 
492  Description []
493 
494  SideEffects []
495 
496  SeeAlso []
497 
498 ***********************************************************************/
499 Vec_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 
524 /**Function*************************************************************
525 
526  Synopsis [Performs refinement.]
527 
528  Description []
529 
530  SideEffects []
531 
532  SeeAlso []
533 
534 ***********************************************************************/
535 Vec_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 
704 /**Function*************************************************************
705 
706  Synopsis [Adds clauses for the given obj in the given frame.]
707 
708  Description []
709 
710  SideEffects []
711 
712  SeeAlso []
713 
714 ***********************************************************************/
715 void 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 
730 /**Function*************************************************************
731 
732  Synopsis [Duplicates AIG while decoupling nodes duplicated in the mapping.]
733 
734  Description []
735 
736  SideEffects []
737 
738  SeeAlso []
739 
740 ***********************************************************************/
741 void 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 }
752 Gia_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 
814 /**Function*************************************************************
815 
816  Synopsis [Creates a new manager.]
817 
818  Description []
819 
820  SideEffects []
821 
822  SeeAlso []
823 
824 ***********************************************************************/
825 Gla_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 
991 /**Function*************************************************************
992 
993  Synopsis [Creates a new manager.]
994 
995  Description []
996 
997  SideEffects []
998 
999  SeeAlso []
1000 
1001 ***********************************************************************/
1002 Gla_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 
1083 /**Function*************************************************************
1084 
1085  Synopsis [Creates a new manager.]
1086 
1087  Description []
1088 
1089  SideEffects []
1090 
1091  SeeAlso []
1092 
1093 ***********************************************************************/
1094 void 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 
1130 /**Function*************************************************************
1131 
1132  Synopsis [Creates a new manager.]
1133 
1134  Description []
1135 
1136  SideEffects []
1137 
1138  SeeAlso []
1139 
1140 ***********************************************************************/
1141 int 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 
1158 /**Function*************************************************************
1159 
1160  Synopsis [Derives new abstraction map.]
1161 
1162  Description [Returns 1 if node contains abstracted leaf on the path.]
1163 
1164  SideEffects []
1165 
1166  SeeAlso []
1167 
1168 ***********************************************************************/
1169 int 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 }
1184 Vec_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 
1223 /**Function*************************************************************
1224 
1225  Synopsis [Collect pseudo-PIs.]
1226 
1227  Description []
1228 
1229  SideEffects []
1230 
1231  SeeAlso []
1232 
1233 ***********************************************************************/
1234 Vec_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 }
1257 int 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 }
1264 void 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 
1287 /**Function*************************************************************
1288 
1289  Synopsis [Adds CNF for the given timeframe.]
1290 
1291  Description []
1292 
1293  SideEffects []
1294 
1295  SeeAlso []
1296 
1297 ***********************************************************************/
1298 int 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 }
1305 int 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 }
1319 void 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 }
1361 void 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 }
1368 void 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 }
1389 void 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 }
1397 void 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 }
1405 void 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 
1425 /**Function*************************************************************
1426 
1427  Synopsis [Finds the set of clauses involved in the UNSAT core.]
1428 
1429  Description []
1430 
1431  SideEffects []
1432 
1433  SeeAlso []
1434 
1435 ***********************************************************************/
1436 int 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 }
1445 Vec_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 
1498 /**Function*************************************************************
1499 
1500  Synopsis []
1501 
1502  Description []
1503 
1504  SideEffects []
1505 
1506  SeeAlso []
1507 
1508 ***********************************************************************/
1509 void 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 }
1537 void 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 
1563 /**Function*************************************************************
1564 
1565  Synopsis [Send abstracted model or send cancel.]
1566 
1567  Description [Counter-example will be sent automatically when &vta terminates.]
1568 
1569  SideEffects []
1570 
1571  SeeAlso []
1572 
1573 ***********************************************************************/
1574 void 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 }
1589 void 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 
1598 /**Function*************************************************************
1599 
1600  Synopsis [Send abstracted model or send cancel.]
1601 
1602  Description [Counter-example will be sent automatically when &vta terminates.]
1603 
1604  SideEffects []
1605 
1606  SeeAlso []
1607 
1608 ***********************************************************************/
1609 void 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 );
1623  Gia_ManStop( pAbs );
1624 }
1625 
1626 
1627 /**Function*************************************************************
1628 
1629  Synopsis [Performs gate-level abstraction]
1630 
1631  Description []
1632 
1633  SideEffects []
1634 
1635  SeeAlso []
1636 
1637 ***********************************************************************/
1638 int 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  }
1892 finish:
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 
1950 ////////////////////////////////////////////////////////////////////////
1951 /// END OF FILE ///
1952 ////////////////////////////////////////////////////////////////////////
1953 
1954 
1955 ABC_NAMESPACE_IMPL_END
1956 
Rnm_ManMemoryUsage
double Rnm_ManMemoryUsage(Rnm_Man_t *p)
Definition: absRef.c:317
Gla_Man_t_::pGia0
Gia_Man_t * pGia0
Definition: absGlaOld.c:65
sat_solver2_nlearnts
static int sat_solver2_nlearnts(sat_solver2 *s)
Definition: satSolver2.h:200
Rfn_Obj_t
typedefABC_NAMESPACE_IMPL_START struct Rfn_Obj_t_ Rfn_Obj_t
DECLARATIONS ///.
Definition: absGlaOld.c:33
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Gia_ManAppendAnd
static int Gia_ManAppendAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: gia.h:592
Gia_ObjTerSimCo
static void Gia_ObjTerSimCo(Gia_Obj_t *pObj)
Definition: gia.h:797
Gia_GlaSendAbsracted
void Gia_GlaSendAbsracted(Gla_Man_t *p, int fVerbose)
Definition: absGlaOld.c:1574
Gla_Obj_t_::fConst
unsigned fConst
Definition: absGlaOld.c:49
Gla_Man_t_::vAbs
Vec_Int_t * vAbs
Definition: absGlaOld.c:69
Gla_Man_t_::timeCex
abctime timeCex
Definition: absGlaOld.c:99
Gia_GlaAddTimeFrame
void Gia_GlaAddTimeFrame(Gla_Man_t *p, int f)
Definition: absGlaOld.c:1389
Gla_Obj_t_::vFrames
Vec_Int_t vFrames
Definition: absGlaOld.c:58
Abc_FrameIsBridgeMode
ABC_DLL int Abc_FrameIsBridgeMode()
Definition: mainFrame.c:94
Gia_ObjTerSimRo
static void Gia_ObjTerSimRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:808
Gla_ManRefinement2
Vec_Int_t * Gla_ManRefinement2(Gla_Man_t *p)
Definition: absGlaOld.c:535
Gla_Man_t_::pObjs
Gla_Obj_t * pObjs
Definition: absGlaOld.c:71
Gia_ObjTerSimSet0
static void Gia_ObjTerSimSet0(Gia_Obj_t *pObj)
Definition: gia.h:770
Gia_GlaAddToAbs
void Gia_GlaAddToAbs(Gla_Man_t *p, Vec_Int_t *vAbsAdd, int fCheck)
Definition: absGlaOld.c:1368
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
sat_solver2_t::nLearntMax
int nLearntMax
Definition: satSolver2.h:118
Gla_Man_t_::pGia2
Gia_Man_t * pGia2
Definition: absGlaOld.c:93
sat_solver2_t::nLearntStart
int nLearntStart
Definition: satSolver2.h:119
Gla_Man_t_::pSat
sat_solver2 * pSat
Definition: absGlaOld.c:83
Gla_ManRefinement
Vec_Int_t * Gla_ManRefinement(Gla_Man_t *p)
Definition: absGlaOld.c:499
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManToAigSimple
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
sat_solver2_nclauses
static int sat_solver2_nclauses(sat_solver2 *s)
Definition: satSolver2.h:195
Gia_ManVerifyCex
int Gia_ManVerifyCex(Gia_Man_t *pAig, Abc_Cex_t *p, int fDualOut)
DECLARATIONS ///.
Definition: giaCex.c:44
Sat_ProofCore
void * Sat_ProofCore(sat_solver2 *s)
Definition: satSolver2.c:1985
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Gla_Obj_t_::Fanins
int Fanins[4]
Definition: absGlaOld.c:57
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
Gia_ManAppendCo
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Gla_Man_t_::pRnm
Rnm_Man_t * pRnm
Definition: absGlaOld.c:94
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Cmd_CommandExecute
int Cmd_CommandExecute(void *pAbc, char *pCommandLine)
Gla_ManCollectPPis
static Vec_Int_t * Gla_ManCollectPPis(Gla_Man_t *p, Vec_Int_t *vPis)
Definition: absGlaOld.c:1234
Gla_Obj_t_::fPi
unsigned fPi
Definition: absGlaOld.c:50
Gla_ManGetOutLit
int Gla_ManGetOutLit(Gla_Man_t *p, int f)
Definition: absGlaOld.c:1436
Gia_ObjIsTravIdCurrent
static int Gia_ObjIsTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:533
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
l_Undef
#define l_Undef
Definition: SolverTypes.h:86
sat_solver2_memory_proof
double sat_solver2_memory_proof(sat_solver2 *s)
Definition: satSolver2.c:1733
Gia_Man_t_::vObjClasses
Vec_Int_t * vObjClasses
Definition: gia.h:142
Rnm_ManStart
Rnm_Man_t * Rnm_ManStart(Gia_Man_t *pGia)
FUNCTION DEFINITIONS ///.
Definition: absRef.c:264
Gia_ManPo
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
Gia_ManDupMapped
Gia_Man_t * Gia_ManDupMapped(Gia_Man_t *p, Vec_Int_t *vMapping)
Definition: absGlaOld.c:752
Gla_Obj_t_::fCompl0
unsigned fCompl0
Definition: absGlaOld.c:48
lit_var
static int lit_var(lit l)
Definition: satVec.h:145
Abc_FrameIsBatchMode
ABC_DLL int Abc_FrameIsBatchMode()
Definition: mainFrame.c:92
sat_solver2_delete
void sat_solver2_delete(sat_solver2 *s)
Definition: satSolver2.c:1225
Ga2_ManDumpStats
void Ga2_ManDumpStats(Gia_Man_t *pGia, Abs_Par_t *pPars, sat_solver2 *pSat, int iFrame, int fUseN)
Definition: absGla.c:410
Gla_Obj_t_::fPo
unsigned fPo
Definition: absGlaOld.c:51
Gla_Man_t_::pCnf
Cnf_Dat_t * pCnf
Definition: absGlaOld.c:82
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
sat_solver2_t
Definition: satSolver2.h:90
Rnm_Man_t_
Definition: absRef.h:56
Cnf_Dat_t_::vMapping
Vec_Int_t * vMapping
Definition: cnf.h:67
Gia_ManDupAbsGates
Gia_Man_t * Gia_ManDupAbsGates(Gia_Man_t *p, Vec_Int_t *vGateClasses)
Definition: absDup.c:220
Gia_ObjIsConst0
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Vec_SetAlloc
static Vec_Set_t * Vec_SetAlloc(int nPageSize)
Definition: vecSet.h:128
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
Gla_ManAddClauses
void Gla_ManAddClauses(Gla_Man_t *p, int iObj, int iFrame, Vec_Int_t *vLits)
Definition: absGlaOld.c:1319
Gla_ManCollectInternal_rec
void Gla_ManCollectInternal_rec(Gia_Man_t *p, Gia_Obj_t *pGiaObj, Vec_Int_t *vRoAnds)
Definition: absGlaOld.c:219
Rfn_Obj_t_::Sign
unsigned Sign
Definition: absGlaOld.c:40
sat_solver2_t::nLearntDelta
int nLearntDelta
Definition: satSolver2.h:120
memcpy
char * memcpy()
Gla_Obj_t_::fAbs
unsigned fAbs
Definition: absGlaOld.c:47
Gia_ManToBridgeBadAbs
int Gia_ManToBridgeBadAbs(FILE *pFile)
Definition: utilBridge.c:199
Vec_IntSetEntry
static void Vec_IntSetEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:418
l_True
#define l_True
Definition: SolverTypes.h:84
Gla_ObjForEachFanin
#define Gla_ObjForEachFanin(p, pObj, pFanin, i)
Definition: absGlaOld.c:127
sat_solver2_new
sat_solver2 * sat_solver2_new(void)
Definition: satSolver2.c:1109
Vec_IntGetEntry
static int Vec_IntGetEntry(Vec_Int_t *p, int i)
Definition: bblif.c:401
Gla_ManGetVar
static int Gla_ManGetVar(Gla_Man_t *p, int iObj, int iFrame)
Definition: absGlaOld.c:1305
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
Gia_VtaConvertToGla
Vec_Int_t * Gia_VtaConvertToGla(Gia_Man_t *p, Vec_Int_t *vVta)
Definition: absUtil.c:78
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
Abc_FrameSetStatus
ABC_DLL void Abc_FrameSetStatus(int Status)
Definition: mainFrame.c:88
sat_solver2_addclause
int sat_solver2_addclause(sat_solver2 *s, lit *begin, lit *end, int Id)
Definition: satSolver2.c:1287
Gla_ObjSatValue
static int Gla_ObjSatValue(Gla_Man_t *p, int iGia, int f)
Definition: absGlaOld.c:112
Gla_Obj_t_::iGiaObj
int iGiaObj
Definition: absGlaOld.c:46
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Gla_ManStop
void Gla_ManStop(Gla_Man_t *p)
Definition: absGlaOld.c:1094
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Cnf_Dat_t_
Definition: cnf.h:56
Vec_IntSort
static void Vec_IntSort(Vec_Int_t *p, int fReverse)
Definition: vecInt.h:1293
sat_solver2_t::stats
stats_t stats
Definition: satSolver2.h:172
Gla_Man_t_::timeInit
abctime timeInit
Definition: absGlaOld.c:96
Gla_Man_t_::timeOther
abctime timeOther
Definition: absGlaOld.c:100
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Rfn_Obj_t_::fPPi
unsigned fPPi
Definition: absGlaOld.c:38
Vec_IntReverseOrder
static void Vec_IntReverseOrder(Vec_Int_t *p)
Definition: vecInt.h:1042
sat_solver2_var_value
static int sat_solver2_var_value(sat_solver2 *s, int v)
Definition: satSolver2.h:210
Gla_Man_t_::pPars
Abs_Par_t * pPars
Definition: absGlaOld.c:67
Gia_Obj_t_
Definition: gia.h:75
Gla_Man_t_::pGia
Gia_Man_t * pGia
Definition: absGlaOld.c:66
Abc_CexMakeTriv
Abc_Cex_t * Abc_CexMakeTriv(int nRegs, int nTruePis, int nTruePos, int iFrameOut)
Definition: utilCex.c:85
Cnf_Dat_t_::pObj2Clause
int * pObj2Clause
Definition: cnf.h:64
Gla_ObjClearRef
static void Gla_ObjClearRef(Rfn_Obj_t *p)
Definition: absGlaOld.c:115
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition: abc_global.h:223
sat_solver2_memory
double sat_solver2_memory(sat_solver2 *s, int fAll)
Definition: satSolver2.c:1692
Gla_ObjRef
static Rfn_Obj_t * Gla_ObjRef(Gla_Man_t *p, Gia_Obj_t *pObj, int f)
Definition: absGlaOld.c:114
Gia_GlaAbsCount
int Gia_GlaAbsCount(Gla_Man_t *p, int fRo, int fAnd)
Definition: absGlaOld.c:1141
Gia_VtaPerformInt
int Gia_VtaPerformInt(Gia_Man_t *pAig, Abs_Par_t *pPars)
Definition: absVta.c:1492
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition: gia.h:74
Gla_ManForEachObjAbs
#define Gla_ManForEachObjAbs(p, pObj, i)
Definition: absGlaOld.c:121
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Rfn_Obj_t_::Prio
unsigned Prio
Definition: absGlaOld.c:39
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Gla_Man_t_::vAddedNew
Vec_Int_t * vAddedNew
Definition: absGlaOld.c:85
Gla_Man_t
struct Gla_Man_t_ Gla_Man_t
Definition: absGlaOld.c:61
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Gla_ObjId
static int Gla_ObjId(Gla_Man_t *p, Gla_Obj_t *pObj)
Definition: absGlaOld.c:109
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Rfn_Obj_t_::Value
unsigned Value
Definition: absGlaOld.c:36
Rfn_Obj_t_::fVisit
unsigned fVisit
Definition: absGlaOld.c:37
Cnf_Dat_t_::pClauses
int ** pClauses
Definition: cnf.h:62
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
sat_solver2_simplify
int sat_solver2_simplify(sat_solver2 *s)
Definition: satSolver2.c:996
Rnm_ManStop
void Rnm_ManStop(Rnm_Man_t *p, int fProfile)
Definition: absRef.c:285
Prf_ManAlloc
static Prf_Man_t * Prf_ManAlloc()
FUNCTION DECLARATIONS ///.
Definition: satProof2.h:81
sat_solver2_rollback
void sat_solver2_rollback(sat_solver2 *s)
Definition: satSolver2.c:1586
Gia_ObjFanin1Copy
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
Vec_IntAddToEntry
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
Gia_ObjIsRo
static int Gia_ObjIsRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:443
Abc_FrameSetCex
ABC_DLL void Abc_FrameSetCex(Abc_Cex_t *pCex)
Definition: mainFrame.c:86
Gia_Man_t_::vGateClasses
Vec_Int_t * vGateClasses
Definition: gia.h:141
Gla_ManExplorePPis
void Gla_ManExplorePPis(Gla_Man_t *p, Vec_Int_t *vPPis)
Definition: absGlaOld.c:1264
sat_solver2_t::nDBreduces
int nDBreduces
Definition: satSolver2.h:122
Gia_ObjRoToRi
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
Gia_ObjIsRi
static int Gia_ObjIsRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:444
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Gia_ObjSetTravIdCurrent
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
Abc_CexFreeP
void Abc_CexFreeP(Abc_Cex_t **p)
Definition: utilCex.c:350
Gia_GlaAddToCounters
void Gia_GlaAddToCounters(Gla_Man_t *p, Vec_Int_t *vCore)
Definition: absGlaOld.c:1361
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
Abc_FrameGetGlobalFrame
void * Abc_FrameGetGlobalFrame()
Definition: mainFrame.c:593
if
if(last==0)
Definition: sparse_int.h:34
Gia_Man_t_::pSpec
char * pSpec
Definition: gia.h:98
Gia_ManStaticFanoutStart
void Gia_ManStaticFanoutStart(Gia_Man_t *p)
Definition: giaFanout.c:238
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Gla_Obj_t_::fMark
unsigned fMark
Definition: absGlaOld.c:55
Vec_IntUniqify
static int Vec_IntUniqify(Vec_Int_t *p)
Definition: vecInt.h:1314
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
sprintf
char * sprintf()
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Counter
static int Counter
Definition: extraBddMisc.c:1877
Gla_Man_t_::pvRefis
Vec_Int_t * pvRefis
Definition: absGlaOld.c:91
Gla_Man_t_::nObjAdded
int nObjAdded
Definition: absGlaOld.c:80
Cnf_DeriveOther
Cnf_Dat_t * Cnf_DeriveOther(Aig_Man_t *pAig, int fSkipTtMin)
Definition: cnfCore.c:219
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
Gia_ObjPrint
void Gia_ObjPrint(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaUtil.c:1258
Vec_IntGetEntryP
static int * Vec_IntGetEntryP(Vec_Int_t *p, int i)
Definition: vecInt.h:618
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
sat_solver2_bookmark
static void sat_solver2_bookmark(sat_solver2 *s)
Definition: satSolver2.h:248
Gia_GlaSendCancel
void Gia_GlaSendCancel(Gla_Man_t *p, int fVerbose)
Definition: absGlaOld.c:1589
Vec_IntCap
static int Vec_IntCap(Vec_Int_t *p)
Definition: vecInt.h:368
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact)
Definition: giaAiger.c:1024
Gia_ObjForEachFanoutStatic
#define Gia_ObjForEachFanoutStatic(p, pObj, pFanout, i)
Definition: gia.h:946
Gla_ManCollectFanins
void Gla_ManCollectFanins(Gla_Man_t *p, Gla_Obj_t *pGla, int iObj, Vec_Int_t *vFanins)
Definition: absGlaOld.c:715
Vec_IntForEachEntryDouble
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition: vecInt.h:66
Gia_ObjFanin0Copy
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
sat_solver2_t::nConfLimit
ABC_INT64_T nConfLimit
Definition: satSolver2.h:173
Gla_Man_t_
Definition: absGlaOld.c:62
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Gla_Man_t_::nSatVars
int nSatVars
Definition: absGlaOld.c:81
sat_solver2_add_buffer
static int sat_solver2_add_buffer(sat_solver2 *pSat, int iVarA, int iVarB, int fCompl, int fMark, int Id)
Definition: satSolver2.h:275
stats_t::conflicts
ABC_INT64_T conflicts
Definition: satVec.h:154
Gla_ManGiaObj
static Gia_Obj_t * Gla_ManGiaObj(Gla_Man_t *p, Gla_Obj_t *pObj)
Definition: absGlaOld.c:111
Rfn_Obj_t_
Definition: absGlaOld.c:34
Gla_Man_t_::pObjRoot
Gla_Obj_t * pObjRoot
Definition: absGlaOld.c:70
Prf_ManRestart
static void Prf_ManRestart(Prf_Man_t *p, Vec_Int_t *vId2Pr, int iFirst, int nWidth)
Definition: satProof2.h:120
Gla_Man_t_::nAbsOld
int nAbsOld
Definition: absGlaOld.c:74
Gia_ManDupMapped_rec
void Gia_ManDupMapped_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Gia_Man_t *pNew)
Definition: absGlaOld.c:741
Gla_ManObj
static Gla_Obj_t * Gla_ManObj(Gla_Man_t *p, int i)
Definition: absGlaOld.c:110
Gla_ManForEachObj
#define Gla_ManForEachObj(p, pObj)
Definition: absGlaOld.c:119
Gia_ObjTerSimGet1
static int Gia_ObjTerSimGet1(Gia_Obj_t *pObj)
Definition: gia.h:776
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Prf_ManGrow
static void Prf_ManGrow(Prf_Man_t *p, int nWidth)
Definition: satProof2.h:129
Gla_ManCheckVar
static int Gla_ManCheckVar(Gla_Man_t *p, int iObj, int iFrame)
Definition: absGlaOld.c:1298
Gla_ManAbsPrintFrame
void Gla_ManAbsPrintFrame(Gla_Man_t *p, int nCoreSize, int nFrames, int nConfls, int nCexes, abctime Time)
Definition: absGlaOld.c:1509
Abc_FrameSetNFrames
ABC_DLL void Abc_FrameSetNFrames(int nFrames)
Definition: mainFrame.c:87
Gla_Man_t_::timeSat
abctime timeSat
Definition: absGlaOld.c:97
lit_sign
static int lit_sign(lit l)
Definition: satVec.h:146
Vec_IntShrink
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
Gia_GlaDumpAbsracted
void Gia_GlaDumpAbsracted(Gla_Man_t *p, int fVerbose)
Definition: absGlaOld.c:1609
sat_solver2_t::pPrf1
Vec_Set_t * pPrf1
Definition: satSolver2.h:162
Gia_GlaAddOneSlice
void Gia_GlaAddOneSlice(Gla_Man_t *p, int fCur, Vec_Int_t *vCore)
Definition: absGlaOld.c:1397
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_ObjRiToRo
static Gia_Obj_t * Gia_ObjRiToRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:447
Gia_Man_t_
Definition: gia.h:95
ABC_PRMP
#define ABC_PRMP(a, f, F)
Definition: abc_global.h:227
sat_solver2_nvars
static int sat_solver2_nvars(sat_solver2 *s)
Definition: satSolver2.h:190
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Gla_Obj_t_::fRi
unsigned fRi
Definition: absGlaOld.c:53
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
Gla_ManStart2
Gla_Man_t * Gla_ManStart2(Gia_Man_t *pGia, Abs_Par_t *pPars)
Definition: absGlaOld.c:1002
Gia_ObjTerSimSetC
static void Gia_ObjTerSimSetC(Gia_Obj_t *pObj)
Definition: gia.h:769
Gla_Man_t_::timeUnsat
abctime timeUnsat
Definition: absGlaOld.c:98
Gia_ManToBridgeAbsNetlist
int Gia_ManToBridgeAbsNetlist(FILE *pFile, void *p, int pkg_type)
Definition: utilBridge.c:189
Gia_ManPerformGlaOld
int Gia_ManPerformGlaOld(Gia_Man_t *pAig, Abs_Par_t *pPars, int fStartVta)
Definition: absGlaOld.c:1638
sat_solver2_add_const
static int sat_solver2_add_const(sat_solver2 *pSat, int iVar, int fCompl, int fMark, int Id)
Definition: satSolver2.h:263
Gia_ObjTerSimSet1
static void Gia_ObjTerSimSet1(Gia_Obj_t *pObj)
Definition: gia.h:771
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
sat_solver2_t::pPrf2
Prf_Man_t * pPrf2
Definition: satSolver2.h:166
l_False
#define l_False
Definition: SolverTypes.h:85
Gla_Man_t_::nCexes
int nCexes
Definition: absGlaOld.c:79
Gia_ObjFaninId0p
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
Gla_Man_t_::nObjs
int nObjs
Definition: absGlaOld.c:73
Gla_Man_t_::vObjCounts
Vec_Int_t * vObjCounts
Definition: absGlaOld.c:86
Gia_ObjIsPo
static int Gia_ObjIsPo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:442
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Gla_ManForEachObjAbsVec
#define Gla_ManForEachObjAbsVec(vVec, p, pObj, i)
Definition: absGlaOld.c:123
Gla_Obj_t_
Definition: absGlaOld.c:44
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
Prf_ManStopP
static void Prf_ManStopP(Prf_Man_t **p)
Definition: satProof2.h:99
Gla_ManTranslate
Vec_Int_t * Gla_ManTranslate(Gla_Man_t *p)
Definition: absGlaOld.c:1184
Gla_ManCountPPis
int Gla_ManCountPPis(Gla_Man_t *p)
Definition: absGlaOld.c:1257
Gla_Obj_t
struct Gla_Obj_t_ Gla_Obj_t
Definition: absGlaOld.c:43
Gla_ManRollBack
void Gla_ManRollBack(Gla_Man_t *p)
Definition: absGlaOld.c:1405
assert
#define assert(ex)
Definition: util_old.h:213
Extra_FileNameGenericAppend
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition: extraUtilFile.c:185
Vec_IntEntryP
static int * Vec_IntEntryP(Vec_Int_t *p, int i)
Definition: vecInt.h:417
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
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Gla_Man_t_::nProofIds
int nProofIds
Definition: absGlaOld.c:89
BRIDGE_ABS_NETLIST
#define BRIDGE_ABS_NETLIST
Definition: abc_global.h:295
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Gla_Obj_t_::fRo
unsigned fRo
Definition: absGlaOld.c:52
Gia_ManForEachObj1
#define Gia_ManForEachObj1(p, pObj, i)
Definition: gia.h:986
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
Gla_ManDeriveCex
Abc_Cex_t * Gla_ManDeriveCex(Gla_Man_t *p, Vec_Int_t *vPis)
Definition: absGlaOld.c:188
Gla_Obj_t_::nFanins
unsigned nFanins
Definition: absGlaOld.c:56
Gla_ManStart
Gla_Man_t * Gla_ManStart(Gia_Man_t *pGia0, Abs_Par_t *pPars)
Definition: absGlaOld.c:825
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_IntPushUnique
static int Vec_IntPushUnique(Vec_Int_t *p, int Entry)
Definition: vecInt.h:832
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition: utilCex.c:371
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
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
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Gla_Man_t_::vTemp
Vec_Int_t * vTemp
Definition: absGlaOld.c:84
Cnf_Dat_t_::nLiterals
int nLiterals
Definition: cnf.h:60
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
sat_solver2_t::nRuntimeLimit
abctime nRuntimeLimit
Definition: satSolver2.h:175
Gia_ObjTerSimSetX
static void Gia_ObjTerSimSetX(Gia_Obj_t *pObj)
Definition: gia.h:772
Abc_PrintInt
static void Abc_PrintInt(int i)
Definition: abc_global.h:342
sat_solver2_nconflicts
static int sat_solver2_nconflicts(sat_solver2 *s)
Definition: satSolver2.h:205
sat_solver2_t::nLearntRatio
int nLearntRatio
Definition: satSolver2.h:121
Gla_Man_t_::vCoreCounts
Vec_Int_t * vCoreCounts
Definition: absGlaOld.c:87
Gla_Obj_t_::fAnd
unsigned fAnd
Definition: absGlaOld.c:54
Gia_ObjCioId
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Gia_Man_t_::vLutConfigs
Vec_Int_t * vLutConfigs
Definition: gia.h:134
Abs_Par_t
typedefABC_NAMESPACE_HEADER_START struct Abs_Par_t_ Abs_Par_t
INCLUDES ///.
Definition: abs.h:46
Gla_Man_t_::pObj2Obj
unsigned * pObj2Obj
Definition: absGlaOld.c:72
Gia_ObjTerSimAnd
static void Gia_ObjTerSimAnd(Gia_Obj_t *pObj)
Definition: gia.h:785
ABC_FALLOC
#define ABC_FALLOC(type, num)
Definition: abc_global.h:231
Gla_Man_t_::vProofIds
Vec_Int_t * vProofIds
Definition: absGlaOld.c:88
sat_solver2_set_runtime_limit
static abctime sat_solver2_set_runtime_limit(sat_solver2 *s, abctime Limit)
Definition: satSolver2.h:234
Gia_GlaPrepareCexAndMap
void Gia_GlaPrepareCexAndMap(Gla_Man_t *p, Abc_Cex_t **ppCex, Vec_Int_t **pvMap)
FUNCTION DEFINITIONS ///.
Definition: absGlaOld.c:149
Gia_ObjIsPi
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Gia_Man_t_::pCexSeq
Abc_Cex_t * pCexSeq
Definition: gia.h:136
Cnf_Dat_t_::pObj2Count
int * pObj2Count
Definition: cnf.h:65
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Gla_ManReportMemory
void Gla_ManReportMemory(Gla_Man_t *p)
Definition: absGlaOld.c:1537