luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Fixing a typo.

This commit is contained in:
Alan Mishchenko 2023-09-08 19:57:45 +07:00
parent f844fb1057
commit 55aba1731c
6 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/saig/saigTrans.c
View File

@ -6,7 +6,7 @@
PackageName [Sequential AIG package.]
Synopsis [Dynamic simplication of the transition relation.]
Synopsis [Dynamic simplification of the transition relation.]
Author [Alan Mishchenko]

2
src/proof/fraig/fraigInt.h
View File

@ -383,7 +383,7 @@ extern void Fraig_NodeSimulate( Fraig_Node_t * pNode, int iWordSt
/*=== fraigPrime.c =============================================================*/
extern int s_FraigPrimes[FRAIG_MAX_PRIMES];
/*=== fraigSat.c ===============================================================*/
extern int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit );
extern int Fraig_NodeIsImplification( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit );
/*=== fraigTable.c =============================================================*/
extern Fraig_HashTable_t * Fraig_HashTableCreate( int nSize );
extern void Fraig_HashTableFree( Fraig_HashTable_t * p );

2
src/proof/fraig/fraigSat.c
View File

@ -548,7 +548,7 @@ p->time3 += Abc_Clock() - clk;
SeeAlso []
***********************************************************************/
int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit )
int Fraig_NodeIsImplification( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit )
{
int RetValue, RetValue1, i, fComp;
abctime clk;

4
src/proof/fraig/fraigUtil.c
View File

@ -872,13 +872,13 @@ clk = Abc_Clock();
pNode2 = vPivots->pArray[k];
if ( Fraig_NodeSimsContained( pMan, pNode, pNode2 ) )
{
if ( Fraig_NodeIsImplication( pMan, pNode, pNode2, -1 ) )
if ( Fraig_NodeIsImplification( pMan, pNode, pNode2, -1 ) )
nProved++;
Counter++;
}
else if ( Fraig_NodeSimsContained( pMan, pNode2, pNode ) )
{
if ( Fraig_NodeIsImplication( pMan, pNode2, pNode, -1 ) )
if ( Fraig_NodeIsImplification( pMan, pNode2, pNode, -1 ) )
nProved++;
Counter++;
}

4
src/sat/glucose/AbcGlucose.cpp
View File

@ -842,7 +842,7 @@ void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars, int fDumpCnf )
if ( pPars->pre )
{
S.eliminate(true);
printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
printf( "c Simplification removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
if ( fDumpCnf )
@ -1510,7 +1510,7 @@ int Glucose_SolveAig(Gia_Man_t * p, Glucose_Pars * pPars)
if (pPars->pre)
{
S.eliminate(true);
printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
printf( "c Simplification removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}

4
src/sat/glucose2/AbcGlucose2.cpp
View File

@ -869,7 +869,7 @@ void Glucose2_SolveCnf( char * pFileName, Glucose2_Pars * pPars )
if ( pPars->pre )
{
S.eliminate(true);
printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
printf( "c Simplification removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
@ -1528,7 +1528,7 @@ int Glucose2_SolveAig(Gia_Man_t * p, Glucose2_Pars * pPars)
if (pPars->pre)
{
S.eliminate(true);
printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
printf( "c Simplification removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}