diff options
| -rw-r--r-- | abclib.dsp | 8 | ||||
| -rw-r--r-- | src/aig/gia/gia.h | 2 | ||||
| -rw-r--r-- | src/aig/gia/giaAbsGla2.c | 116 | ||||
| -rw-r--r-- | src/aig/gia/giaAbsPth.c | 88 | ||||
| -rw-r--r-- | src/aig/gia/giaAbsVta.c | 35 | ||||
| -rw-r--r-- | src/aig/gia/module.make | 1 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 20 |
7 files changed, 213 insertions, 57 deletions
@@ -2383,6 +2383,10 @@ SOURCE=.\src\map\scl\sclTime.c # End Source File # Begin Source File +SOURCE=.\src\map\scl\sclUpsize.c +# End Source File +# Begin Source File + SOURCE=.\src\map\scl\sclUtil.c # End Source File # End Group @@ -3423,6 +3427,10 @@ SOURCE=.\src\aig\gia\giaAbsOut.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaAbsPth.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaAbsRef.c # End Source File # Begin Source File diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 099c693b..a00b7111 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -233,12 +233,14 @@ struct Gia_ParVta_t_ int fUseFullProof; // use full proof for UNSAT cores int fDumpVabs; // dumps the abstracted model int fDumpMabs; // dumps the original AIG with abstraction map + int fCallProver; // calls the prover char * pFileVabs; // dumps the abstracted model into this file int fVerbose; // verbose flag int fVeryVerbose; // print additional information int iFrame; // the number of frames covered int iFrameProved; // the number of frames proved int nFramesNoChange; // the number of last frames without changes + int nFramesNoChangeLim; // the number of last frames without changes to dump abstraction }; static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); } diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index 9ca58bb9..55f79ac7 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -125,6 +125,12 @@ static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) return Lit; } + +// calling pthreads +extern void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose ); +extern void Gia_Ga2ProveCancel( int fVerbose ); +extern int Gia_Ga2ProveCheck( int fVerbose ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -1423,26 +1429,33 @@ char * Ga2_GlaGetFileName( Ga2_Man_t * p, int fAbs ) void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose ) { -// if ( fVerbose ) -// Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName ); - if ( p->pPars->fDumpVabs ) + char * pFileName; + assert( p->pPars->fDumpMabs || p->pPars->fDumpVabs || p->pPars->fCallProver ); + if ( p->pPars->fDumpMabs ) { + pFileName = Ga2_GlaGetFileName(p, 0); + if ( fVerbose ) + Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName ); + // dump abstraction map + Vec_IntFreeP( &p->pGia->vGateClasses ); + p->pGia->vGateClasses = Ga2_ManAbsTranslate( p ); + Gia_WriteAiger( p->pGia, pFileName, 0, 0 ); + } + if ( p->pPars->fDumpVabs || p->pPars->fCallProver ) + { + Vec_Int_t * vGateClasses; + Gia_Man_t * pAbs; + pFileName = Ga2_GlaGetFileName(p, 1); + if ( fVerbose ) + Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName ); // dump absracted model - Vec_Int_t * vGateClasses = Ga2_ManAbsTranslate( p ); - Gia_Man_t * pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses ); + vGateClasses = Ga2_ManAbsTranslate( p ); + pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses ); Gia_ManCleanValue( p->pGia ); - Gia_WriteAiger( pAbs, Ga2_GlaGetFileName(p, 1), 0, 0 ); + Gia_WriteAiger( pAbs, pFileName, 0, 0 ); Gia_ManStop( pAbs ); Vec_IntFreeP( &vGateClasses ); } - else if ( p->pPars->fDumpMabs ) - { - // dump abstraction map - Vec_IntFreeP( &p->pGia->vGateClasses ); - p->pGia->vGateClasses = Ga2_ManAbsTranslate( p ); - Gia_WriteAiger( p->pGia, Ga2_GlaGetFileName(p, 0), 0, 0 ); - } - else assert( 0 ); } /**Function************************************************************* @@ -1499,7 +1512,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Ga2_Man_t * p; Vec_Int_t * vCore, * vPPis; clock_t clk2, clk = clock(); - int Status = l_Undef, RetValue = -1, fOneIsSent = 0; + int Status = l_Undef, RetValue = -1, iFrameTryProve = -1, fOneIsSent = 0; int i, c, f, Lit; // check trivial case assert( Gia_ManPoNum(pAig) == 1 ); @@ -1618,6 +1631,11 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Gia_Ga2SendCancel( p, pPars->fVerbose ); fOneIsSent = 0; } + if ( iFrameTryProve >= 0 ) + { + Gia_Ga2ProveCancel( pPars->fVerbose ); + iFrameTryProve = -1; + } if ( c == 0 ) { @@ -1723,8 +1741,16 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) // print statistics if ( pPars->fVerbose ) Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 ); - if ( c > 0 ) + // check if abstraction was proved + if ( Gia_Ga2ProveCheck( pPars->fVerbose ) ) + { + RetValue = 1; + goto finish; + } + if ( c > 0 ) { + if ( p->pPars->fVeryVerbose ) + Abc_Print( 1, "\n" ); // recompute the abstraction Vec_IntFreeP( &pAig->vGateClasses ); pAig->vGateClasses = Ga2_ManAbsTranslate( p ); @@ -1734,18 +1760,12 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Status = l_Undef; goto finish; } - // speak to the bridge - if ( Abc_FrameIsBridgeMode() ) - { - // cancel old one if it was sent - if ( fOneIsSent ) - Gia_Ga2SendCancel( p, pPars->fVerbose ); - // send new one - Gia_Ga2SendAbsracted( p, pPars->fVerbose ); - fOneIsSent = 1; - } + } + // check the number of stable frames + if ( p->pPars->nFramesNoChange == p->pPars->nFramesNoChangeLim ) + { // dump the model into file - if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs ) + if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs || p->pPars->fCallProver ) { char Command[1000]; Abc_FrameSetStatus( -1 ); @@ -1755,25 +1775,45 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ); Ga2_GlaDumpAbsracted( p, pPars->fVerbose ); } - if ( p->pPars->fVeryVerbose ) - Abc_Print( 1, "\n" ); - // if abstraction grew more than a certain percentage, force a restart - if ( pPars->nRatioMax == 0 ) - break; - if ( (f > 20 || Vec_IntSize(p->vAbs) > 100) && Vec_IntSize(p->vAbs) - nAbsOld >= nAbsOld * pPars->nRatioMax / 100 ) + // call the prover + if ( p->pPars->fCallProver ) { - if ( p->pPars->fVerbose ) - Abc_Print( 1, "Forcing restart because abstraction grew from %d to %d (more than %d %%).\n", - nAbsOld, Vec_IntSize(p->vAbs), pPars->nRatioMax ); - break; + // cancel old one if it is proving + if ( iFrameTryProve >= 0 ) + Gia_Ga2ProveCancel( pPars->fVerbose ); + // prove new one + Gia_Ga2ProveAbsracted( Ga2_GlaGetFileName(p, 1), pPars->fVerbose ); + iFrameTryProve = f; + } + // speak to the bridge + if ( Abc_FrameIsBridgeMode() ) + { + // cancel old one if it was sent + if ( fOneIsSent ) + Gia_Ga2SendCancel( p, pPars->fVerbose ); + // send new one + Gia_Ga2SendAbsracted( p, pPars->fVerbose ); + fOneIsSent = 1; } } + // if abstraction grew more than a certain percentage, force a restart + if ( pPars->nRatioMax == 0 ) + break; + if ( c > 0 && (f > 20 || Vec_IntSize(p->vAbs) > 100) && Vec_IntSize(p->vAbs) - nAbsOld >= nAbsOld * pPars->nRatioMax / 100 ) + { + if ( p->pPars->fVerbose ) + Abc_Print( 1, "Forcing restart because abstraction grew from %d to %d (more than %d %%).\n", + nAbsOld, Vec_IntSize(p->vAbs), pPars->nRatioMax ); + break; + } } } finish: Prf_ManStopP( &p->pSat->pPrf2 ); // analize the results - if ( pAig->pCexSeq == NULL ) + if ( RetValue == 1 ) + Abc_Print( 1, "GLA completed %d frames and proved abstraction derived in frame %d. ", p->pPars->iFrameProved+1, iFrameTryProve ); + else if ( pAig->pCexSeq == NULL ) { // if ( pAig->vGateClasses != NULL ) // Abc_Print( 1, "Replacing the old abstraction by a new one.\n" ); diff --git a/src/aig/gia/giaAbsPth.c b/src/aig/gia/giaAbsPth.c new file mode 100644 index 00000000..31f63674 --- /dev/null +++ b/src/aig/gia/giaAbsPth.c @@ -0,0 +1,88 @@ +/**CFile**************************************************************** + + FileName [giaAbsPth.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Interface to pthreads.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaAbsPth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" + +// comment this out to disable pthreads +//#define ABC_USE_PTHREADS + +#ifdef ABC_USE_PTHREADS + +#ifdef WIN32 +#include "../lib/pthread.h" +#else +#include <pthread.h> +#include <unistd.h> +#endif + +#endif + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Start and stop proving abstracted model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +#ifndef ABC_USE_PTHREADS + +void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose ) {} +void Gia_Ga2ProveCancel( int fVerbose ) {} +int Gia_Ga2ProveCheck( int fVerbose ) { return 0; } + +#else // pthreads are used + +void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose ) +{ + Abc_Print( 1, "Trying to prove abstraction.\n" ); +} +void Gia_Ga2ProveCancel( int fVerbose ) +{ + Abc_Print( 1, "Canceling attempt to prove abstraction.\n" ); +} +int Gia_Ga2ProveCheck( int fVerbose ) +{ + return 0; +} + +#endif + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index b5115947..517c1d3d 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -148,23 +148,24 @@ extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame ); void Gia_VtaSetDefaultParams( Gia_ParVta_t * p ) { memset( p, 0, sizeof(Gia_ParVta_t) ); - p->nFramesMax = 0; // maximum frames - p->nFramesStart = 0; // starting frame - p->nFramesPast = 4; // overlap frames - p->nConfLimit = 0; // conflict limit - p->nLearnedMax = 1000; // max number of learned clauses - p->nLearnedStart = 1000; // max number of learned clauses - p->nLearnedDelta = 200; // max number of learned clauses - p->nLearnedPerce = 70; // max number of learned clauses - p->nTimeOut = 0; // timeout in seconds - p->nRatioMin = 20; // stop when less than this % of object is abstracted - p->nRatioMax = 30; // restart when more than this % of object is abstracted - p->fUseTermVars = 0; // use terminal variables - p->fUseRollback = 0; // use rollback to the starting number of frames - p->fPropFanout = 1; // propagate fanouts during refinement - p->fVerbose = 0; // verbose flag - p->iFrame = -1; // the number of frames covered - p->iFrameProved = -1; // the number of frames proved + p->nFramesMax = 0; // maximum frames + p->nFramesStart = 0; // starting frame + p->nFramesPast = 4; // overlap frames + p->nConfLimit = 0; // conflict limit + p->nLearnedMax = 1000; // max number of learned clauses + p->nLearnedStart = 1000; // max number of learned clauses + p->nLearnedDelta = 200; // max number of learned clauses + p->nLearnedPerce = 70; // max number of learned clauses + p->nTimeOut = 0; // timeout in seconds + p->nRatioMin = 0; // stop when less than this % of object is abstracted + p->nRatioMax = 30; // restart when more than this % of object is abstracted + p->fUseTermVars = 0; // use terminal variables + p->fUseRollback = 0; // use rollback to the starting number of frames + p->fPropFanout = 1; // propagate fanouts during refinement + p->fVerbose = 0; // verbose flag + p->iFrame = -1; // the number of frames covered + p->iFrameProved = -1; // the number of frames proved + p->nFramesNoChangeLim = 1; // the number of frames without change to dump abstraction } /**Function************************************************************* diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 833f551c..ea3ca24d 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -4,6 +4,7 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaAbsGla2.c \ src/aig/gia/giaAbsIter.c \ src/aig/gia/giaAbsOut.c \ + src/aig/gia/giaAbsPth.c \ src/aig/gia/giaAbsRef.c \ src/aig/gia/giaAbsRef2.c \ src/aig/gia/giaAbsVta.c \ diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d47418a1..fe054071 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -28342,7 +28342,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) int c, fStartVta = 0, fNewAlgo = 1; Gia_VtaSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPAtrfkadmnscbpwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPBAtrfkadmnscbpqwvh" ) ) != EOF ) { switch ( c ) { @@ -28445,6 +28445,17 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nRatioMax < 0 ) goto usage; break; + case 'B': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFramesNoChangeLim = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFramesNoChangeLim < 0 ) + goto usage; + break; case 'A': if ( globalUtilOptind >= argc ) { @@ -28490,6 +28501,9 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'p': pPars->fUseFullProof ^= 1; break; + case 'q': + pPars->fCallProver ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -28538,7 +28552,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &gla [-FSCLDETRP num] [-A file] [-fkadmnscbpwvh]\n" ); + Abc_Print( -2, "usage: &gla [-FSCLDETRPB num] [-A file] [-fkadmnscbpqwvh]\n" ); Abc_Print( -2, "\t fixed-time-frame gate-level proof- and cex-based abstraction\n" ); Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart ); @@ -28549,6 +28563,7 @@ usage: Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut ); Abc_Print( -2, "\t-R num : minimum percentage of abstracted objects (0<=num<=100) [default = %d]\n", pPars->nRatioMin ); Abc_Print( -2, "\t-P num : maximum percentage of added objects before a restart (0<=num<=100) [default = %d]\n", pPars->nRatioMax ); + Abc_Print( -2, "\t-B num : the number of stable frames to dump abstraction or call prover (0<=num<=100) [default = %d]\n", pPars->nFramesNoChangeLim ); Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" ); Abc_Print( -2, "\t-f : toggle propagating fanout implications [default = %s]\n", pPars->fPropFanout? "yes": "no" ); Abc_Print( -2, "\t-k : toggle using VTA to kick start GLA for starting frames [default = %s]\n", fStartVta? "yes": "no" ); @@ -28560,6 +28575,7 @@ usage: Abc_Print( -2, "\t-c : toggle using naive (2-input AND node) CNF encoding [default = %s]\n", pPars->fUseSimple? "yes": "no" ); Abc_Print( -2, "\t-b : toggle CNF construction without hashing [default = %s]\n", pPars->fSkipHash? "yes": "no" ); Abc_Print( -2, "\t-p : toggle using full-proof for UNSAT cores [default = %s]\n", pPars->fUseFullProof? "yes": "no" ); + Abc_Print( -2, "\t-q : toggle calling the prover [default = %s]\n", pPars->fCallProver? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); |