summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abci/abcExact.c15
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 )
{