Skip to content

A
abc
Commit 94376645 by Alan Mishchenko
Options

Multi-output property solver.

parent 7d2b77af
Showing with 127 additions and 29 deletions
src/base/abci/abc.c
...@@ -2447,13 +2447,16 @@ usage: ...@@ -2447,13 +2447,16 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
int c; int c, fShort = 1;
// set defaults // set defaults
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
case 's':
fShort ^= 1;
break;
case 'h': case 'h':
goto usage; goto usage;
default: default:
...@@ -2492,16 +2495,26 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2492,16 +2495,26 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
if ( pAbc->vStatuses ) if ( pAbc->vStatuses )
{ {
int i, Entry; if ( fShort )
Vec_IntForEachEntry( pAbc->vStatuses, Entry, i ) {
printf( "%d=%d ", i, Entry ); printf( "Status array contains %d SAT, %d UNSAT, and %d UNDEC entries (out of %d).",
Vec_IntCountEntry(pAbc->vStatuses, 0), Vec_IntCountEntry(pAbc->vStatuses, 1),
Vec_IntCountEntry(pAbc->vStatuses, -1), Vec_IntSize(pAbc->vStatuses) );
}
else
{
int i, Entry;
Vec_IntForEachEntry( pAbc->vStatuses, Entry, i )
printf( "%d=%d ", i, Entry );
}
printf( "\n" ); printf( "\n" );
} }
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: print_status [-h]\n" ); Abc_Print( -2, "usage: print_status [-sh]\n" );
Abc_Print( -2, "\t prints verification status\n" ); Abc_Print( -2, "\t prints verification status\n" );
Abc_Print( -2, "\t-s : toggle using short print-out [default = %s]\n", fShort? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t-h : print the command usage\n");
return 1; return 1;
} }
...@@ -32333,18 +32346,61 @@ usage: ...@@ -32333,18 +32346,61 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
extern int Gia_ManMultiProve( Gia_Man_t * p, int fVerbose ); extern int Gia_ManMultiProve( Gia_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fUseSyn, int fVerbose, int fVeryVerbose );
Vec_Int_t * vStatuses; Vec_Int_t * vStatuses;
char * pCommLine = NULL; int TimeOutGlo = 30;
int TimeOutLoc = 2;
int TimeOutInc = 2;
int fUseSyn = 0;
int c, fVerbose = 0; int c, fVerbose = 0;
int fVeryVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "TLMsvwh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
TimeOutGlo = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( TimeOutGlo < 0 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
TimeOutLoc = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( TimeOutLoc <= 0 )
goto usage;
break;
case 'M':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
TimeOutInc = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( TimeOutInc <= 0 )
goto usage;
break;
case 's':
fUseSyn ^= 1;
break;
case 'v': case 'v':
fVerbose ^= 1; fVerbose ^= 1;
break; break;
case 'w':
fVeryVerbose ^= 1;
break;
case 'h': case 'h':
goto usage; goto usage;
default: default:
...@@ -32356,16 +32412,21 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -32356,16 +32412,21 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" ); Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" );
return 1; return 1;
} }
pAbc->Status = Gia_ManMultiProve( pAbc->pGia, fVerbose ); pAbc->Status = Gia_ManMultiProve( pAbc->pGia, TimeOutGlo, TimeOutLoc, TimeOutInc, fUseSyn, fVerbose, fVeryVerbose );
vStatuses = Abc_FrameDeriveStatusArray( pAbc->pGia->vSeqModelVec ); vStatuses = Abc_FrameDeriveStatusArray( pAbc->pGia->vSeqModelVec );
Abc_FrameReplacePoStatuses( pAbc, &vStatuses ); Abc_FrameReplacePoStatuses( pAbc, &vStatuses );
Abc_FrameReplaceCexVec( pAbc, &pAbc->pGia->vSeqModelVec ); Abc_FrameReplaceCexVec( pAbc, &pAbc->pGia->vSeqModelVec );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &mprove [-vh]\n" ); Abc_Print( -2, "usage: &mprove [-TLM num] [-svwh]\n" );
Abc_Print( -2, "\t proves multi-output testcase by applying several engines\n" ); Abc_Print( -2, "\t proves multi-output testcase by applying several engines\n" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", TimeOutGlo );
Abc_Print( -2, "\t-L num : approximate local runtime limit in seconds [default = %d]\n", TimeOutLoc );
Abc_Print( -2, "\t-M num : approximate multiple of the local runtime limit [default = %d]\n", TimeOutInc );
Abc_Print( -2, "\t-s : toggle using combinational synthesis [default = %s]\n", fUseSyn? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing additional verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t-h : print the command usage\n");
return 1; return 1;
} }
src/proof/ssw/sswRarity.c
...@@ -1054,7 +1054,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ) ...@@ -1054,7 +1054,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
if ( !pPars->fSilent ) if ( !pPars->fSilent )
{ {
if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" ); if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart ); Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts and solved %d outputs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved );
Abc_Print( 1, "Reached timeout (%d sec).\n", pPars->TimeOut ); Abc_Print( 1, "Reached timeout (%d sec).\n", pPars->TimeOut );
} }
goto finish; goto finish;
...@@ -1064,7 +1064,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ) ...@@ -1064,7 +1064,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
if ( !pPars->fSilent ) if ( !pPars->fSilent )
{ {
if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" ); if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart ); Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts and solved %d outputs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved );
Abc_Print( 1, "Reached gap timeout (%d sec).\n", pPars->TimeOutGap ); Abc_Print( 1, "Reached gap timeout (%d sec).\n", pPars->TimeOutGap );
} }
goto finish; goto finish;
......
src/sat/bmc/bmcMulti.c
...@@ -105,7 +105,30 @@ void Gia_ManMultiReport( Aig_Man_t * p, char * pStr, int nTotalPo, int nTotalSiz ...@@ -105,7 +105,30 @@ void Gia_ManMultiReport( Aig_Man_t * p, char * pStr, int nTotalPo, int nTotalSiz
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fVerbose ) Aig_Man_t * Gia_ManMultiProveSyn( Aig_Man_t * p, int fVerbose, int fVeryVerbose )
{
Aig_Man_t * pAig;
Gia_Man_t * pGia, * pTemp;
pGia = Gia_ManFromAig( p );
pGia = Gia_ManAigSyn2( pTemp = pGia, 0, 0 );
Gia_ManStop( pTemp );
pAig = Gia_ManToAig( pGia, 0 );
Gia_ManStop( pGia );
return pAig;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fUseSyn, int fVerbose, int fVeryVerbose )
{ {
Ssw_RarPars_t ParsSim, * pParsSim = &ParsSim; Ssw_RarPars_t ParsSim, * pParsSim = &ParsSim;
Saig_ParBmc_t ParsBmc, * pParsBmc = &ParsBmc; Saig_ParBmc_t ParsBmc, * pParsBmc = &ParsBmc;
...@@ -117,22 +140,18 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc, ...@@ -117,22 +140,18 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
int nTotalPo = Saig_ManPoNum(p); int nTotalPo = Saig_ManPoNum(p);
int nTotalSize = Aig_ManObjNum(p); int nTotalSize = Aig_ManObjNum(p);
int i, RetValue = -1; int i, RetValue = -1;
if ( fVerbose )
printf( "MultiProve parameters: Global timeout = %d sec. Local timeout = %d sec. Time increase = %d.\n", TimeOutGlo, TimeOutLoc, TimeOutInc );
// create output map // create output map
vOutMap = Vec_IntStartNatural( Saig_ManPoNum(p) ); // maps current outputs into their original IDs vOutMap = Vec_IntStartNatural( Saig_ManPoNum(p) ); // maps current outputs into their original IDs
vCexes = Vec_PtrStart( Saig_ManPoNum(p) ); // maps solved outputs into their CEXes (or markers) vCexes = Vec_PtrStart( Saig_ManPoNum(p) ); // maps solved outputs into their CEXes (or markers)
for ( i = 0; i < 1000; i++ ) for ( i = 0; i < 1000; i++ )
{ {
// synthesize
// p = Gia_ManMultiProveSyn( pTemp = p );
// Aig_ManStop( pTemp );
// if ( fVerbose )
// Gia_ManMultiReport( p, "SYN", nTotalPo, nTotalSize, clkStart );
// perform SIM3 // perform SIM3
Ssw_RarSetDefaultParams( pParsSim ); Ssw_RarSetDefaultParams( pParsSim );
pParsSim->fSolveAll = 1; pParsSim->fSolveAll = 1;
pParsSim->fNotVerbose = 1; pParsSim->fNotVerbose = 1;
pParsSim->fSilent = 1; pParsSim->fSilent = !fVeryVerbose;
pParsSim->TimeOut = TimeOutLoc; pParsSim->TimeOut = TimeOutLoc;
pParsSim->nRandSeed = (i * 17) % 500; pParsSim->nRandSeed = (i * 17) % 500;
RetValue *= Ssw_RarSimulate( p, pParsSim ); RetValue *= Ssw_RarSimulate( p, pParsSim );
...@@ -147,14 +166,21 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc, ...@@ -147,14 +166,21 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
Vec_IntFree( vLeftOver ); Vec_IntFree( vLeftOver );
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
} }
// if ( fVerbose ) if ( fVerbose )
Gia_ManMultiReport( p, "SIM", nTotalPo, nTotalSize, clkStart ); Gia_ManMultiReport( p, "SIM", nTotalPo, nTotalSize, clkStart );
// check timeout
if ( nTimeToStop && Abc_Clock() > nTimeToStop )
{
printf( "Global timeout (%d sec) is reached.\n", TimeOutGlo );
break;
}
// perform BMC // perform BMC
Saig_ParBmcSetDefaultParams( pParsBmc ); Saig_ParBmcSetDefaultParams( pParsBmc );
pParsBmc->fSolveAll = 1; pParsBmc->fSolveAll = 1;
pParsBmc->fNotVerbose = 1; pParsBmc->fNotVerbose = 1;
pParsBmc->fSilent = 1; pParsBmc->fSilent = !fVeryVerbose;
pParsBmc->nTimeOut = TimeOutLoc; pParsBmc->nTimeOut = TimeOutLoc;
RetValue *= Saig_ManBmcScalable( p, pParsBmc ); RetValue *= Saig_ManBmcScalable( p, pParsBmc );
// sort outputs // sort outputs
...@@ -168,28 +194,39 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc, ...@@ -168,28 +194,39 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
Vec_IntFree( vLeftOver ); Vec_IntFree( vLeftOver );
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
} }
// if ( fVerbose ) if ( fVerbose )
Gia_ManMultiReport( p, "BMC", nTotalPo, nTotalSize, clkStart ); Gia_ManMultiReport( p, "BMC", nTotalPo, nTotalSize, clkStart );
// increase timeout // check timeout
TimeOutLoc *= TimeOutInc;
if ( nTimeToStop && Abc_Clock() > nTimeToStop ) if ( nTimeToStop && Abc_Clock() > nTimeToStop )
{ {
printf( "Global timeout (%d sec) is reached.\n", TimeOutGlo ); printf( "Global timeout (%d sec) is reached.\n", TimeOutGlo );
break; break;
} }
// synthesize
if ( fUseSyn )
{
p = Gia_ManMultiProveSyn( pTemp = p, fVerbose, fVeryVerbose );
Aig_ManStop( pTemp );
if ( fVerbose )
Gia_ManMultiReport( p, "SYN", nTotalPo, nTotalSize, clkStart );
}
// increase timeout
TimeOutLoc *= TimeOutInc;
} }
Vec_IntFree( vOutMap ); Vec_IntFree( vOutMap );
Aig_ManStop( p ); Aig_ManStop( p );
return vCexes; return vCexes;
} }
int Gia_ManMultiProve( Gia_Man_t * p, int fVerbose ) int Gia_ManMultiProve( Gia_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fUseSyn, int fVerbose, int fVeryVerbose )
{ {
Aig_Man_t * pAig; Aig_Man_t * pAig;
if ( p->vSeqModelVec ) if ( p->vSeqModelVec )
Vec_PtrFreeFree( p->vSeqModelVec ), p->vSeqModelVec = NULL; Vec_PtrFreeFree( p->vSeqModelVec ), p->vSeqModelVec = NULL;
pAig = Gia_ManToAig( p, 0 ); pAig = Gia_ManToAig( p, 0 );
p->vSeqModelVec = Gia_ManMultiProveAig( pAig, 30, 2, 2, fVerbose ); p->vSeqModelVec = Gia_ManMultiProveAig( pAig, TimeOutGlo, TimeOutLoc, TimeOutInc, fUseSyn, fVerbose, fVeryVerbose );
assert( Vec_PtrSize(p->vSeqModelVec) == Gia_ManPoNum(p) ); assert( Vec_PtrSize(p->vSeqModelVec) == Gia_ManPoNum(p) );
// Aig_ManStop( pAig ); // Aig_ManStop( pAig );
return Vec_PtrCountZero(p->vSeqModelVec) == Vec_PtrSize(p->vSeqModelVec) ? -1 : 0; return Vec_PtrCountZero(p->vSeqModelVec) == Vec_PtrSize(p->vSeqModelVec) ? -1 : 0;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment