diff options
| author | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-08-29 13:37:29 +0200 |
|---|---|---|
| committer | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-08-29 13:37:29 +0200 |
| commit | 7e3032c0dd5333f449d76056663408357e750706 (patch) | |
| tree | c76d6afa9e3f0d24c25ad7c9650e6f83e97bd044 /src/base/abci | |
| parent | 2d71abd581e5c1572bdc83a15f0b5dbdd1cc0e28 (diff) | |
| download | abc-7e3032c0dd5333f449d76056663408357e750706.tar.gz abc-7e3032c0dd5333f449d76056663408357e750706.tar.bz2 abc-7e3032c0dd5333f449d76056663408357e750706.zip | |
Improvements to BMS.
Diffstat (limited to 'src/base/abci')
| -rw-r--r-- | src/base/abci/abcExact.c | 56 |
1 files changed, 55 insertions, 1 deletions
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index f328d9b3..0ba83e84 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -1163,6 +1163,60 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes ) } } + /* only binary clauses */ + if ( 1 ) /* TODO: add some meaningful parameter */ + { + for ( i = 0; i < pSes->nGates; ++i ) + { + pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 0 ); + pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 0 ); + pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 0 ); + sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ); + + pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 1 ); + pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 0 ); + pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 ); + sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ); + + pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 0 ); + pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 1 ); + pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 ); + sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ); + } + + for ( i = 0; i < pSes->nGates; ++i ) + for ( k = 1; k < pSes->nSpecVars + i; ++k ) + for ( j = 0; j < k; ++j ) + { + pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 ); + + for ( kk = 1; kk < pSes->nSpecVars + i; ++kk ) + for ( jj = 0; jj < kk; ++jj ) + { + if ( k == kk && j == jj ) continue; + pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, jj, kk ), 1 ); + + if ( pLits[0] < pLits[1] ) + sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ); + } + } + + /* Vec_IntGrowResize( vLits, pSes->nGates * ( pSes->nSpecVars + pSes->nGates - 2 ) ); */ + + /* for ( j = 0; j < pSes->nSpecVars; ++j ) */ + /* { */ + /* jj = 0; */ + /* for ( i = 0; i < pSes->nGates; ++i ) */ + /* { */ + /* for ( k = 0; k < j; ++k ) */ + /* Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, k, j ), 0 ) ); */ + /* for ( k = j + 1; k < pSes->nSpecVars + i; ++k ) */ + /* Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 0 ) ); */ + /* } */ + /* sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntArray( vLits ) + jj ); */ + /* } */ + } + /* EXTRA clauses: use gate i at least once */ Vec_IntGrowResize( vLits, pSes->nSpecFunc + pSes->nGates * ( pSes->nSpecVars + pSes->nGates - 2 ) ); for ( i = 0; i < pSes->nGates; ++i ) @@ -1208,7 +1262,7 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes ) for ( q = 1; q < pSes->nSpecVars; ++q ) for ( p = 0; p < q; ++p ) if ( Extra_TruthVarsSymm( (unsigned*)( pSes->pSpec ), pSes->nSpecVars, p, q ) && - ( !pSes->pArrTimeProfile || ( pSes->pArrTimeProfile[p] == pSes->pArrTimeProfile[q] ) ) ) + ( !pSes->pArrTimeProfile || ( pSes->pArrTimeProfile[p] <= pSes->pArrTimeProfile[q] ) ) ) { if ( pSes->fSatVerbose ) printf( "variables %d and %d are symmetric\n", p, q ); |