summaryrefslogtreecommitdiffstats
path: root/src/aig/fra
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/fra')
-rw-r--r--src/aig/fra/fra.h2
-rw-r--r--src/aig/fra/fraCec.c19
-rw-r--r--src/aig/fra/fraInd.c6
-rw-r--r--src/aig/fra/fraSec.c63
-rw-r--r--src/aig/fra/fraSec80516.zipbin3502 -> 0 bytes
-rw-r--r--src/aig/fra/fraSim.c5
6 files changed, 65 insertions, 30 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 7549dfca..025ce046 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -104,6 +104,7 @@ struct Fra_Ssw_t_
int fWriteImps; // write implications into a file
int fUse1Hot; // use one-hotness constraints
int fVerbose; // enable verbose output
+ int fSilent; // disable any output
int nIters; // the number of iterations performed
float TimeLimit; // the runtime budget for this call
};
@@ -121,6 +122,7 @@ struct Fra_Sec_t_
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 fSilent; // disables all output
int fVerbose; // enables verbose reporting of statistics
int fVeryVerbose; // enables very verbose reporting
int TimeLimit; // enables the timeout
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index e91478a4..d67839a4 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -53,19 +53,22 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe
// derive CNF
pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
// pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
- // convert into the SAT solver
+ // convert into SAT solver
pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
- // add the OR clause for the outputs
- Cnf_DataWriteOrClause( pSat, pCnf );
- vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
- Cnf_DataFree( pCnf );
- // solve SAT
if ( pSat == NULL )
{
- Vec_IntFree( vCiIds );
-// printf( "Trivially unsat\n" );
+ Cnf_DataFree( pCnf );
return 1;
}
+ // add the OR clause for the outputs
+ if ( !Cnf_DataWriteOrClause( pSat, pCnf ) )
+ {
+ sat_solver_delete( pSat );
+ Cnf_DataFree( pCnf );
+ return 1;
+ }
+ vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
+ Cnf_DataFree( pCnf );
// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index df92792a..9c52d0e2 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -422,7 +422,8 @@ PRT( "Time", clock() - clk );
if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop )
{
- printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
+ if ( !pParams->fSilent )
+ printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
goto finish;
}
@@ -452,7 +453,8 @@ PRT( "Time", clock() - clk );
if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop )
{
- printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
+ if ( !pParams->fSilent )
+ printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
goto finish;
}
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 4528b9c4..96c0de77 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -53,11 +53,12 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
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->fSilent = 0; // disables all output
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
+ p->fReportSolution = 0; // enables specialized format for reporting solution
}
/**Function*************************************************************
@@ -158,7 +159,8 @@ clk = clock();
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
- printf( "Runtime limit exceeded.\n" );
+ if ( !pParSec->fSilent )
+ printf( "Runtime limit exceeded.\n" );
RetValue = -1;
TimeOut = 1;
goto finish;
@@ -166,14 +168,16 @@ clk = clock();
}
pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
- Aig_ManStop( pTemp );
if ( pNew == NULL )
{
if ( p->pSeqModel )
{
RetValue = 0;
- printf( "Networks are NOT EQUIVALENT after simulation. " );
+ if ( !pParSec->fSilent )
+ {
+ printf( "Networks are NOT EQUIVALENT after simulation. " );
PRT( "Time", clock() - clkTotal );
+ }
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: FAIL " );
@@ -186,6 +190,7 @@ PRT( "Time", clock() - clkTotal );
TimeOut = 1;
goto finish;
}
+ Aig_ManStop( pTemp );
if ( pParSec->fVerbose )
{
@@ -201,7 +206,8 @@ PRT( "Time", clock() - clk );
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
- printf( "Runtime limit exceeded.\n" );
+ if ( !pParSec->fSilent )
+ printf( "Runtime limit exceeded.\n" );
RetValue = -1;
TimeOut = 1;
goto finish;
@@ -235,7 +241,8 @@ PRT( "Time", clock() - clk );
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
- printf( "Runtime limit exceeded.\n" );
+ if ( !pParSec->fSilent )
+ printf( "Runtime limit exceeded.\n" );
RetValue = -1;
TimeOut = 1;
goto finish;
@@ -273,7 +280,8 @@ PRT( "Time", clock() - clk );
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
- printf( "Runtime limit exceeded.\n" );
+ if ( !pParSec->fSilent )
+ printf( "Runtime limit exceeded.\n" );
RetValue = -1;
TimeOut = 1;
goto finish;
@@ -283,6 +291,7 @@ PRT( "Time", clock() - clk );
clk = clock();
pPars->nFramesK = nFrames;
pPars->TimeLimit = TimeLeft;
+ pPars->fSilent = pParSec->fSilent;
pNew = Fra_FraigInduction( pTemp = pNew, pPars );
if ( pNew == NULL )
{
@@ -357,8 +366,11 @@ PRT( "Time", clock() - clk );
Fra_SmlStop( pSml );
Aig_ManStop( pNew );
RetValue = 0;
- printf( "Networks are NOT EQUIVALENT after simulation. " );
+ if ( !pParSec->fSilent )
+ {
+ printf( "Networks are NOT EQUIVALENT after simulation. " );
PRT( "Time", clock() - clkTotal );
+ }
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: FAIL " );
@@ -399,10 +411,10 @@ PRT( "Time", clock() - clk );
// try reachability analysis
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 );
+ extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent );
pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew);
pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew);
- RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 );
+ RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0, pParSec->fSilent );
}
// try one-output at a time
@@ -414,8 +426,9 @@ PRT( "Time", clock() - clk );
for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ )
if ( !Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) )
Counter++;
- printf( "*** The miter has %d outputs (out of %d total) unsolved in the multi-output form.\n",
- Counter, Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) );
+ if ( !pParSec->fSilent )
+ printf( "*** The miter has %d outputs (out of %d total) unsolved in the multi-output form.\n",
+ Counter, Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) );
iCount = 0;
for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ )
{
@@ -427,7 +440,8 @@ PRT( "Time", clock() - clk );
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
- printf( "Runtime limit exceeded.\n" );
+ if ( !pParSec->fSilent )
+ printf( "Runtime limit exceeded.\n" );
TimeOut = 1;
goto finish;
}
@@ -438,7 +452,8 @@ PRT( "Time", clock() - clk );
if ( Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) )
continue;
iCount++;
- printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter );
+ if ( !pParSec->fSilent )
+ printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter );
pNew2 = Aig_ManDupOneOutput( pNew, i );
TimeLimitCopy = pParSec->TimeLimit;
@@ -462,15 +477,19 @@ PRT( "Time", clock() - clk );
RetValue = -1;
else
RetValue = 1;
- printf( "*** Finished running separate outputs of the miter.\n" );
+ if ( !pParSec->fSilent )
+ printf( "*** Finished running separate outputs of the miter.\n" );
}
finish:
// report the miter
if ( RetValue == 1 )
{
- printf( "Networks are equivalent. " );
+ if ( !pParSec->fSilent )
+ {
+ printf( "Networks are equivalent. " );
PRT( "Time", clock() - clkTotal );
+ }
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: PASS " );
@@ -479,8 +498,11 @@ PRT( "Time", clock() - clkTotal );
}
else if ( RetValue == 0 )
{
- printf( "Networks are NOT EQUIVALENT. " );
+ if ( !pParSec->fSilent )
+ {
+ printf( "Networks are NOT EQUIVALENT. " );
PRT( "Time", clock() - clkTotal );
+ }
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: FAIL " );
@@ -489,14 +511,17 @@ PRT( "Time", clock() - clkTotal );
}
else
{
- printf( "Networks are UNDECIDED. " );
+ if ( !pParSec->fSilent )
+ {
+ printf( "Networks are UNDECIDED. " );
PRT( "Time", clock() - clkTotal );
+ }
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: UNDECIDED " );
PRT( "Time", clock() - clkTotal );
}
- if ( !TimeOut )
+ if ( !TimeOut && !pParSec->fSilent )
{
static int Counter = 1;
char pFileName[1000];
diff --git a/src/aig/fra/fraSec80516.zip b/src/aig/fra/fraSec80516.zip
deleted file mode 100644
index 0adf10df..00000000
--- a/src/aig/fra/fraSec80516.zip
+++ /dev/null
Binary files differ
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 00a35fcd..53493201 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -1119,20 +1119,22 @@ int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p )
RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
// write the output file
- fprintf( pFile, "1\n" );
for ( i = 0; i <= p->iFrame; i++ )
{
+/*
Aig_ManForEachLoSeq( pAig, pObj, k )
{
pSims = Fra_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
fprintf( pFile, " " );
+*/
Aig_ManForEachPiSeq( pAig, pObj, k )
{
pSims = Fra_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
+/*
fprintf( pFile, " " );
Aig_ManForEachPoSeq( pAig, pObj, k )
{
@@ -1145,6 +1147,7 @@ int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p )
pSims = Fra_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
+*/
fprintf( pFile, "\n" );
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-13 10:10:13 +0000