diff options
| author | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-10-26 17:54:00 +0200 |
|---|---|---|
| committer | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-10-26 17:54:00 +0200 |
| commit | bab90943dc6e1aefe0ccb7b522bcf79e2d080e3d (patch) | |
| tree | 8c801df1db3c4364e2627964b79f51d69da7d4c9 /src/base/abci/abcExact.c | |
| parent | 0a87e72c6d2b2eeb01b7abdc95fb81be658d6d0a (diff) | |
| download | abc-bab90943dc6e1aefe0ccb7b522bcf79e2d080e3d.tar.gz abc-bab90943dc6e1aefe0ccb7b522bcf79e2d080e3d.tar.bz2 abc-bab90943dc6e1aefe0ccb7b522bcf79e2d080e3d.zip | |
Exact synthesis.
Diffstat (limited to 'src/base/abci/abcExact.c')
| -rw-r--r-- | src/base/abci/abcExact.c | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index c1def074..2221d83a 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -1405,6 +1405,21 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes ) } Vec_IntFree( vLits ); + /* EXTRA clauses: no reapplying operand */ + if ( pSes->nGates > 1 ) + for ( i = 0; i < pSes->nGates - 1; ++i ) + for ( ii = i + 1; ii < pSes->nGates; ++ii ) + 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 ); + pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, j, pSes->nSpecVars + i ), 1 ); + sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ); + + pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, k, pSes->nSpecVars + i ), 1 ); + sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ); + } + /* EXTRA clauses: co-lexicographic order */ for ( i = 0; i < pSes->nGates - 1; ++i ) { |