diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-02-27 21:11:05 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-02-27 21:11:05 -0800 |
| commit | b556c2591e8dc6e35d523971aa467bce4ad6200e (patch) | |
| tree | c8c3a60b07901c71cdd1d7bfd5c20d7188c424cc /src/sat | |
| parent | caa2227b1127802e4b35f296106ca19e113ea601 (diff) | |
| download | abc-b556c2591e8dc6e35d523971aa467bce4ad6200e.tar.gz abc-b556c2591e8dc6e35d523971aa467bce4ad6200e.tar.bz2 abc-b556c2591e8dc6e35d523971aa467bce4ad6200e.zip | |
Changes to LUT mappers.
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/bsat/satSolver.h | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 0d46b86b..345bbd28 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -368,6 +368,52 @@ 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 ) +{ + 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[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 ); + 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 ); + 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 ); + 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 ); + 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 ); + Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + return 6; +} static inline int sat_solver_add_xor_and( sat_solver * pSat, int iVarF, int iVarA, int iVarB, int iVarC ) { // F = (a (+) b) * c |