summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/fra/fra.h27
-rw-r--r--src/aig/fra/fraSec.c154
-rw-r--r--src/aig/ioa/ioaUtil.c19
-rw-r--r--src/aig/nwk/nwkMan.c15
-rw-r--r--src/aig/saig/saigBmc.c2
-rw-r--r--src/aig/saig/saigInter.c5
6 files changed, 148 insertions, 74 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index f7ad40dd..7cb846fa 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -51,6 +51,7 @@ extern "C" {
typedef struct Fra_Par_t_ Fra_Par_t;
typedef struct Fra_Ssw_t_ Fra_Ssw_t;
+typedef struct Fra_Sec_t_ Fra_Sec_t;
typedef struct Fra_Man_t_ Fra_Man_t;
typedef struct Fra_Cla_t_ Fra_Cla_t;
typedef struct Fra_Sml_t_ Fra_Sml_t;
@@ -87,7 +88,7 @@ struct Fra_Par_t_
int fDontShowBar; // does not show progressbar during fraiging
};
-// seq SAT sweeping parametesr
+// seq SAT sweeping parameters
struct Fra_Ssw_t_
{
int nPartSize; // size of the partition
@@ -107,6 +108,27 @@ struct Fra_Ssw_t_
float TimeLimit; // the runtime budget for this call
};
+// SEC parametesr
+struct Fra_Sec_t_
+{
+ int fTryComb; // try CEC call as a preprocessing step
+ int fTryBmc; // try BMC call as a preprocessing step
+ int nFramesMax; // the max number of frames used for induction
+ int fPhaseAbstract; // enables phase abstraction
+ int fRetimeFirst; // enables most-forward retiming at the beginning
+ int fRetimeRegs; // enables min-register retiming at the beginning
+ int fFraiging; // enables fraiging at the beginning
+ int fInterpolation; // enables interpolation
+ int fReachability; // enables BDD based reachability
+ int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove
+ int fVerbose; // enables verbose reporting of statistics
+ int fVeryVerbose; // enables very verbose reporting
+ int TimeLimit; // enables the timeout
+ // internal parameters
+ int fRecursive; // set to 1 when SEC is called recursively
+ int fReportSolution; // enables report solution in a special form
+};
+
// FRAIG equivalence classes
struct Fra_Cla_t_
{
@@ -329,7 +351,8 @@ extern int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig
extern int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
/*=== fraSec.c ========================================================*/
-extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit );
+extern void Fra_SecSetDefaultParams( Fra_Sec_t * p );
+extern int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec );
/*=== fraSim.c ========================================================*/
extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index db8027d9..b8f93f57 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -40,12 +40,44 @@
SeeAlso []
***********************************************************************/
-int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit )
+void Fra_SecSetDefaultParams( Fra_Sec_t * p )
+{
+ memset( p, 0, sizeof(Fra_Sec_t) );
+ p->fTryComb = 1; // try CEC call as a preprocessing step
+ p->fTryBmc = 1; // try BMC call as a preprocessing step
+ p->nFramesMax = 2; // the max number of frames used for induction
+ p->fPhaseAbstract = 1; // enables phase abstraction
+ p->fRetimeFirst = 1; // enables most-forward retiming at the beginning
+ p->fRetimeRegs = 1; // enables min-register retiming at the beginning
+ p->fFraiging = 1; // enables fraiging at the beginning
+ p->fInterpolation = 1; // enables interpolation
+ p->fReachability = 1; // enables BDD based reachability
+ p->fStopOnFirstFail = 1; // enables stopping after first output of a miter has failed to prove
+ p->fVerbose = 0; // enables verbose reporting of statistics
+ p->fVeryVerbose = 0; // enables very verbose reporting
+ p->TimeLimit = 0; // enables the timeout
+ // internal parameters
+ p->fReportSolution = 1; // enables specialized format for reporting solution
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec )
{
Fra_Ssw_t Pars, * pPars = &Pars;
Fra_Sml_t * pSml;
Aig_Man_t * pNew, * pTemp;
int nFrames, RetValue, nIter, clk, clkTotal = clock();
+ int TimeOut = 0;
int fLatchCorr = 0;
float TimeLeft = 0.0;
@@ -58,8 +90,8 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetime
// prepare parameters
memset( pPars, 0, sizeof(Fra_Ssw_t) );
pPars->fLatchCorr = fLatchCorr;
- pPars->fVerbose = fVeryVerbose;
- if ( fVerbose )
+ pPars->fVerbose = pParSec->fVeryVerbose;
+ if ( pParSec->fVerbose )
{
printf( "Original miter: Latches = %5d. Nodes = %6d.\n",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -72,7 +104,7 @@ clk = clock();
pNew = Aig_ManReduceLaches( pNew, 0 );
if ( pNew->nRegs )
pNew = Aig_ManConstReduce( pNew, 0 );
- if ( fVerbose )
+ if ( pParSec->fVerbose )
{
printf( "Sequential cleanup: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -84,14 +116,14 @@ PRT( "Time", clock() - clk );
// perform phase abstraction
clk = clock();
- if ( fPhaseAbstract )
+ if ( pParSec->fPhaseAbstract )
{
extern Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose );
pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew);
pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew);
pNew = Saig_ManPhaseAbstractAuto( pTemp = pNew, 0 );
Aig_ManStop( pTemp );
- if ( fVerbose )
+ if ( pParSec->fVerbose )
{
printf( "Phase abstraction: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -100,12 +132,12 @@ PRT( "Time", clock() - clk );
}
// perform forward retiming
- if ( fRetimeFirst && pNew->nRegs )
+ if ( pParSec->fRetimeFirst && pNew->nRegs )
{
clk = clock();
pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
Aig_ManStop( pTemp );
- if ( fVerbose )
+ if ( pParSec->fVerbose )
{
printf( "Forward retiming: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -120,22 +152,24 @@ clk = clock();
pNew = Aig_ManDupOrdered( pTemp = pNew );
// pNew = Aig_ManDupDfs( pTemp = pNew );
Aig_ManStop( pTemp );
- if ( RetValue == -1 && TimeLimit )
+ if ( RetValue == -1 && pParSec->TimeLimit )
{
- TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+ TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
printf( "Runtime limit exceeded.\n" );
RetValue = -1;
+ TimeOut = 1;
goto finish;
}
}
- pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, fVeryVerbose, &nIter, TimeLeft );
+ pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
if ( pNew == NULL )
{
pNew = pTemp;
RetValue = -1;
+ TimeOut = 1;
goto finish;
}
p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
@@ -148,7 +182,7 @@ PRT( "Time", clock() - clkTotal );
return RetValue;
}
- if ( fVerbose )
+ if ( pParSec->fVerbose )
{
printf( "Latch-corr (I=%3d): Latches = %5d. Nodes = %6d. ",
nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -156,25 +190,26 @@ PRT( "Time", clock() - clk );
}
}
- if ( RetValue == -1 && TimeLimit )
+ if ( RetValue == -1 && pParSec->TimeLimit )
{
- TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+ TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
printf( "Runtime limit exceeded.\n" );
RetValue = -1;
+ TimeOut = 1;
goto finish;
}
}
// perform fraiging
- if ( fFraiging )
+ if ( pParSec->fFraiging )
{
clk = clock();
pNew = Fra_FraigEquivence( pTemp = pNew, 100, 0 );
Aig_ManStop( pTemp );
- if ( fVerbose )
+ if ( pParSec->fVerbose )
{
printf( "Fraiging: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -189,20 +224,21 @@ PRT( "Time", clock() - clk );
if ( RetValue >= 0 )
goto finish;
- if ( RetValue == -1 && TimeLimit )
+ if ( RetValue == -1 && pParSec->TimeLimit )
{
- TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+ TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
printf( "Runtime limit exceeded.\n" );
RetValue = -1;
+ TimeOut = 1;
goto finish;
}
}
// perform min-area retiming
- if ( fRetimeRegs && pNew->nRegs )
+ if ( pParSec->fRetimeRegs && pNew->nRegs )
{
extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
clk = clock();
@@ -213,7 +249,7 @@ clk = clock();
Aig_ManStop( pTemp );
pNew = Aig_ManDupOrdered( pTemp = pNew );
Aig_ManStop( pTemp );
- if ( fVerbose )
+ if ( pParSec->fVerbose )
{
printf( "Min-reg retiming: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -224,16 +260,17 @@ PRT( "Time", clock() - clk );
// perform seq sweeping while increasing the number of frames
RetValue = Fra_FraigMiterStatus( pNew );
if ( RetValue == -1 )
- for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
+ for ( nFrames = 1; nFrames <= pParSec->nFramesMax; nFrames *= 2 )
{
- if ( RetValue == -1 && TimeLimit )
+ if ( RetValue == -1 && pParSec->TimeLimit )
{
- TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+ TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
printf( "Runtime limit exceeded.\n" );
RetValue = -1;
+ TimeOut = 1;
goto finish;
}
}
@@ -246,11 +283,12 @@ clk = clock();
{
pNew = pTemp;
RetValue = -1;
+ TimeOut = 1;
goto finish;
}
Aig_ManStop( pTemp );
RetValue = Fra_FraigMiterStatus( pNew );
- if ( fVerbose )
+ if ( pParSec->fVerbose )
{
printf( "K-step (K=%2d,I=%3d): Latches = %5d. Nodes = %6d. ",
nFrames, pPars->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -260,7 +298,7 @@ PRT( "Time", clock() - clk );
break;
// perform retiming
-// if ( fRetimeFirst && pNew->nRegs )
+// if ( pParSec->fRetimeFirst && pNew->nRegs )
if ( pNew->nRegs )
{
extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
@@ -272,7 +310,7 @@ clk = clock();
Aig_ManStop( pTemp );
pNew = Aig_ManDupOrdered( pTemp = pNew );
Aig_ManStop( pTemp );
- if ( fVerbose )
+ if ( pParSec->fVerbose )
{
printf( "Min-reg retiming: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -290,7 +328,7 @@ clk = clock();
// pNew = Dar_ManRewriteDefault( pTemp = pNew );
pNew = Dar_ManCompress2( pTemp = pNew, 1, 0, 1, 0 );
Aig_ManStop( pTemp );
- if ( fVerbose )
+ if ( pParSec->fVerbose )
{
printf( "Rewriting: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -302,7 +340,7 @@ PRT( "Time", clock() - clk );
{
clk = clock();
pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000) );
- if ( fVerbose )
+ if ( pParSec->fVerbose )
{
printf( "Seq simulation : Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -327,14 +365,14 @@ PRT( "Time", clock() - clkTotal );
// try interplation
clk = clock();
- if ( RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 )
+ if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 )
{
extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth );
int Depth;
pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew);
pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew);
- RetValue = Saig_Interpolate( pNew, 5000, 0, 1, fVeryVerbose, &Depth );
- if ( fVerbose )
+ RetValue = Saig_Interpolate( pNew, 5000, 0, 1, pParSec->fVeryVerbose, &Depth );
+ if ( pParSec->fVerbose )
{
if ( RetValue == 1 )
printf( "Property proved using interpolation. " );
@@ -349,7 +387,7 @@ PRT( "Time", clock() - clk );
}
// try reachability analysis
- if ( RetValue == -1 && Aig_ManRegNum(pNew) < 200 && Aig_ManRegNum(pNew) > 0 )
+ if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < 150 )
{
extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew);
@@ -371,14 +409,16 @@ PRT( "Time", clock() - clk );
iCount = 0;
for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ )
{
+ int TimeLimitCopy = 0;
// get the remaining time for this output
- if ( TimeLimit )
+ if ( pParSec->TimeLimit )
{
- TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+ TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
printf( "Runtime limit exceeded.\n" );
+ TimeOut = 1;
goto finish;
}
TimeLimit2 = 1 + (int)TimeLeft;
@@ -390,12 +430,23 @@ PRT( "Time", clock() - clk );
iCount++;
printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter );
pNew2 = Aig_ManDupOneOutput( pNew, i );
- RetValue2 = Fra_FraigSec( pNew2, nFramesMax, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, TimeLimit2 );
+
+ TimeLimitCopy = pParSec->TimeLimit;
+ pParSec->TimeLimit = TimeLimit2;
+ pParSec->fRecursive = 1;
+ RetValue2 = Fra_FraigSec( pNew2, pParSec );
+ pParSec->fRecursive = 0;
+ pParSec->TimeLimit = TimeLimitCopy;
+
Aig_ManStop( pNew2 );
if ( RetValue2 == 0 )
goto finish;
if ( RetValue2 == -1 )
+ {
fOneUnsolved = 1;
+ if ( pParSec->fStopOnFirstFail )
+ break;
+ }
}
if ( fOneUnsolved )
RetValue = -1;
@@ -410,23 +461,42 @@ finish:
{
printf( "Networks are equivalent. " );
PRT( "Time", clock() - clkTotal );
+ if ( pParSec->fReportSolution && !pParSec->fRecursive )
+ {
+ printf( "SOLUTION: PASS " );
+PRT( "Time", clock() - clkTotal );
+ }
}
else if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT. " );
PRT( "Time", clock() - clkTotal );
+ if ( pParSec->fReportSolution && !pParSec->fRecursive )
+ {
+ printf( "SOLUTION: FAIL " );
+PRT( "Time", clock() - clkTotal );
+ }
}
- else
+ else
{
- static int Counter = 1;
- char pFileName[1000];
printf( "Networks are UNDECIDED. " );
PRT( "Time", clock() - clkTotal );
- sprintf( pFileName, "sm%03d.aig", Counter++ );
- Ioa_WriteAiger( pNew, pFileName, 0, 0 );
- printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
+ if ( pParSec->fReportSolution && !pParSec->fRecursive )
+ {
+ printf( "SOLUTION: UNDECIDED " );
+PRT( "Time", clock() - clkTotal );
+ }
+ if ( !TimeOut )
+ {
+ static int Counter = 1;
+ char pFileName[1000];
+ sprintf( pFileName, "sm%03d.aig", Counter++ );
+ Ioa_WriteAiger( pNew, pFileName, 0, 0 );
+ printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
+ }
}
- Aig_ManStop( pNew );
+ if ( pNew )
+ Aig_ManStop( pNew );
return RetValue;
}
diff --git a/src/aig/ioa/ioaUtil.c b/src/aig/ioa/ioaUtil.c
index 6063d8be..b0e5618b 100644
--- a/src/aig/ioa/ioaUtil.c
+++ b/src/aig/ioa/ioaUtil.c
@@ -69,20 +69,10 @@ int Ioa_FileSize( char * pFileName )
***********************************************************************/
char * Ioa_FileNameGeneric( char * FileName )
{
- char * pDot;
- char * pUnd;
- char * pRes;
-
- // find the generic name of the file
+ char * pDot, * pRes;
pRes = Aig_UtilStrsav( FileName );
- // find the pointer to the "." symbol in the file name
-// pUnd = strstr( FileName, "_" );
- pUnd = NULL;
- pDot = strstr( FileName, "." );
- if ( pUnd )
- pRes[pUnd - FileName] = 0;
- else if ( pDot )
- pRes[pDot - FileName] = 0;
+ if ( (pDot = strrchr( pRes, '.' )) )
+ *pDot = 0;
return pRes;
}
@@ -107,8 +97,7 @@ char * Ioa_FileNameGenericAppend( char * pBase, char * pSuffix )
return Buffer;
}
strcpy( Buffer, pBase );
- pDot = strstr( Buffer, "." );
- if ( pDot )
+ if ( (pDot = strrchr( Buffer, '.' )) )
*pDot = 0;
strcat( Buffer, pSuffix );
// find the last occurrance of slash
diff --git a/src/aig/nwk/nwkMan.c b/src/aig/nwk/nwkMan.c
index 55c5354c..da402f21 100644
--- a/src/aig/nwk/nwkMan.c
+++ b/src/aig/nwk/nwkMan.c
@@ -174,19 +174,10 @@ int Nwk_ManCompareAndSaveBest( Nwk_Man_t * pNtk, void * pNtl )
***********************************************************************/
char * Nwk_FileNameGeneric( char * FileName )
{
- char * pDot;
- char * pUnd;
- char * pRes;
- // find the generic name of the file
+ char * pDot, * pRes;
pRes = Aig_UtilStrsav( FileName );
- // find the pointer to the "." symbol in the file name
-// pUnd = strstr( FileName, "_" );
- pUnd = NULL;
- pDot = strstr( FileName, "." );
- if ( pUnd )
- pRes[pUnd - FileName] = 0;
- else if ( pDot )
- pRes[pDot - FileName] = 0;
+ if ( (pDot = strrchr( pRes, '.' )) )
+ *pDot = 0;
return pRes;
}
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index f6a42c8b..952094ce 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -182,7 +182,6 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
Aig_Man_t * pFrames, * pAigTemp;
Aig_Obj_t * pObj;
int status, clk, Lit, i, RetValue = 1;
- *piFrame = -1;
// derive the timeframes
clk = clock();
if ( nSizeMax > 0 )
@@ -192,6 +191,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
}
else
pFrames = Saig_ManFramesBmc( pAig, nFrames );
+ *piFrame = nFrames;
if ( fVerbose )
{
printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c
index 3adcc568..889e6298 100644
--- a/src/aig/saig/saigInter.c
+++ b/src/aig/saig/saigInter.c
@@ -178,6 +178,7 @@ Aig_Man_t * Saig_ManTransformed( Aig_Man_t * p )
Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
{
pObj = Aig_Mux( pNew, pCtrl, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) );
+// pObj = Aig_Mux( pNew, pCtrl, Aig_ManConst0(pNew), Aig_ObjChild0Copy(pObjLi) );
Aig_ObjCreatePo( pNew, pObj );
}
Aig_ManCleanup( pNew );
@@ -566,10 +567,10 @@ p->timeCnf += clock() - clk;
// iterate the interpolation procedure
for ( i = 0; ; i++ )
{
- if ( p->nFrames + i >= 100 )
+ if ( p->nFrames + i >= 75 )
{
if ( fVerbose )
- printf( "Reached limit (%d) on the number of timeframes.\n", 100 );
+ printf( "Reached limit (%d) on the number of timeframes.\n", 75 );
p->timeTotal = clock() - clkTotal;
Saig_ManagerFree( p );
return -1;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-08 17:32:19 +0000