summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c55
-rw-r--r--src/base/abci/abcDar.c7
-rw-r--r--src/proof/ssw/sswRarity.c2
-rw-r--r--src/sat/bmc/bmc.h12
-rw-r--r--src/sat/bmc/bmcBmc3.c2
-rw-r--r--src/sat/bmc/bmcMulti.c52
6 files changed, 79 insertions, 51 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b8b5f5c4..d4cec6dd 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -32346,16 +32346,15 @@ usage:
***********************************************************************/
int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern int Gia_ManMultiProve( Gia_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fUseSyn, int fVerbose, int fVeryVerbose );
- Vec_Int_t * vStatuses;
- int TimeOutGlo = 30;
- int TimeOutLoc = 2;
- int TimeOutInc = 2;
- int fUseSyn = 0;
- int c, fVerbose = 0;
- int fVeryVerbose = 0;
+ extern int Gia_ManMultiProve( Gia_Man_t * p, Bmc_MulPar_t * pPars );
+ Vec_Int_t * vStatuses; int c;
+ Bmc_MulPar_t Pars, * pPars = &Pars;
+ memset( pPars, 0, sizeof(Bmc_MulPar_t) );
+ pPars->TimeOutGlo = 30;
+ pPars->TimeOutLoc = 2;
+ pPars->TimeOutInc = 100;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "TLMsvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "TLMsdvwh" ) ) != EOF )
{
switch ( c )
{
@@ -32365,9 +32364,9 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
- TimeOutGlo = atoi(argv[globalUtilOptind]);
+ pPars->TimeOutGlo = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( TimeOutGlo < 0 )
+ if ( pPars->TimeOutGlo < 0 )
goto usage;
break;
case 'L':
@@ -32376,9 +32375,9 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
- TimeOutLoc = atoi(argv[globalUtilOptind]);
+ pPars->TimeOutLoc = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( TimeOutLoc <= 0 )
+ if ( pPars->TimeOutLoc <= 0 )
goto usage;
break;
case 'M':
@@ -32387,19 +32386,22 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
- TimeOutInc = atoi(argv[globalUtilOptind]);
+ pPars->TimeOutInc = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( TimeOutInc <= 0 )
+ if ( pPars->TimeOutInc <= 0 )
goto usage;
break;
case 's':
- fUseSyn ^= 1;
+ pPars->fUseSyn ^= 1;
+ break;
+ case 'd':
+ pPars->fDumpFinal ^= 1;
break;
case 'v':
- fVerbose ^= 1;
+ pPars->fVerbose ^= 1;
break;
case 'w':
- fVeryVerbose ^= 1;
+ pPars->fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
@@ -32412,21 +32414,22 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" );
return 1;
}
- pAbc->Status = Gia_ManMultiProve( pAbc->pGia, TimeOutGlo, TimeOutLoc, TimeOutInc, fUseSyn, fVerbose, fVeryVerbose );
+ pAbc->Status = Gia_ManMultiProve( pAbc->pGia, pPars );
vStatuses = Abc_FrameDeriveStatusArray( pAbc->pGia->vSeqModelVec );
Abc_FrameReplacePoStatuses( pAbc, &vStatuses );
Abc_FrameReplaceCexVec( pAbc, &pAbc->pGia->vSeqModelVec );
return 0;
usage:
- Abc_Print( -2, "usage: &mprove [-TLM num] [-svwh]\n" );
+ Abc_Print( -2, "usage: &mprove [-TLM num] [-sdvwh]\n" );
Abc_Print( -2, "\t proves multi-output testcase by applying several engines\n" );
- 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-T num : approximate global runtime limit in seconds [default = %d]\n", pPars->TimeOutGlo );
+ Abc_Print( -2, "\t-L num : approximate local runtime limit in seconds [default = %d]\n", pPars->TimeOutLoc );
+ Abc_Print( -2, "\t-M num : percentage of local runtime limit increase [default = %d]\n", pPars->TimeOutInc );
+ Abc_Print( -2, "\t-s : toggle using combinational synthesis [default = %s]\n", pPars->fUseSyn? "yes": "no" );
+ Abc_Print( -2, "\t-d : toggle dumping invariant into a file [default = %s]\n", pPars->fDumpFinal? "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 additional verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index d662f376..4800557a 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2174,16 +2174,17 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
{
int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
- Abc_Print( 1, "None of the %d outputs is found to be SAT. ", nOutputs );
+ Abc_Print( 1, "None of the %d outputs is found to be SAT", nOutputs );
else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
- Abc_Print( 1, "All %d outputs are found to be SAT. ", nOutputs );
+ Abc_Print( 1, "All %d outputs are found to be SAT", nOutputs );
else
{
Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
if ( pPars->nDropOuts )
Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs );
- Abc_Print( 1, ". " );
}
+ Abc_Print( 1, " after %d frames", pPars->iFrame );
+ Abc_Print( 1, ". " );
}
}
ABC_PRT( "Time", Abc_Clock() - clk );
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 39f95e14..2dd51f38 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -1112,12 +1112,14 @@ finish:
}
if ( pPars->nSolved )
{
+/*
if ( !pPars->fSilent )
{
if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved, Saig_ManPoNum(p->pAig) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
+*/
}
else if ( r == pPars->nRounds && f == pPars->nFrames )
{
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index ff1e005b..1a98001a 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -91,6 +91,18 @@ struct Bmc_AndPar_t_
int nFailOuts; // the number of failed outputs
int nDropOuts; // the number of dropped outputs
};
+
+typedef struct Bmc_MulPar_t_ Bmc_MulPar_t;
+struct Bmc_MulPar_t_
+{
+ int TimeOutGlo;
+ int TimeOutLoc;
+ int TimeOutInc;
+ int fUseSyn;
+ int fDumpFinal;
+ int fVerbose;
+ int fVeryVerbose;
+};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index ea08c1e4..4cc2a692 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1353,7 +1353,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
goto finish;
}
// consider the next timeframe
- if ( RetValue == -1 && pPars->nStart == 0 && !nJumpFrame )
+ if ( (RetValue == -1 || pPars->fSolveAll) && pPars->nStart == 0 && !nJumpFrame )
pPars->iFrame = f-1;
// map nodes of this section
Vec_PtrPush( p->vId2Var, Vec_IntStartFull(p->nObjNums) );
diff --git a/src/sat/bmc/bmcMulti.c b/src/sat/bmc/bmcMulti.c
index 975783d9..6b60daf9 100644
--- a/src/sat/bmc/bmcMulti.c
+++ b/src/sat/bmc/bmcMulti.c
@@ -20,7 +20,9 @@
#include "bmc.h"
#include "proof/ssw/ssw.h"
+#include "misc/extra/extra.h"
#include "aig/gia/giaAig.h"
+#include "aig/ioa/ioa.h"
ABC_NAMESPACE_IMPL_START
@@ -128,7 +130,7 @@ Aig_Man_t * Gia_ManMultiProveSyn( Aig_Man_t * p, int fVerbose, int fVeryVerbose
SeeAlso []
***********************************************************************/
-Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fUseSyn, int fVerbose, int fVeryVerbose )
+Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
{
Ssw_RarPars_t ParsSim, * pParsSim = &ParsSim;
Saig_ParBmc_t ParsBmc, * pParsBmc = &ParsBmc;
@@ -136,12 +138,12 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
Vec_Ptr_t * vCexes;
Aig_Man_t * pTemp;
abctime clkStart = Abc_Clock();
- int nTimeToStop = TimeOutGlo ? TimeOutGlo * CLOCKS_PER_SEC + Abc_Clock(): 0;
+ int nTimeToStop = pPars->TimeOutGlo ? pPars->TimeOutGlo * CLOCKS_PER_SEC + Abc_Clock(): 0;
int nTotalPo = Saig_ManPoNum(p);
int nTotalSize = Aig_ManObjNum(p);
int i, RetValue = -1;
- if ( fVerbose )
- printf( "MultiProve parameters: Global timeout = %d sec. Local timeout = %d sec. Time increase = %d.\n", TimeOutGlo, TimeOutLoc, TimeOutInc );
+ if ( pPars->fVerbose )
+ printf( "MultiProve parameters: Global timeout = %d sec. Local timeout = %d sec. Time increase = %d %%.\n", pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc );
// create output map
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)
@@ -151,8 +153,8 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
Ssw_RarSetDefaultParams( pParsSim );
pParsSim->fSolveAll = 1;
pParsSim->fNotVerbose = 1;
- pParsSim->fSilent = !fVeryVerbose;
- pParsSim->TimeOut = TimeOutLoc;
+ pParsSim->fSilent = !pPars->fVeryVerbose;
+ pParsSim->TimeOut = pPars->TimeOutLoc;
pParsSim->nRandSeed = (i * 17) % 500;
RetValue *= Ssw_RarSimulate( p, pParsSim );
// sort outputs
@@ -166,13 +168,13 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
Vec_IntFree( vLeftOver );
Aig_ManStop( pTemp );
}
- if ( fVerbose )
+ if ( pPars->fVerbose )
Gia_ManMultiReport( p, "SIM", nTotalPo, nTotalSize, clkStart );
// check timeout
- if ( nTimeToStop && Abc_Clock() > nTimeToStop )
+ if ( nTimeToStop && pPars->TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop )
{
- printf( "Global timeout (%d sec) is reached.\n", TimeOutGlo );
+ printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
break;
}
@@ -180,9 +182,12 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
Saig_ParBmcSetDefaultParams( pParsBmc );
pParsBmc->fSolveAll = 1;
pParsBmc->fNotVerbose = 1;
- pParsBmc->fSilent = !fVeryVerbose;
- pParsBmc->nTimeOut = TimeOutLoc;
+ pParsBmc->fSilent = !pPars->fVeryVerbose;
+ pParsBmc->nTimeOut = pPars->TimeOutLoc;
RetValue *= Saig_ManBmcScalable( p, pParsBmc );
+ if ( pPars->fVeryVerbose )
+ Abc_Print( 1, "Some outputs are SAT (%d out of %d) after %d frames.\n",
+ Saig_ManPoNum(p) - Vec_PtrCountZero(p->vSeqModelVec), Saig_ManPoNum(p), pParsBmc->iFrame );
// sort outputs
if ( p->vSeqModelVec )
{
@@ -194,41 +199,46 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
Vec_IntFree( vLeftOver );
Aig_ManStop( pTemp );
}
- if ( fVerbose )
+ if ( pPars->fVerbose )
Gia_ManMultiReport( p, "BMC", nTotalPo, nTotalSize, clkStart );
// check timeout
- if ( nTimeToStop && Abc_Clock() > nTimeToStop )
+ if ( nTimeToStop && pPars->TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop )
{
- printf( "Global timeout (%d sec) is reached.\n", TimeOutGlo );
+ printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
break;
}
// synthesize
- if ( fUseSyn )
+ if ( pPars->fUseSyn )
{
- p = Gia_ManMultiProveSyn( pTemp = p, fVerbose, fVeryVerbose );
+ p = Gia_ManMultiProveSyn( pTemp = p, pPars->fVerbose, pPars->fVeryVerbose );
Aig_ManStop( pTemp );
- if ( fVerbose )
+ if ( pPars->fVerbose )
Gia_ManMultiReport( p, "SYN", nTotalPo, nTotalSize, clkStart );
}
// increase timeout
- TimeOutLoc *= TimeOutInc;
+ pPars->TimeOutLoc += pPars->TimeOutLoc * pPars->TimeOutInc / 100;
}
Vec_IntFree( vOutMap );
+ if ( pPars->fDumpFinal )
+ {
+ char * pFileName = Extra_FileNameGenericAppend( p->pName, "_out.aig" );
+ Ioa_WriteAiger( p, pFileName, 0, 0 );
+ printf( "Final AIG was dumped into file \"%s\".\n", pFileName );
+ }
Aig_ManStop( p );
return vCexes;
}
-int Gia_ManMultiProve( Gia_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fUseSyn, int fVerbose, int fVeryVerbose )
+int Gia_ManMultiProve( Gia_Man_t * p, Bmc_MulPar_t * pPars )
{
Aig_Man_t * pAig;
if ( p->vSeqModelVec )
Vec_PtrFreeFree( p->vSeqModelVec ), p->vSeqModelVec = NULL;
pAig = Gia_ManToAig( p, 0 );
- p->vSeqModelVec = Gia_ManMultiProveAig( pAig, TimeOutGlo, TimeOutLoc, TimeOutInc, fUseSyn, fVerbose, fVeryVerbose );
+ p->vSeqModelVec = Gia_ManMultiProveAig( pAig, pPars ); // deletes pAig
assert( Vec_PtrSize(p->vSeqModelVec) == Gia_ManPoNum(p) );
-// Aig_ManStop( pAig );
return Vec_PtrCountZero(p->vSeqModelVec) == Vec_PtrSize(p->vSeqModelVec) ? -1 : 0;
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-29 11:25:48 +0000