diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-03-05 23:00:30 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-03-05 23:00:30 -0800 |
| commit | 6da21b8b884632c901ae10955e23c0c8206e7e58 (patch) | |
| tree | 29e14c72c7e6e2bf2780268a7ed9390f88b56a5d /src/sat/bsat | |
| parent | ddc522a0c03ead1f84e45e515105a750f84ff265 (diff) | |
| download | abc-6da21b8b884632c901ae10955e23c0c8206e7e58.tar.gz abc-6da21b8b884632c901ae10955e23c0c8206e7e58.tar.bz2 abc-6da21b8b884632c901ae10955e23c0c8206e7e58.zip | |
Experiments with SAT-based cube enumeration.
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satSolver.h | 38 |
1 files changed, 19 insertions, 19 deletions
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index c82879de..ebc555d9 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -374,53 +374,53 @@ static inline int sat_solver_add_xor( sat_solver * pSat, int iVarA, int iVarB, i assert( Cid ); return 4; } -static inline int sat_solver_add_mux( sat_solver * pSat, int iVarC, int iVarT, int iVarE, int iVarZ ) +static inline int sat_solver_add_mux( sat_solver * pSat, int iVarZ, int iVarC, int iVarT, int iVarE, int iComplC, int iComplT, int iComplE, int iComplZ ) { lit Lits[3]; int Cid; assert( iVarC >= 0 && iVarT >= 0 && iVarE >= 0 && iVarZ >= 0 ); - Lits[0] = toLitCond( iVarC, 1 ); - Lits[1] = toLitCond( iVarT, 1 ); + Lits[0] = toLitCond( iVarC, 1 ^ iComplC ); + Lits[1] = toLitCond( iVarT, 1 ^ iComplT ); Lits[2] = toLitCond( iVarZ, 0 ); Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); assert( Cid ); - Lits[0] = toLitCond( iVarC, 1 ); - Lits[1] = toLitCond( iVarT, 0 ); - Lits[2] = toLitCond( iVarZ, 1 ); + Lits[0] = toLitCond( iVarC, 1 ^ iComplC ); + Lits[1] = toLitCond( iVarT, 0 ^ iComplT ); + Lits[2] = toLitCond( iVarZ, 1 ^ iComplZ ); Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); assert( Cid ); - Lits[0] = toLitCond( iVarC, 0 ); - Lits[1] = toLitCond( iVarE, 1 ); - Lits[2] = toLitCond( iVarZ, 0 ); + Lits[0] = toLitCond( iVarC, 0 ^ iComplC ); + Lits[1] = toLitCond( iVarE, 1 ^ iComplE ); + Lits[2] = toLitCond( iVarZ, 0 ^ iComplZ ); Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); assert( Cid ); - Lits[0] = toLitCond( iVarC, 0 ); - Lits[1] = toLitCond( iVarE, 0 ); - Lits[2] = toLitCond( iVarZ, 1 ); + Lits[0] = toLitCond( iVarC, 0 ^ iComplC ); + Lits[1] = toLitCond( iVarE, 0 ^ iComplE ); + Lits[2] = toLitCond( iVarZ, 1 ^ iComplZ ); Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); assert( Cid ); if ( iVarT == iVarE ) return 4; - Lits[0] = toLitCond( iVarT, 0 ); - Lits[1] = toLitCond( iVarE, 0 ); - Lits[2] = toLitCond( iVarZ, 1 ); + Lits[0] = toLitCond( iVarT, 0 ^ iComplT ); + Lits[1] = toLitCond( iVarE, 0 ^ iComplE ); + Lits[2] = toLitCond( iVarZ, 1 ^ iComplZ ); Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); assert( Cid ); - Lits[0] = toLitCond( iVarT, 1 ); - Lits[1] = toLitCond( iVarE, 1 ); - Lits[2] = toLitCond( iVarZ, 0 ); + Lits[0] = toLitCond( iVarT, 1 ^ iComplT ); + Lits[1] = toLitCond( iVarE, 1 ^ iComplE ); + Lits[2] = toLitCond( iVarZ, 0 ^ iComplZ ); Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); assert( Cid ); return 6; } -static inline int sat_solver_add_mux41( sat_solver * pSat, int iVarC0, int iVarC1, int iVarD0, int iVarD1, int iVarD2, int iVarD3, int iVarZ ) +static inline int sat_solver_add_mux41( sat_solver * pSat, int iVarZ, int iVarC0, int iVarC1, int iVarD0, int iVarD1, int iVarD2, int iVarD3 ) { lit Lits[4]; int Cid; |