From bab90943dc6e1aefe0ccb7b522bcf79e2d080e3d Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Wed, 26 Oct 2016 17:54:00 +0200 Subject: Exact synthesis. --- src/base/abci/abcExact.c | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'src') 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 ) { -- cgit v1.2.3