From 360e85fce2f343fc2a68d1e330ab86e3062c9948 Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Wed, 24 Aug 2016 17:08:06 +0200 Subject: Fix errors in BMS. --- src/base/abci/abcExact.c | 26 ++++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index cb48478b..770afb0a 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -720,10 +720,10 @@ static inline void Ses_ManComputeTopDec( Ses_Man_t * pSes ) for ( i = 0; i < pSes->nSpecWords; ++i ) { - fAnd &= ( pVar[i] & pSes->pSpec[i] & mask ) != ( pSes->pSpec[i] & mask ); - fAndC &= ( ~pVar[i] & pSes->pSpec[i] & mask ) != ( pSes->pSpec[i] & mask ); - fOr &= ( pVar[i] & pSes->pSpec[i] & mask ) != ( pVar[i] & mask ); - fOrC &= ( ~pVar[i] & pSes->pSpec[i] & mask ) != ( ~pVar[i] & mask ); + fAnd &= ( pVar[i] & pSes->pSpec[i] & mask ) == ( pSes->pSpec[i] & mask ); + fAndC &= ( ~pVar[i] & pSes->pSpec[i] & mask ) == ( pSes->pSpec[i] & mask ); + fOr &= ( pVar[i] & pSes->pSpec[i] & mask ) == ( pVar[i] & mask ); + fOrC &= ( ~pVar[i] & pSes->pSpec[i] & mask ) == ( ~pVar[i] & mask ); } pSes->pDecVars |= ( fAnd | fAndC | fOr | fOrC ) << l; @@ -924,6 +924,7 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes ) Vec_Int_t * vLits = NULL; for ( t = 0; t < pSes->nRows; ++t ) + { for ( i = 0; i < pSes->nGates; ++i ) { /* main clauses */ @@ -950,6 +951,14 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes ) } } + if ( pSes->nSpecFunc == 1 ) + { + pLits[0] = Abc_Var2Lit( Ses_ManSimVar( pSes, pSes->nGates - 1, t ), 1 - Abc_TtGetBit( pSes->pSpec, t + 1 ) ); + if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ) + return 0; + } + } + /* if there is only one output, we know it must point to the last gate */ if ( pSes->nSpecFunc == 1 ) { @@ -969,13 +978,6 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes ) return 0; } - for ( t = 0; t < pSes->nRows; ++t ) - { - pLits[0] = Abc_Var2Lit( Ses_ManSimVar( pSes, pSes->nGates - 1, t ), 1 - Abc_TtGetBit( pSes->pSpec, t + 1 ) ); - if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ) - return 0; - } - vLits = Vec_IntAlloc( 0u ); } else @@ -1093,7 +1095,7 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes ) if ( pSes->nMaxDepth == -1 && pSes->nSpecFunc == 1 ) /* only check if there is one output function */ for ( q = 1; q < pSes->nSpecVars; ++q ) for ( p = 0; p < q; ++p ) - if ( Extra_TruthVarsSymm( (unsigned*)( &pSes->pSpec[h << 2] ), pSes->nSpecVars, p, q ) ) + if ( Extra_TruthVarsSymm( (unsigned*)( pSes->pSpec ), pSes->nSpecVars, p, q ) ) { if ( pSes->fVeryVerbose ) printf( "variables %d and %d are symmetric\n", p, q ); -- cgit v1.2.3