From 9b059e3085eaa55817684926b3c508ba7fe0075f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 15 Mar 2008 08:01:00 -0700 Subject: Version abc80315 --- src/aig/aig/aigInter.c | 8 +++++--- src/aig/bdc/bdcCore.c | 2 +- src/base/abci/abc.c | 46 ++++++++++++++++++++++++++++++++++++++-------- src/base/abci/abcDar.c | 23 +++++++++++++++-------- src/base/abci/abcDelay.c | 31 ++++++++++++++++++++++++++++++- src/base/io/io.c | 2 +- src/sat/bsat/satInterA.c | 2 +- 7 files changed, 91 insertions(+), 23 deletions(-) diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c index d6b724c7..b58b758d 100644 --- a/src/aig/aig/aigInter.c +++ b/src/aig/aig/aigInter.c @@ -143,7 +143,7 @@ void Aig_ManInterFast( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose ) +Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fRelation, int fVerbose ) { void * pSatCnf = NULL; Inta_Man_t * pManInter; @@ -187,9 +187,10 @@ clk = clock(); sat_solver_store_mark_clauses_a( pSat ); // update the last clause + if ( fRelation ) { extern int sat_solver_store_change_last( sat_solver * pSat ); -// iLast = sat_solver_store_change_last( pSat ); + iLast = sat_solver_store_change_last( pSat ); } // add clauses of B @@ -207,7 +208,8 @@ clk = clock(); // add PI clauses // collect the common variables vVarsAB = Vec_IntAlloc( Aig_ManPiNum(pManOn) ); -// Vec_IntPush( vVarsAB, iLast ); + if ( fRelation ) + Vec_IntPush( vVarsAB, iLast ); Aig_ManForEachPi( pManOn, pObj, i ) { diff --git a/src/aig/bdc/bdcCore.c b/src/aig/bdc/bdcCore.c index 13275377..67b6bcdc 100644 --- a/src/aig/bdc/bdcCore.c +++ b/src/aig/bdc/bdcCore.c @@ -44,7 +44,7 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ) Bdc_Man_t * p; p = ALLOC( Bdc_Man_t, 1 ); memset( p, 0, sizeof(Bdc_Man_t) ); - assert( pPars->nVarsMax > 3 && pPars->nVarsMax < 16 ); + assert( pPars->nVarsMax > 2 && pPars->nVarsMax < 16 ); p->pPars = pPars; p->nWords = Kit_TruthWordNum( pPars->nVarsMax ); p->nDivsLimit = 200; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4262cd0d..204525d9 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -6809,24 +6809,29 @@ usage: int Abc_CommandInter( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; - Abc_Ntk_t * pNtk, * pNtkRes, * pNtk1, * pNtk2; + Abc_Ntk_t * pNtk, * pNtk1, * pNtk2, * pNtkRes = NULL; char ** pArgvNew; int nArgcNew; int c, fDelete1, fDelete2; + int fRelation; int fVerbose; - extern Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - fVerbose = 0; + fRelation = 0; + fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "rvh" ) ) != EOF ) { switch ( c ) { + case 'r': + fRelation ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -6843,10 +6848,19 @@ int Abc_CommandInter( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; if ( nArgcNew == 0 ) { + Abc_Obj_t * pObj; + int i; printf( "Deriving new circuit structure for the current network.\n" ); - Abc_ObjXorFaninC( Abc_NtkPo(pNtk2,0), 0 ); + Abc_NtkForEachPo( pNtk2, pObj, i ) + Abc_ObjXorFaninC( pObj, 0 ); + } + if ( fRelation && Abc_NtkCoNum(pNtk1) != 1 ) + { + printf( "Computation of interplants as a relation only works for single-output functions.\n" ); + printf( "Use command \"cone\" to extract one output cone from the multi-output network.\n" ); } - pNtkRes = Abc_NtkInter( pNtk1, pNtk2, fVerbose ); + else + pNtkRes = Abc_NtkInter( pNtk1, pNtk2, fRelation, fVerbose ); if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); @@ -6859,10 +6873,26 @@ int Abc_CommandInter( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: inter [-vh] \n" ); - fprintf( pErr, "\t derives interpolant of two networks (onset and offset)\n" ); + fprintf( pErr, "usage: inter [-rvh] \n" ); + fprintf( pErr, "\t derives interpolant of two networks representing onset and offset;\n" ); + fprintf( pErr, "\t-r : toggle computing interpolant as a relation [default = %s]\n", fRelation? "yes": "no" ); fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\t \n" ); + fprintf( pErr, "\t Comments:\n" ); + fprintf( pErr, "\t \n" ); + fprintf( pErr, "\t The networks given on the command line should have the same CIs/COs.\n" ); + fprintf( pErr, "\t If only one network is given on the command line, this network\n" ); + fprintf( pErr, "\t is assumed to be the offset, while the current network is the onset.\n" ); + fprintf( pErr, "\t If no network is given on the command line, the current network is\n" ); + fprintf( pErr, "\t assumed to be the onset and its complement is taken to be the offset.\n" ); + fprintf( pErr, "\t The resulting interpolant is stored as the current network.\n" ); + fprintf( pErr, "\t To verify that the interpolant agrees with the onset and the offset,\n" ); + fprintf( pErr, "\t save it in file \"inter.blif\" and run the following:\n" ); + fprintf( pErr, "\t (a) \"miter -i ; iprove\"\n" ); + fprintf( pErr, "\t (b) \"miter -i ; iprove\"\n" ); + fprintf( pErr, "\t where is the network derived by complementing the\n" ); + fprintf( pErr, "\t outputs of : \"r ; st -i; w \"\n" ); return 1; } diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index adf1f6e6..367ba727 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1530,14 +1530,14 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose ) +Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation, int fVerbose ) { - extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose ); + extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fRelation, int fVerbose ); Abc_Ntk_t * pNtkAig; Aig_Man_t * pManOn, * pManOff, * pManAig; if ( Abc_NtkCoNum(pNtkOn) != 1 || Abc_NtkCoNum(pNtkOff) != 1 ) { - printf( "Currently works only for single output networks.\n" ); + printf( "Currently works only for single-output networks.\n" ); return NULL; } if ( Abc_NtkCiNum(pNtkOn) != Abc_NtkCiNum(pNtkOff) ) @@ -1553,7 +1553,7 @@ Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbo if ( pManOff == NULL ) return NULL; // derive the interpolant - pManAig = Aig_ManInter( pManOn, pManOff, fVerbose ); + pManAig = Aig_ManInter( pManOn, pManOff, fRelation, fVerbose ); if ( pManAig == NULL ) { printf( "Interpolant computation failed.\n" ); @@ -1561,8 +1561,15 @@ Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbo } Aig_ManStop( pManOn ); Aig_ManStop( pManOff ); + // for the relation, add an extra input + if ( fRelation ) + { + Abc_Obj_t * pObj; + pObj = Abc_NtkCreatePi( pNtkOff ); + Abc_ObjAssignName( pObj, "New", NULL ); + } // create logic network - pNtkAig = Abc_NtkFromDar( pNtkOn, pManAig ); + pNtkAig = Abc_NtkFromDar( pNtkOff, pManAig ); Aig_ManStop( pManAig ); return pNtkAig; } @@ -1609,7 +1616,7 @@ int timeInt; SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose ) +Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation, int fVerbose ) { Abc_Ntk_t * pNtkOn1, * pNtkOff1, * pNtkInter1, * pNtkInter; Abc_Obj_t * pObj; @@ -1623,7 +1630,7 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose // Abc_NtkInterFast( pNtkOn, pNtkOff, fVerbose ); // consider the case of one output if ( Abc_NtkCoNum(pNtkOn) == 1 ) - return Abc_NtkInterOne( pNtkOn, pNtkOff, fVerbose ); + return Abc_NtkInterOne( pNtkOn, pNtkOff, fRelation, fVerbose ); // start the new newtork pNtkInter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); pNtkInter->pName = Extra_UtilStrsav(pNtkOn->pName); @@ -1652,7 +1659,7 @@ timeInt = 0; Abc_ObjXorFaninC( Abc_NtkPo(pNtkInter1, 0), 0 ); } else - pNtkInter1 = Abc_NtkInterOne( pNtkOn1, pNtkOff1, fVerbose ); + pNtkInter1 = Abc_NtkInterOne( pNtkOn1, pNtkOff1, 0, fVerbose ); if ( pNtkInter1 ) { Abc_NtkAppend( pNtkInter, pNtkInter1, 1 ); diff --git a/src/base/abci/abcDelay.c b/src/base/abci/abcDelay.c index 553bb2fc..847f1c75 100644 --- a/src/base/abci/abcDelay.c +++ b/src/base/abci/abcDelay.c @@ -566,7 +566,7 @@ Abc_Ntk_t * Abc_NtkSpeedup( Abc_Ntk_t * pNtk, int fUseLutLib, int Percentage, in if ( !fVeryVerbose && nTimeCris == 0 ) continue; Counter++; - // count the total number of timingn critical second-generation nodes + // count the total number of timing critical second-generation nodes Vec_PtrClear( vTimeCries ); if ( nTimeCris ) { @@ -602,6 +602,35 @@ Abc_Ntk_t * Abc_NtkSpeedup( Abc_Ntk_t * pNtk, int fUseLutLib, int Percentage, in // add the node to choices if ( Vec_PtrSize(vTimeCries) == 0 || Vec_PtrSize(vTimeCries) > Degree ) continue; + // order the fanins in the increasing order of criticalily + if ( Vec_PtrSize(vTimeCries) > 1 ) + { + pFanin = Vec_PtrEntry( vTimeCries, 0 ); + pFanin2 = Vec_PtrEntry( vTimeCries, 1 ); + if ( Abc_ObjSlack(pFanin) < Abc_ObjSlack(pFanin2) ) + { + Vec_PtrWriteEntry( vTimeCries, 0, pFanin2 ); + Vec_PtrWriteEntry( vTimeCries, 1, pFanin ); + } + } + if ( Vec_PtrSize(vTimeCries) > 2 ) + { + pFanin = Vec_PtrEntry( vTimeCries, 1 ); + pFanin2 = Vec_PtrEntry( vTimeCries, 2 ); + if ( Abc_ObjSlack(pFanin) < Abc_ObjSlack(pFanin2) ) + { + Vec_PtrWriteEntry( vTimeCries, 1, pFanin2 ); + Vec_PtrWriteEntry( vTimeCries, 2, pFanin ); + } + pFanin = Vec_PtrEntry( vTimeCries, 0 ); + pFanin2 = Vec_PtrEntry( vTimeCries, 1 ); + if ( Abc_ObjSlack(pFanin) < Abc_ObjSlack(pFanin2) ) + { + Vec_PtrWriteEntry( vTimeCries, 0, pFanin2 ); + Vec_PtrWriteEntry( vTimeCries, 1, pFanin ); + } + } + // add choice Abc_NtkSpeedupNode( pNtk, pNtkNew, pNode, vTimeFanins, vTimeCries ); } Vec_PtrFree( vTimeCries ); diff --git a/src/base/io/io.c b/src/base/io/io.c index 551feb0b..e1ff3b08 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -825,7 +825,7 @@ int IoCommandReadTruth( Abc_Frame_t * pAbc, int argc, char ** argv ) pSopCover = Abc_SopFromTruthHex(argv[globalUtilOptind]); else pSopCover = Abc_SopFromTruthBin(argv[globalUtilOptind]); - if ( pSopCover == NULL ) + if ( pSopCover == NULL || pSopCover[0] == 0 ) { fprintf( pAbc->Err, "Reading truth table has failed.\n" ); return 1; diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c index 513a9044..62d0f43c 100644 --- a/src/sat/bsat/satInterA.c +++ b/src/sat/bsat/satInterA.c @@ -947,7 +947,7 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in if ( fVerbose ) { - PRT( "Interpo", clock() - clkTotal ); +// PRT( "Interpo", clock() - clkTotal ); printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), -- cgit v1.2.3