From 6da21b8b884632c901ae10955e23c0c8206e7e58 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 5 Mar 2015 23:00:30 -0800 Subject: Experiments with SAT-based cube enumeration. --- src/map/if/ifSat.c | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'src/map/if/ifSat.c') 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 ) -- cgit v1.2.3