abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fraHot.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [fraHot.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [New FRAIG package.]
8 
9  Synopsis [Computing and using one-hotness conditions.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 30, 2007.]
16 
17  Revision [$Id: fraHot.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "fra.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 static inline int Fra_RegToLit( int n, int c ) { return c? -n-1 : n+1; }
31 static inline int Fra_LitReg( int n ) { return (n>0)? n-1 : -n-1; }
32 static inline int Fra_LitSign( int n ) { return (n<0); }
33 
34 ////////////////////////////////////////////////////////////////////////
35 /// FUNCTION DEFINITIONS ///
36 ////////////////////////////////////////////////////////////////////////
37 
38 /**Function*************************************************************
39 
40  Synopsis [Returns 1 if simulation info is composed of all zeros.]
41 
42  Description []
43 
44  SideEffects []
45 
46  SeeAlso []
47 
48 ***********************************************************************/
49 int Fra_OneHotNodeIsConst( Fra_Sml_t * pSeq, Aig_Obj_t * pObj )
50 {
51  unsigned * pSims;
52  int i;
53  pSims = Fra_ObjSim(pSeq, pObj->Id);
54  for ( i = pSeq->nWordsPref; i < pSeq->nWordsTotal; i++ )
55  if ( pSims[i] )
56  return 0;
57  return 1;
58 }
59 
60 /**Function*************************************************************
61 
62  Synopsis [Returns 1 if simulation infos are equal.]
63 
64  Description []
65 
66  SideEffects []
67 
68  SeeAlso []
69 
70 ***********************************************************************/
71 int Fra_OneHotNodesAreEqual( Fra_Sml_t * pSeq, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
72 {
73  unsigned * pSims0, * pSims1;
74  int i;
75  pSims0 = Fra_ObjSim(pSeq, pObj0->Id);
76  pSims1 = Fra_ObjSim(pSeq, pObj1->Id);
77  for ( i = pSeq->nWordsPref; i < pSeq->nWordsTotal; i++ )
78  if ( pSims0[i] != pSims1[i] )
79  return 0;
80  return 1;
81 }
82 
83 /**Function*************************************************************
84 
85  Synopsis [Returns 1 if implications holds.]
86 
87  Description []
88 
89  SideEffects []
90 
91  SeeAlso []
92 
93 ***********************************************************************/
94 int Fra_OneHotNodesAreClause( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2, int fCompl1, int fCompl2 )
95 {
96  unsigned * pSim1, * pSim2;
97  int k;
98  pSim1 = Fra_ObjSim(pSeq, pObj1->Id);
99  pSim2 = Fra_ObjSim(pSeq, pObj2->Id);
100  if ( fCompl1 && fCompl2 )
101  {
102  for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
103  if ( pSim1[k] & pSim2[k] )
104  return 0;
105  }
106  else if ( fCompl1 )
107  {
108  for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
109  if ( pSim1[k] & ~pSim2[k] )
110  return 0;
111  }
112  else if ( fCompl2 )
113  {
114  for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
115  if ( ~pSim1[k] & pSim2[k] )
116  return 0;
117  }
118  else
119  assert( 0 );
120  return 1;
121 }
122 
123 /**Function*************************************************************
124 
125  Synopsis [Computes one-hot implications.]
126 
127  Description []
128 
129  SideEffects []
130 
131  SeeAlso []
132 
133 ***********************************************************************/
134 Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim )
135 {
136  int fSkipConstEqu = 1;
137  Vec_Int_t * vOneHots;
138  Aig_Obj_t * pObj1, * pObj2;
139  int i, k;
140  int nTruePis = Aig_ManCiNum(pSim->pAig) - Aig_ManRegNum(pSim->pAig);
141  assert( pSim->pAig == p->pManAig );
142  vOneHots = Vec_IntAlloc( 100 );
143  Aig_ManForEachLoSeq( pSim->pAig, pObj1, i )
144  {
145  if ( fSkipConstEqu && Fra_OneHotNodeIsConst(pSim, pObj1) )
146  continue;
147  assert( i-nTruePis >= 0 );
148 // Aig_ManForEachLoSeq( pSim->pAig, pObj2, k )
149 // Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vPis, pObj2, k, Aig_ManCiNum(p)-Aig_ManRegNum(p) )
150  Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vCis, pObj2, k, i+1 )
151  {
152  if ( fSkipConstEqu && Fra_OneHotNodeIsConst(pSim, pObj2) )
153  continue;
154  if ( fSkipConstEqu && Fra_OneHotNodesAreEqual( pSim, pObj1, pObj2 ) )
155  continue;
156  assert( k-nTruePis >= 0 );
157  if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 1, 1 ) )
158  {
159  Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 1) );
160  Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 1) );
161  continue;
162  }
163  if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 0, 1 ) )
164  {
165  Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 0) );
166  Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 1) );
167  continue;
168  }
169  if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 1, 0 ) )
170  {
171  Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 1) );
172  Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 0) );
173  continue;
174  }
175  }
176  }
177  return vOneHots;
178 }
179 
180 /**Function*************************************************************
181 
182  Synopsis [Assumes one-hot implications in the SAT solver.]
183 
184  Description []
185 
186  SideEffects []
187 
188  SeeAlso []
189 
190 **********************************************************************/
191 void Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots )
192 {
193  Aig_Obj_t * pObj1, * pObj2;
194  int i, Out1, Out2, pLits[2];
195  int nPiNum = Aig_ManCiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
196  assert( p->pPars->nFramesK == 1 ); // add to only one frame
197  for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
198  {
199  Out1 = Vec_IntEntry( vOneHots, i );
200  Out2 = Vec_IntEntry( vOneHots, i+1 );
201  if ( Out1 == 0 && Out2 == 0 )
202  continue;
203  pObj1 = Aig_ManCi( p->pManFraig, nPiNum + Fra_LitReg(Out1) );
204  pObj2 = Aig_ManCi( p->pManFraig, nPiNum + Fra_LitReg(Out2) );
205  pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), Fra_LitSign(Out1) );
206  pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), Fra_LitSign(Out2) );
207  // add constraint to solver
208  if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) )
209  {
210  printf( "Fra_OneHotAssume(): Adding clause makes SAT solver unsat.\n" );
211  sat_solver_delete( p->pSat );
212  p->pSat = NULL;
213  return;
214  }
215  }
216 }
217 
218 /**Function*************************************************************
219 
220  Synopsis [Checks one-hot implications.]
221 
222  Description []
223 
224  SideEffects []
225 
226  SeeAlso []
227 
228 **********************************************************************/
229 void Fra_OneHotCheck( Fra_Man_t * p, Vec_Int_t * vOneHots )
230 {
231  Aig_Obj_t * pObj1, * pObj2;
232  int RetValue, i, Out1, Out2;
233  int nTruePos = Aig_ManCoNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
234  for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
235  {
236  Out1 = Vec_IntEntry( vOneHots, i );
237  Out2 = Vec_IntEntry( vOneHots, i+1 );
238  if ( Out1 == 0 && Out2 == 0 )
239  continue;
240  pObj1 = Aig_ManCo( p->pManFraig, nTruePos + Fra_LitReg(Out1) );
241  pObj2 = Aig_ManCo( p->pManFraig, nTruePos + Fra_LitReg(Out2) );
242  RetValue = Fra_NodesAreClause( p, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) );
243  if ( RetValue != 1 )
244  {
245  p->pCla->fRefinement = 1;
246  if ( RetValue == 0 )
247  Fra_SmlResimulate( p );
248  if ( Vec_IntEntry(vOneHots, i) != 0 )
249  printf( "Fra_OneHotCheck(): Clause is not refined!\n" );
250  assert( Vec_IntEntry(vOneHots, i) == 0 );
251  }
252  }
253 }
254 
255 /**Function*************************************************************
256 
257  Synopsis [Removes those implications that no longer hold.]
258 
259  Description [Returns 1 if refinement has happened.]
260 
261  SideEffects []
262 
263  SeeAlso []
264 
265 ***********************************************************************/
266 int Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vOneHots )
267 {
268  Aig_Obj_t * pObj1, * pObj2;
269  int i, Out1, Out2, RetValue = 0;
270  int nPiNum = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
271  assert( p->pSml->pAig == p->pManAig );
272  for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
273  {
274  Out1 = Vec_IntEntry( vOneHots, i );
275  Out2 = Vec_IntEntry( vOneHots, i+1 );
276  if ( Out1 == 0 && Out2 == 0 )
277  continue;
278  // get the corresponding nodes
279  pObj1 = Aig_ManCi( p->pManAig, nPiNum + Fra_LitReg(Out1) );
280  pObj2 = Aig_ManCi( p->pManAig, nPiNum + Fra_LitReg(Out2) );
281  // check if implication holds using this simulation info
282  if ( !Fra_OneHotNodesAreClause( p->pSml, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) ) )
283  {
284  Vec_IntWriteEntry( vOneHots, i, 0 );
285  Vec_IntWriteEntry( vOneHots, i+1, 0 );
286  RetValue = 1;
287  }
288  }
289  return RetValue;
290 }
291 
292 /**Function*************************************************************
293 
294  Synopsis [Removes those implications that no longer hold.]
295 
296  Description [Returns 1 if refinement has happened.]
297 
298  SideEffects []
299 
300  SeeAlso []
301 
302 ***********************************************************************/
303 int Fra_OneHotCount( Fra_Man_t * p, Vec_Int_t * vOneHots )
304 {
305  int i, Out1, Out2, Counter = 0;
306  for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
307  {
308  Out1 = Vec_IntEntry( vOneHots, i );
309  Out2 = Vec_IntEntry( vOneHots, i+1 );
310  if ( Out1 == 0 && Out2 == 0 )
311  continue;
312  Counter++;
313  }
314  return Counter;
315 }
316 
317 /**Function*************************************************************
318 
319  Synopsis [Estimates the coverage of state space by clauses.]
320 
321  Description []
322 
323  SideEffects []
324 
325  SeeAlso []
326 
327 ***********************************************************************/
328 void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots )
329 {
330  int nSimWords = (1<<14);
331  int nRegs = Aig_ManRegNum(p->pManAig);
332  Vec_Ptr_t * vSimInfo;
333  unsigned * pSim1, * pSim2, * pSimTot;
334  int i, w, Out1, Out2, nCovered, Counter = 0;
335  abctime clk = Abc_Clock();
336 
337  // generate random sim-info at register outputs
338  vSimInfo = Vec_PtrAllocSimInfo( nRegs + 1, nSimWords );
339 // srand( 0xAABBAABB );
340  Aig_ManRandom(1);
341  for ( i = 0; i < nRegs; i++ )
342  {
343  pSim1 = (unsigned *)Vec_PtrEntry( vSimInfo, i );
344  for ( w = 0; w < nSimWords; w++ )
345  pSim1[w] = Fra_ObjRandomSim();
346  }
347  pSimTot = (unsigned *)Vec_PtrEntry( vSimInfo, nRegs );
348 
349  // collect simulation info
350  memset( pSimTot, 0, sizeof(unsigned) * nSimWords );
351  for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
352  {
353  Out1 = Vec_IntEntry( vOneHots, i );
354  Out2 = Vec_IntEntry( vOneHots, i+1 );
355  if ( Out1 == 0 && Out2 == 0 )
356  continue;
357 //printf( "(%c%d,%c%d) ",
358 //Fra_LitSign(Out1)? '-': '+', Fra_LitReg(Out1),
359 //Fra_LitSign(Out2)? '-': '+', Fra_LitReg(Out2) );
360  Counter++;
361  pSim1 = (unsigned *)Vec_PtrEntry( vSimInfo, Fra_LitReg(Out1) );
362  pSim2 = (unsigned *)Vec_PtrEntry( vSimInfo, Fra_LitReg(Out2) );
363  if ( Fra_LitSign(Out1) && Fra_LitSign(Out2) )
364  for ( w = 0; w < nSimWords; w++ )
365  pSimTot[w] |= pSim1[w] & pSim2[w];
366  else if ( Fra_LitSign(Out1) )
367  for ( w = 0; w < nSimWords; w++ )
368  pSimTot[w] |= pSim1[w] & ~pSim2[w];
369  else if ( Fra_LitSign(Out2) )
370  for ( w = 0; w < nSimWords; w++ )
371  pSimTot[w] |= ~pSim1[w] & pSim2[w];
372  else
373  assert( 0 );
374  }
375 //printf( "\n" );
376  // count the total number of patterns contained in the don't-care
377  nCovered = 0;
378  for ( w = 0; w < nSimWords; w++ )
379  nCovered += Aig_WordCountOnes( pSimTot[w] );
380  Vec_PtrFree( vSimInfo );
381  // print the result
382  printf( "Care states ratio = %f. ", 1.0 * (nSimWords * 32 - nCovered) / (nSimWords * 32) );
383  printf( "(%d out of %d patterns) ", nSimWords * 32 - nCovered, nSimWords * 32 );
384  ABC_PRT( "Time", Abc_Clock() - clk );
385 }
386 
387 /**Function*************************************************************
388 
389  Synopsis [Creates one-hotness EXDC.]
390 
391  Description []
392 
393  SideEffects []
394 
395  SeeAlso []
396 
397 ***********************************************************************/
398 Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots )
399 {
400  Aig_Man_t * pNew;
401  Aig_Obj_t * pObj1, * pObj2, * pObj;
402  int i, Out1, Out2, nTruePis;
403  pNew = Aig_ManStart( Vec_IntSize(vOneHots)/2 );
404 // for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
405 // Aig_ObjCreateCi(pNew);
406  Aig_ManForEachCi( p->pManAig, pObj, i )
407  Aig_ObjCreateCi(pNew);
408  nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
409  for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
410  {
411  Out1 = Vec_IntEntry( vOneHots, i );
412  Out2 = Vec_IntEntry( vOneHots, i+1 );
413  if ( Out1 == 0 && Out2 == 0 )
414  continue;
415  pObj1 = Aig_ManCi( pNew, nTruePis + Fra_LitReg(Out1) );
416  pObj2 = Aig_ManCi( pNew, nTruePis + Fra_LitReg(Out2) );
417  pObj1 = Aig_NotCond( pObj1, Fra_LitSign(Out1) );
418  pObj2 = Aig_NotCond( pObj2, Fra_LitSign(Out2) );
419  pObj = Aig_Or( pNew, pObj1, pObj2 );
420  Aig_ObjCreateCo( pNew, pObj );
421  }
422  Aig_ManCleanup(pNew);
423 // printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManCoNum(pNew) );
424  return pNew;
425 }
426 
427 
428 /**Function*************************************************************
429 
430  Synopsis [Assumes one-hot implications in the SAT solver.]
431 
432  Description []
433 
434  SideEffects []
435 
436  SeeAlso []
437 
438 **********************************************************************/
439 void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots )
440 {
441  Vec_Int_t * vGroup;
442  Aig_Obj_t * pObj1, * pObj2;
443  int k, i, j, Out1, Out2, pLits[2];
444  //
445  // these constrants should be added to different timeframes!
446  // (also note that PIs follow first - then registers)
447  //
448  Vec_PtrForEachEntry( Vec_Int_t *, vOnehots, vGroup, k )
449  {
450  Vec_IntForEachEntry( vGroup, Out1, i )
451  Vec_IntForEachEntryStart( vGroup, Out2, j, i+1 )
452  {
453  pObj1 = Aig_ManCi( p->pManFraig, Out1 );
454  pObj2 = Aig_ManCi( p->pManFraig, Out2 );
455  pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), 1 );
456  pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), 1 );
457  // add constraint to solver
458  if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) )
459  {
460  printf( "Fra_OneHotAddKnownConstraint(): Adding clause makes SAT solver unsat.\n" );
461  sat_solver_delete( p->pSat );
462  p->pSat = NULL;
463  return;
464  }
465  }
466  }
467 }
468 
469 
470 ////////////////////////////////////////////////////////////////////////
471 /// END OF FILE ///
472 ////////////////////////////////////////////////////////////////////////
473 
474 
475 ABC_NAMESPACE_IMPL_END
476 
memset
char * memset()
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Fra_OneHotCompute
Vec_Int_t * Fra_OneHotCompute(Fra_Man_t *p, Fra_Sml_t *pSim)
Definition: fraHot.c:134
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Fra_Man_t_::pManAig
Aig_Man_t * pManAig
Definition: fra.h:191
Fra_Cla_t_::fRefinement
int fRefinement
Definition: fra.h:162
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition: vecPtr.h:57
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
Fra_Sml_t_::pAig
Aig_Man_t * pAig
Definition: fra.h:173
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
Fra_Man_t_::pCla
Fra_Cla_t * pCla
Definition: fra.h:198
Fra_Man_t_::pPars
Fra_Par_t * pPars
Definition: fra.h:189
Fra_Man_t_::pSat
sat_solver * pSat
Definition: fra.h:210
Fra_OneHotEstimateCoverage
void Fra_OneHotEstimateCoverage(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition: fraHot.c:328
Fra_Man_t_::pSml
Fra_Sml_t * pSml
Definition: fra.h:200
Fra_OneHotNodesAreClause
int Fra_OneHotNodesAreClause(Fra_Sml_t *pSeq, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2, int fCompl1, int fCompl2)
Definition: fraHot.c:94
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Fra_RegToLit
static ABC_NAMESPACE_IMPL_START int Fra_RegToLit(int n, int c)
DECLARATIONS ///.
Definition: fraHot.c:30
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Fra_ObjSim
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Fra_OneHotRefineUsingCex
int Fra_OneHotRefineUsingCex(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition: fraHot.c:266
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Fra_OneHotCount
int Fra_OneHotCount(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition: fraHot.c:303
Fra_Man_t_::pManFraig
Aig_Man_t * pManFraig
Definition: fra.h:192
Aig_WordCountOnes
static int Aig_WordCountOnes(unsigned uWord)
Definition: aig.h:229
Fra_Sml_t_
Definition: fra.h:171
Fra_ObjRandomSim
static unsigned Fra_ObjRandomSim()
Definition: fra.h:258
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Fra_NodesAreClause
int Fra_NodesAreClause(Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew, int fComplL, int fComplR)
Definition: fraSat.c:317
Aig_ManCi
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
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
Fra_LitReg
static int Fra_LitReg(int n)
Definition: fraHot.c:31
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Fra_OneHotCreateExdc
Aig_Man_t * Fra_OneHotCreateExdc(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition: fraHot.c:398
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Aig_Or
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:259
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Counter
static int Counter
Definition: extraBddMisc.c:1877
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
Fra_OneHotNodesAreEqual
int Fra_OneHotNodesAreEqual(Fra_Sml_t *pSeq, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
Definition: fraHot.c:71
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Fra_SmlResimulate
void Fra_SmlResimulate(Fra_Man_t *p)
Definition: fraSim.c:703
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Aig_ManForEachLoSeq
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition: aig.h:441
Fra_Man_t_
Definition: fra.h:186
Fra_ObjSatNum
static int Fra_ObjSatNum(Aig_Obj_t *pObj)
Definition: fra.h:266
Fra_OneHotAssume
void Fra_OneHotAssume(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition: fraHot.c:191
assert
#define assert(ex)
Definition: util_old.h:213
Fra_OneHotCheck
void Fra_OneHotCheck(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition: fraHot.c:229
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
Fra_Sml_t_::nWordsPref
int nWordsPref
Definition: fra.h:178
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Fra_OneHotNodeIsConst
int Fra_OneHotNodeIsConst(Fra_Sml_t *pSeq, Aig_Obj_t *pObj)
FUNCTION DEFINITIONS ///.
Definition: fraHot.c:49
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Fra_LitSign
static int Fra_LitSign(int n)
Definition: fraHot.c:32
Vec_PtrAllocSimInfo
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
Fra_OneHotAddKnownConstraint
void Fra_OneHotAddKnownConstraint(Fra_Man_t *p, Vec_Ptr_t *vOnehots)
Definition: fraHot.c:439
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223