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/map/if/ifSat.c | |
| 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/map/if/ifSat.c')
| -rw-r--r-- | src/map/if/ifSat.c | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c index 4af55203..4709d88c 100644 --- a/src/map/if/ifSat.c +++ b/src/map/if/ifSat.c @@ -54,10 +54,11 @@ void * If_ManSatBuildXY( int nLutSize ) sat_solver_setnvars( p, nVars ); for ( m = 0; m < nMintsF; m++ ) sat_solver_add_mux( p, + iVarM + m, iVarP0 + m % nMintsL, iVarP1 + 2 * (m / nMintsL) + 1, iVarP1 + 2 * (m / nMintsL), - iVarM + m ); + 0, 0, 0, 0 ); return p; } void * If_ManSatBuildXYZ( int nLutSize ) @@ -73,13 +74,13 @@ void * If_ManSatBuildXYZ( int nLutSize ) sat_solver_setnvars( p, nVars ); for ( m = 0; m < nMintsF; m++ ) sat_solver_add_mux41( p, + iVarM + m, iVarP0 + m % nMintsL, iVarP1 + (m >> nLutSize) % nMintsL, iVarP2 + 4 * (m >> (2 * nLutSize)) + 0, iVarP2 + 4 * (m >> (2 * nLutSize)) + 1, iVarP2 + 4 * (m >> (2 * nLutSize)) + 2, - iVarP2 + 4 * (m >> (2 * nLutSize)) + 3, - iVarM + m ); + iVarP2 + 4 * (m >> (2 * nLutSize)) + 3 ); return p; } void If_ManSatUnbuild( void * p ) |