summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abcProve.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci/abcProve.c')
-rw-r--r--src/base/abci/abcProve.c143
1 files changed, 83 insertions, 60 deletions
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index ae4bb250..c0e904bf 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -20,6 +20,7 @@
#include "abc.h"
#include "fraig.h"
+#include "math.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -32,10 +33,11 @@ extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue, int * pNumFails );
static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-
+
/**Function*************************************************************
Synopsis [Attempts to solve the miter using a number of tricks.]
@@ -50,106 +52,126 @@ static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fV
SeeAlso []
***********************************************************************/
-int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fUseRewrite, int fUseFraig, int fVerbose )
+int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
{
+ Prove_Params_t * pParams = pPars;
Abc_Ntk_t * pNtk, * pNtkTemp;
- int nConfsStart = 1000, nImpsStart = 0, nBTLimitStart = 2; // was 5000
- int nConfs, nImps, nBTLimit, RetValue, nSatFails;
- int nIter = 0, clk, timeStart = clock();
+ int RetValue, nIter, Counter, clk, timeStart = clock();
// get the starting network
pNtk = *ppNtk;
assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkPoNum(pNtk) == 1 );
- // set the initial limits
- nConfs = !nConfLimit? nConfsStart : ABC_MIN( nConfsStart, nConfLimit );
- nImps = !nImpLimit ? nImpsStart : ABC_MIN( nImpsStart , nImpLimit );
- nBTLimit = nBTLimitStart;
-
- if ( fVerbose )
- printf( "Global resource limits: ConfsLim = %6d. ImpsLim = %d.\n", nConfLimit, nImpLimit );
+ if ( pParams->fVerbose )
+ {
+ printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n",
+ pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" );
+ printf( "Mitering = %d (%3.1f). Rewriting = %d (%3.1f). Fraiging = %d (%3.1f).\n",
+ pParams->nMiteringLimitStart, pParams->nMiteringLimitMulti,
+ pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti,
+ pParams->nFraigingLimitStart, pParams->nFraigingLimitMulti );
+ printf( "Mitering last = %d.\n",
+ pParams->nMiteringLimitLast );
+ }
// if SAT only, solve without iteration
- if ( !fUseRewrite && !fUseFraig )
+ if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
{
clk = clock();
- RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, 0 );
- Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose );
+ RetValue = Abc_NtkMiterSat( pNtk, pParams->nMiteringLimitLast, 0, 0, 0 );
+ Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
*ppNtk = pNtk;
return RetValue;
}
// check the current resource limits
- do {
- nIter++;
-
- if ( fVerbose )
+ for ( nIter = 0; nIter < pParams->nItersMax; nIter++ )
+ {
+ if ( pParams->fVerbose )
{
- printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter, nConfs, nBTLimit );
+ printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1,
+ (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)),
+ (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) );
fflush( stdout );
}
// try brute-force SAT
clk = clock();
- RetValue = Abc_NtkMiterSat( pNtk, nConfs, nImps, 0 );
- Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose );
+ RetValue = Abc_NtkMiterSat( pNtk, (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), 0, 0, 0 );
+ Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
if ( RetValue >= 0 )
break;
- if ( fUseRewrite )
+ // try rewriting
+ if ( pParams->fUseRewriting )
{
clk = clock();
-
- // try rewriting
- Abc_NtkRewrite( pNtk, 0, 0, 0 );
- if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
- break;
- Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
- if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
- break;
- pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp );
- if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
- break;
-
- Abc_NtkMiterPrint( pNtk, "Rewriting ", clk, fVerbose );
+ Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
+ while ( 1 )
+ {
+ Abc_NtkRewrite( pNtk, 0, 0, 0 );
+ if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
+ break;
+ if ( --Counter == 0 )
+ break;
+ Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
+ if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
+ break;
+ if ( --Counter == 0 )
+ break;
+ pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp );
+ if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
+ break;
+ if ( --Counter == 0 )
+ break;
+ }
+ Abc_NtkMiterPrint( pNtk, "Rewriting ", clk, pParams->fVerbose );
}
-
- if ( fUseFraig )
+
+ if ( pParams->fUseFraiging )
{
+ int nSatFails;
// try FRAIGing
clk = clock();
- pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, nBTLimit, &RetValue, &nSatFails ); Abc_NtkDelete( pNtkTemp );
- Abc_NtkMiterPrint( pNtk, "FRAIGing ", clk, fVerbose );
+ pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)), &RetValue, &nSatFails ); Abc_NtkDelete( pNtkTemp );
+ Abc_NtkMiterPrint( pNtk, "FRAIGing ", clk, pParams->fVerbose );
// printf( "NumFails = %d\n", nSatFails );
if ( RetValue >= 0 )
break;
}
- else
- nSatFails = 1000;
-
- // increase resource limits
-// nConfs = ABC_MIN( nConfs * 3 / 2, 1000000000 ); // was 4/2
- nConfs = nSatFails * nBTLimit / 2;
- nImps = ABC_MIN( nImps * 3 / 2, 1000000000 );
- nBTLimit = ABC_MIN( nBTLimit * 8, 1000000000 );
-
- // timeout at 5 minutes
-// if ( clock() - timeStart >= 1200 * CLOCKS_PER_SEC )
-// break;
- if ( nIter == 7 )
- break;
}
-// while ( (nConfLimit == 0 || nConfs <= nConfLimit) &&
-// (nImpLimit == 0 || nImps <= nImpLimit ) );
- while ( 1 );
// try to prove it using brute force SAT
+ if ( RetValue < 0 && pParams->fUseBdds )
+ {
+ if ( pParams->fVerbose )
+ {
+ printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit );
+ fflush( stdout );
+ }
+ clk = clock();
+ pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 );
+ if ( pNtk )
+ {
+ Abc_NtkDelete( pNtkTemp );
+ RetValue = ( (Abc_NtkNodeNum(pNtk) == 1) && (Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pData == Cudd_ReadLogicZero(pNtk->pManFunc)) );
+ }
+ else
+ pNtk = pNtkTemp;
+ Abc_NtkMiterPrint( pNtk, "BDD building", clk, pParams->fVerbose );
+ }
+
if ( RetValue < 0 )
{
+ if ( pParams->fVerbose )
+ {
+ printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast );
+ fflush( stdout );
+ }
clk = clock();
- RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, 0 );
- Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose );
+ RetValue = Abc_NtkMiterSat( pNtk, pParams->nMiteringLimitLast, 0, 0, 0 );
+ Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
}
// assign the model if it was proved by rewriting (const 1 miter)
@@ -240,7 +262,8 @@ void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose
{
if ( !fVerbose )
return;
- printf( "Nodes = %7d. Levels = %4d. ", Abc_NtkNodeNum(pNtk), Abc_AigGetLevelNum(pNtk) );
+ printf( "Nodes = %7d. Levels = %4d. ", Abc_NtkNodeNum(pNtk),
+ Abc_NtkIsStrash(pNtk)? Abc_AigGetLevelNum(pNtk) : Abc_NtkGetLevelNum(pNtk) );
PRT( pString, clock() - clk );
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-06 23:45:57 +0000