{-# language NoMonomorphismRestriction #-}
{-# language ScopedTypeVariables #-}

module Satchmo.Unary.Op.Common 
       
( iszero, equals
, lt, le, ge, eq, gt
, min, max
, minimum, maximum
, select, antiselect
, add_quadratic, add_by_odd_even_merge, add_by_bitonic_sort
)          
       
where


import Prelude 
  hiding ( and, or, not, compare, min, max, minimum, maximum )
import qualified Prelude

import qualified Satchmo.Code as C

import Satchmo.Unary.Data 
    (Number, make, bits, width, constant)

import Satchmo.Boolean (MonadSAT, Boolean, Booleans, fun2, fun3, and, or, not, xor, assert, boolean, monadic)
import qualified  Satchmo.Boolean as B

import Control.Monad ( forM, when, foldM, guard )
import qualified Data.Map as M
import Data.List ( transpose )

iszero :: Number -> m Boolean
iszero Number
n = case Number -> [Boolean]
bits Number
n of
    [] -> Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
True
    Boolean
x : [Boolean]
xs -> Boolean -> m Boolean
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Boolean -> m Boolean) -> Boolean -> m Boolean
forall a b. (a -> b) -> a -> b
$ Boolean -> Boolean
not Boolean
x
    
extended :: MonadSAT m 
         => ( [(Boolean,Boolean)] -> m a )
         -> Number -> Number
         -> m a
extended :: forall (m :: * -> *) a.
MonadSAT m =>
([(Boolean, Boolean)] -> m a) -> Number -> Number -> m a
extended [(Boolean, Boolean)] -> m a
action Number
a Number
b = do
    Boolean
f <- Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
False
    let zipf :: [Boolean] -> [Boolean] -> [(Boolean, Boolean)]
zipf [] [] = []
        zipf (Boolean
x:[Boolean]
xs) [] = (Boolean
x,Boolean
f) (Boolean, Boolean) -> [(Boolean, Boolean)] -> [(Boolean, Boolean)]
forall a. a -> [a] -> [a]
: [Boolean] -> [Boolean] -> [(Boolean, Boolean)]
zipf [Boolean]
xs []
        zipf [] (Boolean
y:[Boolean]
ys) = (Boolean
f,Boolean
y) (Boolean, Boolean) -> [(Boolean, Boolean)] -> [(Boolean, Boolean)]
forall a. a -> [a] -> [a]
: [Boolean] -> [Boolean] -> [(Boolean, Boolean)]
zipf [] [Boolean]
ys
        zipf (Boolean
x:[Boolean]
xs) (Boolean
y:[Boolean]
ys) = (Boolean
x,Boolean
y) (Boolean, Boolean) -> [(Boolean, Boolean)] -> [(Boolean, Boolean)]
forall a. a -> [a] -> [a]
: [Boolean] -> [Boolean] -> [(Boolean, Boolean)]
zipf [Boolean]
xs [Boolean]
ys
    [(Boolean, Boolean)] -> m a
action ([(Boolean, Boolean)] -> m a) -> [(Boolean, Boolean)] -> m a
forall a b. (a -> b) -> a -> b
$ [Boolean] -> [Boolean] -> [(Boolean, Boolean)]
zipf ( Number -> [Boolean]
bits Number
a ) ( Number -> [Boolean]
bits Number
b )    
        

le, ge, eq, equals, gt, lt 
  :: MonadSAT m => Number -> Number -> m Boolean

for :: [a] -> (a -> b) -> [b]
for = ((a -> b) -> [a] -> [b]) -> [a] -> (a -> b) -> [b]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map

equals :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
equals = ([(Boolean, Boolean)] -> m Boolean)
-> Number -> Number -> m Boolean
forall (m :: * -> *) a.
MonadSAT m =>
([(Boolean, Boolean)] -> m a) -> Number -> Number -> m a
extended (([(Boolean, Boolean)] -> m Boolean)
 -> Number -> Number -> m Boolean)
-> ([(Boolean, Boolean)] -> m Boolean)
-> Number
-> Number
-> m Boolean
forall a b. (a -> b) -> a -> b
$ \ [(Boolean, Boolean)]
xys -> ([Boolean] -> m Boolean) -> [m Boolean] -> m Boolean
forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and ([m Boolean] -> m Boolean) -> [m Boolean] -> m Boolean
forall a b. (a -> b) -> a -> b
$ 
    [(Boolean, Boolean)]
-> ((Boolean, Boolean) -> m Boolean) -> [m Boolean]
forall {a} {b}. [a] -> (a -> b) -> [b]
for [(Boolean, Boolean)]
xys (((Boolean, Boolean) -> m Boolean) -> [m Boolean])
-> ((Boolean, Boolean) -> m Boolean) -> [m Boolean]
forall a b. (a -> b) -> a -> b
$ \ (Boolean
x,Boolean
y) -> (Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==) Boolean
x Boolean
y

le :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
le = ([(Boolean, Boolean)] -> m Boolean)
-> Number -> Number -> m Boolean
forall (m :: * -> *) a.
MonadSAT m =>
([(Boolean, Boolean)] -> m a) -> Number -> Number -> m a
extended (([(Boolean, Boolean)] -> m Boolean)
 -> Number -> Number -> m Boolean)
-> ([(Boolean, Boolean)] -> m Boolean)
-> Number
-> Number
-> m Boolean
forall a b. (a -> b) -> a -> b
$ \ [(Boolean, Boolean)]
xys -> ([Boolean] -> m Boolean) -> [m Boolean] -> m Boolean
forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and ([m Boolean] -> m Boolean) -> [m Boolean] -> m Boolean
forall a b. (a -> b) -> a -> b
$ 
    [(Boolean, Boolean)]
-> ((Boolean, Boolean) -> m Boolean) -> [m Boolean]
forall {a} {b}. [a] -> (a -> b) -> [b]
for [(Boolean, Boolean)]
xys (((Boolean, Boolean) -> m Boolean) -> [m Boolean])
-> ((Boolean, Boolean) -> m Boolean) -> [m Boolean]
forall a b. (a -> b) -> a -> b
$ \ (Boolean
x,Boolean
y) -> (Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 Bool -> Bool -> Bool
forall a. Ord a => a -> a -> Bool
(<=) Boolean
x Boolean
y

ge :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
ge = (Number -> Number -> m Boolean) -> Number -> Number -> m Boolean
forall a b c. (a -> b -> c) -> b -> a -> c
flip Number -> Number -> m Boolean
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
le

eq :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
eq = Number -> Number -> m Boolean
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
equals

lt :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
lt Number
a Number
b = (Boolean -> Boolean) -> m Boolean -> m Boolean
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Boolean -> Boolean
not (m Boolean -> m Boolean) -> m Boolean -> m Boolean
forall a b. (a -> b) -> a -> b
$ Number -> Number -> m Boolean
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
ge Number
a Number
b

gt :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
gt = (Number -> Number -> m Boolean) -> Number -> Number -> m Boolean
forall a b c. (a -> b -> c) -> b -> a -> c
flip Number -> Number -> m Boolean
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
lt

min :: Number -> Number -> m Number
min Number
a Number
b = do 
    [Boolean]
cs <- ([(Boolean, Boolean)] -> m [Boolean])
-> Number -> Number -> m [Boolean]
forall (m :: * -> *) a.
MonadSAT m =>
([(Boolean, Boolean)] -> m a) -> Number -> Number -> m a
extended ( \ [(Boolean, Boolean)]
xys -> 
        [(Boolean, Boolean)]
-> ((Boolean, Boolean) -> m Boolean) -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Boolean, Boolean)]
xys (((Boolean, Boolean) -> m Boolean) -> m [Boolean])
-> ((Boolean, Boolean) -> m Boolean) -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ \ (Boolean
x,Boolean
y) -> [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [Boolean
x,Boolean
y] ) Number
a Number
b
    Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number -> m Number) -> Number -> m Number
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
cs                              
                          
max :: Number -> Number -> m Number
max Number
a Number
b = do
    [Boolean]
cs <- ([(Boolean, Boolean)] -> m [Boolean])
-> Number -> Number -> m [Boolean]
forall (m :: * -> *) a.
MonadSAT m =>
([(Boolean, Boolean)] -> m a) -> Number -> Number -> m a
extended ( \ [(Boolean, Boolean)]
xys -> 
        [(Boolean, Boolean)]
-> ((Boolean, Boolean) -> m Boolean) -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Boolean, Boolean)]
xys (((Boolean, Boolean) -> m Boolean) -> m [Boolean])
-> ((Boolean, Boolean) -> m Boolean) -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ \ (Boolean
x,Boolean
y) -> [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [Boolean
x,Boolean
y] ) Number
a Number
b
    Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number -> m Number) -> Number -> m Number
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
cs                      

-- | maximum (x:xs) = foldM max x xs
maximum :: [Number] -> m Number
maximum [Number
x] = Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Number
x
maximum [Number]
xs | Bool -> Bool
Prelude.not ( [Number] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Number]
xs ) = do
    Boolean
f <- Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
False
    let w :: Int
w = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
Prelude.maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (Number -> Int) -> [Number] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Number -> Int
width [Number]
xs
        fill :: Number -> [Boolean]
fill Number
x = Number -> [Boolean]
bits Number
x [Boolean] -> [Boolean] -> [Boolean]
forall a. [a] -> [a] -> [a]
++ Int -> Boolean -> [Boolean]
forall a. Int -> a -> [a]
replicate (Int
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Number -> Int
width Number
x) Boolean
f
    [Boolean]
ys <- [[Boolean]] -> ([Boolean] -> m Boolean) -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( [[Boolean]] -> [[Boolean]]
forall a. [[a]] -> [[a]]
transpose ([[Boolean]] -> [[Boolean]]) -> [[Boolean]] -> [[Boolean]]
forall a b. (a -> b) -> a -> b
$ (Number -> [Boolean]) -> [Number] -> [[Boolean]]
forall a b. (a -> b) -> [a] -> [b]
map Number -> [Boolean]
fill [Number]
xs ) [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
B.or
    Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number -> m Number) -> Number -> m Number
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
ys

-- | minimum (x:xs) = foldM min x xs
minimum :: [Number] -> m Number
minimum [Number
x] = Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Number
x
minimum [Number]
xs | Bool -> Bool
Prelude.not ( [Number] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Number]
xs ) = do
    Boolean
f <- Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
False
    let w :: Int
w = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
Prelude.maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (Number -> Int) -> [Number] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Number -> Int
width [Number]
xs
        fill :: Number -> [Boolean]
fill Number
x = Number -> [Boolean]
bits Number
x [Boolean] -> [Boolean] -> [Boolean]
forall a. [a] -> [a] -> [a]
++ Int -> Boolean -> [Boolean]
forall a. Int -> a -> [a]
replicate (Int
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Number -> Int
width Number
x) Boolean
f
    [Boolean]
ys <- [[Boolean]] -> ([Boolean] -> m Boolean) -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( [[Boolean]] -> [[Boolean]]
forall a. [[a]] -> [[a]]
transpose ([[Boolean]] -> [[Boolean]]) -> [[Boolean]] -> [[Boolean]]
forall a b. (a -> b) -> a -> b
$ (Number -> [Boolean]) -> [Number] -> [[Boolean]]
forall a b. (a -> b) -> [a] -> [b]
map Number -> [Boolean]
fill [Number]
xs ) [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
B.and
    Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number -> m Number) -> Number -> m Number
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
ys


-- | when f is False, switch off all bits
select :: Boolean -> Number -> m Number
select Boolean
f Number
a = do
    [Boolean]
bs <- [Boolean] -> (Boolean -> m Boolean) -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( Number -> [Boolean]
bits Number
a ) ((Boolean -> m Boolean) -> m [Boolean])
-> (Boolean -> m Boolean) -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ \ Boolean
b -> [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [Boolean
f,Boolean
b]
    Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number -> m Number) -> Number -> m Number
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
bs

-- | when p is True, switch ON all bits
antiselect :: Boolean -> Number -> m Number
antiselect Boolean
p Number
n = do
    [Boolean]
bs <- [Boolean] -> (Boolean -> m Boolean) -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( Number -> [Boolean]
bits Number
n ) ((Boolean -> m Boolean) -> m [Boolean])
-> (Boolean -> m Boolean) -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ \ Boolean
b -> [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
B.or [Boolean
p, Boolean
b]
    Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number -> m Number) -> Number -> m Number
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
bs

-- | reduce number to given bit width,
-- and return also the carry bit
cutoff_with_carry :: MonadSAT m 
                  => Maybe Int -> Number -> m (Number, Boolean)
cutoff_with_carry :: forall (m :: * -> *).
MonadSAT m =>
Maybe Int -> Number -> m (Number, Boolean)
cutoff_with_carry Maybe Int
mwidth Number
n = do
    Boolean
f <- Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
False
    case Maybe Int
mwidth of
        Maybe Int
Nothing -> (Number, Boolean) -> m (Number, Boolean)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number
n , Boolean
f )
        Just Int
width -> do
            let ( [Boolean]
pre, [Boolean]
post ) = Int -> [Boolean] -> ([Boolean], [Boolean])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
width ([Boolean] -> ([Boolean], [Boolean]))
-> [Boolean] -> ([Boolean], [Boolean])
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
n
            (Number, Boolean) -> m (Number, Boolean)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ( [Boolean] -> Number
make [Boolean]
pre, case [Boolean]
post of
                [] -> Boolean
f
                Boolean
carry : [Boolean]
_ -> Boolean
carry )

cutoff :: Maybe Int -> Number -> m Number
cutoff Maybe Int
mwidth Number
n = do
    ( Number
result, Boolean
carry ) <- Maybe Int -> Number -> m (Number, Boolean)
forall (m :: * -> *).
MonadSAT m =>
Maybe Int -> Number -> m (Number, Boolean)
cutoff_with_carry Maybe Int
mwidth Number
n
    [Boolean] -> m ()
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [ Boolean -> Boolean
not Boolean
carry ]
    Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Number
result

-- | 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_quadratic :: MonadSAT m => Maybe Int -> Number -> Number -> m Number
add_quadratic :: forall (m :: * -> *).
MonadSAT m =>
Maybe Int -> Number -> Number -> m Number
add_quadratic Maybe Int
mwidth Number
a Number
b = do
    Boolean
t <- Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
True
    [(Int, [Boolean])]
pairs <- [m (Int, [Boolean])] -> m [(Int, [Boolean])]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([m (Int, [Boolean])] -> m [(Int, [Boolean])])
-> [m (Int, [Boolean])] -> m [(Int, [Boolean])]
forall a b. (a -> b) -> a -> b
$ do
        (Int
i,Boolean
x) <- [Int] -> [Boolean] -> [(Int, Boolean)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 .. ] ([Boolean] -> [(Int, Boolean)]) -> [Boolean] -> [(Int, Boolean)]
forall a b. (a -> b) -> a -> b
$ Boolean
t Boolean -> [Boolean] -> [Boolean]
forall a. a -> [a] -> [a]
: Number -> [Boolean]
bits Number
a
        (Int
j,Boolean
y) <- [Int] -> [Boolean] -> [(Int, Boolean)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 .. ] ([Boolean] -> [(Int, Boolean)]) -> [Boolean] -> [(Int, Boolean)]
forall a b. (a -> b) -> a -> b
$ Boolean
t Boolean -> [Boolean] -> [Boolean]
forall a. a -> [a] -> [a]
: Number -> [Boolean]
bits Number
b
        Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
        Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ case Maybe Int
mwidth of
            Just Int
width -> Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
width Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
            Maybe Int
Nothing    -> Bool
True
        m (Int, [Boolean]) -> [m (Int, [Boolean])]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (m (Int, [Boolean]) -> [m (Int, [Boolean])])
-> m (Int, [Boolean]) -> [m (Int, [Boolean])]
forall a b. (a -> b) -> a -> b
$ do Boolean
z <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [Boolean
x,Boolean
y] ; (Int, [Boolean]) -> m (Int, [Boolean])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
j, [Boolean
z])
    [Boolean]
cs <- [[Boolean]] -> ([Boolean] -> m Boolean) -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( ((Int, [Boolean]) -> [Boolean])
-> [(Int, [Boolean])] -> [[Boolean]]
forall a b. (a -> b) -> [a] -> [b]
map (Int, [Boolean]) -> [Boolean]
forall a b. (a, b) -> b
snd ([(Int, [Boolean])] -> [[Boolean]])
-> [(Int, [Boolean])] -> [[Boolean]]
forall a b. (a -> b) -> a -> b
$ Map Int [Boolean] -> [(Int, [Boolean])]
forall k a. Map k a -> [(k, a)]
M.toAscList (Map Int [Boolean] -> [(Int, [Boolean])])
-> Map Int [Boolean] -> [(Int, [Boolean])]
forall a b. (a -> b) -> a -> b
$ ([Boolean] -> [Boolean] -> [Boolean])
-> [(Int, [Boolean])] -> Map Int [Boolean]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith [Boolean] -> [Boolean] -> [Boolean]
forall a. [a] -> [a] -> [a]
(++) [(Int, [Boolean])]
pairs ) [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or
    Maybe Int -> Number -> m Number
forall {m :: * -> *}. MonadSAT m => Maybe Int -> Number -> m Number
cutoff Maybe Int
mwidth (Number -> m Number) -> Number -> m Number
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
cs


  
-- | works for all widths
add_by_odd_even_merge :: Maybe Int -> Number -> Number -> m Number
add_by_odd_even_merge Maybe Int
mwidth Number
a Number
b = do
    [Boolean]
zs <- [Boolean] -> [Boolean] -> m [Boolean]
forall {m :: * -> *}.
MonadSAT m =>
[Boolean] -> [Boolean] -> m [Boolean]
oe_merge (Number -> [Boolean]
bits Number
a) (Number -> [Boolean]
bits Number
b)
    Maybe Int -> Number -> m Number
forall {m :: * -> *}. MonadSAT m => Maybe Int -> Number -> m Number
cutoff Maybe Int
mwidth (Number -> m Number) -> Number -> m Number
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
zs
    
-- | 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>
add_by_bitonic_sort :: Maybe Int -> Number -> Number -> m Number
add_by_bitonic_sort Maybe Int
mwidth Number
a Number
b = do
    let n :: Int
n = [Boolean] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ( Number -> [Boolean]
bits Number
a) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Boolean] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Number -> [Boolean]
bits Number
b)
    Boolean
f <- Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
False        
    let input :: [Boolean]
input =    (Number -> [Boolean]
bits Number
a) -- decreasing
                [Boolean] -> [Boolean] -> [Boolean]
forall a. [a] -> [a] -> [a]
++ Int -> Boolean -> [Boolean]
forall a. Int -> a -> [a]
replicate (Int -> Int
forall {t}. Integral t => t -> t
fill Int
n) Boolean
f
                [Boolean] -> [Boolean] -> [Boolean]
forall a. [a] -> [a] -> [a]
++ ([Boolean] -> [Boolean]
forall a. [a] -> [a]
reverse ([Boolean] -> [Boolean]) -> [Boolean] -> [Boolean]
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
b) -- increasing
    [Boolean]
zs <- [Boolean] -> m [Boolean]
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m [Boolean]
bitonic_sort [Boolean]
input
    Maybe Int -> Number -> m Number
forall {m :: * -> *}. MonadSAT m => Maybe Int -> Number -> m Number
cutoff Maybe Int
mwidth (Number -> m Number) -> Number -> m Number
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
zs

-- | distance to next power of two
fill :: t -> t
fill t
n = if t
n t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= t
1 then t
0 else
            let (t
d,t
m) = t -> t -> (t, t)
forall a. Integral a => a -> a -> (a, a)
divMod t
n t
2
            in  t
m t -> t -> t
forall a. Num a => a -> a -> a
+ t
2t -> t -> t
forall a. Num a => a -> a -> a
*t -> t
fill (t
dt -> t -> t
forall a. Num a => a -> a -> a
+t
m) 

-- |  <http://www.iti.fh-flensburg.de/lang/algorithmen/sortieren/bitonic/bitonicen.htm>
bitonic_sort :: [Boolean] -> m [Boolean]
bitonic_sort [ ] = [Boolean] -> m [Boolean]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [ ]    
bitonic_sort [Boolean
z] = [Boolean] -> m [Boolean]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [Boolean
z]
bitonic_sort [Boolean]
zs = do 
    let (Int
h,Int
0) = Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
divMod ([Boolean] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Boolean]
zs) Int
2
        ([Boolean]
pre, [Boolean]
post) = Int -> [Boolean] -> ([Boolean], [Boolean])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
h [Boolean]
zs
    [Boolean]
hi <- [(Boolean, Boolean)]
-> ((Boolean, Boolean) -> m Boolean) -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( [Boolean] -> [Boolean] -> [(Boolean, Boolean)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Boolean]
pre [Boolean]
post ) (((Boolean, Boolean) -> m Boolean) -> m [Boolean])
-> ((Boolean, Boolean) -> m Boolean) -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ \ (Boolean
x,Boolean
y) -> [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or  [Boolean
x,Boolean
y]
    [Boolean]
lo <- [(Boolean, Boolean)]
-> ((Boolean, Boolean) -> m Boolean) -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( [Boolean] -> [Boolean] -> [(Boolean, Boolean)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Boolean]
pre [Boolean]
post ) (((Boolean, Boolean) -> m Boolean) -> m [Boolean])
-> ((Boolean, Boolean) -> m Boolean) -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ \ (Boolean
x,Boolean
y) -> [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [Boolean
x,Boolean
y]
    [Boolean]
shi <- [Boolean] -> m [Boolean]
bitonic_sort [Boolean]
hi
    [Boolean]
slo <- [Boolean] -> m [Boolean]
bitonic_sort [Boolean]
lo
    [Boolean] -> m [Boolean]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Boolean] -> m [Boolean]) -> [Boolean] -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ [Boolean]
shi [Boolean] -> [Boolean] -> [Boolean]
forall a. [a] -> [a] -> [a]
++ [Boolean]
slo
    
-- | <http://www.iti.fh-flensburg.de/lang/algorithmen/sortieren/networks/oemen.htm>

oe_merge :: [Boolean] -> [Boolean] -> m [Boolean]
oe_merge  [] [Boolean]
ys = [Boolean] -> m [Boolean]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [Boolean]
ys
oe_merge  [Boolean]
xs [] = [Boolean] -> m [Boolean]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [Boolean]
xs
oe_merge  [Boolean
x] [Boolean
y] = do
    Boolean -> Boolean -> m [Boolean]
forall {m :: * -> *}.
MonadSAT m =>
Boolean -> Boolean -> m [Boolean]
comparator Boolean
x Boolean
y
oe_merge  [Boolean]
xs [Boolean]
ys = do
    let ( [Boolean]
xo, [Boolean]
xe ) = [Boolean] -> ([Boolean], [Boolean])
forall {a}. [a] -> ([a], [a])
divide [Boolean]
xs
        ( [Boolean]
yo, [Boolean]
ye ) = [Boolean] -> ([Boolean], [Boolean])
forall {a}. [a] -> ([a], [a])
divide [Boolean]
ys
    ~(Boolean
m : [Boolean]
mo) <- [Boolean] -> [Boolean] -> m [Boolean]
oe_merge  [Boolean]
xo [Boolean]
yo
    [Boolean]
me <- [Boolean] -> [Boolean] -> m [Boolean]
oe_merge  [Boolean]
xe [Boolean]
ye
    [Boolean]
re <- [Boolean] -> [Boolean] -> m [Boolean]
forall {m :: * -> *}.
MonadSAT m =>
[Boolean] -> [Boolean] -> m [Boolean]
repair [Boolean]
me [Boolean]
mo
    [Boolean] -> m [Boolean]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Boolean] -> m [Boolean]) -> [Boolean] -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ Boolean
m Boolean -> [Boolean] -> [Boolean]
forall a. a -> [a] -> [a]
: [Boolean]
re

divide :: [a] -> ([a], [a])
divide (a
x : [a]
xs) = 
    let ( [a]
this, [a]
that ) = [a] -> ([a], [a])
divide [a]
xs
    in  ( a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
that, [a]
this )
divide [] = ( [], [] )

repair :: [Boolean] -> [Boolean] -> m [Boolean]
repair (Boolean
x:[Boolean]
xs) (Boolean
y:[Boolean]
ys) = do
    [Boolean]
here <- Boolean -> Boolean -> m [Boolean]
forall {m :: * -> *}.
MonadSAT m =>
Boolean -> Boolean -> m [Boolean]
comparator Boolean
x Boolean
y
    [Boolean]
later <- [Boolean] -> [Boolean] -> m [Boolean]
repair [Boolean]
xs [Boolean]
ys
    [Boolean] -> m [Boolean]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Boolean] -> m [Boolean]) -> [Boolean] -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ [Boolean]
here [Boolean] -> [Boolean] -> [Boolean]
forall a. [a] -> [a] -> [a]
++ [Boolean]
later
repair [] [] = [Boolean] -> m [Boolean]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
repair [Boolean
x] [] = [Boolean] -> m [Boolean]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [Boolean
x]
repair [] [Boolean
y] = [Boolean] -> m [Boolean]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [Boolean
y]

comparator :: Boolean -> Boolean -> m [Boolean]
comparator Boolean
x Boolean
y = do
    Boolean
hi <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
Satchmo.Boolean.or [Boolean
x, Boolean
y]
    Boolean
lo <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
Satchmo.Boolean.and [Boolean
x, Boolean
y]
    [Boolean] -> m [Boolean]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Boolean
hi, Boolean
lo ]