diff options
| author | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-09-09 12:08:52 +0200 |
|---|---|---|
| committer | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-09-09 12:08:52 +0200 |
| commit | 5b2472d4b719875c8017814c9c81bcd4f4691011 (patch) | |
| tree | 54d05b9db9ac2668f319ca610660bcaa25a9a556 /src/base | |
| parent | 6d7f2c4d54935ddef131a26b9da96026c3510b20 (diff) | |
| download | abc-5b2472d4b719875c8017814c9c81bcd4f4691011.tar.gz abc-5b2472d4b719875c8017814c9c81bcd4f4691011.tar.bz2 abc-5b2472d4b719875c8017814c9c81bcd4f4691011.zip | |
Missing case in BMS.
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abci/abcExact.c | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index 4a743abc..58e4db14 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -1344,7 +1344,10 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes ) Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 0 ) ); break; case 4: /* OR(!x,g) */ - assert( 0 ); /* should be impossible since all gates are normal */ + Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 0 ) ); + Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 1 ) ); + Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 0 ) ); + break; case 5: /* XOR(x,g) */ Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 0 ) ); Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 0 ) ); |