abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
saigConstr2.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [saigConstr2.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Sequential AIG package.]
8 
9  Synopsis [Functional constraint detection.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: saigConstr2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "saig.h"
22 #include "sat/cnf/cnf.h"
23 #include "sat/bsat/satSolver.h"
24 #include "bool/kit/kit.h"
25 #include "misc/bar/bar.h"
26 
27 ABC_NAMESPACE_IMPL_START
28 
29 
30 
31 ////////////////////////////////////////////////////////////////////////
32 /// DECLARATIONS ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 static inline Aig_Obj_t * Aig_ObjFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return pObjMap[nFs*pObj->Id + i]; }
36 static inline void Aig_ObjSetFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { pObjMap[nFs*pObj->Id + i] = pNode; }
37 
38 static inline Aig_Obj_t * Aig_ObjChild0Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin0(pObj)? Aig_NotCond(Aig_ObjFrames(pObjMap,nFs,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; }
39 static inline Aig_Obj_t * Aig_ObjChild1Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin1(pObj)? Aig_NotCond(Aig_ObjFrames(pObjMap,nFs,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; }
40 
41 ////////////////////////////////////////////////////////////////////////
42 /// FUNCTION DEFINITIONS ///
43 ////////////////////////////////////////////////////////////////////////
44 
45 /**Function*************************************************************
46 
47  Synopsis [Returns the probability of POs being 1 under rand seq sim.]
48 
49  Description []
50 
51  SideEffects []
52 
53  SeeAlso []
54 
55 ***********************************************************************/
56 int Ssw_ManProfileConstraints( Aig_Man_t * p, int nWords, int nFrames, int fVerbose )
57 {
58  Vec_Ptr_t * vInfo;
59  Vec_Int_t * vProbs, * vProbs2;
60  Aig_Obj_t * pObj, * pObjLi;
61  unsigned * pInfo, * pInfo0, * pInfo1, * pInfoMask, * pInfoMask2;
62  int i, w, f, RetValue = 1;
63  abctime clk = Abc_Clock();
64  if ( fVerbose )
65  printf( "Simulating %d nodes and %d flops for %d frames with %d words... ",
66  Aig_ManNodeNum(p), Aig_ManRegNum(p), nFrames, nWords );
67  Aig_ManRandom( 1 );
68  vInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p)+2, nWords );
69  Vec_PtrCleanSimInfo( vInfo, 0, nWords );
70  vProbs = Vec_IntStart( Saig_ManPoNum(p) );
71  vProbs2 = Vec_IntStart( Saig_ManPoNum(p) );
72  // start the constant
73  pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(Aig_ManConst1(p)) );
74  for ( w = 0; w < nWords; w++ )
75  pInfo[w] = ~0;
76  // start the flop inputs
77  Saig_ManForEachLi( p, pObj, i )
78  {
79  pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
80  for ( w = 0; w < nWords; w++ )
81  pInfo[w] = 0;
82  }
83  // get the info mask
84  pInfoMask = (unsigned *)Vec_PtrEntry( vInfo, Aig_ManObjNumMax(p) ); // PO failed
85  pInfoMask2 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ManObjNumMax(p)+1 ); // constr failed
86  for ( f = 0; f < nFrames; f++ )
87  {
88  // assign primary inputs
89  Saig_ManForEachPi( p, pObj, i )
90  {
91  pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
92  for ( w = 0; w < nWords; w++ )
93  pInfo[w] = Aig_ManRandom( 0 );
94  }
95  // move the flop values
96  Saig_ManForEachLiLo( p, pObjLi, pObj, i )
97  {
98  pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
99  pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObjLi) );
100  for ( w = 0; w < nWords; w++ )
101  pInfo[w] = pInfo0[w];
102  }
103  // simulate the nodes
104  Aig_ManForEachNode( p, pObj, i )
105  {
106  pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
107  pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjFaninId0(pObj) );
108  pInfo1 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjFaninId1(pObj) );
109  if ( Aig_ObjFaninC0(pObj) )
110  {
111  if ( Aig_ObjFaninC1(pObj) )
112  for ( w = 0; w < nWords; w++ )
113  pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
114  else
115  for ( w = 0; w < nWords; w++ )
116  pInfo[w] = ~pInfo0[w] & pInfo1[w];
117  }
118  else
119  {
120  if ( Aig_ObjFaninC1(pObj) )
121  for ( w = 0; w < nWords; w++ )
122  pInfo[w] = pInfo0[w] & ~pInfo1[w];
123  else
124  for ( w = 0; w < nWords; w++ )
125  pInfo[w] = pInfo0[w] & pInfo1[w];
126  }
127  }
128  // clean the mask
129  for ( w = 0; w < nWords; w++ )
130  pInfoMask[w] = pInfoMask2[w] = 0;
131  // simulate the primary outputs
132  Aig_ManForEachCo( p, pObj, i )
133  {
134  pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
135  pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjFaninId0(pObj) );
136  if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) || i >= Saig_ManPoNum(p) )
137  {
138  if ( Aig_ObjFaninC0(pObj) )
139  {
140  for ( w = 0; w < nWords; w++ )
141  pInfo[w] = ~pInfo0[w];
142  }
143  else
144  {
145  for ( w = 0; w < nWords; w++ )
146  pInfo[w] = pInfo0[w];
147  }
148  }
149  else
150  {
151  if ( Aig_ObjFaninC0(pObj) )
152  {
153  for ( w = 0; w < nWords; w++ )
154  pInfo[w] |= ~pInfo0[w];
155  }
156  else
157  {
158  for ( w = 0; w < nWords; w++ )
159  pInfo[w] |= pInfo0[w];
160  }
161  }
162  // collect patterns when one of the outputs fails
163  if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
164  {
165  for ( w = 0; w < nWords; w++ )
166  pInfoMask[w] |= pInfo[w];
167  }
168  else if ( i < Saig_ManPoNum(p) )
169  {
170  for ( w = 0; w < nWords; w++ )
171  pInfoMask2[w] |= pInfo[w];
172  }
173  }
174  // compare the PO values (mask=1 => out=0) or UNSAT(mask=1 & out=1)
175  Saig_ManForEachPo( p, pObj, i )
176  {
177  pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
178  for ( w = 0; w < nWords; w++ )
179  Vec_IntAddToEntry( vProbs, i, Aig_WordCountOnes(pInfo[w]) );
180  if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
181  {
182  // chek the output
183  for ( w = 0; w < nWords; w++ )
184  if ( pInfo[w] & ~pInfoMask2[w] )
185  break;
186  if ( w == nWords )
187  continue;
188  printf( "Primary output %d fails on some input patterns.\n", i );
189  }
190  else
191  {
192  // collect patterns that block the POs
193  for ( w = 0; w < nWords; w++ )
194  Vec_IntAddToEntry( vProbs2, i, Aig_WordCountOnes(pInfo[w] & pInfoMask[w]) );
195  }
196  }
197  }
198  if ( fVerbose )
199  Abc_PrintTime( 1, "T", Abc_Clock() - clk );
200  // print the state
201  if ( fVerbose )
202  {
203  Saig_ManForEachPo( p, pObj, i )
204  {
205  if ( i < Saig_ManPoNum(p) - Saig_ManConstrNum(p) )
206  printf( "Primary output : " );
207  else
208  printf( "Constraint %3d : ", i-(Saig_ManPoNum(p) - Saig_ManConstrNum(p)) );
209  printf( "ProbOne = %f ", (float)Vec_IntEntry(vProbs, i)/(32*nWords*nFrames) );
210  printf( "ProbOneC = %f ", (float)Vec_IntEntry(vProbs2, i)/(32*nWords*nFrames) );
211  printf( "AllZeroValue = %d ", Aig_ObjPhase(pObj) );
212  printf( "\n" );
213  }
214  }
215 
216  // print the states
217  Vec_PtrFree( vInfo );
218  Vec_IntFree( vProbs );
219  Vec_IntFree( vProbs2 );
220  return RetValue;
221 }
222 
223 /**Function*************************************************************
224 
225  Synopsis [Creates COI of the property output.]
226 
227  Description []
228 
229  SideEffects []
230 
231  SeeAlso []
232 
233 ***********************************************************************/
234 Aig_Man_t * Saig_ManCreateIndMiter( Aig_Man_t * pAig, Vec_Vec_t * vCands )
235 {
236  int nFrames = 2;
237  Vec_Ptr_t * vNodes;
238  Aig_Man_t * pFrames;
239  Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
240  Aig_Obj_t ** pObjMap;
241  int i, f, k;
242 
243  // create mapping for the frames nodes
244  pObjMap = ABC_CALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
245 
246  // start the fraig package
247  pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
248  pFrames->pName = Abc_UtilStrsav( pAig->pName );
249  pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
250  // map constant nodes
251  for ( f = 0; f < nFrames; f++ )
252  Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
253  // create PI nodes for the frames
254  for ( f = 0; f < nFrames; f++ )
255  Aig_ManForEachPiSeq( pAig, pObj, i )
256  Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreateCi(pFrames) );
257  // set initial state for the latches
258  Aig_ManForEachLoSeq( pAig, pObj, i )
259  Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreateCi(pFrames) );
260 
261  // add timeframes
262  for ( f = 0; f < nFrames; f++ )
263  {
264  // add internal nodes of this frame
265  Aig_ManForEachNode( pAig, pObj, i )
266  {
267  pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Aig_ObjChild1Frames(pObjMap,nFrames,pObj,f) );
268  Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
269  }
270  // set the latch inputs and copy them into the latch outputs of the next frame
271  Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
272  {
273  pObjNew = Aig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f);
274  if ( f < nFrames - 1 )
275  Aig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew );
276  }
277  }
278 
279  // go through the candidates
280  Vec_VecForEachLevel( vCands, vNodes, i )
281  {
282  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
283  {
284  Aig_Obj_t * pObjR = Aig_Regular(pObj);
285  Aig_Obj_t * pNode0 = pObjMap[nFrames*Aig_ObjId(pObjR)+0];
286  Aig_Obj_t * pNode1 = pObjMap[nFrames*Aig_ObjId(pObjR)+1];
287  Aig_Obj_t * pFan0 = Aig_NotCond( pNode0, Aig_IsComplement(pObj) );
288  Aig_Obj_t * pFan1 = Aig_NotCond( pNode1, !Aig_IsComplement(pObj) );
289  Aig_Obj_t * pMiter = Aig_And( pFrames, pFan0, pFan1 );
290  Aig_ObjCreateCo( pFrames, pMiter );
291  }
292  }
293  Aig_ManCleanup( pFrames );
294  ABC_FREE( pObjMap );
295 
296 //Aig_ManShow( pAig, 0, NULL );
297 //Aig_ManShow( pFrames, 0, NULL );
298  return pFrames;
299 }
300 
301 /**Function*************************************************************
302 
303  Synopsis [Performs inductive check for one of the constraints.]
304 
305  Description []
306 
307  SideEffects []
308 
309  SeeAlso []
310 
311 ***********************************************************************/
312 int Saig_ManFilterUsingIndOne_new( Aig_Man_t * p, Aig_Man_t * pFrame, sat_solver * pSat, Cnf_Dat_t * pCnf, int nConfs, int nProps, int Counter )
313 {
314  Aig_Obj_t * pObj;
315  int Lit, status;
316  pObj = Aig_ManCo( pFrame, Counter );
317  Lit = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 );
318  status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 );
319  if ( status == l_False )
320  return 1;
321  if ( status == l_Undef )
322  {
323 // printf( "Solver returned undecided.\n" );
324  return 0;
325  }
326  assert( status == l_True );
327  return 0;
328 }
329 
330 /**Function*************************************************************
331 
332  Synopsis [Detects constraints functionally.]
333 
334  Description []
335 
336  SideEffects []
337 
338  SeeAlso []
339 
340 ***********************************************************************/
341 void Saig_ManFilterUsingInd( Aig_Man_t * p, Vec_Vec_t * vCands, int nConfs, int nProps, int fVerbose )
342 {
343  Vec_Ptr_t * vNodes;
344  Aig_Man_t * pFrames;
345  sat_solver * pSat;
346  Cnf_Dat_t * pCnf;
347  Aig_Obj_t * pObj;
348  int i, k, k2, Counter;
349 /*
350  Vec_VecForEachLevel( vCands, vNodes, i )
351  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
352  printf( "%d ", Aig_ObjId(Aig_Regular(pObj)) );
353  printf( "\n" );
354 */
355  // create timeframes
356 // pFrames = Saig_ManUnrollInd( p );
357  pFrames = Saig_ManCreateIndMiter( p, vCands );
358  assert( Aig_ManCoNum(pFrames) == Vec_VecSizeSize(vCands) );
359  // start the SAT solver
360  pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) );
361  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
362  // check candidates
363  if ( fVerbose )
364  printf( "Filtered cands: " );
365  Counter = 0;
366  Vec_VecForEachLevel( vCands, vNodes, i )
367  {
368  k2 = 0;
369  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
370  {
371  if ( Saig_ManFilterUsingIndOne_new( p, pFrames, pSat, pCnf, nConfs, nProps, Counter++ ) )
372 // if ( Saig_ManFilterUsingIndOne_old( p, pSat, pCnf, nConfs, pObj ) )
373  {
374  Vec_PtrWriteEntry( vNodes, k2++, pObj );
375  if ( fVerbose )
376  printf( "%d:%s%d ", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
377  }
378  }
379  Vec_PtrShrink( vNodes, k2 );
380  }
381  if ( fVerbose )
382  printf( "\n" );
383  // clean up
384  Cnf_DataFree( pCnf );
385  sat_solver_delete( pSat );
386  if ( fVerbose )
387  Aig_ManPrintStats( pFrames );
388  Aig_ManStop( pFrames );
389 }
390 
391 
392 
393 
394 /**Function*************************************************************
395 
396  Synopsis [Creates COI of the property output.]
397 
398  Description []
399 
400  SideEffects []
401 
402  SeeAlso []
403 
404 ***********************************************************************/
405 Aig_Man_t * Saig_ManUnrollCOI_( Aig_Man_t * p, int nFrames )
406 {
407  Aig_Man_t * pFrames;
408  Aig_Obj_t ** pObjMap;
409  int i;
410 //Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFrames, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t *** ppObjMap )
411  pFrames = Aig_ManFrames( p, nFrames, 0, 1, 1, 0, &pObjMap );
412  for ( i = 0; i < nFrames * Aig_ManObjNumMax(p); i++ )
413  if ( pObjMap[i] && Aig_ObjIsNone( Aig_Regular(pObjMap[i]) ) )
414  pObjMap[i] = NULL;
415  assert( p->pObjCopies == NULL );
416  p->pObjCopies = pObjMap;
417  return pFrames;
418 }
419 
420 /**Function*************************************************************
421 
422  Synopsis [Creates COI of the property output.]
423 
424  Description []
425 
426  SideEffects []
427 
428  SeeAlso []
429 
430 ***********************************************************************/
431 Aig_Man_t * Saig_ManUnrollCOI( Aig_Man_t * pAig, int nFrames )
432 {
433  Aig_Man_t * pFrames;
434  Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
435  Aig_Obj_t ** pObjMap;
436  int i, f;
437  // create mapping for the frames nodes
438  pObjMap = ABC_CALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
439  // start the fraig package
440  pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
441  pFrames->pName = Abc_UtilStrsav( pAig->pName );
442  pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
443  // map constant nodes
444  for ( f = 0; f < nFrames; f++ )
445  Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
446  // create PI nodes for the frames
447  for ( f = 0; f < nFrames; f++ )
448  Aig_ManForEachPiSeq( pAig, pObj, i )
449  Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreateCi(pFrames) );
450  // set initial state for the latches
451  Aig_ManForEachLoSeq( pAig, pObj, i )
452  Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreateCi(pFrames) );
453  // add timeframes
454  for ( f = 0; f < nFrames; f++ )
455  {
456  Aig_ManForEachNode( pAig, pObj, i )
457  {
458  pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Aig_ObjChild1Frames(pObjMap,nFrames,pObj,f) );
459  Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
460  }
461  // set the latch inputs and copy them into the latch outputs of the next frame
462  Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
463  {
464  pObjNew = Aig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f);
465  if ( f < nFrames - 1 )
466  Aig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew );
467  }
468  }
469  // create the only output
470  for ( f = nFrames-1; f < nFrames; f++ )
471  {
472  Aig_ManForEachPoSeq( pAig, pObj, i )
473  {
474  pObjNew = Aig_ObjCreateCo( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f) );
475  Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
476  }
477  }
478  // created lots of dangling nodes - no sweeping!
479  //Aig_ManCleanup( pFrames );
480  assert( pAig->pObjCopies == NULL );
481  pAig->pObjCopies = pObjMap;
482  return pFrames;
483 }
484 
485 
486 /**Function*************************************************************
487 
488  Synopsis [Collects and saves values of the SAT variables.]
489 
490  Description []
491 
492  SideEffects []
493 
494  SeeAlso []
495 
496 ***********************************************************************/
497 void Saig_CollectSatValues( sat_solver * pSat, Cnf_Dat_t * pCnf, Vec_Ptr_t * vInfo, int * piPat )
498 {
499  Aig_Obj_t * pObj;
500  unsigned * pInfo;
501  int i;
502  Aig_ManForEachObj( pCnf->pMan, pObj, i )
503  {
504  if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
505  continue;
506  assert( pCnf->pVarNums[i] > 0 );
507  pInfo = (unsigned *)Vec_PtrEntry( vInfo, i );
508  if ( Abc_InfoHasBit(pInfo, *piPat) != sat_solver_var_value(pSat, pCnf->pVarNums[i]) )
509  Abc_InfoXorBit(pInfo, *piPat);
510  }
511 }
512 
513 /**Function*************************************************************
514 
515  Synopsis [Runs the SAT test for the node in one polarity.]
516 
517  Description []
518 
519  SideEffects []
520 
521  SeeAlso []
522 
523 ***********************************************************************/
524 int Saig_DetectTryPolarity( sat_solver * pSat, int nConfs, int nProps, Cnf_Dat_t * pCnf, Aig_Obj_t * pObj, int iPol, Vec_Ptr_t * vInfo, int * piPat, int fVerbose )
525 {
526  Aig_Obj_t * pOut = Aig_ManCo( pCnf->pMan, 0 );
527  int status, Lits[2];
528 // ABC_INT64_T nOldConfs = pSat->stats.conflicts;
529 // ABC_INT64_T nOldImps = pSat->stats.propagations;
530  Lits[0] = toLitCond( pCnf->pVarNums[Aig_ObjId(pOut)], 0 );
531  Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !iPol );
532  status = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nConfs, (ABC_INT64_T)nProps, 0, 0 );
533  if ( status == l_False )
534  {
535 // printf( "u%d(%d) ", (int)(pSat->stats.conflicts-nOldConfs), (int)(pSat->stats.propagations-nOldImps) );
536  return 1;
537  }
538  if ( status == l_Undef )
539  {
540 // printf( "Solver returned undecided.\n" );
541  return 0;
542  }
543 // printf( "s%d(%d) ", (int)(pSat->stats.conflicts-nOldConfs), (int)(pSat->stats.propagations-nOldImps) );
544  assert( status == l_True );
545  Saig_CollectSatValues( pSat, pCnf, vInfo, piPat );
546  (*piPat)++;
547  if ( *piPat == Vec_PtrReadWordsSimInfo(vInfo) * 32 )
548  {
549  if ( fVerbose )
550  printf( "Warning: Reached the limit on the number of patterns.\n" );
551  *piPat = 0;
552  }
553  return 0;
554 }
555 
556 /**Function*************************************************************
557 
558  Synopsis [Returns the number of variables implied by the output.]
559 
560  Description []
561 
562  SideEffects []
563 
564  SeeAlso []
565 
566 ***********************************************************************/
567 Vec_Vec_t * Ssw_ManFindDirectImplications( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fVerbose )
568 {
569  Vec_Vec_t * vCands = NULL;
570  Vec_Ptr_t * vNodes;
571  Cnf_Dat_t * pCnf;
572  sat_solver * pSat;
573  Aig_Man_t * pFrames;
574  Aig_Obj_t * pObj, * pRepr, * pReprR;
575  int i, f, k, value;
576  vCands = Vec_VecAlloc( nFrames );
577 
578  // perform unrolling
579  pFrames = Saig_ManUnrollCOI( p, nFrames );
580  assert( Aig_ManCoNum(pFrames) == 1 );
581  // start the SAT solver
582  pCnf = Cnf_DeriveSimple( pFrames, 0 );
583  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
584  if ( pSat != NULL )
585  {
586  Aig_ManIncrementTravId( p );
587  for ( f = 0; f < nFrames; f++ )
588  {
589  Aig_ManForEachObj( p, pObj, i )
590  {
591  if ( !Aig_ObjIsCand(pObj) )
592  continue;
593  if ( Aig_ObjIsTravIdCurrent(p, pObj) )
594  continue;
595  // get the node from timeframes
596  pRepr = p->pObjCopies[nFrames*i + nFrames-1-f];
597  pReprR = Aig_Regular(pRepr);
598  if ( pCnf->pVarNums[Aig_ObjId(pReprR)] < 0 )
599  continue;
600 // value = pSat->assigns[ pCnf->pVarNums[Aig_ObjId(pReprR)] ];
601  value = sat_solver_get_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pReprR)] );
602  if ( value == l_Undef )
603  continue;
604  // label this node as taken
605  Aig_ObjSetTravIdCurrent(p, pObj);
606  if ( Saig_ObjIsLo(p, pObj) )
607  Aig_ObjSetTravIdCurrent( p, Aig_ObjFanin0(Saig_ObjLoToLi(p, pObj)) );
608  // remember the node
609  Vec_VecPush( vCands, f, Aig_NotCond( pObj, (value == l_True) ^ Aig_IsComplement(pRepr) ) );
610  // printf( "%s%d ", (value == l_False)? "":"!", i );
611  }
612  }
613  // printf( "\n" );
614  sat_solver_delete( pSat );
615  }
616  Aig_ManStop( pFrames );
617  Cnf_DataFree( pCnf );
618 
619  if ( fVerbose )
620  {
621  printf( "Found %3d candidates.\n", Vec_VecSizeSize(vCands) );
622  Vec_VecForEachLevel( vCands, vNodes, k )
623  {
624  printf( "Level %d. Cands =%d ", k, Vec_PtrSize(vNodes) );
625 // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
626 // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
627  printf( "\n" );
628  }
629  }
630 
631  ABC_FREE( p->pObjCopies );
632  Saig_ManFilterUsingInd( p, vCands, nConfs, nProps, fVerbose );
633  if ( Vec_VecSizeSize(vCands) )
634  printf( "Found %3d constraints after filtering.\n", Vec_VecSizeSize(vCands) );
635  if ( fVerbose )
636  {
637  Vec_VecForEachLevel( vCands, vNodes, k )
638  {
639  printf( "Level %d. Constr =%d ", k, Vec_PtrSize(vNodes) );
640 // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
641 // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
642  printf( "\n" );
643  }
644  }
645 
646  return vCands;
647 }
648 
649 
650 /**Function*************************************************************
651 
652  Synopsis [Detects constraints functionally.]
653 
654  Description []
655 
656  SideEffects []
657 
658  SeeAlso []
659 
660 ***********************************************************************/
661 Vec_Vec_t * Saig_ManDetectConstrFunc( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fVerbose )
662 {
663  int iPat = 0, nWordsAlloc = 16;
664  Bar_Progress_t * pProgress = NULL;
665  Vec_Vec_t * vCands = NULL;
666  Vec_Ptr_t * vInfo, * vNodes;
667  Aig_Obj_t * pObj, * pRepr, * pObjNew;
668  Aig_Man_t * pFrames;
669  sat_solver * pSat;
670  Cnf_Dat_t * pCnf;
671  unsigned * pInfo;
672  int i, j, k, Lit, status, nCands = 0;
673  assert( Saig_ManPoNum(p) == 1 );
674  if ( Saig_ManPoNum(p) != 1 )
675  {
676  printf( "The number of outputs is different from 1.\n" );
677  return NULL;
678  }
679 //printf( "Implications = %d.\n", Ssw_ManCountImplications(p, nFrames) );
680 
681  // perform unrolling
682  pFrames = Saig_ManUnrollCOI( p, nFrames );
683  assert( Aig_ManCoNum(pFrames) == 1 );
684  if ( fVerbose )
685  {
686  printf( "Detecting constraints with %d frames, %d conflicts, and %d propagations.\n", nFrames, nConfs, nProps );
687  printf( "Frames: " );
688  Aig_ManPrintStats( pFrames );
689  }
690 // Aig_ManShow( pFrames, 0, NULL );
691 
692  // start the SAT solver
693  pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) );
694  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
695 //printf( "Implications = %d.\n", pSat->qhead );
696 
697  // solve the original problem
698  Lit = toLitCond( pCnf->pVarNums[Aig_ObjId(Aig_ManCo(pFrames,0))], 0 );
699  status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 );
700  if ( status == l_False )
701  {
702  printf( "The problem is trivially UNSAT (inductive with k=%d).\n", nFrames-1 );
703  Cnf_DataFree( pCnf );
704  sat_solver_delete( pSat );
705  Aig_ManStop( pFrames );
706  return NULL;
707  }
708  if ( status == l_Undef )
709  {
710  printf( "Solver could not solve the original problem.\n" );
711  Cnf_DataFree( pCnf );
712  sat_solver_delete( pSat );
713  Aig_ManStop( pFrames );
714  return NULL;
715  }
716  assert( status == l_True );
717 
718  // create simulation info
719  vInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pFrames), nWordsAlloc );
720  Vec_PtrCleanSimInfo( vInfo, 0, nWordsAlloc );
721  Saig_CollectSatValues( pSat, pCnf, vInfo, &iPat );
722  Aig_ManForEachObj( pFrames, pObj, i )
723  {
724  pInfo = (unsigned *)Vec_PtrEntry( vInfo, i );
725  if ( pInfo[0] & 1 )
726  memset( (char*)pInfo, 0xff, 4*nWordsAlloc );
727  }
728 // Aig_ManShow( pFrames, 0, NULL );
729 // Aig_ManShow( p, 0, NULL );
730 
731  // consider the nodes for ci=>!Out and label when it holds
732  pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pFrames) );
733  Aig_ManCleanMarkAB( pFrames );
734  Aig_ManForEachObj( pFrames, pObj, i )
735  {
736  if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
737  continue;
738  Bar_ProgressUpdate( pProgress, i, NULL );
739  // check if the node is available in both polarities
740  pInfo = (unsigned *)Vec_PtrEntry( vInfo, i );
741  for ( k = 0; k < nWordsAlloc; k++ )
742  if ( pInfo[k] != ~0 )
743  break;
744  if ( k == nWordsAlloc )
745  {
746  if ( Saig_DetectTryPolarity(pSat, nConfs, nProps, pCnf, pObj, 0, vInfo, &iPat, fVerbose) ) // !pObj is a constr
747  {
748  pObj->fMarkA = 1, nCands++;
749 // printf( "!%d ", Aig_ObjId(pObj) );
750  }
751  continue;
752  }
753  for ( k = 0; k < nWordsAlloc; k++ )
754  if ( pInfo[k] != 0 )
755  break;
756  if ( k == nWordsAlloc )
757  {
758  if ( Saig_DetectTryPolarity(pSat, nConfs, nProps, pCnf, pObj, 1, vInfo, &iPat, fVerbose) ) // pObj is a constr
759  {
760  pObj->fMarkB = 1, nCands++;
761 // printf( "%d ", Aig_ObjId(pObj) );
762  }
763  continue;
764  }
765  }
766  Bar_ProgressStop( pProgress );
767  if ( nCands )
768  {
769 
770 // printf( "\n" );
771  if ( fVerbose )
772  printf( "Found %3d classes of candidates.\n", nCands );
773  vCands = Vec_VecAlloc( nFrames );
774  for ( k = 0; k < nFrames; k++ )
775  {
776  Aig_ManForEachObj( p, pObj, i )
777  {
778  if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
779  continue;
780  pRepr = p->pObjCopies[nFrames*i + nFrames-1-k];
781 // pRepr = p->pObjCopies[nFrames*i + k];
782  if ( pRepr == NULL )
783  continue;
784  if ( Aig_Regular(pRepr)->fMarkA ) // !pObj is a constr
785  {
786  pObjNew = Aig_NotCond(pObj, !Aig_IsComplement(pRepr));
787 
788  for ( j = 0; j < k; j++ )
789  if ( Vec_PtrFind( Vec_VecEntry(vCands, j), pObjNew ) >= 0 )
790  break;
791  if ( j == k )
792  Vec_VecPush( vCands, k, pObjNew );
793 // printf( "%d->!%d ", Aig_ObjId(Aig_Regular(pRepr)), Aig_ObjId(pObj) );
794  }
795  else if ( Aig_Regular(pRepr)->fMarkB ) // pObj is a constr
796  {
797  pObjNew = Aig_NotCond(pObj, Aig_IsComplement(pRepr));
798 
799  for ( j = 0; j < k; j++ )
800  if ( Vec_PtrFind( Vec_VecEntry(vCands, j), pObjNew ) >= 0 )
801  break;
802  if ( j == k )
803  Vec_VecPush( vCands, k, pObjNew );
804 // printf( "%d->%d ", Aig_ObjId(Aig_Regular(pRepr)), Aig_ObjId(pObj) );
805  }
806  }
807  }
808 
809 // printf( "\n" );
810  if ( fVerbose )
811  {
812  printf( "Found %3d candidates.\n", Vec_VecSizeSize(vCands) );
813  Vec_VecForEachLevel( vCands, vNodes, k )
814  {
815  printf( "Level %d. Cands =%d ", k, Vec_PtrSize(vNodes) );
816 // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
817 // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
818  printf( "\n" );
819  }
820  }
821 
822  ABC_FREE( p->pObjCopies );
823  Saig_ManFilterUsingInd( p, vCands, nConfs, nProps, fVerbose );
824  if ( Vec_VecSizeSize(vCands) )
825  printf( "Found %3d constraints after filtering.\n", Vec_VecSizeSize(vCands) );
826  if ( fVerbose )
827  {
828  Vec_VecForEachLevel( vCands, vNodes, k )
829  {
830  printf( "Level %d. Constr =%d ", k, Vec_PtrSize(vNodes) );
831 // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
832 // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
833  printf( "\n" );
834  }
835  }
836  }
837  Vec_PtrFree( vInfo );
838  Cnf_DataFree( pCnf );
839  sat_solver_delete( pSat );
840  Aig_ManCleanMarkAB( pFrames );
841  Aig_ManStop( pFrames );
842  return vCands;
843 }
844 
845 /**Function*************************************************************
846 
847  Synopsis [Experimental procedure.]
848 
849  Description []
850 
851  SideEffects []
852 
853  SeeAlso []
854 
855 ***********************************************************************/
856 void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose )
857 {
858  Vec_Vec_t * vCands;
859  if ( fOldAlgo )
860  vCands = Saig_ManDetectConstrFunc( p, nFrames, nConfs, nProps, fVerbose );
861  else
862  vCands = Ssw_ManFindDirectImplications( p, nFrames, nConfs, nProps, fVerbose );
863  Vec_VecFreeP( &vCands );
864 }
865 
866 /**Function*************************************************************
867 
868  Synopsis [Duplicates the AIG while unfolding constraints.]
869 
870  Description []
871 
872  SideEffects []
873 
874  SeeAlso []
875 
876 ***********************************************************************/
877 Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose )
878 {
879  Aig_Man_t * pNew;
880  Vec_Vec_t * vCands;
881  Vec_Ptr_t * vNodes, * vNewFlops;
882  Aig_Obj_t * pObj;
883  int i, j, k, nNewFlops;
884  if ( fOldAlgo )
885  vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose );
886  else
887  vCands = Ssw_ManFindDirectImplications( pAig, nFrames, nConfs, nProps, fVerbose );
888  if ( vCands == NULL || Vec_VecSizeSize(vCands) == 0 )
889  {
890  Vec_VecFreeP( &vCands );
891  return Aig_ManDupDfs( pAig );
892  }
893  // create new manager
894  pNew = Aig_ManDupWithoutPos( pAig );
895  pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands);
896  // add normal POs
897  Saig_ManForEachPo( pAig, pObj, i )
898  Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
899  // create constraint outputs
900  vNewFlops = Vec_PtrAlloc( 100 );
901  Vec_VecForEachLevel( vCands, vNodes, i )
902  {
903  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
904  {
905  Vec_PtrPush( vNewFlops, Aig_ObjRealCopy(pObj) );
906  for ( j = 0; j < i; j++ )
907  Vec_PtrPush( vNewFlops, Aig_ObjCreateCi(pNew) );
908  Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrPop(vNewFlops) );
909  }
910  }
911  // add latch outputs
912  Saig_ManForEachLi( pAig, pObj, i )
913  Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
914  // add new latch outputs
915  nNewFlops = 0;
916  Vec_VecForEachLevel( vCands, vNodes, i )
917  {
918  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
919  {
920  for ( j = 0; j < i; j++ )
921  Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vNewFlops, nNewFlops++) );
922  }
923  }
924  assert( nNewFlops == Vec_PtrSize(vNewFlops) );
925  Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + nNewFlops );
926  Vec_VecFreeP( &vCands );
927  Vec_PtrFree( vNewFlops );
928  return pNew;
929 }
930 
931 /**Function*************************************************************
932 
933  Synopsis [Duplicates the AIG while unfolding constraints.]
934 
935  Description []
936 
937  SideEffects []
938 
939  SeeAlso []
940 
941 ***********************************************************************/
942 Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose )
943 {
944  Aig_Man_t * pAigNew;
945  Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
946  int i;
947  if ( Aig_ManConstrNum(pAig) == 0 )
948  return Aig_ManDupDfs( pAig );
949  assert( Aig_ManConstrNum(pAig) < Saig_ManPoNum(pAig) );
950  // start the new manager
951  pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
952  pAigNew->pName = Abc_UtilStrsav( pAig->pName );
953  pAigNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
954  // map the constant node
955  Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
956  // create variables for PIs
957  Aig_ManForEachCi( pAig, pObj, i )
958  pObj->pData = Aig_ObjCreateCi( pAigNew );
959  // add internal nodes of this frame
960  Aig_ManForEachNode( pAig, pObj, i )
961  pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
962 
963  // OR the constraint outputs
964  pMiter = Aig_ManConst0( pAigNew );
965  Saig_ManForEachPo( pAig, pObj, i )
966  {
967  if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
968  continue;
969  pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
970  }
971 
972  // create additional flop
973  if ( Saig_ManRegNum(pAig) > 0 )
974  {
975  pFlopOut = Aig_ObjCreateCi( pAigNew );
976  pFlopIn = Aig_Or( pAigNew, pMiter, pFlopOut );
977  }
978  else
979  pFlopIn = pMiter;
980 
981  // create primary output
982  Saig_ManForEachPo( pAig, pObj, i )
983  {
984  if ( i >= Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
985  continue;
986  pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
987  Aig_ObjCreateCo( pAigNew, pMiter );
988  }
989 
990  // transfer to register outputs
991  Saig_ManForEachLi( pAig, pObj, i )
992  Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
993 
994  // create additional flop
995  if ( Saig_ManRegNum(pAig) > 0 )
996  {
997  Aig_ObjCreateCo( pAigNew, pFlopIn );
998  Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 );
999  }
1000 
1001  // perform cleanup
1002  Aig_ManCleanup( pAigNew );
1003  Aig_ManSeqCleanup( pAigNew );
1004  return pAigNew;
1005 }
1006 
1007 ////////////////////////////////////////////////////////////////////////
1008 /// END OF FILE ///
1009 ////////////////////////////////////////////////////////////////////////
1010 
1011 #include "saigUnfold2.c"
1012 ABC_NAMESPACE_IMPL_END
1013 
memset
char * memset()
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Vec_VecForEachLevel
#define Vec_VecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition: vecVec.h:55
Aig_ObjFrames
static ABC_NAMESPACE_IMPL_START Aig_Obj_t * Aig_ObjFrames(Aig_Obj_t **pObjMap, int nFs, Aig_Obj_t *pObj, int i)
DECLARATIONS ///.
Definition: saigConstr2.c:35
Aig_ObjChild0Frames
static Aig_Obj_t * Aig_ObjChild0Frames(Aig_Obj_t **pObjMap, int nFs, Aig_Obj_t *pObj, int i)
Definition: saigConstr2.c:38
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Aig_ObjPhase
static int Aig_ObjPhase(Aig_Obj_t *pObj)
Definition: aig.h:298
Vec_VecPush
static void Vec_VecPush(Vec_Vec_t *p, int Level, void *Entry)
Definition: vecVec.h:456
Vec_VecAlloc
static Vec_Vec_t * Vec_VecAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecVec.h:145
Aig_ObjFaninId0
static int Aig_ObjFaninId0(Aig_Obj_t *pObj)
Definition: aig.h:304
Aig_ManConstrNum
static int Aig_ManConstrNum(Aig_Man_t *p)
Definition: aig.h:261
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
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_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
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Aig_ManSeqCleanup
int Aig_ManSeqCleanup(Aig_Man_t *p)
Definition: aigScl.c:158
l_Undef
#define l_Undef
Definition: SolverTypes.h:86
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition: aig.h:80
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_Obj_t_::pData
void * pData
Definition: aig.h:87
Abc_InfoXorBit
static void Abc_InfoXorBit(unsigned *p, int i)
Definition: abc_global.h:260
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
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_ManDupDfs
Aig_Man_t * Aig_ManDupDfs(Aig_Man_t *p)
Definition: aigDup.c:563
Aig_ManPrintStats
void Aig_ManPrintStats(Aig_Man_t *p)
Definition: aigMan.c:379
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Vec_PtrCleanSimInfo
static void Vec_PtrCleanSimInfo(Vec_Ptr_t *vInfo, int iWord, int nWords)
Definition: vecPtr.h:968
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition: cnf.h:63
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition: aig.h:79
Aig_ManConst0
static Aig_Obj_t * Aig_ManConst0(Aig_Man_t *p)
Definition: aig.h:263
l_True
#define l_True
Definition: SolverTypes.h:84
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Saig_ManUnrollCOI
Aig_Man_t * Saig_ManUnrollCOI(Aig_Man_t *pAig, int nFrames)
Definition: saigConstr2.c:431
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
Aig_Not
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
Aig_ObjSetFrames
static void Aig_ObjSetFrames(Aig_Obj_t **pObjMap, int nFs, Aig_Obj_t *pObj, int i, Aig_Obj_t *pNode)
Definition: saigConstr2.c:36
Aig_ObjFaninId1
static int Aig_ObjFaninId1(Aig_Obj_t *pObj)
Definition: aig.h:305
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Cnf_Dat_t_::pMan
Aig_Man_t * pMan
Definition: cnf.h:58
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Cnf_Dat_t_
Definition: cnf.h:56
Vec_PtrPop
static void * Vec_PtrPop(Vec_Ptr_t *p)
Definition: vecPtr.h:677
nWords
int nWords
Definition: abcNpn.c:127
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Aig_ManNodeNum
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Vec_PtrFind
static int Vec_PtrFind(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:694
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Aig_ManFrames
Aig_Man_t * Aig_ManFrames(Aig_Man_t *pAig, int nFs, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t ***ppObjMap)
FUNCTION DEFINITIONS ///.
Definition: aigFrames.c:51
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Saig_ManFilterUsingInd
void Saig_ManFilterUsingInd(Aig_Man_t *p, Vec_Vec_t *vCands, int nConfs, int nProps, int fVerbose)
Definition: saigConstr2.c:341
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Saig_ManFilterUsingIndOne_new
int Saig_ManFilterUsingIndOne_new(Aig_Man_t *p, Aig_Man_t *pFrame, sat_solver *pSat, Cnf_Dat_t *pCnf, int nConfs, int nProps, int Counter)
Definition: saigConstr2.c:312
Aig_ObjRealCopy
static Aig_Obj_t * Aig_ObjRealCopy(Aig_Obj_t *pObj)
Definition: aig.h:320
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Saig_ManConstrNum
static int Saig_ManConstrNum(Aig_Man_t *p)
Definition: saig.h:78
Aig_WordCountOnes
static int Aig_WordCountOnes(unsigned uWord)
Definition: aig.h:229
Bar_ProgressUpdate
static void Bar_ProgressUpdate(Bar_Progress_t *p, int nItemsCur, char *pString)
Definition: bar.h:63
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Aig_ManSetRegNum
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Vec_IntAddToEntry
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
Aig_ManForEachLiLoSeq
#define Aig_ManForEachLiLoSeq(p, pObjLi, pObjLo, k)
Definition: aig.h:450
Aig_ObjIsNone
static int Aig_ObjIsNone(Aig_Obj_t *pObj)
Definition: aig.h:273
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
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Aig_ObjChild1Copy
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
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
Counter
static int Counter
Definition: extraBddMisc.c:1877
Aig_ObjChild1Frames
static Aig_Obj_t * Aig_ObjChild1Frames(Aig_Obj_t **pObjMap, int nFs, Aig_Obj_t *pObj, int i)
Definition: saigConstr2.c:39
Aig_ObjChild0Copy
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
Bar_Progress_t_
DECLARATIONS ///.
Definition: bar.c:36
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Saig_ManRegNum
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
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
Saig_DetectTryPolarity
int Saig_DetectTryPolarity(sat_solver *pSat, int nConfs, int nProps, Cnf_Dat_t *pCnf, Aig_Obj_t *pObj, int iPol, Vec_Ptr_t *vInfo, int *piPat, int fVerbose)
Definition: saigConstr2.c:524
Saig_CollectSatValues
void Saig_CollectSatValues(sat_solver *pSat, Cnf_Dat_t *pCnf, Vec_Ptr_t *vInfo, int *piPat)
Definition: saigConstr2.c:497
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Vec_PtrReadWordsSimInfo
static int Vec_PtrReadWordsSimInfo(Vec_Ptr_t *p)
Definition: vecPtr.h:952
Cnf_DataWriteIntoSolver
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:463
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Cnf_DeriveSimple
Cnf_Dat_t * Cnf_DeriveSimple(Aig_Man_t *p, int nOutputs)
Definition: cnfWrite.c:587
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Saig_ManDupUnfoldConstrsFunc
Aig_Man_t * Saig_ManDupUnfoldConstrsFunc(Aig_Man_t *pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose)
Definition: saigConstr2.c:877
Aig_ManCleanMarkAB
void Aig_ManCleanMarkAB(Aig_Man_t *p)
Definition: aigUtil.c:186
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Vec_VecSizeSize
static int Vec_VecSizeSize(Vec_Vec_t *p)
Definition: vecVec.h:417
Aig_ObjIsCand
static int Aig_ObjIsCand(Aig_Obj_t *pObj)
Definition: aig.h:284
Aig_ManForEachLoSeq
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition: aig.h:441
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
l_False
#define l_False
Definition: SolverTypes.h:85
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Saig_ManDetectConstrFunc
Vec_Vec_t * Saig_ManDetectConstrFunc(Aig_Man_t *p, int nFrames, int nConfs, int nProps, int fVerbose)
Definition: saigConstr2.c:661
Saig_ManUnrollCOI_
Aig_Man_t * Saig_ManUnrollCOI_(Aig_Man_t *p, int nFrames)
Definition: saigConstr2.c:405
Saig_ManDetectConstrFuncTest
void Saig_ManDetectConstrFuncTest(Aig_Man_t *p, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose)
Definition: saigConstr2.c:856
value
int value
Definition: misc/espresso/main.h:90
sat_solver_t
Definition: satSolver.h:91
Vec_VecFreeP
static void Vec_VecFreeP(Vec_Vec_t **p)
Definition: vecVec.h:367
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
assert
#define assert(ex)
Definition: util_old.h:213
Saig_ManDupFoldConstrsFunc
Aig_Man_t * Saig_ManDupFoldConstrsFunc(Aig_Man_t *pAig, int fCompl, int fVerbose)
Definition: saigConstr2.c:942
Ssw_ManFindDirectImplications
Vec_Vec_t * Ssw_ManFindDirectImplications(Aig_Man_t *p, int nFrames, int nConfs, int nProps, int fVerbose)
Definition: saigConstr2.c:567
Vec_VecEntry
static Vec_Ptr_t * Vec_VecEntry(Vec_Vec_t *p, int i)
Definition: vecVec.h:271
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
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
Aig_ManForEachPoSeq
#define Aig_ManForEachPoSeq(p, pObj, i)
Definition: aig.h:444
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Vec_PtrShrink
static void Vec_PtrShrink(Vec_Ptr_t *p, int nSizeNew)
Definition: vecPtr.h:528
Aig_ManDupWithoutPos
Aig_Man_t * Aig_ManDupWithoutPos(Aig_Man_t *p)
Definition: aigDup.c:835
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
sat_solver_get_var_value
int sat_solver_get_var_value(sat_solver *s, int v)
Definition: satSolver.c:117
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Bar_ProgressStop
void Bar_ProgressStop(Bar_Progress_t *p)
Definition: bar.c:126
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Saig_ManCreateIndMiter
Aig_Man_t * Saig_ManCreateIndMiter(Aig_Man_t *pAig, Vec_Vec_t *vCands)
Definition: saigConstr2.c:234
Bar_ProgressStart
Bar_Progress_t * Bar_ProgressStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition: bar.c:66
Aig_ManForEachPiSeq
#define Aig_ManForEachPiSeq(p, pObj, i)
SEQUENTIAL ITERATORS ///.
Definition: aig.h:438
Vec_PtrAllocSimInfo
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Ssw_ManProfileConstraints
int Ssw_ManProfileConstraints(Aig_Man_t *p, int nWords, int nFrames, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition: saigConstr2.c:56
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91