From 19c28cae94cd2fe94d7cc7d9542d0fbacd9be95b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 14 Sep 2012 10:27:48 -0700 Subject: Prepared &gla to try abstracting and proving concurrently. --- src/aig/gia/gia.h | 2 + src/aig/gia/giaAbsGla2.c | 116 +++++++++++++++++++++++++++++++---------------- src/aig/gia/giaAbsPth.c | 88 +++++++++++++++++++++++++++++++++++ src/aig/gia/giaAbsVta.c | 35 +++++++------- src/aig/gia/module.make | 1 + 5 files changed, 187 insertions(+), 55 deletions(-) create mode 100644 src/aig/gia/giaAbsPth.c (limited to 'src/aig/gia') 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 +#include +#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 \ -- cgit v1.2.3