abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
saigGlaPba.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [saigGlaPba.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Sequential AIG 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: saigGlaPba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "saig.h"
22 #include "sat/bsat/satSolver.h"
23 #include "sat/bsat/satStore.h"
24 
25 ABC_NAMESPACE_IMPL_START
26 
27 
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 typedef struct Aig_Gla2Man_t_ Aig_Gla2Man_t;
33 struct Aig_Gla2Man_t_
34 {
35  // user data
36  Aig_Man_t * pAig;
37  int nStart;
38  int nFramesMax;
39  int fVerbose;
40  // unrolling
41  Vec_Int_t * vObj2Vec; // maps obj ID into its vec ID
42  Vec_Int_t * vVec2Var; // maps vec ID into its sat Var (nFrames per vec ID)
43  Vec_Int_t * vVar2Inf; // maps sat Var into its frame and obj ID
44  // clause mapping
45  Vec_Int_t * vCla2Obj; // maps clause into its root object
46  Vec_Int_t * vCla2Fra; // maps clause into its frame
47  Vec_Int_t * vVec2Use; // maps vec ID into its used frames (nFrames per vec ID)
48  // SAT solver
49  sat_solver * pSat;
50  // statistics
51  clock_t timePre;
52  clock_t timeSat;
53  clock_t timeTotal;
54 };
55 
56 ////////////////////////////////////////////////////////////////////////
57 /// FUNCTION DEFINITIONS ///
58 ////////////////////////////////////////////////////////////////////////
59 
60 
61 /**Function*************************************************************
62 
63  Synopsis [Adds constant to the solver.]
64 
65  Description []
66 
67  SideEffects []
68 
69  SeeAlso []
70 
71 ***********************************************************************/
72 static inline int Aig_Gla2AddConst( sat_solver * pSat, int iVar, int fCompl )
73 {
74  lit Lit = toLitCond( iVar, fCompl );
75  if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) )
76  return 0;
77  return 1;
78 }
79 
80 /**Function*************************************************************
81 
82  Synopsis [Adds buffer to the solver.]
83 
84  Description []
85 
86  SideEffects []
87 
88  SeeAlso []
89 
90 ***********************************************************************/
91 static inline int Aig_Gla2AddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
92 {
93  lit Lits[2];
94 
95  Lits[0] = toLitCond( iVar0, 0 );
96  Lits[1] = toLitCond( iVar1, !fCompl );
97  if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
98  return 0;
99 
100  Lits[0] = toLitCond( iVar0, 1 );
101  Lits[1] = toLitCond( iVar1, fCompl );
102  if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
103  return 0;
104 
105  return 1;
106 }
107 
108 /**Function*************************************************************
109 
110  Synopsis [Adds buffer to the solver.]
111 
112  Description []
113 
114  SideEffects []
115 
116  SeeAlso []
117 
118 ***********************************************************************/
119 static inline int Aig_Gla2AddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
120 {
121  lit Lits[3];
122 
123  Lits[0] = toLitCond( iVar, 1 );
124  Lits[1] = toLitCond( iVar0, fCompl0 );
125  if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
126  return 0;
127 
128  Lits[0] = toLitCond( iVar, 1 );
129  Lits[1] = toLitCond( iVar1, fCompl1 );
130  if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
131  return 0;
132 
133  Lits[0] = toLitCond( iVar, 0 );
134  Lits[1] = toLitCond( iVar0, !fCompl0 );
135  Lits[2] = toLitCond( iVar1, !fCompl1 );
136  if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
137  return 0;
138 
139  return 1;
140 }
141 
142 
143 /**Function*************************************************************
144 
145  Synopsis [Finds existing SAT variable or creates a new one.]
146 
147  Description []
148 
149  SideEffects []
150 
151  SeeAlso []
152 
153 ***********************************************************************/
154 int Aig_Gla2FetchVar( Aig_Gla2Man_t * p, Aig_Obj_t * pObj, int k )
155 {
156  int i, iVecId, iSatVar;
157  assert( k < p->nFramesMax );
158  iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
159  if ( iVecId == 0 )
160  {
161  iVecId = Vec_IntSize( p->vVec2Var ) / p->nFramesMax;
162  for ( i = 0; i < p->nFramesMax; i++ )
163  Vec_IntPush( p->vVec2Var, 0 );
164  Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), iVecId );
165  }
166  iSatVar = Vec_IntEntry( p->vVec2Var, iVecId * p->nFramesMax + k );
167  if ( iSatVar == 0 )
168  {
169  iSatVar = Vec_IntSize( p->vVar2Inf ) / 2;
170  Vec_IntPush( p->vVar2Inf, Aig_ObjId(pObj) );
171  Vec_IntPush( p->vVar2Inf, k );
172  Vec_IntWriteEntry( p->vVec2Var, iVecId * p->nFramesMax + k, iSatVar );
173  }
174  return iSatVar;
175 }
176 
177 /**Function*************************************************************
178 
179  Synopsis [Assigns variables to the AIG nodes.]
180 
181  Description []
182 
183  SideEffects []
184 
185  SeeAlso []
186 
187 ***********************************************************************/
188 void Aig_Gla2AssignVars_rec( Aig_Gla2Man_t * p, Aig_Obj_t * pObj, int f )
189 {
190  int nVars = Vec_IntSize(p->vVar2Inf);
191  Aig_Gla2FetchVar( p, pObj, f );
192  if ( nVars == Vec_IntSize(p->vVar2Inf) )
193  return;
194  if ( Aig_ObjIsConst1(pObj) )
195  return;
196  if ( Saig_ObjIsPo( p->pAig, pObj ) )
197  {
198  Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0(pObj), f );
199  return;
200  }
201  if ( Aig_ObjIsCi( pObj ) )
202  {
203  if ( Saig_ObjIsLo(p->pAig, pObj) && f > 0 )
204  Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p->pAig, pObj) ), f-1 );
205  return;
206  }
207  assert( Aig_ObjIsNode(pObj) );
208  Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0(pObj), f );
209  Aig_Gla2AssignVars_rec( p, Aig_ObjFanin1(pObj), f );
210 }
211 
212 /**Function*************************************************************
213 
214  Synopsis [Creates SAT solver.]
215 
216  Description []
217 
218  SideEffects []
219 
220  SeeAlso []
221 
222 ***********************************************************************/
223 int Aig_Gla2CreateSatSolver( Aig_Gla2Man_t * p )
224 {
225  Vec_Int_t * vPoLits;
226  Aig_Obj_t * pObj;
227  int i, f, ObjId, nVars, RetValue = 1;
228 
229  // assign variables
230  for ( f = p->nFramesMax - 1; f >= 0; f-- )
231 // for ( f = 0; f < p->nFramesMax; f++ )
232  Aig_Gla2AssignVars_rec( p, Aig_ManCo(p->pAig, 0), f );
233 
234  // create SAT solver
235  p->pSat = sat_solver_new();
236  sat_solver_store_alloc( p->pSat );
237  sat_solver_setnvars( p->pSat, Vec_IntSize(p->vVar2Inf)/2 );
238 
239  // add clauses
240  nVars = Vec_IntSize( p->vVar2Inf );
241  Vec_IntForEachEntryDouble( p->vVar2Inf, ObjId, f, i )
242  {
243  if ( ObjId == -1 )
244  continue;
245  pObj = Aig_ManObj( p->pAig, ObjId );
246  if ( Aig_ObjIsNode(pObj) )
247  {
248  RetValue &= Aig_Gla2AddNode( p->pSat, Aig_Gla2FetchVar(p, pObj, f),
249  Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObj), f),
250  Aig_Gla2FetchVar(p, Aig_ObjFanin1(pObj), f),
251  Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
252  Vec_IntPush( p->vCla2Obj, ObjId );
253  Vec_IntPush( p->vCla2Obj, ObjId );
254  Vec_IntPush( p->vCla2Obj, ObjId );
255 
256  Vec_IntPush( p->vCla2Fra, f );
257  Vec_IntPush( p->vCla2Fra, f );
258  Vec_IntPush( p->vCla2Fra, f );
259  }
260  else if ( Saig_ObjIsLo(p->pAig, pObj) )
261  {
262  if ( f == 0 )
263  {
264  RetValue &= Aig_Gla2AddConst( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 1 );
265  Vec_IntPush( p->vCla2Obj, ObjId );
266 
267  Vec_IntPush( p->vCla2Fra, f );
268  }
269  else
270  {
271  Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
272  RetValue &= Aig_Gla2AddBuffer( p->pSat, Aig_Gla2FetchVar(p, pObj, f),
273  Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObjLi), f-1),
274  Aig_ObjFaninC0(pObjLi) );
275  Vec_IntPush( p->vCla2Obj, ObjId );
276  Vec_IntPush( p->vCla2Obj, ObjId );
277 
278  Vec_IntPush( p->vCla2Fra, f );
279  Vec_IntPush( p->vCla2Fra, f );
280  }
281  }
282  else if ( Saig_ObjIsPo(p->pAig, pObj) )
283  {
284  RetValue &= Aig_Gla2AddBuffer( p->pSat, Aig_Gla2FetchVar(p, pObj, f),
285  Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObj), f),
286  Aig_ObjFaninC0(pObj) );
287  Vec_IntPush( p->vCla2Obj, ObjId );
288  Vec_IntPush( p->vCla2Obj, ObjId );
289 
290  Vec_IntPush( p->vCla2Fra, f );
291  Vec_IntPush( p->vCla2Fra, f );
292  }
293  else if ( Aig_ObjIsConst1(pObj) )
294  {
295  RetValue &= Aig_Gla2AddConst( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 0 );
296  Vec_IntPush( p->vCla2Obj, ObjId );
297 
298  Vec_IntPush( p->vCla2Fra, f );
299  }
300  else assert( Saig_ObjIsPi(p->pAig, pObj) );
301  }
302 
303  // add output clause
304  vPoLits = Vec_IntAlloc( p->nFramesMax );
305  for ( f = p->nStart; f < p->nFramesMax; f++ )
306  Vec_IntPush( vPoLits, 2 * Aig_Gla2FetchVar(p, Aig_ManCo(p->pAig, 0), f) );
307  RetValue &= sat_solver_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) );
308  Vec_IntFree( vPoLits );
309  Vec_IntPush( p->vCla2Obj, 0 );
310  Vec_IntPush( p->vCla2Fra, 0 );
311  assert( Vec_IntSize(p->vCla2Fra) == Vec_IntSize(p->vCla2Obj) );
312 
313  assert( nVars == Vec_IntSize(p->vVar2Inf) );
314  assert( ((Sto_Man_t *)p->pSat->pStore)->nClauses == Vec_IntSize(p->vCla2Obj) );
315 // Sto_ManDumpClauses( ((Sto_Man_t *)p->pSat->pStore), "temp_sto.cnf" );
316  sat_solver_store_mark_roots( p->pSat );
317 
318  if ( p->fVerbose )
319  printf( "The resulting SAT problem contains %d variables and %d clauses.\n",
320  p->pSat->size, p->pSat->stats.clauses );
321  return RetValue;
322 }
323 
324 /**Function*************************************************************
325 
326  Synopsis []
327 
328  Description []
329 
330  SideEffects []
331 
332  SeeAlso []
333 
334 ***********************************************************************/
335 Aig_Gla2Man_t * Aig_Gla2ManStart( Aig_Man_t * pAig, int nStart, int nFramesMax, int fVerbose )
336 {
337  Aig_Gla2Man_t * p;
338  int i;
339 
340  p = ABC_CALLOC( Aig_Gla2Man_t, 1 );
341  p->pAig = pAig;
342 
343  p->vObj2Vec = Vec_IntStart( Aig_ManObjNumMax(pAig) );
344  p->vVec2Var = Vec_IntAlloc( 1 << 20 );
345  p->vVar2Inf = Vec_IntAlloc( 1 << 20 );
346  p->vCla2Obj = Vec_IntAlloc( 1 << 20 );
347  p->vCla2Fra = Vec_IntAlloc( 1 << 20 );
348 
349  // skip first vector ID
350  p->nStart = nStart;
351  p->nFramesMax = nFramesMax;
352  p->fVerbose = fVerbose;
353  for ( i = 0; i < p->nFramesMax; i++ )
354  Vec_IntPush( p->vVec2Var, -1 );
355 
356  // skip first SAT variable
357  Vec_IntPush( p->vVar2Inf, -1 );
358  Vec_IntPush( p->vVar2Inf, -1 );
359  return p;
360 }
361 
362 /**Function*************************************************************
363 
364  Synopsis []
365 
366  Description []
367 
368  SideEffects []
369 
370  SeeAlso []
371 
372 ***********************************************************************/
373 void Aig_Gla2ManStop( Aig_Gla2Man_t * p )
374 {
375  Vec_IntFreeP( &p->vObj2Vec );
376  Vec_IntFreeP( &p->vVec2Var );
377  Vec_IntFreeP( &p->vVar2Inf );
378  Vec_IntFreeP( &p->vCla2Obj );
379  Vec_IntFreeP( &p->vCla2Fra );
380  Vec_IntFreeP( &p->vVec2Use );
381 
382  if ( p->pSat )
383  sat_solver_delete( p->pSat );
384  ABC_FREE( p );
385 }
386 
387 
388 /**Function*************************************************************
389 
390  Synopsis [Finds the set of clauses involved in the UNSAT core.]
391 
392  Description []
393 
394  SideEffects []
395 
396  SeeAlso []
397 
398 ***********************************************************************/
399 Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbose, int * piRetValue )
400 {
401  Vec_Int_t * vCore;
402  void * pSatCnf;
403  Intp_Man_t * pManProof;
404  int RetValue;
405  clock_t clk = clock();
406  if ( piRetValue )
407  *piRetValue = -1;
408  // solve the problem
409  RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
410  if ( RetValue == l_Undef )
411  {
412  printf( "Conflict limit is reached.\n" );
413  return NULL;
414  }
415  if ( RetValue == l_True )
416  {
417  printf( "The BMC problem is SAT.\n" );
418  if ( piRetValue )
419  *piRetValue = 0;
420  return NULL;
421  }
422  if ( fVerbose )
423  {
424  printf( "SAT solver returned UNSAT after %7d conflicts. ", (int)pSat->stats.conflicts );
425  Abc_PrintTime( 1, "Time", clock() - clk );
426  }
427  assert( RetValue == l_False );
428  pSatCnf = sat_solver_store_release( pSat );
429  // derive the UNSAT core
430  clk = clock();
431  pManProof = Intp_ManAlloc();
432  vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0, 0 );
433  Intp_ManFree( pManProof );
434  if ( fVerbose )
435  {
436  printf( "SAT core contains %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver_nclauses(pSat) );
437  Abc_PrintTime( 1, "Time", clock() - clk );
438  }
439  Sto_ManFree( (Sto_Man_t *)pSatCnf );
440  return vCore;
441 }
442 
443 /**Function*************************************************************
444 
445  Synopsis [Collects abstracted objects.]
446 
447  Description []
448 
449  SideEffects []
450 
451  SeeAlso []
452 
453 ***********************************************************************/
454 Vec_Int_t * Aig_Gla2ManCollect( Aig_Gla2Man_t * p, Vec_Int_t * vCore )
455 {
456  Vec_Int_t * vResult;
457  Aig_Obj_t * pObj;
458  int i, ClaId, iVecId;
459 // p->vVec2Use = Vec_IntStart( Vec_IntSize(p->vVec2Var) );
460 
461  vResult = Vec_IntStart( Aig_ManObjNumMax(p->pAig) );
462  Vec_IntWriteEntry( vResult, 0, 1 ); // add const1
463  Vec_IntForEachEntry( vCore, ClaId, i )
464  {
465  pObj = Aig_ManObj( p->pAig, Vec_IntEntry(p->vCla2Obj, ClaId) );
466  if ( Saig_ObjIsPi(p->pAig, pObj) || Saig_ObjIsPo(p->pAig, pObj) || Aig_ObjIsConst1(pObj) )
467  continue;
468  assert( Saig_ObjIsLo(p->pAig, pObj) || Aig_ObjIsNode(pObj) );
469  Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), 1 );
470 /*
471  // add flop inputs with multiple fanouts
472  if ( Saig_ObjIsLo(p->pAig, pObj) )
473  {
474  Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
475  if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin0(pObjLi)) )
476 // if ( Aig_ObjRefs( Aig_ObjFanin0(pObjLi) ) > 1 )
477  Vec_IntWriteEntry( vResult, Aig_ObjFaninId0(pObjLi), 1 );
478  }
479  else
480  {
481  if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin0(pObj)) )
482  Vec_IntWriteEntry( vResult, Aig_ObjFaninId0(pObj), 1 );
483  if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin1(pObj)) )
484  Vec_IntWriteEntry( vResult, Aig_ObjFaninId1(pObj), 1 );
485  }
486 */
487  if ( p->vVec2Use )
488  {
489  iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
490  Vec_IntWriteEntry( p->vVec2Use, iVecId * p->nFramesMax + Vec_IntEntry(p->vCla2Fra, ClaId), 1 );
491  }
492  }
493 // printf( "Number of entries %d\n", Vec_IntCountPositive(vResult) );
494 
495  // count the number of objects in each frame
496  if ( p->vVec2Use )
497  {
498  Vec_Int_t * vCounts = Vec_IntStart( p->nFramesMax );
499  int v, f, Entry, nVecIds = Vec_IntSize(p->vVec2Use) / p->nFramesMax;
500  for ( f = 0; f < p->nFramesMax; f++ )
501  for ( v = 0; v < nVecIds; v++ )
502  if ( Vec_IntEntry( p->vVec2Use, v * p->nFramesMax + f ) )
503  Vec_IntAddToEntry( vCounts, f, 1 );
504  Vec_IntForEachEntry( vCounts, Entry, f )
505  printf( "%d ", Entry );
506  printf( "\n" );
507  Vec_IntFree( vCounts );
508  }
509  return vResult;
510 }
511 
512 /**Function*************************************************************
513 
514  Synopsis [Performs gate-level localization abstraction.]
515 
516  Description [Returns array of objects included in the abstraction. This array
517  may contain only const1, flop outputs, and internal nodes, that is, objects
518  that should have clauses added to the SAT solver.]
519 
520  SideEffects []
521 
522  SeeAlso []
523 
524 ***********************************************************************/
525 Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose )
526 {
527  Aig_Gla2Man_t * p;
528  Vec_Int_t * vCore, * vResult;
529  clock_t nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0;
530  clock_t clk, clk2 = clock();
531  assert( Saig_ManPoNum(pAig) == 1 );
532 
533  if ( fVerbose )
534  {
535  if ( TimeLimit )
536  printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFramesMax, TimeLimit );
537  else
538  printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFramesMax );
539  }
540 
541  // start the solver
542  clk = clock();
543  p = Aig_Gla2ManStart( pAig, nStart, nFramesMax, fVerbose );
544  if ( !Aig_Gla2CreateSatSolver( p ) )
545  {
546  printf( "Error! SAT solver became UNSAT.\n" );
547  Aig_Gla2ManStop( p );
548  return NULL;
549  }
550  sat_solver_set_random( p->pSat, fSkipRand );
551  p->timePre += clock() - clk;
552 
553  // set runtime limit
554  if ( TimeLimit )
555  sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
556 
557  // compute UNSAT core
558  clk = clock();
559  vCore = Saig_AbsSolverUnsatCore( p->pSat, nConfLimit, fVerbose, NULL );
560  if ( vCore == NULL )
561  {
562  Aig_Gla2ManStop( p );
563  return NULL;
564  }
565  p->timeSat += clock() - clk;
566  p->timeTotal += clock() - clk2;
567 
568  // print stats
569  if ( fVerbose )
570  {
571  ABC_PRTP( "Pre ", p->timePre, p->timeTotal );
572  ABC_PRTP( "Sat ", p->timeSat, p->timeTotal );
573  ABC_PRTP( "Total ", p->timeTotal, p->timeTotal );
574  }
575 
576  // prepare return value
577  vResult = Aig_Gla2ManCollect( p, vCore );
578  Vec_IntFree( vCore );
579  Aig_Gla2ManStop( p );
580  return vResult;
581 }
582 
583 ////////////////////////////////////////////////////////////////////////
584 /// END OF FILE ///
585 ////////////////////////////////////////////////////////////////////////
586 
587 
588 ABC_NAMESPACE_IMPL_END
589 
sat_solver_set_runtime_limit
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Intp_ManUnsatCore
void * Intp_ManUnsatCore(Intp_Man_t *p, Sto_Man_t *pCnf, int fLearned, int fVerbose)
Definition: satInterP.c:963
Intp_Man_t_
Definition: satInterP.c:40
Sto_Man_t_
Definition: satStore.h:82
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
Aig_Gla2Man_t_::timePre
clock_t timePre
Definition: saigGlaPba.c:51
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
l_Undef
#define l_Undef
Definition: SolverTypes.h:86
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
sat_solver_solve
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
Aig_Gla2Man_t_::vVec2Use
Vec_Int_t * vVec2Use
Definition: saigGlaPba.c:47
Aig_Gla2Man_t
typedefABC_NAMESPACE_IMPL_START struct Aig_Gla2Man_t_ Aig_Gla2Man_t
DECLARATIONS ///.
Definition: saigGlaPba.c:32
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
sat_solver_store_release
void * sat_solver_store_release(sat_solver *s)
Definition: satSolver.c:1949
sat_solver_set_random
static int sat_solver_set_random(sat_solver *s, int fNotUseRandom)
Definition: satSolver.h:240
Aig_Gla2Man_t_::fVerbose
int fVerbose
Definition: saigGlaPba.c:39
l_True
#define l_True
Definition: SolverTypes.h:84
Aig_ManObj
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
Aig_Gla2Man_t_::vObj2Vec
Vec_Int_t * vObj2Vec
Definition: saigGlaPba.c:41
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
sat_solver_t::stats
stats_t stats
Definition: satSolver.h:156
Aig_Gla2Man_t_::nStart
int nStart
Definition: saigGlaPba.c:37
lit
int lit
Definition: satVec.h:130
Intp_ManAlloc
Intp_Man_t * Intp_ManAlloc()
FUNCTION DEFINITIONS ///.
Definition: satInterP.c:96
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition: abc_global.h:223
Aig_Gla2Man_t_::timeSat
clock_t timeSat
Definition: saigGlaPba.c:52
Aig_Gla2Man_t_::nFramesMax
int nFramesMax
Definition: saigGlaPba.c:38
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Aig_Gla2Man_t_::timeTotal
clock_t timeTotal
Definition: saigGlaPba.c:53
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Intp_ManFree
void Intp_ManFree(Intp_Man_t *p)
Definition: satInterP.c:178
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Aig_Gla2AddConst
static int Aig_Gla2AddConst(sat_solver *pSat, int iVar, int fCompl)
FUNCTION DEFINITIONS ///.
Definition: saigGlaPba.c:72
Aig_Gla2CreateSatSolver
int Aig_Gla2CreateSatSolver(Aig_Gla2Man_t *p)
Definition: saigGlaPba.c:223
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Vec_IntAddToEntry
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
sat_solver_store_alloc
void sat_solver_store_alloc(sat_solver *s)
Definition: satSolver.c:1916
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Saig_ObjIsPo
static int Saig_ObjIsPo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:83
Aig_Gla2ManStop
void Aig_Gla2ManStop(Aig_Gla2Man_t *p)
Definition: saigGlaPba.c:373
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Aig_Gla2Man_t_
Definition: saigGlaPba.c:33
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Aig_Gla2AssignVars_rec
void Aig_Gla2AssignVars_rec(Aig_Gla2Man_t *p, Aig_Obj_t *pObj, int f)
Definition: saigGlaPba.c:188
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Aig_Gla2AddBuffer
static int Aig_Gla2AddBuffer(sat_solver *pSat, int iVar0, int iVar1, int fCompl)
Definition: saigGlaPba.c:91
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Vec_IntForEachEntryDouble
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition: vecInt.h:66
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Aig_Gla2Man_t_::vCla2Obj
Vec_Int_t * vCla2Obj
Definition: saigGlaPba.c:45
sat_solver_nclauses
int sat_solver_nclauses(sat_solver *s)
Definition: satSolver.c:1902
Aig_Gla2Man_t_::vVec2Var
Vec_Int_t * vVec2Var
Definition: saigGlaPba.c:42
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
sat_solver_store_mark_roots
void sat_solver_store_mark_roots(sat_solver *s)
Definition: satSolver.c:1939
stats_t::conflicts
ABC_INT64_T conflicts
Definition: satVec.h:154
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Sto_ManFree
void Sto_ManFree(Sto_Man_t *p)
Definition: satStore.c:143
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Aig_Gla2Man_t_::vCla2Fra
Vec_Int_t * vCla2Fra
Definition: saigGlaPba.c:46
Aig_Gla2FetchVar
int Aig_Gla2FetchVar(Aig_Gla2Man_t *p, Aig_Obj_t *pObj, int k)
Definition: saigGlaPba.c:154
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
l_False
#define l_False
Definition: SolverTypes.h:85
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
sat_solver_t
Definition: satSolver.h:91
Aig_Gla2Man_t_::pSat
sat_solver * pSat
Definition: saigGlaPba.c:49
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
assert
#define assert(ex)
Definition: util_old.h:213
Aig_Gla2Man_t_::vVar2Inf
Vec_Int_t * vVar2Inf
Definition: saigGlaPba.c:43
Aig_Gla2Man_t_::pAig
Aig_Man_t * pAig
Definition: saigGlaPba.c:36
Aig_Gla2AddNode
static int Aig_Gla2AddNode(sat_solver *pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1)
Definition: saigGlaPba.c:119
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Aig_Gla2ManCollect
Vec_Int_t * Aig_Gla2ManCollect(Aig_Gla2Man_t *p, Vec_Int_t *vCore)
Definition: saigGlaPba.c:454
Aig_Gla2ManPerform
Vec_Int_t * Aig_Gla2ManPerform(Aig_Man_t *pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose)
Definition: saigGlaPba.c:525
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
Aig_Gla2ManStart
Aig_Gla2Man_t * Aig_Gla2ManStart(Aig_Man_t *pAig, int nStart, int nFramesMax, int fVerbose)
Definition: saigGlaPba.c:335
Saig_AbsSolverUnsatCore
Vec_Int_t * Saig_AbsSolverUnsatCore(sat_solver *pSat, int nConfMax, int fVerbose, int *piRetValue)
Definition: saigGlaPba.c:399