abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fraInd.c File Reference
#include "fra.h"
#include "sat/cnf/cnf.h"
#include "opt/dar/dar.h"
#include "aig/saig/saig.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Fra_FraigInductionRewrite (Fra_Man_t *p)
 DECLARATIONS ///. More...
 
static void Fra_FramesConstrainNode (Aig_Man_t *pManFraig, Aig_Obj_t *pObj, int iFrame)
 
Aig_Man_tFra_FramesWithClasses (Fra_Man_t *p)
 
void Fra_FramesAddMore (Aig_Man_t *p, int nFrames)
 
Aig_Man_tFra_FraigInductionPart (Aig_Man_t *pAig, Fra_Ssw_t *pPars)
 
Aig_Man_tFra_FraigInduction (Aig_Man_t *pManAig, Fra_Ssw_t *pParams)
 
int Fra_FraigInductionTest (char *pFileName, Fra_Ssw_t *pParams)
 

Function Documentation

Aig_Man_t* Fra_FraigInduction ( Aig_Man_t pManAig,
Fra_Ssw_t pParams 
)

Function*************************************************************

Synopsis [Performs sequential SAT sweeping.]

Description []

SideEffects []

SeeAlso []

Definition at line 344 of file fraInd.c.

345 {
346  int fUseSimpleCnf = 0;
347  int fUseOldSimulation = 0;
348  // other paramaters affecting performance
349  // - presence of FRAIGing in Abc_NtkDarSeqSweep()
350  // - using distance-1 patterns in Fra_SmlAssignDist1()
351  // - the number of simulation patterns
352  // - the number of BMC frames
353 
354  Fra_Man_t * p;
355  Fra_Par_t Pars, * pPars = &Pars;
356  Aig_Obj_t * pObj;
357  Cnf_Dat_t * pCnf;
358  Aig_Man_t * pManAigNew = NULL;
359  int nNodesBeg, nRegsBeg;
360  int nIter = -1; // Suppress "might be used uninitialized"
361  int i;
362  abctime clk = Abc_Clock(), clk2;
363  abctime TimeToStop = pParams->TimeLimit ? pParams->TimeLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;
364 
365  if ( Aig_ManNodeNum(pManAig) == 0 )
366  {
367  pParams->nIters = 0;
368  // Ntl_ManFinalize() needs the following to satisfy an assertion
369  Aig_ManReprStart(pManAig,Aig_ManObjNumMax(pManAig));
370  return Aig_ManDupOrdered(pManAig);
371  }
372  assert( Aig_ManRegNum(pManAig) > 0 );
373  assert( pParams->nFramesK > 0 );
374 //Aig_ManShow( pManAig, 0, NULL );
375 
376  if ( pParams->fWriteImps && pParams->nPartSize > 0 )
377  {
378  pParams->nPartSize = 0;
379  printf( "Partitioning was disabled to allow implication writing.\n" );
380  }
381  // perform partitioning
382  if ( (pParams->nPartSize > 0 && pParams->nPartSize < Aig_ManRegNum(pManAig))
383  || (pManAig->vClockDoms && Vec_VecSize(pManAig->vClockDoms) > 0) )
384  return Fra_FraigInductionPart( pManAig, pParams );
385 
386  nNodesBeg = Aig_ManNodeNum(pManAig);
387  nRegsBeg = Aig_ManRegNum(pManAig);
388 
389  // enhance the AIG by adding timeframes
390 // Fra_FramesAddMore( pManAig, 3 );
391 
392  // get parameters
393  Fra_ParamsDefaultSeq( pPars );
394  pPars->nFramesP = pParams->nFramesP;
395  pPars->nFramesK = pParams->nFramesK;
396  pPars->nMaxImps = pParams->nMaxImps;
397  pPars->nMaxLevs = pParams->nMaxLevs;
398  pPars->fVerbose = pParams->fVerbose;
399  pPars->fRewrite = pParams->fRewrite;
400  pPars->fLatchCorr = pParams->fLatchCorr;
401  pPars->fUseImps = pParams->fUseImps;
402  pPars->fWriteImps = pParams->fWriteImps;
403  pPars->fUse1Hot = pParams->fUse1Hot;
404 
405  assert( !(pPars->nFramesP > 0 && pPars->fUse1Hot) );
406  assert( !(pPars->nFramesK > 1 && pPars->fUse1Hot) );
407 
408  // start the fraig manager for this run
409  p = Fra_ManStart( pManAig, pPars );
410  p->pPars->nBTLimitNode = 0;
411  // derive and refine e-classes using K initialized frames
412  if ( fUseOldSimulation )
413  {
414  if ( pPars->nFramesP > 0 )
415  {
416  pPars->nFramesP = 0;
417  printf( "Fra_FraigInduction(): Prefix cannot be used.\n" );
418  }
419  p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
420  Fra_SmlSimulate( p, 1 );
421  }
422  else
423  {
424  // bug: r iscas/blif/s5378.blif ; st; ssw -v
425  // bug: r iscas/blif/s1238.blif ; st; ssw -v
426  // refine the classes with more simulation rounds
427 if ( pPars->fVerbose )
428 printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
429  p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1, 1 ); //pPars->nFramesK + 1, 1 );
430 if ( pPars->fVerbose )
431 {
432 ABC_PRT( "Time", Abc_Clock() - clk );
433 }
434  Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, p->pPars->nMaxLevs );
435 // Fra_ClassesPostprocess( p->pCla );
436  // compute one-hotness conditions
437  if ( p->pPars->fUse1Hot )
438  p->vOneHots = Fra_OneHotCompute( p, p->pSml );
439  // allocate new simulation manager for simulating counter-examples
440  Fra_SmlStop( p->pSml );
441  p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
442  }
443 
444  // select the most expressive implications
445  if ( pPars->fUseImps )
446  p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr );
447 
448  if ( pParams->TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
449  {
450  if ( !pParams->fSilent )
451  printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
452  goto finish;
453  }
454 
455  // perform BMC (for the min number of frames)
456  Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK+1 ); // +1 is needed to prevent non-refinement
457 //Fra_ClassesPrint( p->pCla, 1 );
458 // if ( p->vCex == NULL )
459 // p->vCex = Vec_IntAlloc( 1000 );
460 
462  p->nNodesBeg = nNodesBeg; // Aig_ManNodeNum(pManAig);
463  p->nRegsBeg = nRegsBeg; // Aig_ManRegNum(pManAig);
464 
465  // dump AIG of the timeframes
466 // pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK );
467 // Aig_ManDumpBlif( pManAigNew, "frame_aig.blif", NULL, NULL );
468 // Fra_ManPartitionTest2( pManAigNew );
469 // Aig_ManStop( pManAigNew );
470 
471  // iterate the inductive case
472  p->pCla->fRefinement = 1;
473  for ( nIter = 0; p->pCla->fRefinement; nIter++ )
474  {
475  int nLitsOld = Fra_ClassesCountLits(p->pCla);
476  int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
477  int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0;
478  abctime clk3 = Abc_Clock();
479 
480  if ( pParams->TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
481  {
482  if ( !pParams->fSilent )
483  printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
484  goto finish;
485  }
486 
487  // mark the classes as non-refined
488  p->pCla->fRefinement = 0;
489  // derive non-init K-timeframes while implementing e-classes
490 clk2 = Abc_Clock();
492 p->timeTrav += Abc_Clock() - clk2;
493 //Aig_ManDumpBlif( p->pManFraig, "testaig.blif", NULL, NULL );
494 
495  // perform AIG rewriting
496  if ( p->pPars->fRewrite )
498 
499  // convert the manager to SAT solver (the last nLatches outputs are inputs)
500  if ( fUseSimpleCnf || pPars->fUseImps )
502  else
503  pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
504 // Cnf_DataTranformPolarity( pCnf, 0 );
505 //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
506 
507  p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
508  p->nSatVars = pCnf->nVars;
509  assert( p->pSat != NULL );
510  if ( p->pSat == NULL )
511  printf( "Fra_FraigInduction(): Computed CNF is not valid.\n" );
512  if ( pPars->fUseImps )
513  {
514  Fra_ImpAddToSolver( p, p->pCla->vImps, pCnf->pVarNums );
515  if ( p->pSat == NULL )
516  printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" );
517  }
518 
519  // set the pointers to the manager
520  Aig_ManForEachObj( p->pManFraig, pObj, i )
521  pObj->pData = p;
522 
523  // prepare solver for fraiging the last timeframe
524  Fra_ManClean( p, Aig_ManObjNumMax(p->pManFraig) + Aig_ManNodeNum(p->pManAig) );
525 
526  // transfer PI/LO variable numbers
527  Aig_ManForEachObj( p->pManFraig, pObj, i )
528  {
529  if ( pCnf->pVarNums[pObj->Id] == -1 )
530  continue;
531  Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
532  Fra_ObjSetFaninVec( pObj, (Vec_Ptr_t *)1 );
533  }
534  Cnf_DataFree( pCnf );
535 
536  // add one-hotness clauses
537  if ( p->pPars->fUse1Hot )
538  Fra_OneHotAssume( p, p->vOneHots );
539 // if ( p->pManAig->vOnehots )
540 // Fra_OneHotAddKnownConstraint( p, p->pManAig->vOnehots );
541 
542  // report the intermediate results
543  if ( pPars->fVerbose )
544  {
545  printf( "%3d : C = %6d. Cl = %6d. L = %6d. LR = %6d. ",
546  nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
547  Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
548  if ( p->pCla->vImps )
549  printf( "I = %6d. ", Vec_IntSize(p->pCla->vImps) );
550  if ( p->pPars->fUse1Hot )
551  printf( "1h = %6d. ", Fra_OneHotCount(p, p->vOneHots) );
552  printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) );
553 // printf( "\n" );
554  }
555 
556  // perform sweeping
557  p->nSatCallsRecent = 0;
558  p->nSatCallsSkipped = 0;
559 clk2 = Abc_Clock();
560  if ( p->pPars->fUse1Hot )
561  Fra_OneHotCheck( p, p->vOneHots );
562  Fra_FraigSweep( p );
563  if ( pPars->fVerbose )
564  {
565  ABC_PRT( "T", Abc_Clock() - clk3 );
566  }
567 
568 // Sat_SolverPrintStats( stdout, p->pSat );
569  // remove FRAIG and SAT solver
570  Aig_ManStop( p->pManFraig ); p->pManFraig = NULL;
571 // printf( "Vars = %d. Clauses = %d. Learnts = %d.\n", p->pSat->size, p->pSat->clauses.size, p->pSat->learnts.size );
572  sat_solver_delete( p->pSat ); p->pSat = NULL;
573  memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
574 // printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped );
575  assert( p->vTimeouts == NULL );
576  if ( p->vTimeouts )
577  printf( "Fra_FraigInduction(): SAT solver timed out!\n" );
578  // check if refinement has happened
579 // p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla));
580  if ( p->pCla->fRefinement &&
581  nLitsOld == Fra_ClassesCountLits(p->pCla) &&
582  nImpsOld == (p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0) &&
583  nHotsOld == (p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0) )
584  {
585  printf( "Fra_FraigInduction(): Internal error. The result may not verify.\n" );
586  break;
587  }
588  }
589 /*
590  // verify implications using simulation
591  if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
592  {
593  int Temp;
594  abctime clk = Abc_Clock();
595  if ( Temp = Fra_ImpVerifyUsingSimulation( p ) )
596  printf( "Implications failing the simulation test = %d (out of %d). ", Temp, Vec_IntSize(p->pCla->vImps) );
597  else
598  printf( "All %d implications have passed the simulation test. ", Vec_IntSize(p->pCla->vImps) );
599  ABC_PRT( "Time", Abc_Clock() - clk );
600  }
601 */
602 
603  // move the classes into representatives and reduce AIG
604 clk2 = Abc_Clock();
605  if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) )
606  {
607  extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
608  Aig_Man_t * pNew;
609  char * pFileName = Ioa_FileNameGenericAppend( p->pManAig->pName, "_care.aig" );
610  printf( "Care one-hotness clauses will be written into file \"%s\".\n", pFileName );
611  pManAigNew = Aig_ManDupOrdered( pManAig );
612  pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
613  Ioa_WriteAiger( pNew, pFileName, 0, 1 );
614  Aig_ManStop( pNew );
615  }
616  else
617  {
618  // Fra_ClassesPrint( p->pCla, 1 );
619  Fra_ClassesSelectRepr( p->pCla );
620  Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
621  pManAigNew = Aig_ManDupRepr( pManAig, 0 );
622  }
623  // add implications to the manager
624 // if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
625 // Fra_ImpRecordInManager( p, pManAigNew );
626  // cleanup the new manager
627  Aig_ManSeqCleanup( pManAigNew );
628  // remove pointers to the dead nodes
629 // Aig_ManForEachObj( pManAig, pObj, i )
630 // if ( pObj->pData && Aig_ObjIsNone(pObj->pData) )
631 // pObj->pData = NULL;
632 // Aig_ManCountMergeRegs( pManAigNew );
633 p->timeTrav += Abc_Clock() - clk2;
634 p->timeTotal = Abc_Clock() - clk;
635  // get the final stats
636  p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
637  p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
638  p->nRegsEnd = Aig_ManRegNum(pManAigNew);
639  // free the manager
640 finish:
641  Fra_ManStop( p );
642  // check the output
643 // if ( Aig_ManCoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
644 // if ( Aig_ObjChild0( Aig_ManCo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
645 // printf( "Proved output constant 0.\n" );
646  pParams->nIters = nIter;
647  return pManAigNew;
648 }
char * memset()
int fSilent
Definition: fra.h:108
int fRewrite
Definition: fra.h:102
int fUse1Hot
Definition: fra.h:106
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
int fRefinement
Definition: fra.h:162
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fra_Man_t * Fra_ManStart(Aig_Man_t *pManAig, Fra_Par_t *pParams)
Definition: fraMan.c:104
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Fra_Sml_t * Fra_SmlSimulateSeq(Aig_Man_t *pAig, int nPref, int nFrames, int nWords, int fCheckMiter)
Definition: fraSim.c:1021
int Aig_ManSeqCleanup(Aig_Man_t *p)
Definition: aigScl.c:158
Fra_Cla_t * pCla
Definition: fra.h:198
int nRegsBeg
Definition: fra.h:226
Fra_Par_t * pPars
Definition: fra.h:189
int Fra_ClassesCountLits(Fra_Cla_t *p)
Definition: fraClass.c:164
sat_solver * pSat
Definition: fra.h:210
Fra_Sml_t * pSml
Definition: fra.h:200
Aig_Man_t * Aig_ManDupOrdered(Aig_Man_t *p)
Definition: aigDup.c:277
int nVars
Definition: cnf.h:59
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Vec_Int_t * vOneHots
Definition: fra.h:208
float TimeLimit
Definition: fra.h:110
abctime timeTrav
Definition: fra.h:241
static void Fra_ObjSetFaninVec(Aig_Obj_t *pObj, Vec_Ptr_t *vFanins)
Definition: fra.h:264
int * pVarNums
Definition: cnf.h:63
int nSatVars
Definition: fra.h:211
int nNodesBeg
Definition: fra.h:224
Vec_Int_t * Fra_ImpDerive(Fra_Man_t *p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr)
Definition: fraImp.c:321
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Definition: cnf.h:56
void Fra_ManClean(Fra_Man_t *p, int nNodesMax)
Definition: fraMan.c:145
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
void Fra_ParamsDefaultSeq(Fra_Par_t *pParams)
Definition: fraMan.c:75
Vec_Int_t * Fra_OneHotCompute(Fra_Man_t *p, Fra_Sml_t *pSim)
Definition: fraHot.c:134
Fra_Sml_t * Fra_SmlStart(Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
Definition: fraSim.c:813
char * Ioa_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition: ioaUtil.c:93
void Fra_ClassesPrepare(Fra_Cla_t *p, int fLatchCorr, int nMaxLevs)
Definition: fraClass.c:276
Aig_Man_t * pManFraig
Definition: fra.h:192
int nFramesP
Definition: fra.h:96
void Fra_FraigSweep(Fra_Man_t *pManAig)
Definition: fraCore.c:310
void Aig_ManReprStart(Aig_Man_t *p, int nIdMax)
DECLARATIONS ///.
Definition: aigRepr.c:45
int fWriteImps
Definition: fra.h:105
static void Fra_ObjSetSatNum(Aig_Obj_t *pObj, int Num)
Definition: fra.h:267
void Fra_BmcPerform(Fra_Man_t *p, int nPref, int nDepth)
Definition: fraBmc.c:311
void Fra_ImpAddToSolver(Fra_Man_t *p, Vec_Int_t *vImps, int *pSatVarNums)
Definition: fraImp.c:428
Definition: aig.h:69
int nFramesK
Definition: fra.h:97
void Ioa_WriteAiger(Aig_Man_t *pMan, char *pFileName, int fWriteSymbols, int fCompact)
Definition: ioaWriteAig.c:446
int nMaxImps
Definition: fra.h:98
Aig_Man_t * Aig_ManDupRepr(Aig_Man_t *p, int fOrdered)
Definition: aigRepr.c:267
Vec_Int_t * vImps
Definition: fra.h:163
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Aig_Man_t * Fra_FraigInductionPart(Aig_Man_t *pAig, Fra_Ssw_t *pPars)
Definition: fraInd.c:253
ABC_NAMESPACE_IMPL_START void Fra_FraigInductionRewrite(Fra_Man_t *p)
DECLARATIONS ///.
Definition: fraInd.c:48
int nPartSize
Definition: fra.h:94
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
void Fra_SmlSimulate(Fra_Man_t *p, int fInit)
Definition: fraSim.c:738
void Fra_ClassesSelectRepr(Fra_Cla_t *p)
Definition: fraClass.c:706
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:463
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Cnf_Dat_t * Cnf_DeriveSimple(Aig_Man_t *p, int nOutputs)
Definition: cnfWrite.c:587
typedefABC_NAMESPACE_HEADER_START struct Fra_Par_t_ Fra_Par_t
INCLUDES ///.
Definition: fra.h:53
void Fra_ManStop(Fra_Man_t *p)
Definition: fraMan.c:240
#define ABC_PRT(a, t)
Definition: abc_global.h:220
int Fra_OneHotCount(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition: fraHot.c:303
void Fra_ClassesCopyReprs(Fra_Cla_t *p, Vec_Ptr_t *vFailed)
Definition: fraClass.c:114
int fUseImps
Definition: fra.h:101
static int Vec_VecSize(Vec_Vec_t *p)
Definition: vecVec.h:222
int fLatchCorr
Definition: fra.h:104
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
int nIters
Definition: fra.h:109
void Fra_OneHotCheck(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition: fraHot.c:229
#define assert(ex)
Definition: util_old.h:213
Aig_Man_t * Fra_OneHotCreateExdc(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition: fraHot.c:398
int fVerbose
Definition: fra.h:107
ABC_INT64_T abctime
Definition: abc_global.h:278
Aig_Man_t * Fra_FramesWithClasses(Fra_Man_t *p)
Definition: fraInd.c:130
int nMaxLevs
Definition: fra.h:99
void Fra_SmlStop(Fra_Sml_t *p)
Definition: fraSim.c:839
int nLitsBeg
Definition: fra.h:222
void Fra_OneHotAssume(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition: fraHot.c:191
Aig_Man_t* Fra_FraigInductionPart ( Aig_Man_t pAig,
Fra_Ssw_t pPars 
)

Function*************************************************************

Synopsis [Performs partitioned sequential SAT sweepingG.]

Description []

SideEffects []

SeeAlso []

Definition at line 253 of file fraInd.c.

254 {
255  int fPrintParts = 0;
256  char Buffer[100];
257  Aig_Man_t * pTemp, * pNew;
258  Vec_Ptr_t * vResult;
259  Vec_Int_t * vPart;
260  int * pMapBack;
261  int i, nCountPis, nCountRegs;
262  int nClasses, nPartSize, fVerbose;
263  abctime clk = Abc_Clock();
264 
265  // save parameters
266  nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
267  fVerbose = pPars->fVerbose; pPars->fVerbose = 0;
268  // generate partitions
269  if ( pAig->vClockDoms )
270  {
271  // divide large clock domains into separate partitions
272  vResult = Vec_PtrAlloc( 100 );
273  Vec_PtrForEachEntry( Vec_Int_t *, (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
274  {
275  if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
276  Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
277  else
278  Vec_PtrPush( vResult, Vec_IntDup(vPart) );
279  }
280  }
281  else
282  vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
283 // vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 );
284 // vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
285  if ( fPrintParts )
286  {
287  // print partitions
288  printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
289  Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
290  {
291  sprintf( Buffer, "part%03d.aig", i );
292  pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
293  Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
294  printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
295  i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
296  Aig_ManStop( pTemp );
297  }
298  }
299 
300  // perform SSW with partitions
301  Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
302  Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
303  {
304  pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
305  // create the projection of 1-hot registers
306  if ( pAig->vOnehots )
307  pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose );
308  // run SSW
309  pNew = Fra_FraigInduction( pTemp, pPars );
310  nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
311  if ( fVerbose )
312  printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n",
313  i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
314  Aig_ManStop( pNew );
315  Aig_ManStop( pTemp );
316  ABC_FREE( pMapBack );
317  }
318  // remap the AIG
319  pNew = Aig_ManDupRepr( pAig, 0 );
320  Aig_ManSeqCleanup( pNew );
321 // Aig_ManPrintStats( pAig );
322 // Aig_ManPrintStats( pNew );
323  Vec_VecFree( (Vec_Vec_t *)vResult );
324  pPars->nPartSize = nPartSize;
325  pPars->fVerbose = fVerbose;
326  if ( fVerbose )
327  {
328  ABC_PRT( "Total time", Abc_Clock() - clk );
329  }
330  return pNew;
331 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Aig_Man_t * Aig_ManRegCreatePart(Aig_Man_t *pAig, Vec_Int_t *vPart, int *pnCountPis, int *pnCountRegs, int **ppMapBack)
Definition: aigPartReg.c:308
Aig_Man_t * Fra_FraigInduction(Aig_Man_t *pManAig, Fra_Ssw_t *pParams)
Definition: fraInd.c:344
static Vec_Int_t * Vec_IntDup(Vec_Int_t *pVec)
Definition: vecInt.h:214
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
void Aig_ManPartDivide(Vec_Ptr_t *vResult, Vec_Int_t *vDomain, int nPartSize, int nOverSize)
Definition: aigPartReg.c:513
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
int Aig_ManSeqCleanup(Aig_Man_t *p)
Definition: aigScl.c:158
Vec_Ptr_t * Aig_ManRegProjectOnehots(Aig_Man_t *pAig, Aig_Man_t *pPart, Vec_Ptr_t *vOnehots, int fVerbose)
Definition: aigPartReg.c:248
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
void Aig_ManReprStart(Aig_Man_t *p, int nIdMax)
DECLARATIONS ///.
Definition: aigRepr.c:45
int Aig_TransferMappedClasses(Aig_Man_t *pAig, Aig_Man_t *pPart, int *pMapBack)
Definition: aigRepr.c:533
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
char * sprintf()
void Ioa_WriteAiger(Aig_Man_t *pMan, char *pFileName, int fWriteSymbols, int fCompact)
Definition: ioaWriteAig.c:446
int nOverSize
Definition: fra.h:95
Aig_Man_t * Aig_ManDupRepr(Aig_Man_t *p, int fOrdered)
Definition: aigRepr.c:267
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
int nPartSize
Definition: fra.h:94
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
#define ABC_FREE(obj)
Definition: abc_global.h:232
#define ABC_PRT(a, t)
Definition: abc_global.h:220
int nIters
Definition: fra.h:109
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
int fVerbose
Definition: fra.h:107
ABC_INT64_T abctime
Definition: abc_global.h:278
Vec_Ptr_t * Aig_ManRegPartitionSimple(Aig_Man_t *pAig, int nPartSize, int nOverSize)
Definition: aigPartReg.c:474
ABC_NAMESPACE_IMPL_START void Fra_FraigInductionRewrite ( Fra_Man_t p)

DECLARATIONS ///.

CFile****************************************************************

FileName [fraInd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [Inductive prover.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id:
fraInd.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Performs AIG rewriting on the constraint manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file fraInd.c.

49 {
50  Aig_Man_t * pTemp;
51  Aig_Obj_t * pObj, * pObjPo;
52  int nTruePis, k, i;
53  abctime clk = Abc_Clock();
54  // perform AIG rewriting on the speculated frames
55 // pTemp = Dar_ManRwsat( pTemp, 1, 0 );
56  pTemp = Dar_ManRewriteDefault( p->pManFraig );
57 // printf( "Before = %6d. After = %6d.\n", Aig_ManNodeNum(p->pManFraig), Aig_ManNodeNum(pTemp) );
58 //Aig_ManDumpBlif( p->pManFraig, "1.blif", NULL, NULL );
59 //Aig_ManDumpBlif( pTemp, "2.blif", NULL, NULL );
60 // Fra_FramesWriteCone( pTemp );
61 // Aig_ManStop( pTemp );
62  // transfer PI/register pointers
63  assert( p->pManFraig->nRegs == pTemp->nRegs );
64  assert( p->pManFraig->nAsserts == pTemp->nAsserts );
65  nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
66  memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
67  Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), p->pPars->nFramesK, Aig_ManConst1(pTemp) );
68  Aig_ManForEachPiSeq( p->pManAig, pObj, i )
69  Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ManCi(pTemp,nTruePis*p->pPars->nFramesK+i) );
70  k = 0;
71  assert( Aig_ManRegNum(p->pManAig) == Aig_ManCoNum(pTemp) - pTemp->nAsserts );
72  Aig_ManForEachLoSeq( p->pManAig, pObj, i )
73  {
74  pObjPo = Aig_ManCo(pTemp, pTemp->nAsserts + k++);
75  Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ObjChild0(pObjPo) );
76  }
77  // exchange
78  Aig_ManStop( p->pManFraig );
79  p->pManFraig = pTemp;
80 p->timeRwr += Abc_Clock() - clk;
81 }
char * memset()
Aig_Man_t * pManAig
Definition: fra.h:191
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Fra_Par_t * pPars
Definition: fra.h:189
abctime timeRwr
Definition: fra.h:242
static abctime Abc_Clock()
Definition: abc_global.h:279
static void Fra_ObjSetFraig(Aig_Obj_t *pObj, int i, Aig_Obj_t *pNode)
Definition: fra.h:261
int nFramesAll
Definition: fra.h:194
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Aig_Man_t * pManFraig
Definition: fra.h:192
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Aig_Man_t * Dar_ManRewriteDefault(Aig_Man_t *pAig)
DECLARATIONS ///.
Definition: darScript.c:48
Definition: aig.h:69
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
int nSizeAlloc
Definition: fra.h:196
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Aig_Obj_t ** pMemFraig
Definition: fra.h:195
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition: aig.h:441
#define assert(ex)
Definition: util_old.h:213
ABC_INT64_T abctime
Definition: abc_global.h:278
#define Aig_ManForEachPiSeq(p, pObj, i)
SEQUENTIAL ITERATORS ///.
Definition: aig.h:438
int Fra_FraigInductionTest ( char *  pFileName,
Fra_Ssw_t pParams 
)

Function*************************************************************

Synopsis [Outputs a set of pairs of equivalent nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 661 of file fraInd.c.

662 {
663  FILE * pFile;
664  char * pFilePairs;
665  Aig_Man_t * pMan, * pNew;
666  Aig_Obj_t * pObj, * pRepr;
667  int * pNum2Id;
668  int i, Counter = 0;
669  pMan = Saig_ManReadBlif( pFileName );
670  if ( pMan == NULL )
671  return 0;
672  // perform seq SAT sweeping
673  pNew = Fra_FraigInduction( pMan, pParams );
674  if ( pNew == NULL )
675  {
676  Aig_ManStop( pMan );
677  return 0;
678  }
679  if ( pParams->fVerbose )
680  {
681  printf( "Original AIG: " );
682  Aig_ManPrintStats( pMan );
683  printf( "Reduced AIG: " );
684  Aig_ManPrintStats( pNew );
685  }
686  Aig_ManStop( pNew );
687  pNum2Id = (int *)pMan->pData;
688  // write the output file
689  pFilePairs = Aig_FileNameGenericAppend( pFileName, ".pairs" );
690  pFile = fopen( pFilePairs, "w" );
691  Aig_ManForEachObj( pMan, pObj, i )
692  if ( (pRepr = pMan->pReprs[pObj->Id]) )
693  {
694  fprintf( pFile, "%d %d %c\n", pNum2Id[pObj->Id], pNum2Id[pRepr->Id], (Aig_ObjPhase(pObj) ^ Aig_ObjPhase(pRepr))? '-' : '+' );
695  Counter++;
696  }
697  fclose( pFile );
698  if ( pParams->fVerbose )
699  {
700  printf( "Result: %d pairs of seq equiv nodes are written into file \"%s\".\n", Counter, pFilePairs );
701  }
702  Aig_ManStop( pMan );
703  return 1;
704 }
static int Aig_ObjPhase(Aig_Obj_t *pObj)
Definition: aig.h:298
Aig_Man_t * Fra_FraigInduction(Aig_Man_t *pManAig, Fra_Ssw_t *pParams)
Definition: fraInd.c:344
char * Aig_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition: aigUtil.c:1070
Aig_Man_t * Saig_ManReadBlif(char *pFileName)
Definition: saigIoa.c:246
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
void Aig_ManPrintStats(Aig_Man_t *p)
Definition: aigMan.c:379
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
static int Counter
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
int fVerbose
Definition: fra.h:107
int Id
Definition: aig.h:85
void Fra_FramesAddMore ( Aig_Man_t p,
int  nFrames 
)

Function*************************************************************

Synopsis [Prepares the inductive case with speculative reduction.]

Description []

SideEffects []

SeeAlso []

Definition at line 197 of file fraInd.c.

198 {
199  Aig_Obj_t * pObj, ** pLatches;
200  int i, k, f, nNodesOld;
201  // set copy pointer of each object to point to itself
202  Aig_ManForEachObj( p, pObj, i )
203  pObj->pData = pObj;
204  // iterate and add objects
205  nNodesOld = Aig_ManObjNumMax(p);
206  pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) );
207  for ( f = 0; f < nFrames; f++ )
208  {
209  // clean latch inputs and outputs
210  Aig_ManForEachLiSeq( p, pObj, i )
211  pObj->pData = NULL;
212  Aig_ManForEachLoSeq( p, pObj, i )
213  pObj->pData = NULL;
214  // save the latch input values
215  k = 0;
216  Aig_ManForEachLiSeq( p, pObj, i )
217  {
218  if ( Aig_ObjFanin0(pObj)->pData )
219  pLatches[k++] = Aig_ObjChild0Copy(pObj);
220  else
221  pLatches[k++] = NULL;
222  }
223  // insert them as the latch output values
224  k = 0;
225  Aig_ManForEachLoSeq( p, pObj, i )
226  pObj->pData = pLatches[k++];
227  // create the next time frame of nodes
228  Aig_ManForEachNode( p, pObj, i )
229  {
230  if ( i > nNodesOld )
231  break;
232  if ( Aig_ObjFanin0(pObj)->pData && Aig_ObjFanin1(pObj)->pData )
233  pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
234  else
235  pObj->pData = NULL;
236  }
237  }
238  ABC_FREE( pLatches );
239 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
for(p=first;p->value< newval;p=p->next)
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Definition: aig.h:69
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
#define ABC_FREE(obj)
Definition: abc_global.h:232
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition: aig.h:441
#define Aig_ManForEachLiSeq(p, pObj, i)
Definition: aig.h:447
static void Fra_FramesConstrainNode ( Aig_Man_t pManFraig,
Aig_Obj_t pObj,
int  iFrame 
)
inlinestatic

Function*************************************************************

Synopsis [Performs speculative reduction for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 94 of file fraInd.c.

95 {
96  Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
97  // skip nodes without representative
98  if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
99  return;
100  assert( pObjRepr->Id < pObj->Id );
101  // get the new node
102  pObjNew = Fra_ObjFraig( pObj, iFrame );
103  // get the new node of the representative
104  pObjReprNew = Fra_ObjFraig( pObjRepr, iFrame );
105  // if this is the same node, no need to add constraints
106  if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
107  return;
108  // these are different nodes - perform speculative reduction
109  pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
110  // set the new node
111  Fra_ObjSetFraig( pObj, iFrame, pObjNew2 );
112  // add the constraint
113  pMiter = Aig_Exor( pManFraig, pObjNew, pObjReprNew );
114  pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
115  assert( Aig_ObjPhaseReal(pMiter) == 1 );
116  Aig_ObjCreateCo( pManFraig, pMiter );
117 }
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Aig_Obj_t * Aig_Exor(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:220
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
static void Fra_ObjSetFraig(Aig_Obj_t *pObj, int i, Aig_Obj_t *pNode)
Definition: fra.h:261
static Aig_Obj_t * Fra_ObjFraig(Aig_Obj_t *pObj, int i)
Definition: fra.h:260
static int Aig_ObjPhaseReal(Aig_Obj_t *pObj)
Definition: aig.h:299
Definition: aig.h:69
unsigned int fPhase
Definition: aig.h:78
static Aig_Obj_t * Fra_ClassObjRepr(Aig_Obj_t *pObj)
Definition: fra.h:269
#define assert(ex)
Definition: util_old.h:213
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
int Id
Definition: aig.h:85
Aig_Man_t* Fra_FramesWithClasses ( Fra_Man_t p)

Function*************************************************************

Synopsis [Prepares the inductive case with speculative reduction.]

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file fraInd.c.

131 {
132  Aig_Man_t * pManFraig;
133  Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
134  int i, k, f;
135  assert( p->pManFraig == NULL );
136  assert( Aig_ManRegNum(p->pManAig) > 0 );
138 
139  // start the fraig package
140  pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) * p->nFramesAll );
141  pManFraig->pName = Abc_UtilStrsav( p->pManAig->pName );
142  pManFraig->pSpec = Abc_UtilStrsav( p->pManAig->pSpec );
143  pManFraig->nRegs = p->pManAig->nRegs;
144  // create PI nodes for the frames
145  for ( f = 0; f < p->nFramesAll; f++ )
146  Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), f, Aig_ManConst1(pManFraig) );
147  for ( f = 0; f < p->nFramesAll; f++ )
148  Aig_ManForEachPiSeq( p->pManAig, pObj, i )
149  Fra_ObjSetFraig( pObj, f, Aig_ObjCreateCi(pManFraig) );
150  // create latches for the first frame
151  Aig_ManForEachLoSeq( p->pManAig, pObj, i )
152  Fra_ObjSetFraig( pObj, 0, Aig_ObjCreateCi(pManFraig) );
153 
154  // add timeframes
155 // pManFraig->fAddStrash = 1;
156  for ( f = 0; f < p->nFramesAll - 1; f++ )
157  {
158  // set the constraints on the latch outputs
159  Aig_ManForEachLoSeq( p->pManAig, pObj, i )
160  Fra_FramesConstrainNode( pManFraig, pObj, f );
161  // add internal nodes of this frame
162  Aig_ManForEachNode( p->pManAig, pObj, i )
163  {
164  pObjNew = Aig_And( pManFraig, Fra_ObjChild0Fra(pObj,f), Fra_ObjChild1Fra(pObj,f) );
165  Fra_ObjSetFraig( pObj, f, pObjNew );
166  Fra_FramesConstrainNode( pManFraig, pObj, f );
167  }
168  // transfer latch input to the latch outputs
169  Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, k )
170  Fra_ObjSetFraig( pObjLo, f+1, Fra_ObjChild0Fra(pObjLi,f) );
171  }
172 // pManFraig->fAddStrash = 0;
173  // mark the asserts
174  pManFraig->nAsserts = Aig_ManCoNum(pManFraig);
175  // add the POs for the latch outputs of the last frame
176  Aig_ManForEachLoSeq( p->pManAig, pObj, i )
177  Aig_ObjCreateCo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) );
178 
179  // remove dangling nodes
180  Aig_ManCleanup( pManFraig );
181  // make sure the satisfying assignment is node assigned
182  assert( pManFraig->pData == NULL );
183  return pManFraig;
184 }
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Aig_Man_t * pManAig
Definition: fra.h:191
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
static Aig_Obj_t * Fra_ObjChild0Fra(Aig_Obj_t *pObj, int i)
Definition: fra.h:272
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
for(p=first;p->value< newval;p=p->next)
static void Fra_ObjSetFraig(Aig_Obj_t *pObj, int i, Aig_Obj_t *pNode)
Definition: fra.h:261
static void Fra_FramesConstrainNode(Aig_Man_t *pManFraig, Aig_Obj_t *pObj, int iFrame)
Definition: fraInd.c:94
int nFramesAll
Definition: fra.h:194
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Aig_Man_t * pManFraig
Definition: fra.h:192
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
static Aig_Obj_t * Fra_ObjFraig(Aig_Obj_t *pObj, int i)
Definition: fra.h:260
#define Aig_ManForEachLiLoSeq(p, pObjLi, pObjLo, k)
Definition: aig.h:450
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Definition: aig.h:69
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition: aig.h:441
#define assert(ex)
Definition: util_old.h:213
static Aig_Obj_t * Fra_ObjChild1Fra(Aig_Obj_t *pObj, int i)
Definition: fra.h:273
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
#define Aig_ManForEachPiSeq(p, pObj, i)
SEQUENTIAL ITERATORS ///.
Definition: aig.h:438