diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-12-06 09:53:25 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-12-06 09:53:25 -0800 |
| commit | b258db83b8b9becc444baf11732597c000651020 (patch) | |
| tree | 1697f6f95481127f80f353870a8389b4dc083f16 /src/sat | |
| parent | 3f35ac8180bf69655662c2ccd2de9411b3533cf4 (diff) | |
| download | abc-b258db83b8b9becc444baf11732597c000651020.tar.gz abc-b258db83b8b9becc444baf11732597c000651020.tar.bz2 abc-b258db83b8b9becc444baf11732597c000651020.zip | |
An improvement to 'twoexact' and 'lutexact'.
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/bmc/bmcMaj.c | 23 | ||||
| -rw-r--r-- | src/sat/bmc/bmcMaj2.c | 24 |
2 files changed, 39 insertions, 8 deletions
diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index 463e9197..0b09e311 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -438,7 +438,14 @@ int Exa_ManMarkup( Exa_Man_t * p ) { for ( k = 0; k < 2; k++ ) { - for ( j = 0; j < i - k; j++ ) + if ( i == p->nObjs - 1 && k == 0 ) + { + j = p->nObjs - 2; + Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); + p->VarMarks[i][k][j] = p->iVar++; + continue; + } + for ( j = 1 - k; j < i - k; j++ ) { Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); p->VarMarks[i][k][j] = p->iVar++; @@ -789,7 +796,14 @@ static int Exa3_ManMarkup( Exa3_Man_t * p ) { for ( k = 0; k < p->nLutSize; k++ ) { - for ( j = 0; j < i - k; j++ ) + if ( i == p->nObjs - 1 && k == 0 ) + { + j = p->nObjs - 2; + Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); + p->VarMarks[i][k][j] = p->iVar++; + continue; + } + for ( j = p->nLutSize - 1 - k; j < i - k; j++ ) { Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); p->VarMarks[i][k][j] = p->iVar++; @@ -799,11 +813,12 @@ static int Exa3_ManMarkup( Exa3_Man_t * p ) printf( "The number of parameter variables = %d.\n", p->iVar ); return p->iVar; // printout - for ( i = p->nVars; i < p->nObjs; i++ ) + for ( i = p->nObjs - 1; i >= p->nVars; i-- ) { - printf( "Node %d\n", i ); + printf( " Node %2d\n", i ); for ( j = 0; j < p->nObjs; j++ ) { + printf( "Fanin %2d : ", j ); for ( k = 0; k < p->nLutSize; k++ ) printf( "%3d ", p->VarMarks[i][k][j] ); printf( "\n" ); diff --git a/src/sat/bmc/bmcMaj2.c b/src/sat/bmc/bmcMaj2.c index 1c61fec1..46f3f1f2 100644 --- a/src/sat/bmc/bmcMaj2.c +++ b/src/sat/bmc/bmcMaj2.c @@ -544,7 +544,14 @@ static int Exa_ManMarkup( Exa_Man_t * p ) { for ( k = 0; k < 2; k++ ) { - for ( j = 0; j < i - k; j++ ) + if ( i == p->nObjs - 1 && k == 0 ) + { + j = p->nObjs - 2; + Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); + p->VarMarks[i][k][j] = p->iVar++; + continue; + } + for ( j = 1 - k; j < i - k; j++ ) { Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); p->VarMarks[i][k][j] = p->iVar++; @@ -897,7 +904,14 @@ static int Exa3_ManMarkup( Exa3_Man_t * p ) { for ( k = 0; k < p->nLutSize; k++ ) { - for ( j = 0; j < i - k; j++ ) + if ( i == p->nObjs - 1 && k == 0 ) + { + j = p->nObjs - 2; + Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); + p->VarMarks[i][k][j] = p->iVar++; + continue; + } + for ( j = p->nLutSize - 1 - k; j < i - k; j++ ) { Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); p->VarMarks[i][k][j] = p->iVar++; @@ -907,11 +921,13 @@ static int Exa3_ManMarkup( Exa3_Man_t * p ) printf( "The number of parameter variables = %d.\n", p->iVar ); return p->iVar; // printout - for ( i = p->nVars; i < p->nObjs; i++ ) +// for ( i = p->nVars; i < p->nObjs; i++ ) + for ( i = p->nObjs - 1; i >= p->nVars; i-- ) { - printf( "Node %d\n", i ); + printf( " Node %2d\n", i ); for ( j = 0; j < p->nObjs; j++ ) { + printf( "Fanin %2d : ", j ); for ( k = 0; k < p->nLutSize; k++ ) printf( "%3d ", p->VarMarks[i][k][j] ); printf( "\n" ); |