/**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 $]
***********************************************************************/
#include "fra.h"
#include "sat/cnf/cnf.h"
#include "opt/dar/dar.h"
#include "aig/saig/saig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs AIG rewriting on the constraint manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_FraigInductionRewrite( Fra_Man_t * p )
{
Aig_Man_t * pTemp;
Aig_Obj_t * pObj, * pObjPo;
int nTruePis, k, i;
abctime clk = Abc_Clock();
// perform AIG rewriting on the speculated frames
// pTemp = Dar_ManRwsat( pTemp, 1, 0 );
pTemp = Dar_ManRewriteDefault( p->pManFraig );
// printf( "Before = %6d. After = %6d.\n", Aig_ManNodeNum(p->pManFraig), Aig_ManNodeNum(pTemp) );
//Aig_ManDumpBlif( p->pManFraig, "1.blif", NULL, NULL );
//Aig_ManDumpBlif( pTemp, "2.blif", NULL, NULL );
// Fra_FramesWriteCone( pTemp );
// Aig_ManStop( pTemp );
// transfer PI/register pointers
assert( p->pManFraig->nRegs == pTemp->nRegs );
assert( p->pManFraig->nAsserts == pTemp->nAsserts );
nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), p->pPars->nFramesK, Aig_ManConst1(pTemp) );
Aig_ManForEachPiSeq( p->pManAig, pObj, i )
Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ManCi(pTemp,nTruePis*p->pPars->nFramesK+i) );
k = 0;
assert( Aig_ManRegNum(p->pManAig) == Aig_ManCoNum(pTemp) - pTemp->nAsserts );
Aig_ManForEachLoSeq( p->pManAig, pObj, i )
{
pObjPo = Aig_ManCo(pTemp, pTemp->nAsserts + k++);
Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ObjChild0(pObjPo) );
}
// exchange
Aig_ManStop( p->pManFraig );
p->pManFraig = pTemp;
p->timeRwr += Abc_Clock() - clk;
}
/**Function*************************************************************
Synopsis [Performs speculative reduction for one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, int iFrame )
{
Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
// skip nodes without representative
if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
return;
assert( pObjRepr->Id < pObj->Id );
// get the new node
pObjNew = Fra_ObjFraig( pObj, iFrame );
// get the new node of the representative
pObjReprNew = Fra_ObjFraig( pObjRepr, iFrame );
// if this is the same node, no need to add constraints
if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
return;
// these are different nodes - perform speculative reduction
pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
// set the new node
Fra_ObjSetFraig( pObj, iFrame, pObjNew2 );
// add the constraint
pMiter = Aig_Exor( pManFraig, pObjNew, pObjReprNew );
pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
assert( Aig_ObjPhaseReal(pMiter) == 1 );
Aig_ObjCreateCo( pManFraig, pMiter );
}
/**Function*************************************************************
Synopsis [Prepares the inductive case with speculative reduction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
{
Aig_Man_t * pManFraig;
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
int i, k, f;
assert( p->pManFraig == NULL );
assert( Aig_ManRegNum(p->pManAig) > 0 );
assert( Aig_ManRegNum(p->pManAig) < Aig_ManCiNum(p->pManAig) );
// start the fraig package
pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) * p->nFramesAll );
pManFraig->pName = Abc_UtilStrsav( p->pManAig->pName );
pManFraig->pSpec = Abc_UtilStrsav( p->pManAig->pSpec );
pManFraig->nRegs = p->pManAig->nRegs;
// create PI nodes for the frames
for ( f = 0; f < p->nFramesAll; f++ )
Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), f, Aig_ManConst1(pManFraig) );
for ( f = 0; f < p->nFramesAll; f++ )
Aig_ManForEachPiSeq( p->pManAig, pObj, i )
Fra_ObjSetFraig( pObj, f, Aig_ObjCreateCi(pManFraig) );
// create latches for the first frame
Aig_ManForEachLoSeq( p->pManAig, pObj, i )
Fra_ObjSetFraig( pObj, 0, Aig_ObjCreateCi(pManFraig) );
// add timeframes
// pManFraig->fAddStrash = 1;
for ( f = 0; f < p->nFramesAll - 1; f++ )
{
// set the constraints on the latch outputs
Aig_ManForEachLoSeq( p->pManAig, pObj, i )
Fra_FramesConstrainNode( pManFraig, pObj, f );
// add internal nodes of this frame
Aig_ManForEachNode( p->pManAig, pObj, i )
{
pObjNew = Aig_And( pManFraig, Fra_ObjChild0Fra(pObj,f), Fra_ObjChild1Fra(pObj,f) );
Fra_ObjSetFraig( pObj, f, pObjNew );
Fra_FramesConstrainNode( pManFraig, pObj, f );
}
// transfer latch input to the latch outputs
Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, k )
Fra_ObjSetFraig( pObjLo, f+1, Fra_ObjChild0Fra(pObjLi,f) );
}
// pManFraig->fAddStrash = 0;
// mark the asserts
pManFraig->nAsserts = Aig_ManCoNum(pManFraig);
// add the POs for the latch outputs of the last frame
Aig_ManForEachLoSeq( p->pManAig, pObj, i )
Aig_ObjCreateCo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) );
// remove dangling nodes
Aig_ManCleanup( pManFraig );
// make sure the satisfying assignment is node assigned
assert( pManFraig->pData == NULL );
return pManFraig;
}
/**Function*************************************************************
Synopsis [Prepares the inductive case with speculative reduction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
{
Aig_Obj_t * pObj, ** pLatches;
int i, k, f, nNodesOld;
// set copy pointer of each object to point to itself
Aig_ManForEachObj( p, pObj, i )
pObj->pData = pObj;
// iterate and add objects
nNodesOld = Aig_ManObjNumMax(p);
pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) );
for ( f = 0; f < nFrames; f++ )
{
// clean latch inputs and outputs
Aig_ManForEachLiSeq( p, pObj, i )
pObj->pData = NULL;
Aig_ManForEachLoSeq( p, pObj, i )
pObj->pData = NULL;
// save the latch input values
k = 0;
Aig_ManForEachLiSeq( p, pObj, i )
{
if ( Aig_ObjFanin0(pObj)->pData )
pLatches[k++] = Aig_ObjChild0Copy(pObj);
else
pLatches[k++] = NULL;
}
// insert them as the latch output values
k = 0;
Aig_ManForEachLoSeq( p, pObj, i )
pObj->pData = pLatches[k++];
// create the next time frame of nodes
Aig_ManForEachNode( p, pObj, i )
{
if ( i > nNodesOld )
break;
if ( Aig_ObjFanin0(pObj)->pData && Aig_ObjFanin1(pObj)->pData )
pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
else
pObj->pData = NULL;
}
}
ABC_FREE( pLatches );
}
/**Function*************************************************************
Synopsis [Performs partitioned sequential SAT sweepingG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
{
int fPrintParts = 0;
char Buffer[100];
Aig_Man_t * pTemp, * pNew;
Vec_Ptr_t * vResult;
Vec_Int_t * vPart;
int * pMapBack;
int i, nCountPis, nCountRegs;
int nClasses, nPartSize, fVerbose;
abctime clk = Abc_Clock();
// save parameters
nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
fVerbose = pPars->fVerbose; pPars->fVerbose = 0;
// generate partitions
if ( pAig->vClockDoms )
{
// divide large clock domains into separate partitions
vResult = Vec_PtrAlloc( 100 );
Vec_PtrForEachEntry( Vec_Int_t *, (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
{
if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
else
Vec_PtrPush( vResult, Vec_IntDup(vPart) );
}
}
else
vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
// vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 );
// vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
if ( fPrintParts )
{
// print partitions
printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
{
sprintf( Buffer, "part%03d.aig", i );
pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
Aig_ManStop( pTemp );
}
}
// perform SSW with partitions
Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
{
pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
// create the projection of 1-hot registers
if ( pAig->vOnehots )
pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose );
// run SSW
pNew = Fra_FraigInduction( pTemp, pPars );
nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
if ( fVerbose )
printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n",
i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
Aig_ManStop( pNew );
Aig_ManStop( pTemp );
ABC_FREE( pMapBack );
}
// remap the AIG
pNew = Aig_ManDupRepr( pAig, 0 );
Aig_ManSeqCleanup( pNew );
// Aig_ManPrintStats( pAig );
// Aig_ManPrintStats( pNew );
Vec_VecFree( (Vec_Vec_t *)vResult );
pPars->nPartSize = nPartSize;
pPars->fVerbose = fVerbose;
if ( fVerbose )
{
ABC_PRT( "Total time", Abc_Clock() - clk );
}
return pNew;
}
/**Function*************************************************************
Synopsis [Performs sequential SAT sweeping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
{
int fUseSimpleCnf = 0;
int fUseOldSimulation = 0;
// other paramaters affecting performance
// - presence of FRAIGing in Abc_NtkDarSeqSweep()
// - using distance-1 patterns in Fra_SmlAssignDist1()
// - the number of simulation patterns
// - the number of BMC frames
Fra_Man_t * p;
Fra_Par_t Pars, * pPars = &Pars;
Aig_Obj_t * pObj;
Cnf_Dat_t * pCnf;
Aig_Man_t * pManAigNew = NULL;
int nNodesBeg, nRegsBeg;
int nIter = -1; // Suppress "might be used uninitialized"
int i;
abctime clk = Abc_Clock(), clk2;
abctime TimeToStop = pParams->TimeLimit ? pParams->TimeLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;
if ( Aig_ManNodeNum(pManAig) == 0 )
{
pParams->nIters = 0;
// Ntl_ManFinalize() needs the following to satisfy an assertion
Aig_ManReprStart(pManAig,Aig_ManObjNumMax(pManAig));
return Aig_ManDupOrdered(pManAig);
}
assert( Aig_ManRegNum(pManAig) > 0 );
assert( pParams->nFramesK > 0 );
//Aig_ManShow( pManAig, 0, NULL );
if ( pParams->fWriteImps && pParams->nPartSize > 0 )
{
pParams->nPartSize = 0;
printf( "Partitioning was disabled to allow implication writing.\n" );
}
// perform partitioning
if ( (pParams->nPartSize > 0 && pParams->nPartSize < Aig_ManRegNum(pManAig))
|| (pManAig->vClockDoms && Vec_VecSize(pManAig->vClockDoms) > 0) )
return Fra_FraigInductionPart( pManAig, pParams );
nNodesBeg = Aig_ManNodeNum(pManAig);
nRegsBeg = Aig_ManRegNum(pManAig);
// enhance the AIG by adding timeframes
// Fra_FramesAddMore( pManAig, 3 );
// get parameters
Fra_ParamsDefaultSeq( pPars );
pPars->nFramesP = pParams->nFramesP;
pPars->nFramesK = pParams->nFramesK;
pPars->nMaxImps = pParams->nMaxImps;
pPars->nMaxLevs = pParams->nMaxLevs;
pPars->fVerbose = pParams->fVerbose;
pPars->fRewrite = pParams->fRewrite;
pPars->fLatchCorr = pParams->fLatchCorr;
pPars->fUseImps = pParams->fUseImps;
pPars->fWriteImps = pParams->fWriteImps;
pPars->fUse1Hot = pParams->fUse1Hot;
assert( !(pPars->nFramesP > 0 && pPars->fUse1Hot) );
assert( !(pPars->nFramesK > 1 && pPars->fUse1Hot) );
// start the fraig manager for this run
p = Fra_ManStart( pManAig, pPars );
p->pPars->nBTLimitNode = 0;
// derive and refine e-classes using K initialized frames
if ( fUseOldSimulation )
{
if ( pPars->nFramesP > 0 )
{
pPars->nFramesP = 0;
printf( "Fra_FraigInduction(): Prefix cannot be used.\n" );
}
p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
Fra_SmlSimulate( p, 1 );
}
else
{
// bug: r iscas/blif/s5378.blif ; st; ssw -v
// bug: r iscas/blif/s1238.blif ; st; ssw -v
// refine the classes with more simulation rounds
if ( pPars->fVerbose )
printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1, 1 ); //pPars->nFramesK + 1, 1 );
if ( pPars->fVerbose )
{
ABC_PRT( "Time", Abc_Clock() - clk );
}
Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, p->pPars->nMaxLevs );
// Fra_ClassesPostprocess( p->pCla );
// compute one-hotness conditions
if ( p->pPars->fUse1Hot )
p->vOneHots = Fra_OneHotCompute( p, p->pSml );
// allocate new simulation manager for simulating counter-examples
Fra_SmlStop( p->pSml );
p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
}
// select the most expressive implications
if ( pPars->fUseImps )
p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr );
if ( pParams->TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
{
if ( !pParams->fSilent )
printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
goto finish;
}
// perform BMC (for the min number of frames)
Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK+1 ); // +1 is needed to prevent non-refinement
//Fra_ClassesPrint( p->pCla, 1 );
// if ( p->vCex == NULL )
// p->vCex = Vec_IntAlloc( 1000 );
p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
p->nNodesBeg = nNodesBeg; // Aig_ManNodeNum(pManAig);
p->nRegsBeg = nRegsBeg; // Aig_ManRegNum(pManAig);
// dump AIG of the timeframes
// pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK );
// Aig_ManDumpBlif( pManAigNew, "frame_aig.blif", NULL, NULL );
// Fra_ManPartitionTest2( pManAigNew );
// Aig_ManStop( pManAigNew );
// iterate the inductive case
p->pCla->fRefinement = 1;
for ( nIter = 0; p->pCla->fRefinement; nIter++ )
{
int nLitsOld = Fra_ClassesCountLits(p->pCla);
int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0;
abctime clk3 = Abc_Clock();
if ( pParams->TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
{
if ( !pParams->fSilent )
printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
goto finish;
}
// mark the classes as non-refined
p->pCla->fRefinement = 0;
// derive non-init K-timeframes while implementing e-classes
clk2 = Abc_Clock();
p->pManFraig = Fra_FramesWithClasses( p );
p->timeTrav += Abc_Clock() - clk2;
//Aig_ManDumpBlif( p->pManFraig, "testaig.blif", NULL, NULL );
// perform AIG rewriting
if ( p->pPars->fRewrite )
Fra_FraigInductionRewrite( p );
// convert the manager to SAT solver (the last nLatches outputs are inputs)
if ( fUseSimpleCnf || pPars->fUseImps )
pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
else
pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
// Cnf_DataTranformPolarity( pCnf, 0 );
//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
p->nSatVars = pCnf->nVars;
assert( p->pSat != NULL );
if ( p->pSat == NULL )
printf( "Fra_FraigInduction(): Computed CNF is not valid.\n" );
if ( pPars->fUseImps )
{
Fra_ImpAddToSolver( p, p->pCla->vImps, pCnf->pVarNums );
if ( p->pSat == NULL )
printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" );
}
// set the pointers to the manager
Aig_ManForEachObj( p->pManFraig, pObj, i )
pObj->pData = p;
// prepare solver for fraiging the last timeframe
Fra_ManClean( p, Aig_ManObjNumMax(p->pManFraig) + Aig_ManNodeNum(p->pManAig) );
// transfer PI/LO variable numbers
Aig_ManForEachObj( p->pManFraig, pObj, i )
{
if ( pCnf->pVarNums[pObj->Id] == -1 )
continue;
Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
Fra_ObjSetFaninVec( pObj, (Vec_Ptr_t *)1 );
}
Cnf_DataFree( pCnf );
// add one-hotness clauses
if ( p->pPars->fUse1Hot )
Fra_OneHotAssume( p, p->vOneHots );
// if ( p->pManAig->vOnehots )
// Fra_OneHotAddKnownConstraint( p, p->pManAig->vOnehots );
// report the intermediate results
if ( pPars->fVerbose )
{
printf( "%3d : C = %6d. Cl = %6d. L = %6d. LR = %6d. ",
nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
if ( p->pCla->vImps )
printf( "I = %6d. ", Vec_IntSize(p->pCla->vImps) );
if ( p->pPars->fUse1Hot )
printf( "1h = %6d. ", Fra_OneHotCount(p, p->vOneHots) );
printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) );
// printf( "\n" );
}
// perform sweeping
p->nSatCallsRecent = 0;
p->nSatCallsSkipped = 0;
clk2 = Abc_Clock();
if ( p->pPars->fUse1Hot )
Fra_OneHotCheck( p, p->vOneHots );
Fra_FraigSweep( p );
if ( pPars->fVerbose )
{
ABC_PRT( "T", Abc_Clock() - clk3 );
}
// Sat_SolverPrintStats( stdout, p->pSat );
// remove FRAIG and SAT solver
Aig_ManStop( p->pManFraig ); p->pManFraig = NULL;
// printf( "Vars = %d. Clauses = %d. Learnts = %d.\n", p->pSat->size, p->pSat->clauses.size, p->pSat->learnts.size );
sat_solver_delete( p->pSat ); p->pSat = NULL;
memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
// printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped );
assert( p->vTimeouts == NULL );
if ( p->vTimeouts )
printf( "Fra_FraigInduction(): SAT solver timed out!\n" );
// check if refinement has happened
// p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla));
if ( p->pCla->fRefinement &&
nLitsOld == Fra_ClassesCountLits(p->pCla) &&
nImpsOld == (p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0) &&
nHotsOld == (p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0) )
{
printf( "Fra_FraigInduction(): Internal error. The result may not verify.\n" );
break;
}
}
/*
// verify implications using simulation
if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
{
int Temp;
abctime clk = Abc_Clock();
if ( Temp = Fra_ImpVerifyUsingSimulation( p ) )
printf( "Implications failing the simulation test = %d (out of %d). ", Temp, Vec_IntSize(p->pCla->vImps) );
else
printf( "All %d implications have passed the simulation test. ", Vec_IntSize(p->pCla->vImps) );
ABC_PRT( "Time", Abc_Clock() - clk );
}
*/
// move the classes into representatives and reduce AIG
clk2 = Abc_Clock();
if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) )
{
extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
Aig_Man_t * pNew;
char * pFileName = Ioa_FileNameGenericAppend( p->pManAig->pName, "_care.aig" );
printf( "Care one-hotness clauses will be written into file \"%s\".\n", pFileName );
pManAigNew = Aig_ManDupOrdered( pManAig );
pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
Ioa_WriteAiger( pNew, pFileName, 0, 1 );
Aig_ManStop( pNew );
}
else
{
// Fra_ClassesPrint( p->pCla, 1 );
Fra_ClassesSelectRepr( p->pCla );
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
pManAigNew = Aig_ManDupRepr( pManAig, 0 );
}
// add implications to the manager
// if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
// Fra_ImpRecordInManager( p, pManAigNew );
// cleanup the new manager
Aig_ManSeqCleanup( pManAigNew );
// remove pointers to the dead nodes
// Aig_ManForEachObj( pManAig, pObj, i )
// if ( pObj->pData && Aig_ObjIsNone(pObj->pData) )
// pObj->pData = NULL;
// Aig_ManCountMergeRegs( pManAigNew );
p->timeTrav += Abc_Clock() - clk2;
p->timeTotal = Abc_Clock() - clk;
// get the final stats
p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
p->nRegsEnd = Aig_ManRegNum(pManAigNew);
// free the manager
finish:
Fra_ManStop( p );
// check the output
// if ( Aig_ManCoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
// if ( Aig_ObjChild0( Aig_ManCo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
// printf( "Proved output constant 0.\n" );
pParams->nIters = nIter;
return pManAigNew;
}
/**Function*************************************************************
Synopsis [Outputs a set of pairs of equivalent nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_FraigInductionTest( char * pFileName, Fra_Ssw_t * pParams )
{
FILE * pFile;
char * pFilePairs;
Aig_Man_t * pMan, * pNew;
Aig_Obj_t * pObj, * pRepr;
int * pNum2Id;
int i, Counter = 0;
pMan = Saig_ManReadBlif( pFileName );
if ( pMan == NULL )
return 0;
// perform seq SAT sweeping
pNew = Fra_FraigInduction( pMan, pParams );
if ( pNew == NULL )
{
Aig_ManStop( pMan );
return 0;
}
if ( pParams->fVerbose )
{
printf( "Original AIG: " );
Aig_ManPrintStats( pMan );
printf( "Reduced AIG: " );
Aig_ManPrintStats( pNew );
}
Aig_ManStop( pNew );
pNum2Id = (int *)pMan->pData;
// write the output file
pFilePairs = Aig_FileNameGenericAppend( pFileName, ".pairs" );
pFile = fopen( pFilePairs, "w" );
Aig_ManForEachObj( pMan, pObj, i )
if ( (pRepr = pMan->pReprs[pObj->Id]) )
{
fprintf( pFile, "%d %d %c\n", pNum2Id[pObj->Id], pNum2Id[pRepr->Id], (Aig_ObjPhase(pObj) ^ Aig_ObjPhase(pRepr))? '-' : '+' );
Counter++;
}
fclose( pFile );
if ( pParams->fVerbose )
{
printf( "Result: %d pairs of seq equiv nodes are written into file \"%s\".\n", Counter, pFilePairs );
}
Aig_ManStop( pMan );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END