abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
absGla.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [absGla2.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Abstraction package.]
8 
9  Synopsis [Scalable 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: absGla2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "base/main/main.h"
22 #include "sat/cnf/cnf.h"
23 #include "sat/bsat/satSolver2.h"
24 #include "bool/kit/kit.h"
25 #include "abs.h"
26 #include "absRef.h"
27 //#include "absRef2.h"
28 
29 ABC_NAMESPACE_IMPL_START
30 
31 ////////////////////////////////////////////////////////////////////////
32 /// DECLARATIONS ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 #define GA2_BIG_NUM 0x3FFFFFF0
36 
37 typedef struct Ga2_Man_t_ Ga2_Man_t; // manager
38 struct Ga2_Man_t_
39 {
40  // user data
41  Gia_Man_t * pGia; // working AIG manager
42  Abs_Par_t * pPars; // parameters
43  // markings
44  Vec_Ptr_t * vCnfs; // for each object: CNF0, CNF1
45  // abstraction
46  Vec_Int_t * vIds; // abstraction ID for each GIA object
47  Vec_Int_t * vProofIds; // mapping of GIA objects into their proof IDs
48  Vec_Int_t * vAbs; // array of abstracted objects
49  Vec_Int_t * vValues; // array of objects with abstraction ID assigned
50  int nProofIds; // the counter of proof IDs
51  int LimAbs; // limit value for starting abstraction objects
52  int LimPpi; // limit value for starting PPI objects
53  int nMarked; // total number of marked nodes and flops
54  int fUseNewLine; // remember that you used new line
55  // refinement
56  Rnm_Man_t * pRnm; // refinement manager
57 // Rf2_Man_t * pRf2; // refinement manager
58  // SAT solver and variables
59  Vec_Ptr_t * vId2Lit; // mapping, for each timeframe, of object ID into SAT literal
60  sat_solver2 * pSat; // incremental SAT solver
61  int nSatVars; // the number of SAT variables
62  int nCexes; // the number of counter-examples
63  int nObjAdded; // objs added during refinement
64  int nPdrCalls; // count the number of concurrent calls
65  // hash table
66  int * pTable;
67  int nTable;
68  int nHashHit;
69  int nHashMiss;
70  int nHashOver;
71  // temporaries
72  Vec_Int_t * vLits;
73  Vec_Int_t * vIsopMem;
74  char * pSopSizes, ** pSops; // CNF representation
75  // statistics
76  abctime timeStart;
77  abctime timeInit;
78  abctime timeSat;
79  abctime timeUnsat;
80  abctime timeCex;
81  abctime timeOther;
82 };
83 
84 static inline int Ga2_ObjId( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vIds, Gia_ObjId(p->pGia, pObj)); }
85 static inline void Ga2_ObjSetId( Ga2_Man_t * p, Gia_Obj_t * pObj, int i ) { Vec_IntWriteEntry(p->vIds, Gia_ObjId(p->pGia, pObj), i); }
86 
87 static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return (Vec_Int_t *)Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj) ); }
88 static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return (Vec_Int_t *)Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)+1 ); }
89 
90 static inline int Ga2_ObjIsAbs0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return Ga2_ObjId(p,pObj) >= 0 && Ga2_ObjId(p,pObj) < p->LimAbs; }
91 static inline int Ga2_ObjIsLeaf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return Ga2_ObjId(p,pObj) >= p->LimAbs && Ga2_ObjId(p,pObj) < p->LimPpi; }
92 static inline int Ga2_ObjIsAbs( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Ga2_ObjId(p,pObj) >= 0 && Ga2_ObjCnf0(p,pObj); }
93 static inline int Ga2_ObjIsLeaf( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Ga2_ObjId(p,pObj) >= 0 && !Ga2_ObjCnf0(p,pObj); }
94 
95 static inline Vec_Int_t * Ga2_MapFrameMap( Ga2_Man_t * p, int f ) { return (Vec_Int_t *)Vec_PtrEntry( p->vId2Lit, f ); }
96 
97 // returns literal of this object, or -1 if SAT variable of the object is not assigned
98 static inline int Ga2_ObjFindLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
99 {
100 // int Id = Ga2_ObjId(p,pObj);
101  assert( Ga2_ObjId(p,pObj) >= 0 && Ga2_ObjId(p,pObj) < Vec_IntSize(p->vValues) );
102  return Vec_IntEntry( Ga2_MapFrameMap(p, f), Ga2_ObjId(p,pObj) );
103 }
104 // inserts literal of this object
105 static inline void Ga2_ObjAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f, int Lit )
106 {
107 // assert( Lit > 1 );
108  assert( Ga2_ObjFindLit(p, pObj, f) == -1 );
109  Vec_IntSetEntry( Ga2_MapFrameMap(p, f), Ga2_ObjId(p,pObj), Lit );
110 }
111 // returns or inserts-and-returns literal of this object
112 static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
113 {
114  int Lit = Ga2_ObjFindLit( p, pObj, f );
115  if ( Lit == -1 )
116  {
117  Lit = toLitCond( p->nSatVars++, 0 );
118  Ga2_ObjAddLit( p, pObj, f, Lit );
119  }
120 // assert( Lit > 1 );
121  return Lit;
122 }
123 
124 
125 ////////////////////////////////////////////////////////////////////////
126 /// FUNCTION DEFINITIONS ///
127 ////////////////////////////////////////////////////////////////////////
128 
129 /**Function*************************************************************
130 
131  Synopsis [Computes truth table for the marked node.]
132 
133  Description []
134 
135  SideEffects []
136 
137  SeeAlso []
138 
139 ***********************************************************************/
140 unsigned Ga2_ObjComputeTruth_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fFirst )
141 {
142  unsigned Val0, Val1;
143  if ( pObj->fPhase && !fFirst )
144  return pObj->Value;
145  assert( Gia_ObjIsAnd(pObj) );
146  Val0 = Ga2_ObjComputeTruth_rec( p, Gia_ObjFanin0(pObj), 0 );
147  Val1 = Ga2_ObjComputeTruth_rec( p, Gia_ObjFanin1(pObj), 0 );
148  return (Gia_ObjFaninC0(pObj) ? ~Val0 : Val0) & (Gia_ObjFaninC1(pObj) ? ~Val1 : Val1);
149 }
150 unsigned Ga2_ManComputeTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves )
151 {
152  static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
153  Gia_Obj_t * pObj;
154  unsigned Res;
155  int i;
156  Gia_ManForEachObjVec( vLeaves, p, pObj, i )
157  pObj->Value = uTruth5[i];
158  Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 );
159  Gia_ManForEachObjVec( vLeaves, p, pObj, i )
160  pObj->Value = 0;
161  return Res;
162 }
163 
164 /**Function*************************************************************
165 
166  Synopsis [Returns AIG marked for CNF generation.]
167 
168  Description [The marking satisfies the following requirements:
169  Each marked node has the number of marked fanins no more than N.]
170 
171  SideEffects [Uses pObj->fPhase to store the markings.]
172 
173  SeeAlso []
174 
175 ***********************************************************************/
176 int Ga2_ManBreakTree_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fFirst, int N )
177 { // breaks a tree rooted at the node into N-feasible subtrees
178  int Val0, Val1;
179  if ( pObj->fPhase && !fFirst )
180  return 1;
181  Val0 = Ga2_ManBreakTree_rec( p, Gia_ObjFanin0(pObj), 0, N );
182  Val1 = Ga2_ManBreakTree_rec( p, Gia_ObjFanin1(pObj), 0, N );
183  if ( Val0 + Val1 < N )
184  return Val0 + Val1;
185  if ( Val0 + Val1 == N )
186  {
187  pObj->fPhase = 1;
188  return 1;
189  }
190  assert( Val0 + Val1 > N );
191  assert( Val0 < N && Val1 < N );
192  if ( Val0 >= Val1 )
193  {
194  Gia_ObjFanin0(pObj)->fPhase = 1;
195  Val0 = 1;
196  }
197  else
198  {
199  Gia_ObjFanin1(pObj)->fPhase = 1;
200  Val1 = 1;
201  }
202  if ( Val0 + Val1 < N )
203  return Val0 + Val1;
204  if ( Val0 + Val1 == N )
205  {
206  pObj->fPhase = 1;
207  return 1;
208  }
209  assert( 0 );
210  return -1;
211 }
212 int Ga2_ManCheckNodesAnd( Gia_Man_t * p, Vec_Int_t * vNodes )
213 {
214  Gia_Obj_t * pObj;
215  int i;
216  Gia_ManForEachObjVec( vNodes, p, pObj, i )
217  if ( (!Gia_ObjFanin0(pObj)->fPhase && Gia_ObjFaninC0(pObj)) ||
218  (!Gia_ObjFanin1(pObj)->fPhase && Gia_ObjFaninC1(pObj)) )
219  return 0;
220  return 1;
221 }
222 void Ga2_ManCollectNodes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes, int fFirst )
223 {
224  if ( pObj->fPhase && !fFirst )
225  return;
226  assert( Gia_ObjIsAnd(pObj) );
227  Ga2_ManCollectNodes_rec( p, Gia_ObjFanin0(pObj), vNodes, 0 );
228  Ga2_ManCollectNodes_rec( p, Gia_ObjFanin1(pObj), vNodes, 0 );
229  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
230 
231 }
232 void Ga2_ManCollectLeaves_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLeaves, int fFirst )
233 {
234  if ( pObj->fPhase && !fFirst )
235  {
236  Vec_IntPushUnique( vLeaves, Gia_ObjId(p, pObj) );
237  return;
238  }
239  assert( Gia_ObjIsAnd(pObj) );
240  Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin0(pObj), vLeaves, 0 );
241  Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin1(pObj), vLeaves, 0 );
242 }
243 int Ga2_ManMarkup( Gia_Man_t * p, int N, int fSimple )
244 {
245  static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
246 // abctime clk = Abc_Clock();
247  Vec_Int_t * vLeaves;
248  Gia_Obj_t * pObj;
249  int i, k, Leaf, CountMarks;
250 
251  vLeaves = Vec_IntAlloc( 100 );
252 
253  if ( fSimple )
254  {
255  Gia_ManForEachObj( p, pObj, i )
256  pObj->fPhase = !Gia_ObjIsCo(pObj);
257  }
258  else
259  {
260  // label nodes with multiple fanouts and inputs MUXes
261  Gia_ManForEachObj( p, pObj, i )
262  {
263  pObj->Value = 0;
264  if ( !Gia_ObjIsAnd(pObj) )
265  continue;
266  Gia_ObjFanin0(pObj)->Value++;
267  Gia_ObjFanin1(pObj)->Value++;
268  if ( !Gia_ObjIsMuxType(pObj) )
269  continue;
270  Gia_ObjFanin0(Gia_ObjFanin0(pObj))->Value++;
271  Gia_ObjFanin1(Gia_ObjFanin0(pObj))->Value++;
272  Gia_ObjFanin0(Gia_ObjFanin1(pObj))->Value++;
273  Gia_ObjFanin1(Gia_ObjFanin1(pObj))->Value++;
274  }
275  Gia_ManForEachObj( p, pObj, i )
276  {
277  pObj->fPhase = 0;
278  if ( Gia_ObjIsAnd(pObj) )
279  pObj->fPhase = (pObj->Value > 1);
280  else if ( Gia_ObjIsCo(pObj) )
281  Gia_ObjFanin0(pObj)->fPhase = 1;
282  else
283  pObj->fPhase = 1;
284  }
285  // add marks when needed
286  Gia_ManForEachAnd( p, pObj, i )
287  {
288  if ( !pObj->fPhase )
289  continue;
290  Vec_IntClear( vLeaves );
291  Ga2_ManCollectLeaves_rec( p, pObj, vLeaves, 1 );
292  if ( Vec_IntSize(vLeaves) > N )
293  Ga2_ManBreakTree_rec( p, pObj, 1, N );
294  }
295  }
296 
297  // verify that the tree is split correctly
298  Vec_IntFreeP( &p->vMapping );
299  p->vMapping = Vec_IntStart( Gia_ManObjNum(p) );
300  Gia_ManForEachRo( p, pObj, i )
301  {
302  Gia_Obj_t * pObjRi = Gia_ObjRoToRi(p, pObj);
303  assert( pObj->fPhase );
304  assert( Gia_ObjFanin0(pObjRi)->fPhase );
305  // create map
306  Vec_IntWriteEntry( p->vMapping, Gia_ObjId(p, pObj), Vec_IntSize(p->vMapping) );
307  Vec_IntPush( p->vMapping, 1 );
308  Vec_IntPush( p->vMapping, Gia_ObjFaninId0p(p, pObjRi) );
309  Vec_IntPush( p->vMapping, Gia_ObjFaninC0(pObjRi) ? 0x55555555 : 0xAAAAAAAA );
310  Vec_IntPush( p->vMapping, -1 ); // placeholder for ref counter
311  }
312  CountMarks = Gia_ManRegNum(p);
313  Gia_ManForEachAnd( p, pObj, i )
314  {
315  if ( !pObj->fPhase )
316  continue;
317  Vec_IntClear( vLeaves );
318  Ga2_ManCollectLeaves_rec( p, pObj, vLeaves, 1 );
319  assert( Vec_IntSize(vLeaves) <= N );
320  // create map
321  Vec_IntWriteEntry( p->vMapping, i, Vec_IntSize(p->vMapping) );
322  Vec_IntPush( p->vMapping, Vec_IntSize(vLeaves) );
323  Vec_IntForEachEntry( vLeaves, Leaf, k )
324  {
325  Vec_IntPush( p->vMapping, Leaf );
326  Gia_ManObj(p, Leaf)->Value = uTruth5[k];
327  assert( Gia_ManObj(p, Leaf)->fPhase );
328  }
329  Vec_IntPush( p->vMapping, (int)Ga2_ObjComputeTruth_rec( p, pObj, 1 ) );
330  Vec_IntPush( p->vMapping, -1 ); // placeholder for ref counter
331  CountMarks++;
332  }
333 // Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
334  Vec_IntFree( vLeaves );
335  Gia_ManCleanValue( p );
336  return CountMarks;
337 }
338 void Ga2_ManComputeTest( Gia_Man_t * p )
339 {
340  abctime clk;
341 // unsigned uTruth;
342  Gia_Obj_t * pObj;
343  int i, Counter = 0;
344  clk = Abc_Clock();
345  Ga2_ManMarkup( p, 5, 0 );
346  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
347  Gia_ManForEachAnd( p, pObj, i )
348  {
349  if ( !pObj->fPhase )
350  continue;
351 // uTruth = Ga2_ObjTruth( p, pObj );
352 // printf( "%6d : ", Counter );
353 // Kit_DsdPrintFromTruth( &uTruth, Ga2_ObjLeaveNum(p, pObj) );
354 // printf( "\n" );
355  Counter++;
356  }
357  Abc_Print( 1, "Marked AND nodes = %6d. ", Counter );
358  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
359 }
360 
361 /**Function*************************************************************
362 
363  Synopsis []
364 
365  Description []
366 
367  SideEffects []
368 
369  SeeAlso []
370 
371 ***********************************************************************/
372 Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Abs_Par_t * pPars )
373 {
374  Ga2_Man_t * p;
375  p = ABC_CALLOC( Ga2_Man_t, 1 );
376  p->timeStart = Abc_Clock();
377  p->fUseNewLine = 1;
378  // user data
379  p->pGia = pGia;
380  p->pPars = pPars;
381  // markings
382  p->nMarked = Ga2_ManMarkup( pGia, 5, pPars->fUseSimple );
383  p->vCnfs = Vec_PtrAlloc( 1000 );
384  Vec_PtrPush( p->vCnfs, Vec_IntAlloc(0) );
385  Vec_PtrPush( p->vCnfs, Vec_IntAlloc(0) );
386  // abstraction
387  p->vIds = Vec_IntStartFull( Gia_ManObjNum(pGia) );
388  p->vProofIds = Vec_IntAlloc( 0 );
389  p->vAbs = Vec_IntAlloc( 1000 );
390  p->vValues = Vec_IntAlloc( 1000 );
391  // add constant node to abstraction
392  Ga2_ObjSetId( p, Gia_ManConst0(pGia), 0 );
393  Vec_IntPush( p->vValues, 0 );
394  Vec_IntPush( p->vAbs, 0 );
395  // refinement
396  p->pRnm = Rnm_ManStart( pGia );
397 // p->pRf2 = Rf2_ManStart( pGia );
398  // SAT solver and variables
399  p->vId2Lit = Vec_PtrAlloc( 1000 );
400  // temporaries
401  p->vLits = Vec_IntAlloc( 100 );
402  p->vIsopMem = Vec_IntAlloc( 100 );
403  Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
404  // hash table
405  p->nTable = Abc_PrimeCudd(1<<18);
406  p->pTable = ABC_CALLOC( int, 6 * p->nTable );
407  return p;
408 }
409 
410 void Ga2_ManDumpStats( Gia_Man_t * pGia, Abs_Par_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN )
411 {
412  FILE * pFile;
413  char pFileName[32];
414  sprintf( pFileName, "stats_gla%s%s.txt", fUseN ? "n":"", pPars->fUseFullProof ? "p":"" );
415 
416  pFile = fopen( pFileName, "a+" );
417 
418  fprintf( pFile, "%s pi=%d ff=%d and=%d mem=%d bmc=%d",
419  pGia->pName,
420  Gia_ManPiNum(pGia), Gia_ManRegNum(pGia), Gia_ManAndNum(pGia),
421  (int)(1 + sat_solver2_memory_proof(pSat)/(1<<20)),
422  iFrame );
423 
424  if ( pGia->vGateClasses )
425  fprintf( pFile, " ff=%d and=%d",
426  Gia_GlaCountFlops( pGia, pGia->vGateClasses ),
427  Gia_GlaCountNodes( pGia, pGia->vGateClasses ) );
428 
429  fprintf( pFile, "\n" );
430  fclose( pFile );
431 }
432 void Ga2_ManReportMemory( Ga2_Man_t * p )
433 {
434  double memTot = 0;
435  double memAig = 1.0 * p->pGia->nObjsAlloc * sizeof(Gia_Obj_t) + Vec_IntMemory(p->pGia->vMapping);
436  double memSat = sat_solver2_memory( p->pSat, 1 );
437  double memPro = sat_solver2_memory_proof( p->pSat );
438  double memMap = Vec_VecMemoryInt( (Vec_Vec_t *)p->vId2Lit );
439  double memRef = Rnm_ManMemoryUsage( p->pRnm );
440  double memHash= sizeof(int) * 6 * p->nTable;
441  double memOth = sizeof(Ga2_Man_t);
442  memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCnfs );
443  memOth += Vec_IntMemory( p->vIds );
444  memOth += Vec_IntMemory( p->vProofIds );
445  memOth += Vec_IntMemory( p->vAbs );
446  memOth += Vec_IntMemory( p->vValues );
447  memOth += Vec_IntMemory( p->vLits );
448  memOth += Vec_IntMemory( p->vIsopMem );
449  memOth += 336450 + (sizeof(char) + sizeof(char*)) * 65536;
450  memTot = memAig + memSat + memPro + memMap + memRef + memHash + memOth;
451  ABC_PRMP( "Memory: AIG ", memAig, memTot );
452  ABC_PRMP( "Memory: SAT ", memSat, memTot );
453  ABC_PRMP( "Memory: Proof ", memPro, memTot );
454  ABC_PRMP( "Memory: Map ", memMap, memTot );
455  ABC_PRMP( "Memory: Refine ", memRef, memTot );
456  ABC_PRMP( "Memory: Hash ", memHash,memTot );
457  ABC_PRMP( "Memory: Other ", memOth, memTot );
458  ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
459 }
460 void Ga2_ManStop( Ga2_Man_t * p )
461 {
462  Vec_IntFreeP( &p->pGia->vMapping );
463  Gia_ManSetPhase( p->pGia );
464  if ( p->pPars->fVerbose )
465  Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d ObjsAdded = %d\n",
466  sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat),
467  sat_solver2_nconflicts(p->pSat), sat_solver2_nlearnts(p->pSat),
468  p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
469  if ( p->pPars->fVerbose )
470  Abc_Print( 1, "Hash hits = %d. Hash misses = %d. Hash overs = %d. Concurrent calls = %d.\n",
471  p->nHashHit, p->nHashMiss, p->nHashOver, p->nPdrCalls );
472 
473  if( p->pSat ) sat_solver2_delete( p->pSat );
474  Vec_VecFree( (Vec_Vec_t *)p->vCnfs );
475  Vec_VecFree( (Vec_Vec_t *)p->vId2Lit );
476  Vec_IntFree( p->vIds );
477  Vec_IntFree( p->vProofIds );
478  Vec_IntFree( p->vAbs );
479  Vec_IntFree( p->vValues );
480  Vec_IntFree( p->vLits );
481  Vec_IntFree( p->vIsopMem );
482  Rnm_ManStop( p->pRnm, 0 );
483 // Rf2_ManStop( p->pRf2, p->pPars->fVerbose );
484  ABC_FREE( p->pTable );
485  ABC_FREE( p->pSopSizes );
486  ABC_FREE( p->pSops[1] );
487  ABC_FREE( p->pSops );
488  ABC_FREE( p );
489 }
490 
491 
492 /**Function*************************************************************
493 
494  Synopsis [Computes a minimized truth table.]
495 
496  Description [Input literals can be 0/1 (const 0/1), non-trivial literals
497  (integers that are more than 1) and unassigned literals (large integers).
498  This procedure computes the truth table that essentially depends on input
499  variables ordered in the increasing order of their positive literals.]
500 
501  SideEffects []
502 
503  SeeAlso []
504 
505 ***********************************************************************/
506 static inline unsigned Ga2_ObjTruthDepends( unsigned t, int v )
507 {
508  static unsigned uInvTruth5[5] = { 0x55555555, 0x33333333, 0x0F0F0F0F, 0x00FF00FF, 0x0000FFFF };
509  assert( v >= 0 && v <= 4 );
510  return ((t ^ (t >> (1 << v))) & uInvTruth5[v]);
511 }
512 unsigned Ga2_ObjComputeTruthSpecial( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vLits )
513 {
514  int fVerbose = 0;
515  static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
516  unsigned Res;
517  Gia_Obj_t * pObj;
518  int i, Entry;
519 // int Id = Gia_ObjId(p, pRoot);
520  assert( Gia_ObjIsAnd(pRoot) );
521 
522  if ( fVerbose )
523  printf( "Object %d.\n", Gia_ObjId(p, pRoot) );
524 
525  // assign elementary truth tables
526  Gia_ManForEachObjVec( vLeaves, p, pObj, i )
527  {
528  Entry = Vec_IntEntry( vLits, i );
529  assert( Entry >= 0 );
530  if ( Entry == 0 )
531  pObj->Value = 0;
532  else if ( Entry == 1 )
533  pObj->Value = ~0;
534  else // non-trivial literal
535  pObj->Value = uTruth5[i];
536  if ( fVerbose )
537  printf( "%d ", Entry );
538  }
539 
540  if ( fVerbose )
541  {
542  Res = Ga2_ObjTruth( p, pRoot );
543 // Kit_DsdPrintFromTruth( &Res, Vec_IntSize(vLeaves) );
544  printf( "\n" );
545  }
546 
547  // compute truth table
548  Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 );
549  if ( Res != 0 && Res != ~0 )
550  {
551  // find essential variables
552  int nUsed = 0, pUsed[5];
553  for ( i = 0; i < Vec_IntSize(vLeaves); i++ )
554  if ( Ga2_ObjTruthDepends( Res, i ) )
555  pUsed[nUsed++] = i;
556  assert( nUsed > 0 );
557  // order positions by literal value
558  Vec_IntSelectSortCost( pUsed, nUsed, vLits );
559  assert( Vec_IntEntry(vLits, pUsed[0]) <= Vec_IntEntry(vLits, pUsed[nUsed-1]) );
560  // assign elementary truth tables to the leaves
561  Gia_ManForEachObjVec( vLeaves, p, pObj, i )
562  {
563  Entry = Vec_IntEntry( vLits, i );
564  assert( Entry >= 0 );
565  if ( Entry == 0 )
566  pObj->Value = 0;
567  else if ( Entry == 1 )
568  pObj->Value = ~0;
569  else // non-trivial literal
570  pObj->Value = 0xDEADCAFE; // not important
571  }
572  for ( i = 0; i < nUsed; i++ )
573  {
574  Entry = Vec_IntEntry( vLits, pUsed[i] );
575  assert( Entry > 1 );
576  pObj = Gia_ManObj( p, Vec_IntEntry(vLeaves, pUsed[i]) );
577  pObj->Value = Abc_LitIsCompl(Entry) ? ~uTruth5[i] : uTruth5[i];
578 // pObj->Value = uTruth5[i];
579  // remember this literal
580  pUsed[i] = Abc_LitRegular(Entry);
581 // pUsed[i] = Entry;
582  }
583  // compute truth table
584  Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 );
585  // reload the literals
586  Vec_IntClear( vLits );
587  for ( i = 0; i < nUsed; i++ )
588  {
589  Vec_IntPush( vLits, pUsed[i] );
590  assert( Ga2_ObjTruthDepends(Res, i) );
591  if ( fVerbose )
592  printf( "%d ", pUsed[i] );
593  }
594  for ( ; i < 5; i++ )
595  assert( !Ga2_ObjTruthDepends(Res, i) );
596 
597 if ( fVerbose )
598 {
599 // Kit_DsdPrintFromTruth( &Res, nUsed );
600  printf( "\n" );
601 }
602 
603  }
604  else
605  {
606 
607 if ( fVerbose )
608 {
609  Vec_IntClear( vLits );
610  printf( "Const %d\n", Res > 0 );
611 }
612 
613  }
614  Gia_ManForEachObjVec( vLeaves, p, pObj, i )
615  pObj->Value = 0;
616  return Res;
617 }
618 
619 /**Function*************************************************************
620 
621  Synopsis [Returns CNF of the function.]
622 
623  Description []
624 
625  SideEffects []
626 
627  SeeAlso []
628 
629 ***********************************************************************/
630 Vec_Int_t * Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCover )
631 {
632  int RetValue;
633  assert( nVars <= 5 );
634  // transform truth table into the SOP
635  RetValue = Kit_TruthIsop( &uTruth, nVars, vCover, 0 );
636  assert( RetValue == 0 );
637  // check the case of constant cover
638  return Vec_IntDup( vCover );
639 }
640 
641 /**Function*************************************************************
642 
643  Synopsis [Derives CNF for one node.]
644 
645  Description []
646 
647  SideEffects []
648 
649  SeeAlso []
650 
651 ***********************************************************************/
652 static inline void Ga2_ManCnfAddDynamic( Ga2_Man_t * p, int uTruth, int Lits[], int iLitOut, int ProofId )
653 {
654  int i, k, b, Cube, nClaLits, ClaLits[6];
655 // assert( uTruth > 0 && uTruth < 0xffff );
656  for ( i = 0; i < 2; i++ )
657  {
658  if ( i )
659  uTruth = 0xffff & ~uTruth;
660 // Extra_PrintBinary( stdout, &uTruth, 16 ); printf( "\n" );
661  for ( k = 0; k < p->pSopSizes[uTruth]; k++ )
662  {
663  nClaLits = 0;
664  ClaLits[nClaLits++] = i ? lit_neg(iLitOut) : iLitOut;
665  Cube = p->pSops[uTruth][k];
666  for ( b = 3; b >= 0; b-- )
667  {
668  if ( Cube % 3 == 0 ) // value 0 --> add positive literal
669  {
670  assert( Lits[b] > 1 );
671  ClaLits[nClaLits++] = Lits[b];
672  }
673  else if ( Cube % 3 == 1 ) // value 1 --> add negative literal
674  {
675  assert( Lits[b] > 1 );
676  ClaLits[nClaLits++] = lit_neg(Lits[b]);
677  }
678  Cube = Cube / 3;
679  }
680  sat_solver2_addclause( p->pSat, ClaLits, ClaLits+nClaLits, ProofId );
681  }
682  }
683 }
684 void Ga2_ManCnfAddStatic( sat_solver2 * pSat, Vec_Int_t * vCnf0, Vec_Int_t * vCnf1, int Lits[], int iLitOut, int ProofId )
685 {
686  Vec_Int_t * vCnf;
687  int i, k, b, Cube, Literal, nClaLits, ClaLits[6];
688  for ( i = 0; i < 2; i++ )
689  {
690  vCnf = i ? vCnf1 : vCnf0;
691  Vec_IntForEachEntry( vCnf, Cube, k )
692  {
693  nClaLits = 0;
694  ClaLits[nClaLits++] = i ? lit_neg(iLitOut) : iLitOut;
695  for ( b = 0; b < 5; b++ )
696  {
697  Literal = 3 & (Cube >> (b << 1));
698  if ( Literal == 1 ) // value 0 --> add positive literal
699  {
700 // assert( Lits[b] > 1 );
701  ClaLits[nClaLits++] = Lits[b];
702  }
703  else if ( Literal == 2 ) // value 1 --> add negative literal
704  {
705 // assert( Lits[b] > 1 );
706  ClaLits[nClaLits++] = lit_neg(Lits[b]);
707  }
708  else if ( Literal != 0 )
709  assert( 0 );
710  }
711  sat_solver2_addclause( pSat, ClaLits, ClaLits+nClaLits, ProofId );
712  }
713  }
714 }
715 
716 /**Function*************************************************************
717 
718  Synopsis []
719 
720  Description []
721 
722  SideEffects []
723 
724  SeeAlso []
725 
726 ***********************************************************************/
727 static inline unsigned Saig_ManBmcHashKey( int * pArray )
728 {
729  static int s_Primes[5] = { 12582917, 25165843, 50331653, 100663319, 201326611 };
730  unsigned i, Key = 0;
731  for ( i = 0; i < 5; i++ )
732  Key += pArray[i] * s_Primes[i];
733  return Key;
734 }
735 static inline int * Saig_ManBmcLookup( Ga2_Man_t * p, int * pArray )
736 {
737  int * pTable = p->pTable + 6 * (Saig_ManBmcHashKey(pArray) % p->nTable);
738  if ( memcmp( pTable, pArray, 20 ) )
739  {
740  if ( pTable[0] == 0 )
741  p->nHashMiss++;
742  else
743  p->nHashOver++;
744  memcpy( pTable, pArray, 20 );
745  pTable[5] = 0;
746  }
747  else
748  p->nHashHit++;
749  assert( pTable + 5 < pTable + 6 * p->nTable );
750  return pTable + 5;
751 }
752 
753 /**Function*************************************************************
754 
755  Synopsis []
756 
757  Description []
758 
759  SideEffects []
760 
761  SeeAlso []
762 
763 ***********************************************************************/
764 static inline void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs )
765 {
766  unsigned uTruth;
767  int nLeaves;
768 // int Id = Gia_ObjId(p->pGia, pObj);
769  assert( pObj->fPhase );
770  assert( Vec_PtrSize(p->vCnfs) == 2 * Vec_IntSize(p->vValues) );
771  // assign abstraction ID to the node
772  if ( Ga2_ObjId(p,pObj) == -1 )
773  {
774  Ga2_ObjSetId( p, pObj, Vec_IntSize(p->vValues) );
775  Vec_IntPush( p->vValues, Gia_ObjId(p->pGia, pObj) );
776  Vec_PtrPush( p->vCnfs, NULL );
777  Vec_PtrPush( p->vCnfs, NULL );
778  }
779  assert( Ga2_ObjCnf0(p, pObj) == NULL );
780  if ( !fAbs )
781  return;
782  Vec_IntPush( p->vAbs, Gia_ObjId(p->pGia, pObj) );
783  assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
784  // compute parameters
785  nLeaves = Ga2_ObjLeaveNum(p->pGia, pObj);
786  uTruth = Ga2_ObjTruth( p->pGia, pObj );
787  // create CNF for pos/neg phases
788  Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj), Ga2_ManCnfCompute( uTruth, nLeaves, p->vIsopMem) );
789  Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, Ga2_ManCnfCompute(~uTruth, nLeaves, p->vIsopMem) );
790 }
791 
792 static inline void Ga2_ManAddToAbsOneStatic( Ga2_Man_t * p, Gia_Obj_t * pObj, int f, int fUseId )
793 {
794  Vec_Int_t * vLeaves;
795  Gia_Obj_t * pLeaf;
796  int k, Lit, iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f );
797  assert( iLitOut > 1 );
798  assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) );
799  if ( Gia_ObjIsConst0(pObj) || (f == 0 && Gia_ObjIsRo(p->pGia, pObj)) )
800  {
801  iLitOut = Abc_LitNot( iLitOut );
802  sat_solver2_addclause( p->pSat, &iLitOut, &iLitOut + 1, fUseId ? Gia_ObjId(p->pGia, pObj) : -1 );
803  }
804  else
805  {
806  int fUseStatic = 1;
807  Vec_IntClear( p->vLits );
808  vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
809  Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, k )
810  {
811  Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f - Gia_ObjIsRo(p->pGia, pObj) );
812  Vec_IntPush( p->vLits, Lit );
813  if ( Lit < 2 )
814  fUseStatic = 0;
815  }
816  if ( fUseStatic || Gia_ObjIsRo(p->pGia, pObj) )
817  Ga2_ManCnfAddStatic( p->pSat, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, fUseId ? Gia_ObjId(p->pGia, pObj) : -1 );
818  else
819  {
820  unsigned uTruth = Ga2_ObjComputeTruthSpecial( p->pGia, pObj, vLeaves, p->vLits );
821  Ga2_ManCnfAddDynamic( p, uTruth & 0xFFFF, Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj) );
822  }
823  }
824 }
825 static inline void Ga2_ManAddToAbsOneDynamic( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
826 {
827 // int Id = Gia_ObjId(p->pGia, pObj);
828  Vec_Int_t * vLeaves;
829  Gia_Obj_t * pLeaf;
830  unsigned uTruth;
831  int i, Lit;
832 
833  assert( Ga2_ObjIsAbs0(p, pObj) );
834  assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) );
835  if ( Gia_ObjIsConst0(pObj) || (f == 0 && Gia_ObjIsRo(p->pGia, pObj)) )
836  {
837  Ga2_ObjAddLit( p, pObj, f, 0 );
838  }
839  else if ( Gia_ObjIsRo(p->pGia, pObj) )
840  {
841  // if flop is included in the abstraction, but its driver is not
842  // flop input driver has no variable assigned -- we assign it here
843  pLeaf = Gia_ObjRoToRi( p->pGia, pObj );
844  Lit = Ga2_ObjFindOrAddLit( p, Gia_ObjFanin0(pLeaf), f-1 );
845  assert( Lit >= 0 );
846  Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(pLeaf) );
847  Ga2_ObjAddLit( p, pObj, f, Lit );
848  }
849  else
850  {
851  assert( Gia_ObjIsAnd(pObj) );
852  Vec_IntClear( p->vLits );
853  vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
854  Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, i )
855  {
856  if ( Ga2_ObjIsAbs0(p, pLeaf) ) // belongs to original abstraction
857  {
858  Lit = Ga2_ObjFindLit( p, pLeaf, f );
859  assert( Lit >= 0 );
860  }
861  else if ( Ga2_ObjIsLeaf0(p, pLeaf) ) // belongs to original PPIs
862  {
863  Lit = Ga2_ObjFindLit( p, pLeaf, f );
864 // Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f );
865  if ( Lit == -1 )
866  {
867  Lit = GA2_BIG_NUM + 2*i;
868 // assert( 0 );
869  }
870  }
871  else assert( 0 );
872  Vec_IntPush( p->vLits, Lit );
873  }
874 
875  // minimize truth table
876  uTruth = Ga2_ObjComputeTruthSpecial( p->pGia, pObj, vLeaves, p->vLits );
877  if ( uTruth == 0 || uTruth == ~0 ) // const 0 / 1
878  {
879  Lit = (uTruth > 0);
880  Ga2_ObjAddLit( p, pObj, f, Lit );
881  }
882  else if ( uTruth == 0xAAAAAAAA || uTruth == 0x55555555 ) // buffer / inverter
883  {
884  Lit = Vec_IntEntry( p->vLits, 0 );
885  if ( Lit >= GA2_BIG_NUM )
886  {
887  pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, (Lit-GA2_BIG_NUM)/2) );
888  Lit = Ga2_ObjFindLit( p, pLeaf, f );
889  assert( Lit == -1 );
890  Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f );
891  }
892  assert( Lit >= 0 );
893  Lit = Abc_LitNotCond( Lit, uTruth == 0x55555555 );
894  Ga2_ObjAddLit( p, pObj, f, Lit );
895  assert( Lit < 10000000 );
896  }
897  else
898  {
899  assert( Vec_IntSize(p->vLits) > 1 && Vec_IntSize(p->vLits) < 6 );
900  // replace literals
901  Vec_IntForEachEntry( p->vLits, Lit, i )
902  {
903  if ( Lit >= GA2_BIG_NUM )
904  {
905  pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, (Lit-GA2_BIG_NUM)/2) );
906  Lit = Ga2_ObjFindLit( p, pLeaf, f );
907  assert( Lit == -1 );
908  Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f );
909  Vec_IntWriteEntry( p->vLits, i, Lit );
910  }
911  assert( Lit < 10000000 );
912  }
913 
914  // add new nodes
915  if ( Vec_IntSize(p->vLits) == 5 )
916  {
917  Vec_IntClear( p->vLits );
918  Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, i )
919  Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pLeaf, f ) );
920  Lit = Ga2_ObjFindOrAddLit(p, pObj, f);
921  Ga2_ManCnfAddStatic( p->pSat, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), Lit, -1 );
922  }
923  else
924  {
925 // int fUseHash = 1;
926  if ( !p->pPars->fSkipHash )
927  {
928  int * pLookup, nSize = Vec_IntSize(p->vLits);
929  assert( Vec_IntSize(p->vLits) < 5 );
930  assert( Vec_IntEntry(p->vLits, 0) <= Vec_IntEntryLast(p->vLits) );
931  assert( Ga2_ObjFindLit(p, pObj, f) == -1 );
932  for ( i = Vec_IntSize(p->vLits); i < 4; i++ )
933  Vec_IntPush( p->vLits, GA2_BIG_NUM );
934  Vec_IntPush( p->vLits, (int)uTruth );
935  assert( Vec_IntSize(p->vLits) == 5 );
936 
937  // perform structural hashing here!!!
938  pLookup = Saig_ManBmcLookup( p, Vec_IntArray(p->vLits) );
939  if ( *pLookup == 0 )
940  {
941  *pLookup = Ga2_ObjFindOrAddLit(p, pObj, f);
942  Vec_IntShrink( p->vLits, nSize );
943  Ga2_ManCnfAddDynamic( p, uTruth & 0xFFFF, Vec_IntArray(p->vLits), *pLookup, -1 );
944  }
945  else
946  Ga2_ObjAddLit( p, pObj, f, *pLookup );
947 
948  }
949  else
950  {
951  Lit = Ga2_ObjFindOrAddLit(p, pObj, f);
952  Ga2_ManCnfAddDynamic( p, uTruth & 0xFFFF, Vec_IntArray(p->vLits), Lit, -1 );
953  }
954  }
955  }
956  }
957 }
958 
959 void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f )
960 {
961  int fSimple = 0;
962  Gia_Obj_t * pObj;
963  int i;
964  Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
965  {
966  if ( i == p->LimAbs )
967  break;
968  if ( fSimple )
969  Ga2_ManAddToAbsOneStatic( p, pObj, f, 0 );
970  else
971  Ga2_ManAddToAbsOneDynamic( p, pObj, f );
972  }
973  Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
974  if ( i >= p->LimAbs )
975  Ga2_ManAddToAbsOneStatic( p, pObj, f, 1 );
976 // sat_solver2_simplify( p->pSat );
977 }
978 
979 void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
980 {
981  Vec_Int_t * vLeaves;
982  Gia_Obj_t * pObj, * pFanin;
983  int f, i, k;
984  // add abstraction objects
985  Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
986  {
987  Ga2_ManSetupNode( p, pObj, 1 );
988  if ( p->pSat->pPrf2 )
989  Vec_IntWriteEntry( p->vProofIds, Gia_ObjId(p->pGia, pObj), p->nProofIds++ );
990  }
991  // add PPI objects
992  Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
993  {
994  vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
995  Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
996  if ( Ga2_ObjId( p, pFanin ) == -1 )
997  Ga2_ManSetupNode( p, pFanin, 0 );
998  }
999  // add new clauses to the timeframes
1000  for ( f = 0; f <= p->pPars->iFrame; f++ )
1001  {
1002  Vec_IntFillExtra( Ga2_MapFrameMap(p, f), Vec_IntSize(p->vValues), -1 );
1003  Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
1004  Ga2_ManAddToAbsOneStatic( p, pObj, f, 1 );
1005  }
1006 // sat_solver2_simplify( p->pSat );
1007 }
1008 
1009 void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues, int nSatVars )
1010 {
1011  Vec_Int_t * vMap;
1012  Gia_Obj_t * pObj;
1013  int i, k, Entry;
1014  assert( nAbs > 0 );
1015  assert( nValues > 0 );
1016  assert( nSatVars > 0 );
1017  // shrink abstraction
1018  Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
1019  {
1020  if ( !i ) continue;
1021  assert( Ga2_ObjCnf0(p, pObj) != NULL );
1022  assert( Ga2_ObjCnf1(p, pObj) != NULL );
1023  if ( i < nAbs )
1024  continue;
1025  Vec_IntFree( Ga2_ObjCnf0(p, pObj) );
1026  Vec_IntFree( Ga2_ObjCnf1(p, pObj) );
1027  Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj), NULL );
1028  Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, NULL );
1029  }
1030  Vec_IntShrink( p->vAbs, nAbs );
1031  // shrink values
1032  Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
1033  {
1034  assert( Ga2_ObjId(p,pObj) >= 0 );
1035  if ( i < nValues )
1036  continue;
1037  Ga2_ObjSetId( p, pObj, -1 );
1038  }
1039  Vec_IntShrink( p->vValues, nValues );
1040  Vec_PtrShrink( p->vCnfs, 2 * nValues );
1041  // hack to clear constant
1042  if ( nValues == 1 )
1043  nValues = 0;
1044  // clean mapping for each timeframe
1045  Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i )
1046  {
1047  Vec_IntShrink( vMap, nValues );
1048  Vec_IntForEachEntryStart( vMap, Entry, k, p->LimAbs )
1049  if ( Entry >= 2*nSatVars )
1050  Vec_IntWriteEntry( vMap, k, -1 );
1051  }
1052  // shrink SAT variables
1053  p->nSatVars = nSatVars;
1054 }
1055 
1056 /**Function*************************************************************
1057 
1058  Synopsis []
1059 
1060  Description []
1061 
1062  SideEffects []
1063 
1064  SeeAlso []
1065 
1066 ***********************************************************************/
1067 void Ga2_ManAbsTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vClasses, int fFirst )
1068 {
1069  if ( pObj->fPhase && !fFirst )
1070  return;
1071  assert( Gia_ObjIsAnd(pObj) );
1072  Ga2_ManAbsTranslate_rec( p, Gia_ObjFanin0(pObj), vClasses, 0 );
1073  Ga2_ManAbsTranslate_rec( p, Gia_ObjFanin1(pObj), vClasses, 0 );
1074  Vec_IntWriteEntry( vClasses, Gia_ObjId(p, pObj), 1 );
1075 }
1076 
1077 Vec_Int_t * Ga2_ManAbsTranslate( Ga2_Man_t * p )
1078 {
1079  Vec_Int_t * vGateClasses;
1080  Gia_Obj_t * pObj;
1081  int i;
1082  vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) );
1083  Vec_IntWriteEntry( vGateClasses, 0, 1 );
1084  Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
1085  {
1086  if ( Gia_ObjIsAnd(pObj) )
1087  Ga2_ManAbsTranslate_rec( p->pGia, pObj, vGateClasses, 1 );
1088  else if ( Gia_ObjIsRo(p->pGia, pObj) )
1089  Vec_IntWriteEntry( vGateClasses, Gia_ObjId(p->pGia, pObj), 1 );
1090  else if ( !Gia_ObjIsConst0(pObj) )
1091  assert( 0 );
1092 // Gia_ObjPrint( p->pGia, pObj );
1093  }
1094  return vGateClasses;
1095 }
1096 
1097 Vec_Int_t * Ga2_ManAbsDerive( Gia_Man_t * p )
1098 {
1099  Vec_Int_t * vToAdd;
1100  Gia_Obj_t * pObj;
1101  int i;
1102  vToAdd = Vec_IntAlloc( 1000 );
1103  Gia_ManForEachRo( p, pObj, i )
1104  if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, Gia_ObjId(p, pObj)) )
1105  Vec_IntPush( vToAdd, Gia_ObjId(p, pObj) );
1106  Gia_ManForEachAnd( p, pObj, i )
1107  if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, i) )
1108  Vec_IntPush( vToAdd, i );
1109  return vToAdd;
1110 }
1111 
1112 void Ga2_ManRestart( Ga2_Man_t * p )
1113 {
1114  Vec_Int_t * vToAdd;
1115  int Lit = 1;
1116  assert( p->pGia != NULL && p->pGia->vGateClasses != NULL );
1117  assert( Gia_ManPi(p->pGia, 0)->fPhase ); // marks are set
1118  // clear SAT variable numbers (begin with 1)
1119  if ( p->pSat ) sat_solver2_delete( p->pSat );
1120  p->pSat = sat_solver2_new();
1121  p->pSat->nLearntStart = p->pPars->nLearnedStart;
1122  p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
1123  p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
1124  p->pSat->nLearntMax = p->pSat->nLearntStart;
1125  // add clause x0 = 0 (lit0 = 1; lit1 = 0)
1126  sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, -1 );
1127  // remove previous abstraction
1128  Ga2_ManShrinkAbs( p, 1, 1, 1 );
1129  // start new abstraction
1130  vToAdd = Ga2_ManAbsDerive( p->pGia );
1131  assert( p->pSat->pPrf2 == NULL );
1132  assert( p->pPars->iFrame < 0 );
1133  Ga2_ManAddToAbs( p, vToAdd );
1134  Vec_IntFree( vToAdd );
1135  p->LimAbs = Vec_IntSize(p->vAbs);
1136  p->LimPpi = Vec_IntSize(p->vValues);
1137  // set runtime limit
1138  if ( p->pPars->nTimeOut )
1139  sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + p->timeStart );
1140  // clean the hash table
1141  memset( p->pTable, 0, 6 * sizeof(int) * p->nTable );
1142 }
1143 
1144 
1145 /**Function*************************************************************
1146 
1147  Synopsis []
1148 
1149  Description []
1150 
1151  SideEffects []
1152 
1153  SeeAlso []
1154 
1155 ***********************************************************************/
1156 static inline int Ga2_ObjSatValue( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
1157 {
1158  int Lit = Ga2_ObjFindLit( p, pObj, f );
1159  assert( !Gia_ObjIsConst0(pObj) );
1160  if ( Lit == -1 )
1161  return 0;
1162  if ( Abc_Lit2Var(Lit) >= p->pSat->size )
1163  return 0;
1164  return Abc_LitIsCompl(Lit) ^ sat_solver2_var_value( p->pSat, Abc_Lit2Var(Lit) );
1165 }
1166 Abc_Cex_t * Ga2_ManDeriveCex( Ga2_Man_t * p, Vec_Int_t * vPis )
1167 {
1168  Abc_Cex_t * pCex;
1169  Gia_Obj_t * pObj;
1170  int i, f;
1171  pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
1172  pCex->iPo = 0;
1173  pCex->iFrame = p->pPars->iFrame;
1174  Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
1175  {
1176  if ( !Gia_ObjIsPi(p->pGia, pObj) )
1177  continue;
1178  assert( Gia_ObjIsPi(p->pGia, pObj) );
1179  for ( f = 0; f <= pCex->iFrame; f++ )
1180  if ( Ga2_ObjSatValue( p, pObj, f ) )
1181  Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Gia_ObjCioId(pObj) );
1182  }
1183  return pCex;
1184 }
1185 void Ga2_ManRefinePrint( Ga2_Man_t * p, Vec_Int_t * vVec )
1186 {
1187  Gia_Obj_t * pObj, * pFanin;
1188  int i, k;
1189  printf( "\n Unsat core: \n" );
1190  Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
1191  {
1192  Vec_Int_t * vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
1193  printf( "%12d : ", i );
1194  printf( "Obj =%6d ", Gia_ObjId(p->pGia, pObj) );
1195  if ( Gia_ObjIsRo(p->pGia, pObj) )
1196  printf( "ff " );
1197  else
1198  printf( " " );
1199  if ( Ga2_ObjIsAbs0(p, pObj) )
1200  printf( "a " );
1201  else if ( Ga2_ObjIsLeaf0(p, pObj) )
1202  printf( "l " );
1203  else
1204  printf( " " );
1205  printf( "Fanins: " );
1206  Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
1207  {
1208  printf( "%6d ", Gia_ObjId(p->pGia, pFanin) );
1209  if ( Gia_ObjIsRo(p->pGia, pFanin) )
1210  printf( "ff " );
1211  else
1212  printf( " " );
1213  if ( Ga2_ObjIsAbs0(p, pFanin) )
1214  printf( "a " );
1215  else if ( Ga2_ObjIsLeaf0(p, pFanin) )
1216  printf( "l " );
1217  else
1218  printf( " " );
1219  }
1220  printf( "\n" );
1221  }
1222 }
1223 void Ga2_ManRefinePrintPPis( Ga2_Man_t * p )
1224 {
1225  Vec_Int_t * vVec = Vec_IntAlloc( 100 );
1226  Gia_Obj_t * pObj;
1227  int i;
1228  Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
1229  {
1230  if ( !i ) continue;
1231  if ( Ga2_ObjIsAbs(p, pObj) )
1232  continue;
1233  assert( pObj->fPhase );
1234  assert( Ga2_ObjIsLeaf(p, pObj) );
1235  assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj) );
1236  Vec_IntPush( vVec, Gia_ObjId(p->pGia, pObj) );
1237  }
1238  printf( " Current PPIs (%d): ", Vec_IntSize(vVec) );
1239  Vec_IntSort( vVec, 1 );
1240  Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
1241  printf( "%d ", Gia_ObjId(p->pGia, pObj) );
1242  printf( "\n" );
1243  Vec_IntFree( vVec );
1244 }
1245 
1246 
1247 void Ga2_GlaPrepareCexAndMap( Ga2_Man_t * p, Abc_Cex_t ** ppCex, Vec_Int_t ** pvMaps )
1248 {
1249  Abc_Cex_t * pCex;
1250  Vec_Int_t * vMap;
1251  Gia_Obj_t * pObj;
1252  int f, i, k;
1253 /*
1254  Gia_ManForEachObj( p->pGia, pObj, i )
1255  if ( Ga2_ObjId(p, pObj) >= 0 )
1256  assert( Vec_IntEntry(p->vValues, Ga2_ObjId(p, pObj)) == i );
1257 */
1258  // find PIs and PPIs
1259  vMap = Vec_IntAlloc( 1000 );
1260  Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
1261  {
1262  if ( !i ) continue;
1263  if ( Ga2_ObjIsAbs(p, pObj) )
1264  continue;
1265  assert( pObj->fPhase );
1266  assert( Ga2_ObjIsLeaf(p, pObj) );
1267  assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj) );
1268  Vec_IntPush( vMap, Gia_ObjId(p->pGia, pObj) );
1269  }
1270  // derive counter-example
1271  pCex = Abc_CexAlloc( 0, Vec_IntSize(vMap), p->pPars->iFrame+1 );
1272  pCex->iFrame = p->pPars->iFrame;
1273  for ( f = 0; f <= p->pPars->iFrame; f++ )
1274  Gia_ManForEachObjVec( vMap, p->pGia, pObj, k )
1275  if ( Ga2_ObjSatValue( p, pObj, f ) )
1276  Abc_InfoSetBit( pCex->pData, f * Vec_IntSize(vMap) + k );
1277  *pvMaps = vMap;
1278  *ppCex = pCex;
1279 }
1280 Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p )
1281 {
1282  Abc_Cex_t * pCex;
1283  Vec_Int_t * vMap, * vVec;
1284  Gia_Obj_t * pObj;
1285  int i, k;
1286  if ( p->pPars->fAddLayer )
1287  {
1288  // use simplified refinement strategy, which adds logic near at PPI without finding important ones
1289  vVec = Vec_IntAlloc( 100 );
1290  Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
1291  {
1292  if ( !i ) continue;
1293  if ( Ga2_ObjIsAbs(p, pObj) )
1294  continue;
1295  assert( pObj->fPhase );
1296  assert( Ga2_ObjIsLeaf(p, pObj) );
1297  assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj) );
1298  if ( Gia_ObjIsPi(p->pGia, pObj) )
1299  continue;
1300  Vec_IntPush( vVec, Gia_ObjId(p->pGia, pObj) );
1301  }
1302  p->nObjAdded += Vec_IntSize(vVec);
1303  return vVec;
1304  }
1305  Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap );
1306  // Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 );
1307  vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, p->pPars->fNewRefine, 1 );
1308 // printf( "Refinement %d\n", Vec_IntSize(vVec) );
1309  Abc_CexFree( pCex );
1310  if ( Vec_IntSize(vVec) == 0 )
1311  {
1312  Vec_IntFree( vVec );
1313  Abc_CexFreeP( &p->pGia->pCexSeq );
1314  p->pGia->pCexSeq = Ga2_ManDeriveCex( p, vMap );
1315  Vec_IntFree( vMap );
1316  return NULL;
1317  }
1318  Vec_IntFree( vMap );
1319  // remove those already added
1320  k = 0;
1321  Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
1322  if ( !Ga2_ObjIsAbs(p, pObj) )
1323  Vec_IntWriteEntry( vVec, k++, Gia_ObjId(p->pGia, pObj) );
1324  Vec_IntShrink( vVec, k );
1325 
1326  // these objects should be PPIs that are not abstracted yet
1327  Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
1328  assert( pObj->fPhase );//&& Ga2_ObjIsLeaf(p, pObj) );
1329  p->nObjAdded += Vec_IntSize(vVec);
1330  return vVec;
1331 }
1332 
1333 /**Function*************************************************************
1334 
1335  Synopsis [Creates a new manager.]
1336 
1337  Description []
1338 
1339  SideEffects []
1340 
1341  SeeAlso []
1342 
1343 ***********************************************************************/
1344 int Ga2_GlaAbsCount( Ga2_Man_t * p, int fRo, int fAnd )
1345 {
1346  Gia_Obj_t * pObj;
1347  int i, Counter = 0;
1348  if ( fRo )
1349  Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
1350  Counter += Gia_ObjIsRo(p->pGia, pObj);
1351  else if ( fAnd )
1352  Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
1353  Counter += Gia_ObjIsAnd(pObj);
1354  else assert( 0 );
1355  return Counter;
1356 }
1357 
1358 /**Function*************************************************************
1359 
1360  Synopsis []
1361 
1362  Description []
1363 
1364  SideEffects []
1365 
1366  SeeAlso []
1367 
1368 ***********************************************************************/
1369 void Ga2_ManAbsPrintFrame( Ga2_Man_t * p, int nFrames, int nConfls, int nCexes, abctime Time, int fFinal )
1370 {
1371  int fUseNewLine = ((fFinal && nCexes) || p->pPars->fVeryVerbose);
1372  if ( Abc_FrameIsBatchMode() && !fUseNewLine )
1373  return;
1374  p->fUseNewLine = fUseNewLine;
1375  Abc_Print( 1, "%4d :", nFrames );
1376  Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * Vec_IntSize(p->vAbs) / p->nMarked) );
1377  Abc_Print( 1, "%6d", Vec_IntSize(p->vAbs) );
1378  Abc_Print( 1, "%5d", Vec_IntSize(p->vValues)-Vec_IntSize(p->vAbs)-1 );
1379  Abc_Print( 1, "%5d", Ga2_GlaAbsCount(p, 1, 0) );
1380  Abc_Print( 1, "%6d", Ga2_GlaAbsCount(p, 0, 1) );
1381  Abc_Print( 1, "%8d", nConfls );
1382  if ( nCexes == 0 )
1383  Abc_Print( 1, "%5c", '-' );
1384  else
1385  Abc_Print( 1, "%5d", nCexes );
1386  Abc_PrintInt( sat_solver2_nvars(p->pSat) );
1387  Abc_PrintInt( sat_solver2_nclauses(p->pSat) );
1388  Abc_PrintInt( sat_solver2_nlearnts(p->pSat) );
1389  Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
1390  Abc_Print( 1, "%5.0f MB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<20) );
1391  Abc_Print( 1, "%s", fUseNewLine ? "\n" : "\r" );
1392  fflush( stdout );
1393 }
1394 
1395 /**Function*************************************************************
1396 
1397  Synopsis [Send abstracted model or send cancel.]
1398 
1399  Description [Counter-example will be sent automatically when &vta terminates.]
1400 
1401  SideEffects []
1402 
1403  SeeAlso []
1404 
1405 ***********************************************************************/
1406 char * Ga2_GlaGetFileName( Ga2_Man_t * p, int fAbs )
1407 {
1408  static char * pFileNameDef = "glabs.aig";
1409  if ( p->pPars->pFileVabs )
1410  return p->pPars->pFileVabs;
1411  if ( p->pGia->pSpec )
1412  {
1413  if ( fAbs )
1414  return Extra_FileNameGenericAppend( p->pGia->pSpec, "_abs.aig");
1415  else
1416  return Extra_FileNameGenericAppend( p->pGia->pSpec, "_gla.aig");
1417  }
1418  return pFileNameDef;
1419 }
1420 
1421 void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
1422 {
1423  char * pFileName;
1424  assert( p->pPars->fDumpMabs || p->pPars->fDumpVabs );
1425  if ( p->pPars->fDumpMabs )
1426  {
1427  pFileName = Ga2_GlaGetFileName(p, 0);
1428  if ( fVerbose )
1429  Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName );
1430  // dump abstraction map
1431  Vec_IntFreeP( &p->pGia->vGateClasses );
1432  p->pGia->vGateClasses = Ga2_ManAbsTranslate( p );
1433  Gia_AigerWrite( p->pGia, pFileName, 0, 0 );
1434  }
1435  else if ( p->pPars->fDumpVabs )
1436  {
1437  Vec_Int_t * vGateClasses;
1438  Gia_Man_t * pAbs;
1439  pFileName = Ga2_GlaGetFileName(p, 1);
1440  if ( fVerbose )
1441  Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
1442  // dump absracted model
1443  vGateClasses = Ga2_ManAbsTranslate( p );
1444  pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
1445  Gia_ManCleanValue( p->pGia );
1446  Gia_AigerWrite( pAbs, pFileName, 0, 0 );
1447  Gia_ManStop( pAbs );
1448  Vec_IntFreeP( &vGateClasses );
1449  }
1450  else assert( 0 );
1451 }
1452 
1453 /**Function*************************************************************
1454 
1455  Synopsis [Send abstracted model or send cancel.]
1456 
1457  Description [Counter-example will be sent automatically when &vta terminates.]
1458 
1459  SideEffects []
1460 
1461  SeeAlso []
1462 
1463 ***********************************************************************/
1464 void Gia_Ga2SendAbsracted( Ga2_Man_t * p, int fVerbose )
1465 {
1466  Gia_Man_t * pAbs;
1467  Vec_Int_t * vGateClasses;
1468  assert( Abc_FrameIsBridgeMode() );
1469 // if ( fVerbose )
1470 // Abc_Print( 1, "Sending abstracted model...\n" );
1471  // create abstraction (value of p->pGia is not used here)
1472  vGateClasses = Ga2_ManAbsTranslate( p );
1473  pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
1474  Vec_IntFreeP( &vGateClasses );
1475  Gia_ManCleanValue( p->pGia );
1476  // send it out
1477  Gia_ManToBridgeAbsNetlist( stdout, pAbs, BRIDGE_ABS_NETLIST );
1478  Gia_ManStop( pAbs );
1479 }
1480 void Gia_Ga2SendCancel( Ga2_Man_t * p, int fVerbose )
1481 {
1482  extern int Gia_ManToBridgeBadAbs( FILE * pFile );
1483  assert( Abc_FrameIsBridgeMode() );
1484 // if ( fVerbose )
1485 // Abc_Print( 1, "Cancelling previously sent model...\n" );
1486  Gia_ManToBridgeBadAbs( stdout );
1487 }
1488 
1489 /**Function*************************************************************
1490 
1491  Synopsis [Performs gate-level abstraction.]
1492 
1493  Description []
1494 
1495  SideEffects []
1496 
1497  SeeAlso []
1498 
1499 ***********************************************************************/
1500 int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
1501 {
1502  int fUseSecondCore = 1;
1503  Ga2_Man_t * p;
1504  Vec_Int_t * vCore, * vPPis;
1505  abctime clk2, clk = Abc_Clock();
1506  int Status = l_Undef, RetValue = -1, iFrameTryToProve = -1, fOneIsSent = 0;
1507  int i, c, f, Lit;
1508  pPars->iFrame = -1;
1509  // check trivial case
1510  assert( Gia_ManPoNum(pAig) == 1 );
1511  ABC_FREE( pAig->pCexSeq );
1512  if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) )
1513  {
1514  if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) )
1515  {
1516  Abc_Print( 1, "Sequential miter is trivially UNSAT.\n" );
1517  return 1;
1518  }
1519  pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 );
1520  Abc_Print( 1, "Sequential miter is trivially SAT.\n" );
1521  return 0;
1522  }
1523  // create gate classes if not given
1524  if ( pAig->vGateClasses == NULL )
1525  {
1526  pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
1527  Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
1528  Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)), 1 );
1529  }
1530  // start the manager
1531  p = Ga2_ManStart( pAig, pPars );
1532  p->timeInit = Abc_Clock() - clk;
1533  // perform initial abstraction
1534  if ( p->pPars->fVerbose )
1535  {
1536  Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" );
1537  Abc_Print( 1, "FrameMax = %d ConfMax = %d Timeout = %d Limit = %d %% Limit2 = %d %% RatioMax = %d %%\n",
1538  pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin, pPars->nRatioMin2, pPars->nRatioMax );
1539  Abc_Print( 1, "LrnStart = %d LrnDelta = %d LrnRatio = %d %% Skip = %d SimpleCNF = %d Dump = %d\n",
1540  pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs );
1541  if ( pPars->fDumpVabs || pPars->fDumpMabs )
1542  Abc_Print( 1, "%s will be dumped into file \"%s\".\n",
1543  pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map",
1544  Ga2_GlaGetFileName(p, pPars->fDumpVabs) );
1545  Abc_Print( 1, " Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" );
1546  }
1547  // iterate unrolling
1548  for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ )
1549  {
1550  int nAbsOld;
1551  // remember the timeframe
1552  p->pPars->iFrame = -1;
1553  // create new SAT solver
1554  Ga2_ManRestart( p );
1555  // remember abstraction size after the last restart
1556  nAbsOld = Vec_IntSize(p->vAbs);
1557  // unroll the circuit
1558  for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ )
1559  {
1560  // remember current limits
1561  int nConflsBeg = sat_solver2_nconflicts(p->pSat);
1562  int nAbs = Vec_IntSize(p->vAbs);
1563  int nValues = Vec_IntSize(p->vValues);
1564  int nVarsOld;
1565  // remember the timeframe
1566  p->pPars->iFrame = f;
1567  // extend and clear storage
1568  if ( f == Vec_PtrSize(p->vId2Lit) )
1569  Vec_PtrPush( p->vId2Lit, Vec_IntAlloc(0) );
1570  Vec_IntFillExtra( Ga2_MapFrameMap(p, f), Vec_IntSize(p->vValues), -1 );
1571  // add static clauses to this timeframe
1572  Ga2_ManAddAbsClauses( p, f );
1573  // skip checking if skipcheck is enabled (&gla -s)
1574  if ( p->pPars->fUseSkip && f <= p->pPars->iFrameProved )
1575  continue;
1576  // skip checking if we need to skip several starting frames (&gla -S <num>)
1577  if ( p->pPars->nFramesStart && f <= p->pPars->nFramesStart )
1578  continue;
1579  // get the output literal
1580 // Lit = Ga2_ManUnroll_rec( p, Gia_ManPo(pAig,0), f );
1581  Lit = Ga2_ObjFindLit( p, Gia_ObjFanin0(Gia_ManPo(pAig,0)), f );
1582  assert( Lit >= 0 );
1583  Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(Gia_ManPo(pAig,0)) );
1584  if ( Lit == 0 )
1585  continue;
1586  assert( Lit > 1 );
1587  // check for counter-examples
1588  if ( p->nSatVars > sat_solver2_nvars(p->pSat) )
1589  sat_solver2_setnvars( p->pSat, p->nSatVars );
1590  nVarsOld = p->nSatVars;
1591  for ( c = 0; ; c++ )
1592  {
1593  // consider the special case when the target literal is implied false
1594  // by implications which happened as a result of previous refinements
1595  // note that incremental UNSAT core cannot be computed because there is no learned clauses
1596  // in this case, we will assume that UNSAT core cannot reduce the problem
1597  if ( var_is_assigned(p->pSat, Abc_Lit2Var(Lit)) )
1598  {
1599  Prf_ManStopP( &p->pSat->pPrf2 );
1600  break;
1601  }
1602  // perform SAT solving
1603  clk2 = Abc_Clock();
1604  Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1605  if ( Status == l_True ) // perform refinement
1606  {
1607  p->nCexes++;
1608  p->timeSat += Abc_Clock() - clk2;
1609 
1610  // cancel old one if it was sent
1611  if ( Abc_FrameIsBridgeMode() && fOneIsSent )
1612  {
1613  Gia_Ga2SendCancel( p, pPars->fVerbose );
1614  fOneIsSent = 0;
1615  }
1616  if ( iFrameTryToProve >= 0 )
1617  {
1618  Gia_GlaProveCancel( pPars->fVerbose );
1619  iFrameTryToProve = -1;
1620  }
1621 
1622  // perform refinement
1623  clk2 = Abc_Clock();
1624  Rnm_ManSetRefId( p->pRnm, c );
1625  vPPis = Ga2_ManRefine( p );
1626  p->timeCex += Abc_Clock() - clk2;
1627  if ( vPPis == NULL )
1628  {
1629  if ( pPars->fVerbose )
1630  Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, Abc_Clock() - clk, 1 );
1631  goto finish;
1632  }
1633 
1634  if ( c == 0 )
1635  {
1636 // Ga2_ManRefinePrintPPis( p );
1637  // create bookmark to be used for rollback
1638  assert( nVarsOld == p->pSat->size );
1639  sat_solver2_bookmark( p->pSat );
1640  // start incremental proof manager
1641  assert( p->pSat->pPrf2 == NULL );
1642  p->pSat->pPrf2 = Prf_ManAlloc();
1643  if ( p->pSat->pPrf2 )
1644  {
1645  p->nProofIds = 0;
1646  Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
1647  Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vPPis) );
1648  }
1649  }
1650  else
1651  {
1652  // resize the proof logger
1653  if ( p->pSat->pPrf2 )
1654  Prf_ManGrow( p->pSat->pPrf2, p->nProofIds + Vec_IntSize(vPPis) );
1655  }
1656 
1657  Ga2_ManAddToAbs( p, vPPis );
1658  Vec_IntFree( vPPis );
1659  if ( pPars->fVerbose )
1660  Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c+1, Abc_Clock() - clk, 0 );
1661  // check if the number of objects is below limit
1662  if ( pPars->nRatioMin2 && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin2 / 100 )
1663  {
1664  Status = l_Undef;
1665  goto finish;
1666  }
1667  continue;
1668  }
1669  p->timeUnsat += Abc_Clock() - clk2;
1670  if ( Status == l_Undef ) // ran out of resources
1671  goto finish;
1672  if ( p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit ) // timeout
1673  goto finish;
1674  if ( c == 0 )
1675  {
1676  if ( f > p->pPars->iFrameProved )
1677  p->pPars->nFramesNoChange++;
1678  break;
1679  }
1680  if ( f > p->pPars->iFrameProved )
1681  p->pPars->nFramesNoChange = 0;
1682 
1683  // derive the core
1684  assert( p->pSat->pPrf2 != NULL );
1685  vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat );
1686  Prf_ManStopP( &p->pSat->pPrf2 );
1687  // update the SAT solver
1688  sat_solver2_rollback( p->pSat );
1689  // reduce abstraction
1690  Ga2_ManShrinkAbs( p, nAbs, nValues, nVarsOld );
1691 
1692  // purify UNSAT core
1693  if ( fUseSecondCore )
1694  {
1695 // int nOldCore = Vec_IntSize(vCore);
1696  // reverse the order of objects in the core
1697 // Vec_IntSort( vCore, 0 );
1698 // Vec_IntPrint( vCore );
1699  // create bookmark to be used for rollback
1700  assert( nVarsOld == p->pSat->size );
1701  sat_solver2_bookmark( p->pSat );
1702  // start incremental proof manager
1703  assert( p->pSat->pPrf2 == NULL );
1704  p->pSat->pPrf2 = Prf_ManAlloc();
1705  if ( p->pSat->pPrf2 )
1706  {
1707  p->nProofIds = 0;
1708  Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
1709  Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vCore) );
1710 
1711  Ga2_ManAddToAbs( p, vCore );
1712  Vec_IntFree( vCore );
1713  }
1714  // run SAT solver
1715  clk2 = Abc_Clock();
1716  Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1717  if ( Status == l_Undef )
1718  goto finish;
1719  assert( Status == l_False );
1720  p->timeUnsat += Abc_Clock() - clk2;
1721 
1722  // derive the core
1723  assert( p->pSat->pPrf2 != NULL );
1724  vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat );
1725  Prf_ManStopP( &p->pSat->pPrf2 );
1726  // update the SAT solver
1727  sat_solver2_rollback( p->pSat );
1728  // reduce abstraction
1729  Ga2_ManShrinkAbs( p, nAbs, nValues, nVarsOld );
1730 // printf( "\n%4d -> %4d\n", nOldCore, Vec_IntSize(vCore) );
1731  }
1732 
1733  Ga2_ManAddToAbs( p, vCore );
1734 // Ga2_ManRefinePrint( p, vCore );
1735  Vec_IntFree( vCore );
1736  break;
1737  }
1738  // remember the last proved frame
1739  if ( p->pPars->iFrameProved < f )
1740  p->pPars->iFrameProved = f;
1741  // print statistics
1742  if ( pPars->fVerbose )
1743  Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, Abc_Clock() - clk, 1 );
1744  // check if abstraction was proved
1745  if ( Gia_GlaProveCheck( pPars->fVerbose ) )
1746  {
1747  RetValue = 1;
1748  goto finish;
1749  }
1750  if ( c > 0 )
1751  {
1752  if ( p->pPars->fVeryVerbose )
1753  Abc_Print( 1, "\n" );
1754  // recompute the abstraction
1755  Vec_IntFreeP( &pAig->vGateClasses );
1756  pAig->vGateClasses = Ga2_ManAbsTranslate( p );
1757  // check if the number of objects is below limit
1758  if ( pPars->nRatioMin && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin / 100 )
1759  {
1760  Status = l_Undef;
1761  goto finish;
1762  }
1763  }
1764  // check the number of stable frames
1765  if ( p->pPars->nFramesNoChange == p->pPars->nFramesNoChangeLim )
1766  {
1767  // dump the model into file
1768  if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs )
1769  {
1770  char Command[1000];
1771  Abc_FrameSetStatus( -1 );
1772  Abc_FrameSetCex( NULL );
1773  Abc_FrameSetNFrames( f );
1774  sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status"));
1775  Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
1776  Ga2_GlaDumpAbsracted( p, pPars->fVerbose );
1777  }
1778  // call the prover
1779  if ( p->pPars->fCallProver )
1780  {
1781  // cancel old one if it is proving
1782  if ( iFrameTryToProve >= 0 )
1783  Gia_GlaProveCancel( pPars->fVerbose );
1784  // prove new one
1785  Gia_GlaProveAbsracted( pAig, pPars->fSimpProver, pPars->fVeryVerbose );
1786  iFrameTryToProve = f;
1787  p->nPdrCalls++;
1788  }
1789  // speak to the bridge
1790  if ( Abc_FrameIsBridgeMode() )
1791  {
1792  // cancel old one if it was sent
1793  if ( fOneIsSent )
1794  Gia_Ga2SendCancel( p, pPars->fVerbose );
1795  // send new one
1796  Gia_Ga2SendAbsracted( p, pPars->fVerbose );
1797  fOneIsSent = 1;
1798  }
1799  }
1800  // if abstraction grew more than a certain percentage, force a restart
1801  if ( pPars->nRatioMax == 0 )
1802  continue;
1803  if ( c > 0 && (f > 20 || Vec_IntSize(p->vAbs) > 100) && Vec_IntSize(p->vAbs) - nAbsOld >= nAbsOld * pPars->nRatioMax / 100 )
1804  {
1805  if ( p->pPars->fVerbose )
1806  Abc_Print( 1, "Forcing restart because abstraction grew from %d to %d (more than %d %%).\n",
1807  nAbsOld, Vec_IntSize(p->vAbs), pPars->nRatioMax );
1808  break;
1809  }
1810  }
1811  }
1812 finish:
1813  Prf_ManStopP( &p->pSat->pPrf2 );
1814  // cancel old one if it is proving
1815  if ( iFrameTryToProve >= 0 )
1816  Gia_GlaProveCancel( pPars->fVerbose );
1817  // analize the results
1818  if ( !p->fUseNewLine )
1819  Abc_Print( 1, "\n" );
1820  if ( RetValue == 1 )
1821  Abc_Print( 1, "GLA completed %d frames and proved abstraction derived in frame %d ", p->pPars->iFrameProved+1, iFrameTryToProve );
1822  else if ( pAig->pCexSeq == NULL )
1823  {
1824  Vec_IntFreeP( &pAig->vGateClasses );
1825  pAig->vGateClasses = Ga2_ManAbsTranslate( p );
1826  if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit )
1827  Abc_Print( 1, "GLA reached timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
1828  else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
1829  Abc_Print( 1, "GLA exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
1830  else if ( pPars->nRatioMin2 && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin2 / 100 )
1831  Abc_Print( 1, "GLA found that the size of abstraction exceeds %d %% in frame %d during refinement. ", pPars->nRatioMin2, p->pPars->iFrameProved+1 );
1832  else if ( pPars->nRatioMin && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin / 100 )
1833  Abc_Print( 1, "GLA found that the size of abstraction exceeds %d %% in frame %d. ", pPars->nRatioMin, p->pPars->iFrameProved+1 );
1834  else
1835  Abc_Print( 1, "GLA finished %d frames and produced a %d-stable abstraction. ", p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
1836  p->pPars->iFrame = p->pPars->iFrameProved;
1837  }
1838  else
1839  {
1840  if ( p->pPars->fVerbose )
1841  Abc_Print( 1, "\n" );
1842  if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
1843  Abc_Print( 1, " Gia_ManPerformGlaOld(): CEX verification has failed!\n" );
1844  Abc_Print( 1, "True counter-example detected in frame %d. ", f );
1845  p->pPars->iFrame = f - 1;
1846  Vec_IntFreeP( &pAig->vGateClasses );
1847  RetValue = 0;
1848  }
1849  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1850  if ( p->pPars->fVerbose )
1851  {
1852  p->timeOther = (Abc_Clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit;
1853  ABC_PRTP( "Runtime: Initializing", p->timeInit, Abc_Clock() - clk );
1854  ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, Abc_Clock() - clk );
1855  ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, Abc_Clock() - clk );
1856  ABC_PRTP( "Runtime: Refinement ", p->timeCex, Abc_Clock() - clk );
1857  ABC_PRTP( "Runtime: Other ", p->timeOther, Abc_Clock() - clk );
1858  ABC_PRTP( "Runtime: TOTAL ", Abc_Clock() - clk, Abc_Clock() - clk );
1859  Ga2_ManReportMemory( p );
1860  }
1861 // Ga2_ManDumpStats( p->pGia, p->pPars, p->pSat, p->pPars->iFrameProved, 0 );
1862  Ga2_ManStop( p );
1863  fflush( stdout );
1864  return RetValue;
1865 }
1866 
1867 ////////////////////////////////////////////////////////////////////////
1868 /// END OF FILE ///
1869 ////////////////////////////////////////////////////////////////////////
1870 
1871 
1872 ABC_NAMESPACE_IMPL_END
1873 
Rnm_ManMemoryUsage
double Rnm_ManMemoryUsage(Rnm_Man_t *p)
Definition: absRef.c:317
Gia_Man_t_::nObjsAlloc
int nObjsAlloc
Definition: gia.h:102
memset
char * memset()
Gia_ManPerformGla
int Gia_ManPerformGla(Gia_Man_t *pAig, Abs_Par_t *pPars)
Definition: absGla.c:1500
sat_solver2_nlearnts
static int sat_solver2_nlearnts(sat_solver2 *s)
Definition: satSolver2.h:200
Ga2_ObjTruth
static unsigned Ga2_ObjTruth(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: abs.h:115
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Ga2_Man_t_::nHashOver
int nHashOver
Definition: absGla.c:70
Abc_FrameIsBridgeMode
ABC_DLL int Abc_FrameIsBridgeMode()
Definition: mainFrame.c:94
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Abc_PrimeCudd
static int Abc_PrimeCudd(unsigned int p)
Definition: abc_global.h:383
Ga2_ManShrinkAbs
void Ga2_ManShrinkAbs(Ga2_Man_t *p, int nAbs, int nValues, int nSatVars)
Definition: absGla.c:1009
Gia_GlaCountFlops
int Gia_GlaCountFlops(Gia_Man_t *p, Vec_Int_t *vGla)
Definition: absUtil.c:231
sat_solver2_t::nLearntMax
int nLearntMax
Definition: satSolver2.h:118
sat_solver2_t::nLearntStart
int nLearntStart
Definition: satSolver2.h:119
Ga2_Man_t_::vLits
Vec_Int_t * vLits
Definition: absGla.c:72
Ga2_Man_t_::nPdrCalls
int nPdrCalls
Definition: absGla.c:64
sat_solver2_t::size
int size
Definition: satSolver2.h:92
Ga2_ObjId
static int Ga2_ObjId(Ga2_Man_t *p, Gia_Obj_t *pObj)
Definition: absGla.c:84
Ga2_Man_t_::timeCex
abctime timeCex
Definition: absGla.c:80
Gia_GlaProveAbsracted
void Gia_GlaProveAbsracted(Gia_Man_t *p, int fSimpProver, int fVerbose)
DECLARATIONS ///.
Definition: absPth.c:45
Ga2_ManRefinePrint
void Ga2_ManRefinePrint(Ga2_Man_t *p, Vec_Int_t *vVec)
Definition: absGla.c:1185
Ga2_Man_t_::timeSat
abctime timeSat
Definition: absGla.c:78
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Ga2_Man_t_::vCnfs
Vec_Ptr_t * vCnfs
Definition: absGla.c:44
Ga2_ManRefinePrintPPis
void Ga2_ManRefinePrintPPis(Ga2_Man_t *p)
Definition: absGla.c:1223
Vec_IntMemory
static double Vec_IntMemory(Vec_Int_t *p)
Definition: vecInt.h:384
sat_solver2_nclauses
static int sat_solver2_nclauses(sat_solver2 *s)
Definition: satSolver2.h:195
Vec_IntDup
static Vec_Int_t * Vec_IntDup(Vec_Int_t *pVec)
Definition: vecInt.h:214
Gia_ManVerifyCex
int Gia_ManVerifyCex(Gia_Man_t *pAig, Abc_Cex_t *p, int fDualOut)
DECLARATIONS ///.
Definition: giaCex.c:44
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
Gia_GlaProveCancel
void Gia_GlaProveCancel(int fVerbose)
Definition: absPth.c:46
Sat_ProofCore
void * Sat_ProofCore(sat_solver2 *s)
Definition: satSolver2.c:1985
Ga2_ObjLeaveNum
static int Ga2_ObjLeaveNum(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: abs.h:113
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
Ga2_ManAddToAbs
void Ga2_ManAddToAbs(Ga2_Man_t *p, Vec_Int_t *vToAdd)
Definition: absGla.c:979
Vec_VecMemoryInt
static double Vec_VecMemoryInt(Vec_Vec_t *p)
Definition: vecVec.h:304
Ga2_MapFrameMap
static Vec_Int_t * Ga2_MapFrameMap(Ga2_Man_t *p, int f)
Definition: absGla.c:95
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_IntFillExtra
static void Vec_IntFillExtra(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:376
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Ga2_ObjIsAbs0
static int Ga2_ObjIsAbs0(Ga2_Man_t *p, Gia_Obj_t *pObj)
Definition: absGla.c:90
Cmd_CommandExecute
int Cmd_CommandExecute(void *pAbc, char *pCommandLine)
Ga2_Man_t_::vValues
Vec_Int_t * vValues
Definition: absGla.c:49
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
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
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_Man_t_::fUseNewLine
int fUseNewLine
Definition: absGla.c:54
Ga2_ManDumpStats
void Ga2_ManDumpStats(Gia_Man_t *pGia, Abs_Par_t *pPars, sat_solver2 *pSat, int iFrame, int fUseN)
Definition: absGla.c:410
sat_solver2_t
Definition: satSolver2.h:90
Ga2_ManAbsDerive
Vec_Int_t * Ga2_ManAbsDerive(Gia_Man_t *p)
Definition: absGla.c:1097
Rnm_Man_t_
Definition: absRef.h:56
Ga2_ObjSetId
static void Ga2_ObjSetId(Ga2_Man_t *p, Gia_Obj_t *pObj, int i)
Definition: absGla.c:85
Gia_ManCleanValue
void Gia_ManCleanValue(Gia_Man_t *p)
Definition: giaUtil.c:310
Ga2_Man_t_::vProofIds
Vec_Int_t * vProofIds
Definition: absGla.c:47
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
Ga2_ManSetupNode
static void Ga2_ManSetupNode(Ga2_Man_t *p, Gia_Obj_t *pObj, int fAbs)
Definition: absGla.c:764
sat_solver2_t::nLearntDelta
int nLearntDelta
Definition: satSolver2.h:120
Ga2_ManDeriveCex
Abc_Cex_t * Ga2_ManDeriveCex(Ga2_Man_t *p, Vec_Int_t *vPis)
Definition: absGla.c:1166
Ga2_ManCnfAddStatic
void Ga2_ManCnfAddStatic(sat_solver2 *pSat, Vec_Int_t *vCnf0, Vec_Int_t *vCnf1, int Lits[], int iLitOut, int ProofId)
Definition: absGla.c:684
memcpy
char * memcpy()
Gia_ManToBridgeBadAbs
int Gia_ManToBridgeBadAbs(FILE *pFile)
Definition: utilBridge.c:199
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
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
sat_solver2_new
sat_solver2 * sat_solver2_new(void)
Definition: satSolver2.c:1109
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
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Vec_VecFree
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
Vec_IntSort
static void Vec_IntSort(Vec_Int_t *p, int fReverse)
Definition: vecInt.h:1293
Vec_IntStartFull
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
Ga2_Man_t_::nCexes
int nCexes
Definition: absGla.c:62
Ga2_ManCnfCompute
Vec_Int_t * Ga2_ManCnfCompute(unsigned uTruth, int nVars, Vec_Int_t *vCover)
Definition: absGla.c:630
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Ga2_ObjCnf1
static Vec_Int_t * Ga2_ObjCnf1(Ga2_Man_t *p, Gia_Obj_t *pObj)
Definition: absGla.c:88
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
sat_solver2_var_value
static int sat_solver2_var_value(sat_solver2 *s, int v)
Definition: satSolver2.h:210
var_is_assigned
int var_is_assigned(sat_solver2 *s, int v)
Definition: satSolver2.c:83
Gia_Obj_t_
Definition: gia.h:75
sat_solver2_setnvars
void sat_solver2_setnvars(sat_solver2 *s, int n)
Definition: satSolver2.c:1170
Rnm_ManSetRefId
static void Rnm_ManSetRefId(Rnm_Man_t *p, int RefId)
Definition: absRef.h:100
Ga2_ManCnfAddDynamic
static void Ga2_ManCnfAddDynamic(Ga2_Man_t *p, int uTruth, int Lits[], int iLitOut, int ProofId)
Definition: absGla.c:652
Ga2_ObjSatValue
static int Ga2_ObjSatValue(Ga2_Man_t *p, Gia_Obj_t *pObj, int f)
Definition: absGla.c:1156
Abc_CexMakeTriv
Abc_Cex_t * Abc_CexMakeTriv(int nRegs, int nTruePis, int nTruePos, int iFrameOut)
Definition: utilCex.c:85
Ga2_ManReportMemory
void Ga2_ManReportMemory(Ga2_Man_t *p)
Definition: absGla.c:432
Ga2_Man_t_
Definition: absGla.c:38
Ga2_Man_t_::timeInit
abctime timeInit
Definition: absGla.c:77
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
Ga2_ObjIsLeaf0
static int Ga2_ObjIsLeaf0(Ga2_Man_t *p, Gia_Obj_t *pObj)
Definition: absGla.c:91
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
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
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Ga2_Man_t_::nObjAdded
int nObjAdded
Definition: absGla.c:63
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
s_Primes
static int s_Primes[MAX_PRIMES]
Definition: fxuPair.c:30
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Cnf_ReadMsops
void Cnf_ReadMsops(char **ppSopSizes, char ***ppSops)
FUNCTION DEFINITIONS ///.
Definition: cnfData.c:4537
Ga2_ManAbsPrintFrame
void Ga2_ManAbsPrintFrame(Ga2_Man_t *p, int nFrames, int nConfls, int nCexes, abctime Time, int fFinal)
Definition: absGla.c:1369
Ga2_ManStart
Ga2_Man_t * Ga2_ManStart(Gia_Man_t *pGia, Abs_Par_t *pPars)
Definition: absGla.c:372
Ga2_ManCollectNodes_rec
void Ga2_ManCollectNodes_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vNodes, int fFirst)
Definition: absGla.c:222
Gia_ManPi
static Gia_Obj_t * Gia_ManPi(Gia_Man_t *p, int v)
Definition: gia.h:405
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
Ga2_ManCollectLeaves_rec
void Ga2_ManCollectLeaves_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vLeaves, int fFirst)
Definition: absGla.c:232
Ga2_Man_t_::pRnm
Rnm_Man_t * pRnm
Definition: absGla.c:56
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
Kit_TruthIsop
int Kit_TruthIsop(unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
FUNCTION DEFINITIONS ///.
Definition: kitIsop.c:55
sat_solver2_rollback
void sat_solver2_rollback(sat_solver2 *s)
Definition: satSolver2.c:1586
Ga2_Man_t_::vId2Lit
Vec_Ptr_t * vId2Lit
Definition: absGla.c:59
Ga2_ObjIsLeaf
static int Ga2_ObjIsLeaf(Ga2_Man_t *p, Gia_Obj_t *pObj)
Definition: absGla.c:93
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
Ga2_ManComputeTest
void Ga2_ManComputeTest(Gia_Man_t *p)
Definition: absGla.c:338
Ga2_Man_t_::nSatVars
int nSatVars
Definition: absGla.c:61
Gia_Man_t_::vGateClasses
Vec_Int_t * vGateClasses
Definition: gia.h:141
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
Ga2_Man_t_::pPars
Abs_Par_t * pPars
Definition: absGla.c:42
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
Ga2_Man_t_::pGia
Gia_Man_t * pGia
Definition: absGla.c:41
Ga2_Man_t_::nHashHit
int nHashHit
Definition: absGla.c:68
Vec_IntSelectSortCost
static void Vec_IntSelectSortCost(int *pArray, int nSize, Vec_Int_t *vCosts)
Definition: vecInt.h:1766
Abc_CexFreeP
void Abc_CexFreeP(Abc_Cex_t **p)
Definition: utilCex.c:350
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
Gia_Man_t_::pSpec
char * pSpec
Definition: gia.h:98
memcmp
int memcmp()
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Ga2_Man_t_::vIsopMem
Vec_Int_t * vIsopMem
Definition: absGla.c:73
Ga2_ManAbsTranslate_rec
void Ga2_ManAbsTranslate_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vClasses, int fFirst)
Definition: absGla.c:1067
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
Ga2_GlaAbsCount
int Ga2_GlaAbsCount(Ga2_Man_t *p, int fRo, int fAnd)
Definition: absGla.c:1344
Gia_Ga2SendCancel
void Gia_Ga2SendCancel(Ga2_Man_t *p, int fVerbose)
Definition: absGla.c:1480
Ga2_Man_t_::nMarked
int nMarked
Definition: absGla.c:53
Gia_Ga2SendAbsracted
void Gia_Ga2SendAbsracted(Ga2_Man_t *p, int fVerbose)
Definition: absGla.c:1464
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
Ga2_ManAddAbsClauses
void Ga2_ManAddAbsClauses(Ga2_Man_t *p, int f)
Definition: absGla.c:959
sat_solver2_bookmark
static void sat_solver2_bookmark(sat_solver2 *s)
Definition: satSolver2.h:248
Ga2_ObjComputeTruthSpecial
unsigned Ga2_ObjComputeTruthSpecial(Gia_Man_t *p, Gia_Obj_t *pRoot, Vec_Int_t *vLeaves, Vec_Int_t *vLits)
Definition: absGla.c:512
Ga2_ObjFindLit
static int Ga2_ObjFindLit(Ga2_Man_t *p, Gia_Obj_t *pObj, int f)
Definition: absGla.c:98
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
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Ga2_Man_t_::timeStart
abctime timeStart
Definition: absGla.c:76
sat_solver2_t::nConfLimit
ABC_INT64_T nConfLimit
Definition: satSolver2.h:173
Ga2_Man_t_::pTable
int * pTable
Definition: absGla.c:66
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
Ga2_Man_t_::timeOther
abctime timeOther
Definition: absGla.c:81
Ga2_GlaGetFileName
char * Ga2_GlaGetFileName(Ga2_Man_t *p, int fAbs)
Definition: absGla.c:1406
Ga2_ObjFindOrAddLit
static int Ga2_ObjFindOrAddLit(Ga2_Man_t *p, Gia_Obj_t *pObj, int f)
Definition: absGla.c:112
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Gia_ObjIsMuxType
int Gia_ObjIsMuxType(Gia_Obj_t *pNode)
Definition: giaUtil.c:885
Vec_IntEntryLast
static int Vec_IntEntryLast(Vec_Int_t *p)
Definition: bblif.c:319
Ga2_GlaDumpAbsracted
void Ga2_GlaDumpAbsracted(Ga2_Man_t *p, int fVerbose)
Definition: absGla.c:1421
Abc_LitNot
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
Prf_ManRestart
static void Prf_ManRestart(Prf_Man_t *p, Vec_Int_t *vId2Pr, int iFirst, int nWidth)
Definition: satProof2.h:120
Gia_Obj_t_::fPhase
unsigned fPhase
Definition: gia.h:85
Ga2_ManMarkup
int Ga2_ManMarkup(Gia_Man_t *p, int N, int fSimple)
Definition: absGla.c:243
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Ga2_Man_t_::timeUnsat
abctime timeUnsat
Definition: absGla.c:79
Prf_ManGrow
static void Prf_ManGrow(Prf_Man_t *p, int nWidth)
Definition: satProof2.h:129
Ga2_Man_t_::pSat
sat_solver2 * pSat
Definition: absGla.c:60
Abc_FrameSetNFrames
ABC_DLL void Abc_FrameSetNFrames(int nFrames)
Definition: mainFrame.c:87
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Ga2_ObjComputeTruth_rec
unsigned Ga2_ObjComputeTruth_rec(Gia_Man_t *p, Gia_Obj_t *pObj, int fFirst)
FUNCTION DEFINITIONS ///.
Definition: absGla.c:140
Ga2_Man_t_::nProofIds
int nProofIds
Definition: absGla.c:50
Ga2_ObjLeaves
static Vec_Int_t * Ga2_ObjLeaves(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: abs.h:117
Vec_IntShrink
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
Ga2_ManAddToAbsOneStatic
static void Ga2_ManAddToAbsOneStatic(Ga2_Man_t *p, Gia_Obj_t *pObj, int f, int fUseId)
Definition: absGla.c:792
Ga2_ManAbsTranslate
Vec_Int_t * Ga2_ManAbsTranslate(Ga2_Man_t *p)
Definition: absGla.c:1077
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
ABC_PRMP
#define ABC_PRMP(a, f, F)
Definition: abc_global.h:227
GA2_BIG_NUM
#define GA2_BIG_NUM
DECLARATIONS ///.
Definition: absGla.c:35
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
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Ga2_ObjAddLit
static void Ga2_ObjAddLit(Ga2_Man_t *p, Gia_Obj_t *pObj, int f, int Lit)
Definition: absGla.c:105
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
Gia_ManToBridgeAbsNetlist
int Gia_ManToBridgeAbsNetlist(FILE *pFile, void *p, int pkg_type)
Definition: utilBridge.c:189
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
Ga2_ManBreakTree_rec
int Ga2_ManBreakTree_rec(Gia_Man_t *p, Gia_Obj_t *pObj, int fFirst, int N)
Definition: absGla.c:176
sat_solver2_t::pPrf2
Prf_Man_t * pPrf2
Definition: satSolver2.h:166
l_False
#define l_False
Definition: SolverTypes.h:85
Gia_ObjFaninId0p
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
Ga2_Man_t_::nTable
int nTable
Definition: absGla.c:67
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
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
Ga2_GlaPrepareCexAndMap
void Ga2_GlaPrepareCexAndMap(Ga2_Man_t *p, Abc_Cex_t **ppCex, Vec_Int_t **pvMaps)
Definition: absGla.c:1247
Saig_ManBmcLookup
static int * Saig_ManBmcLookup(Ga2_Man_t *p, int *pArray)
Definition: absGla.c:735
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
Prf_ManStopP
static void Prf_ManStopP(Prf_Man_t **p)
Definition: satProof2.h:99
Abc_LitRegular
static int Abc_LitRegular(int Lit)
Definition: abc_global.h:268
Ga2_ManComputeTruth
unsigned Ga2_ManComputeTruth(Gia_Man_t *p, Gia_Obj_t *pRoot, Vec_Int_t *vLeaves)
Definition: absGla.c:150
assert
#define assert(ex)
Definition: util_old.h:213
Extra_FileNameGenericAppend
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition: extraUtilFile.c:185
Ga2_ObjIsAbs
static int Ga2_ObjIsAbs(Ga2_Man_t *p, Gia_Obj_t *pObj)
Definition: absGla.c:92
Gia_ManSetPhase
void Gia_ManSetPhase(Gia_Man_t *p)
Definition: giaUtil.c:379
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
BRIDGE_ABS_NETLIST
#define BRIDGE_ABS_NETLIST
Definition: abc_global.h:295
Ga2_ManRefine
Vec_Int_t * Ga2_ManRefine(Ga2_Man_t *p)
Definition: absGla.c:1280
Ga2_ObjCnf0
static Vec_Int_t * Ga2_ObjCnf0(Ga2_Man_t *p, Gia_Obj_t *pObj)
Definition: absGla.c:87
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Ga2_ManAddToAbsOneDynamic
static void Ga2_ManAddToAbsOneDynamic(Ga2_Man_t *p, Gia_Obj_t *pObj, int f)
Definition: absGla.c:825
Saig_ManBmcHashKey
static unsigned Saig_ManBmcHashKey(int *pArray)
Definition: absGla.c:727
Ga2_Man_t_::pSopSizes
char * pSopSizes
Definition: absGla.c:74
Ga2_Man_t_::LimAbs
int LimAbs
Definition: absGla.c:51
Gia_Man_t_::vMapping
Vec_Int_t * vMapping
Definition: gia.h:131
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_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
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
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
Vec_PtrShrink
static void Vec_PtrShrink(Vec_Ptr_t *p, int nSizeNew)
Definition: vecPtr.h:528
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Ga2_Man_t_::nHashMiss
int nHashMiss
Definition: absGla.c:69
Ga2_Man_t_::vAbs
Vec_Int_t * vAbs
Definition: absGla.c:48
Ga2_Man_t_::LimPpi
int LimPpi
Definition: absGla.c:52
Ga2_ManRestart
void Ga2_ManRestart(Ga2_Man_t *p)
Definition: absGla.c:1112
Ga2_ManCheckNodesAnd
int Ga2_ManCheckNodesAnd(Gia_Man_t *p, Vec_Int_t *vNodes)
Definition: absGla.c:212
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
Ga2_Man_t_::vIds
Vec_Int_t * vIds
Definition: absGla.c:46
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
Ga2_ManStop
void Ga2_ManStop(Ga2_Man_t *p)
Definition: absGla.c:460
Gia_GlaCountNodes
int Gia_GlaCountNodes(Gia_Man_t *p, Vec_Int_t *vGla)
Definition: absUtil.c:240
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_GlaProveCheck
int Gia_GlaProveCheck(int fVerbose)
Definition: absPth.c:47
Abs_Par_t
typedefABC_NAMESPACE_HEADER_START struct Abs_Par_t_ Abs_Par_t
INCLUDES ///.
Definition: abs.h:46
sat_solver2_set_runtime_limit
static abctime sat_solver2_set_runtime_limit(sat_solver2 *s, abctime Limit)
Definition: satSolver2.h:234
Ga2_ObjTruthDepends
static unsigned Ga2_ObjTruthDepends(unsigned t, int v)
Definition: absGla.c:506
Gia_ObjIsPi
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
Ga2_Man_t_::pSops
char ** pSops
Definition: absGla.c:74
Gia_Man_t_::pCexSeq
Abc_Cex_t * pCexSeq
Definition: gia.h:136
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387