diff options
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 ) { |