Satchmo.Unary.Op.Common

Documentation

iszero :: MonadSAT m => Number -> m Boolean

equals :: MonadSAT m => Number -> Number -> m Boolean

lt :: MonadSAT m => Number -> Number -> m Boolean

le :: MonadSAT m => Number -> Number -> m Boolean

ge :: MonadSAT m => Number -> Number -> m Boolean

eq :: MonadSAT m => Number -> Number -> m Boolean

gt :: MonadSAT m => Number -> Number -> m Boolean

min :: MonadSAT m => Number -> Number -> m Number

max :: MonadSAT m => Number -> Number -> m Number

minimum :: MonadSAT m => [Number] -> m Number

minimum (x:xs) = foldM min x xs

maximum :: MonadSAT m => [Number] -> m Number

maximum (x:xs) = foldM max x xs

select :: MonadSAT m => Boolean -> Number -> m Number

when f is False, switch off all bits

antiselect :: MonadSAT m => Boolean -> Number -> m Number

when p is True, switch ON all bits

add_quadratic :: MonadSAT m => Maybe Int -> Number -> Number -> m Number

for both "add" methods: if first arg is Nothing, then result length is sum of argument lengths (cannot overflow). else result is cut off (overflow => unsatisfiable)

add_by_odd_even_merge :: MonadSAT m => Maybe Int -> Number -> Number -> m Number

works for all widths

add_by_bitonic_sort :: MonadSAT m => Maybe Int -> Number -> Number -> m Number

will fill up the input such that length is a power of two. it seems to be hard to improve this, cf http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2009/CS/CS-2009-07