diff options
| author | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-09-09 12:40:55 +0200 |
|---|---|---|
| committer | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-09-09 12:40:55 +0200 |
| commit | 2f2ed1bce15575f37e3a96e3c2f3f9a139e3922e (patch) | |
| tree | e8d8fbd77725dc2dc577f5bef2276f00dee6ecef | |
| parent | 5b2472d4b719875c8017814c9c81bcd4f4691011 (diff) | |
| download | abc-2f2ed1bce15575f37e3a96e3c2f3f9a139e3922e.tar.gz abc-2f2ed1bce15575f37e3a96e3c2f3f9a139e3922e.tar.bz2 abc-2f2ed1bce15575f37e3a96e3c2f3f9a139e3922e.zip | |
Fixes in BMS.
| -rw-r--r-- | src/base/abci/abcExact.c | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index 58e4db14..00d534ec 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -1326,27 +1326,29 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes ) { Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManSelectVar( pSes, pSes->nGates - 1 - i, j, pSes->nSpecVars + pSes->nGates - 2 - i ), 0 ) ); + //printf( "dec %d for var %d\n", pSes->pStairDecFunc[i], j ); + switch ( pSes->pStairDecFunc[i] ) { case 1: /* AND(x,g) */ Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 1 ) ); - 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 ) ); + //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 2: /* AND(!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, 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 ), 1 ) ); break; case 3: /* OR(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, 0, 1 ), 0 ) ); Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 0 ) ); Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 0 ) ); break; case 4: /* OR(!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 ), 1 ) ); - Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 0 ) ); + ////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 ) ); |