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

An improvement to 'twoexact' and 'lutexact'.

This commit is contained in:
Alan Mishchenko 2017-12-06 13:51:10 -08:00
parent e37bbba72d
commit c6b962efc8
3 changed files with 9 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/sat/bmc/bmc.h
View File

@ -36,6 +36,7 @@
ABC_NAMESPACE_HEADER_START
//#define USE_NODE_ORDER 1
//#define USE_FIRST_SPECIAL 1
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///

4
src/sat/bmc/bmcMaj.c
View File

@ -438,6 +438,7 @@ int Exa_ManMarkup( Exa_Man_t * p )
{
for ( k = 0; k < 2; k++ )
{
#ifdef USE_FIRST_SPECIAL
if ( i == p->nObjs - 1 && k == 0 )
{
j = p->nObjs - 2;
@ -445,6 +446,7 @@ int Exa_ManMarkup( Exa_Man_t * p )
p->VarMarks[i][k][j] = p->iVar++;
continue;
}
#endif
for ( j = 1 - k; j < i - k; j++ )
{
Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
@ -817,6 +819,7 @@ static int Exa3_ManMarkup( Exa3_Man_t * p )
{
for ( k = 0; k < p->nLutSize; k++ )
{
#ifdef USE_FIRST_SPECIAL
if ( i == p->nObjs - 1 && k == 0 )
{
j = p->nObjs - 2;
@ -824,6 +827,7 @@ static int Exa3_ManMarkup( Exa3_Man_t * p )
p->VarMarks[i][k][j] = p->iVar++;
continue;
}
#endif
for ( j = p->nLutSize - 1 - k; j < i - k; j++ )
{
Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );

4
src/sat/bmc/bmcMaj2.c
View File

@ -544,6 +544,7 @@ static int Exa_ManMarkup( Exa_Man_t * p )
{
for ( k = 0; k < 2; k++ )
{
#ifdef USE_FIRST_SPECIAL
if ( i == p->nObjs - 1 && k == 0 )
{
j = p->nObjs - 2;
@ -551,6 +552,7 @@ static int Exa_ManMarkup( Exa_Man_t * p )
p->VarMarks[i][k][j] = p->iVar++;
continue;
}
#endif
for ( j = 1 - k; j < i - k; j++ )
{
Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
@ -925,6 +927,7 @@ static int Exa3_ManMarkup( Exa3_Man_t * p )
{
for ( k = 0; k < p->nLutSize; k++ )
{
#ifdef USE_FIRST_SPECIAL
if ( i == p->nObjs - 1 && k == 0 )
{
j = p->nObjs - 2;
@ -932,6 +935,7 @@ static int Exa3_ManMarkup( Exa3_Man_t * p )
p->VarMarks[i][k][j] = p->iVar++;
continue;
}
#endif
for ( j = p->nLutSize - 1 - k; j < i - k; j++ )
{
Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );