{-# LANGUAGE BangPatterns, Safe #-}

{-|
Module      : Dep.Algorithm.Synthesis
Description : A module to convert a 'Three' of 'ThreeValue's into a sum-of-products of a product-of-sums.
Maintainer  : hapytexeu+gh@gmail.com
Stability   : experimental
Portability : POSIX

This module defines functions to generate a /sum-of-products/ or a /product-of-sums/ with the given
function specified by a 'Three'.
-}

module Dep.Algorithm.Synthesis (
    -- * Synthesize a 'Three'
    synthesis, synthesis'
  , synthesisSOP, synthesisSOP'
  , synthesisPOS, synthesisPOS'
    -- * Weigthed variants of the product and sum
  , WeightedProduct, WeightedSum
    -- * Create an upper and lowerbound Three
  , upperbound, lowerbound
    -- * Extract products and sums
  , extractProduct, extractSum
    -- * Processing a 'Three'
  , wipeout, wipeout'
  ) where

import Control.Applicative((<|>))

import Dep.Class.Opposite(opposite)
import Dep.Class.NonDeterministicWalkable(NonDeterministicWalkable(allNstep))
import Dep.Class.Simplify(simplify)
import Dep.Class.Walkable(Walkable(allStep, allWalkValues))
import Dep.Data.LogicItem(Item')
import Dep.Data.Product(Product(Product), Product', SumOfProducts(SumOfProducts), SumOfProducts')
import Dep.Data.Sum(ProductOfSums(ProductOfSums), ProductOfSums', Sum', Sum(Sum))
import Dep.Data.Three(Three(Leaf, Link, Split), depth, wipe)
import Dep.Data.ThreeValue(ThreeValue(DontCare, Zero, One), fromBool, toLower, toUpper)

type WeightedItem = (Int, Item')

-- | A 2-tuple where the first item is the "weight" of the product, and the second one the corresponding 'Product''.
type WeightedProduct = (Int, Product')

-- | A 2-tuple where the first item is the "weight" of the sum, and the second one the corresponding 'Sum''.
type WeightedSum = (Int, Sum')

-- | Create a /simplified/ 'Three' where the 'DontCare' and 'One' map to 'True';
-- and 'Zero' maps to 'False'.
upperbound
  :: Three ThreeValue -- ^ The given 'Three' of 'ThreeValue's where we calculate the /upperbound/ from.
  -> Three Bool -- ^ The corresponding /upperbound/.
upperbound :: Three ThreeValue -> Three Bool
upperbound = Three Bool -> Three Bool
forall a. Simplify a => a -> a
simplify (Three Bool -> Three Bool)
-> (Three ThreeValue -> Three Bool)
-> Three ThreeValue
-> Three Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ThreeValue -> Bool) -> Three ThreeValue -> Three Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ThreeValue -> Bool
toUpper

-- | Create a /simplified/ 'Three' where the 'DontCare' and 'Zero' map to 'False';
-- and 'One' maps to 'True'.
lowerbound
  :: Three ThreeValue -- ^ The given 'Three' of 'ThreeValue's where we calculate the /lowerbound/ from.
  -> Three Bool -- ^ The corresponding /lowerbound/.
lowerbound :: Three ThreeValue -> Three Bool
lowerbound = Three Bool -> Three Bool
forall a. Simplify a => a -> a
simplify (Three Bool -> Three Bool)
-> (Three ThreeValue -> Three Bool)
-> Three ThreeValue
-> Three Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ThreeValue -> Bool) -> Three ThreeValue -> Three Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ThreeValue -> Bool
toLower

_pushVal :: (Int -> Int) -> ThreeValue -> (Int, Product') -> (Int, Product')
_pushVal :: (Int -> Int) -> ThreeValue -> (Int, Product') -> (Int, Product')
_pushVal Int -> Int
f ThreeValue
x = (Int, Product') -> (Int, Product')
go
    where go :: (Int, Product') -> (Int, Product')
go ~(!Int
n, Product'
xs) = (Int -> Int
f Int
n, ThreeValue
xThreeValue -> Product' -> Product'
forall a. a -> [a] -> [a]
:Product'
xs)

_pushVal' :: ThreeValue -> (Int, Product') -> (Int, Product')
_pushVal' :: ThreeValue -> (Int, Product') -> (Int, Product')
_pushVal' = (Int -> Int) -> ThreeValue -> (Int, Product') -> (Int, Product')
_pushVal Int -> Int
forall a. Enum a => a -> a
succ

_pushVal'' :: (Int, Product') -> (Int, Product')
_pushVal'' :: (Int, Product') -> (Int, Product')
_pushVal'' = (Int -> Int) -> ThreeValue -> (Int, Product') -> (Int, Product')
_pushVal Int -> Int
forall a. a -> a
id ThreeValue
DontCare

extractItem
  :: ThreeValue  -- ^ The given 'ThreeValue' we are looking for. Typically this will be 'One' for a sum-of-products, and 'Zero' for a product of sums.
  -> Int  -- Y The maximum depth of the 'Three'.
  -> Three Bool -- ^ A 'Three' of 'Bool's that specifies if 'One' can be assigned to it (so either 'One' or 'DontCare').
  -> Three ThreeValue -- ^ A 'Three' of 'ThreeValue's in which we search for the given element.
  -> Maybe WeightedItem  -- ^ A path to a 'Leaf; with the given 'ThreeValue' together with the number of 'Zero's and 'One's in that path. If no path is found 'Nothing' is returned.
extractItem :: ThreeValue
-> Int -> Three Bool -> Three ThreeValue -> Maybe (Int, Product')
extractItem ThreeValue
x' Int
k Three Bool
_ = Int -> Three ThreeValue -> Maybe (Int, Product')
go Int
k
  where go :: Int -> Three ThreeValue -> Maybe (Int, Product')
go !Int
n (Leaf ThreeValue
x)
          | ThreeValue
x ThreeValue -> ThreeValue -> Bool
forall a. Eq a => a -> a -> Bool
== ThreeValue
x' = (Int, Product') -> Maybe (Int, Product')
forall a. a -> Maybe a
Just (Int
0, Int -> ThreeValue -> Product'
forall a. Int -> a -> [a]
replicate Int
n ThreeValue
DontCare)
          | Bool
otherwise = Maybe (Int, Product')
forall a. Maybe a
Nothing
        go Int
n (Link Three ThreeValue
l) = (Int, Product') -> (Int, Product')
_pushVal'' ((Int, Product') -> (Int, Product'))
-> Maybe (Int, Product') -> Maybe (Int, Product')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Three ThreeValue -> Maybe (Int, Product')
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Three ThreeValue
l
        go Int
n ~(Split Three ThreeValue
la Three ThreeValue
lb) = ((Int, Product') -> (Int, Product'))
-> Maybe (Int, Product') -> Maybe (Int, Product')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ThreeValue -> (Int, Product') -> (Int, Product')
_pushVal' ThreeValue
Zero) (Int -> Three ThreeValue -> Maybe (Int, Product')
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Three ThreeValue
la) Maybe (Int, Product')
-> Maybe (Int, Product') -> Maybe (Int, Product')
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((Int, Product') -> (Int, Product'))
-> Maybe (Int, Product') -> Maybe (Int, Product')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ThreeValue -> (Int, Product') -> (Int, Product')
_pushVal' ThreeValue
One) (Int -> Three ThreeValue -> Maybe (Int, Product')
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Three ThreeValue
lb)


-- | Obtain a 'Product'' together with the number of inputs for the AND gate if the 'Three'
-- contains at least one 'One'.
extractProduct
  :: Int  -- ^ The maximum depth of the 'Three'.
  -> Three Bool -- ^ A 'Three' of 'Bool's that specifies if 'One' can be assigned to it (so either 'One' or 'DontCare').
  -> Three ThreeValue -- ^ The 'Three' of 'ThreeValue's where we try to search for an item.
  -> Maybe WeightedProduct -- ^ A 2-tuple that contains the path to the leaf and the number of 'Zero's and 'One's in the path that measure the "weight" of the AND gate of the product.
extractProduct :: Int -> Three Bool -> Three ThreeValue -> Maybe (Int, Product')
extractProduct = ThreeValue
-> Int -> Three Bool -> Three ThreeValue -> Maybe (Int, Product')
extractItem ThreeValue
One

-- | Obtain a 'Sum'' together with the number of inputs for the OR gates if the 'Three'
-- contains at least one 'Zero'.
extractSum
  :: Int  -- ^ The maximum depth of the 'Three'.
  -> Three Bool -- ^ A 'Three' of 'Bool's that specifies if 'Zero' can be assigned to it (so either 'Zero' or 'DontCare').
  -> Three ThreeValue -- ^ The 'Three' of 'ThreeValue's where we try to search for an item.
  -> Maybe WeightedSum -- ^ A 2-tuple that contains the path to the leaf and the number of 'Zero's and 'One's in the path that measure the "weight" of the OR gate of the product.
extractSum :: Int -> Three Bool -> Three ThreeValue -> Maybe (Int, Product')
extractSum = ThreeValue
-> Int -> Three Bool -> Three ThreeValue -> Maybe (Int, Product')
extractItem ThreeValue
Zero

-- | Convert the items that are accessed by the 'Product''
-- to a 'DontCare', and simplify the 'Three'. After wiping
-- out values, the 'Three' is simplified.
wipeout
  :: Product' -- ^ The product that specifies the path of the element(s) to set to 'DontCare'.
  -> Three ThreeValue  -- ^ The original 'Three' of 'ThreeValue's where we want to convert parts to 'DontCare'.
  -> Three ThreeValue  -- ^ The resulting 'Three' of 'ThreeValue's where items that match the path are wiped out.
wipeout :: Product' -> Three ThreeValue -> Three ThreeValue
wipeout Product'
path = Three ThreeValue -> Three ThreeValue
forall a. Simplify a => a -> a
simplify (Three ThreeValue -> Three ThreeValue)
-> (Three ThreeValue -> Three ThreeValue)
-> Three ThreeValue
-> Three ThreeValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Product' -> Three ThreeValue -> Three ThreeValue
wipeout' Product'
path

-- | Convert the items that are accessed by the 'Product''
-- to a 'DontCare', and simplify the 'Three'.
wipeout'
  :: Product' -- ^ The product that specifies the path of the element(s) to set to 'DontCare'.
  -> Three ThreeValue  -- ^ The original 'Three' of 'ThreeValue's where we want to convert parts to 'DontCare'.
  -> Three ThreeValue  -- ^ The resulting 'Three' of 'ThreeValue's where items that match the path are wiped out.
wipeout' :: Product' -> Three ThreeValue -> Three ThreeValue
wipeout' = ThreeValue -> Product' -> Three ThreeValue -> Three ThreeValue
forall a. a -> Product' -> Three a -> Three a
wipe ThreeValue
DontCare

mergeSide :: (Int -> Maybe WeightedItem) -> Int -> Maybe (Int, Product') -> Maybe WeightedItem
mergeSide :: (Int -> Maybe (Int, Product'))
-> Int -> Maybe (Int, Product') -> Maybe (Int, Product')
mergeSide Int -> Maybe (Int, Product')
f Int
n = Maybe (Int, Product') -> Maybe (Int, Product')
go
    where go :: Maybe (Int, Product') -> Maybe (Int, Product')
go Maybe (Int, Product')
Nothing = Int -> Maybe (Int, Product')
f Int
n
          go j :: Maybe (Int, Product')
j@(~(Just ~(Int
k, Product'
_))) = Int -> Maybe (Int, Product')
f Int
k Maybe (Int, Product')
-> Maybe (Int, Product') -> Maybe (Int, Product')
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe (Int, Product')
j

_minimizeItem' :: ([Bool] -> Bool) -> Int -> [Bool] -> [Three Bool] -> Maybe WeightedItem
_minimizeItem' :: ([Bool] -> Bool)
-> Int -> [Bool] -> [Three Bool] -> Maybe (Int, Product')
_minimizeItem' [Bool] -> Bool
_ Int
n [Bool]
_ [Three Bool]
_ | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = Maybe (Int, Product')
forall a. Maybe a
Nothing
_minimizeItem' [Bool] -> Bool
_ Int
_ [] [Three Bool]
_ = (Int, Product') -> Maybe (Int, Product')
forall a. a -> Maybe a
Just (Int
0, [])
_minimizeItem' [Bool] -> Bool
mg Int
n ~(Bool
x:[Bool]
xs) [Three Bool]
thr
  | [Bool] -> Bool
mg ([Three Bool] -> [Bool] -> [Bool]
forall (f :: * -> *) step (g :: * -> *) (h :: * -> *) a.
(Walkable f step, Foldable f, Foldable g, Functor g, Foldable h) =>
g (f a) -> h step -> [a]
allWalkValues [Three Bool]
stepdc [Bool]
xs) = (Int -> Maybe (Int, Product'))
-> Int -> Maybe (Int, Product') -> Maybe (Int, Product')
mergeSide (\Int
i -> (Int, Product') -> (Int, Product')
pshVal ((Int, Product') -> (Int, Product'))
-> Maybe (Int, Product') -> Maybe (Int, Product')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Bool] -> Bool)
-> Int -> [Bool] -> [Three Bool] -> Maybe (Int, Product')
_minimizeItem' [Bool] -> Bool
mg (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [Bool]
xs ([Three Bool] -> Bool -> [Three Bool]
forall (f :: * -> *) step (g :: * -> *) a.
(Walkable f step, Functor g) =>
g (f a) -> step -> g (f a)
allStep [Three Bool]
thr Bool
x)) Int
n ((Int, Product') -> (Int, Product')
_pushVal'' ((Int, Product') -> (Int, Product'))
-> Maybe (Int, Product') -> Maybe (Int, Product')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Bool] -> Bool)
-> Int -> [Bool] -> [Three Bool] -> Maybe (Int, Product')
_minimizeItem' [Bool] -> Bool
mg Int
n [Bool]
xs [Three Bool]
stepdc)
  | Bool
otherwise = (Int, Product') -> (Int, Product')
pshVal ((Int, Product') -> (Int, Product'))
-> Maybe (Int, Product') -> Maybe (Int, Product')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Bool] -> Bool)
-> Int -> [Bool] -> [Three Bool] -> Maybe (Int, Product')
_minimizeItem' [Bool] -> Bool
mg (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [Bool]
xs [Three Bool]
stepx
  where stepdc :: [Three Bool]
stepdc = [Three Bool] -> ThreeValue -> [Three Bool]
forall (f :: * -> *) step (g :: * -> *) a.
(NonDeterministicWalkable f step, Foldable g) =>
g (f a) -> step -> [f a]
allNstep [Three Bool]
thr ThreeValue
DontCare
        stepx :: [Three Bool]
stepx = [Three Bool] -> Bool -> [Three Bool]
forall (f :: * -> *) step (g :: * -> *) a.
(Walkable f step, Functor g) =>
g (f a) -> step -> g (f a)
allStep [Three Bool]
thr Bool
x
        pshVal :: (Int, Product') -> (Int, Product')
pshVal = ThreeValue -> (Int, Product') -> (Int, Product')
_pushVal' (Bool -> ThreeValue
fromBool Bool
x)

minimizeProduct' :: Int -> [Bool] -> [Three Bool] -> Maybe WeightedProduct
minimizeProduct' :: Int -> [Bool] -> [Three Bool] -> Maybe (Int, Product')
minimizeProduct' = ([Bool] -> Bool)
-> Int -> [Bool] -> [Three Bool] -> Maybe (Int, Product')
_minimizeItem' [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and

minimizeSum' :: Int -> [Bool] -> [Three Bool] -> Maybe WeightedSum
minimizeSum' :: Int -> [Bool] -> [Three Bool] -> Maybe (Int, Product')
minimizeSum' = ([Bool] -> Bool)
-> Int -> [Bool] -> [Three Bool] -> Maybe (Int, Product')
_minimizeItem' (Bool -> Bool
not (Bool -> Bool) -> ([Bool] -> Bool) -> [Bool] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or)

minimizeProduct :: Int -> Product' -> Three Bool -> Product'
minimizeProduct :: Int -> Product' -> Three Bool -> Product'
minimizeProduct Int
wght Product'
prd Three Bool
thr = Product'
-> ((Int, Product') -> Product')
-> Maybe (Int, Product')
-> Product'
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Product'
prd (Int, Product') -> Product'
forall a b. (a, b) -> b
snd (Int -> [Bool] -> [Three Bool] -> Maybe (Int, Product')
minimizeProduct' Int
wght ((ThreeValue -> Bool) -> Product' -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map ThreeValue -> Bool
toUpper Product'
prd) [Three Bool
thr])

minimizeSum :: Int -> Sum' -> Three Bool -> Sum'
minimizeSum :: Int -> Product' -> Three Bool -> Product'
minimizeSum Int
wght Product'
prd Three Bool
thr = Product'
-> ((Int, Product') -> Product')
-> Maybe (Int, Product')
-> Product'
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Product'
prd (Int, Product') -> Product'
forall a b. (a, b) -> b
snd (Int -> [Bool] -> [Three Bool] -> Maybe (Int, Product')
minimizeSum' Int
wght ((ThreeValue -> Bool) -> Product' -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map ThreeValue -> Bool
toUpper Product'
prd) [Three Bool
thr])

-- | Create a 'SumOfProducts' object based on the given 'Three' of 'ThreeValue's. This function acts
-- as an alias for the 'synthesisSOP' function.
synthesis
  :: Three ThreeValue  -- ^ The 'Three' of 'ThreeValue's for which we want to make a logical formula.
  -> SumOfProducts  -- ^ The sum of products that work with the function defined in the 'Three'.
synthesis :: Three ThreeValue -> SumOfProducts
synthesis = [Product] -> SumOfProducts
SumOfProducts ([Product] -> SumOfProducts)
-> (Three ThreeValue -> [Product])
-> Three ThreeValue
-> SumOfProducts
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Product' -> Product) -> [Product'] -> [Product]
forall a b. (a -> b) -> [a] -> [b]
map Product' -> Product
Product ([Product'] -> [Product])
-> (Three ThreeValue -> [Product'])
-> Three ThreeValue
-> [Product]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Three ThreeValue -> [Product']
synthesis'

-- | Create a 'SumOfProducts' object based on the given 'Three' of 'ThreeValue's.
synthesisSOP
  :: Three ThreeValue  -- ^ The 'Three' of 'ThreeValue's for which we want to make a logical formula.
  -> SumOfProducts  -- ^ The sum of products that work with the function defined in the 'Three'.
synthesisSOP :: Three ThreeValue -> SumOfProducts
synthesisSOP = [Product] -> SumOfProducts
SumOfProducts ([Product] -> SumOfProducts)
-> (Three ThreeValue -> [Product])
-> Three ThreeValue
-> SumOfProducts
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Product' -> Product) -> [Product'] -> [Product]
forall a b. (a -> b) -> [a] -> [b]
map Product' -> Product
Product ([Product'] -> [Product])
-> (Three ThreeValue -> [Product'])
-> Three ThreeValue
-> [Product]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Three ThreeValue -> [Product']
synthesisSOP'

-- | Create a 'ProductOfSums' object based on the given 'Three' of 'ThreeValue's.
synthesisPOS
  :: Three ThreeValue  -- ^ The 'Three' of 'ThreeValue's for which we want to make a logical formula.
  -> ProductOfSums  -- ^ The product of sums that work with the function defined in the 'Three'.
synthesisPOS :: Three ThreeValue -> ProductOfSums
synthesisPOS = [Sum] -> ProductOfSums
ProductOfSums ([Sum] -> ProductOfSums)
-> (Three ThreeValue -> [Sum]) -> Three ThreeValue -> ProductOfSums
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Product' -> Sum) -> [Product'] -> [Sum]
forall a b. (a -> b) -> [a] -> [b]
map Product' -> Sum
Sum ([Product'] -> [Sum])
-> (Three ThreeValue -> [Product']) -> Three ThreeValue -> [Sum]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Three ThreeValue -> [Product']
synthesisPOS'

-- | Create a sum-of-products for the given function of 'ThreeValue'. This function is an alias of
-- the 'synthesisSOP' function.
synthesis'
  :: Three ThreeValue  -- ^ The 'Three' of 'ThreeValue's for which we want to make a logical formula.
  -> SumOfProducts'  -- ^ The sum of products that work with the function defined in the 'Three'.
synthesis' :: Three ThreeValue -> [Product']
synthesis' = Three ThreeValue -> [Product']
synthesisSOP'

-- | Create a sum-of-products for the given function of 'ThreeValue'.
synthesisSOP'
  :: Three ThreeValue  -- ^ The 'Three' of 'ThreeValue's for which we want to make a logical formula.
  -> SumOfProducts'  -- ^ The sum of products that work with the function defined in the 'Three'.
synthesisSOP' :: Three ThreeValue -> [Product']
synthesisSOP' = (Three ThreeValue -> Three Bool)
-> (Int -> Three Bool -> Three ThreeValue -> Maybe (Int, Product'))
-> (Int -> Product' -> Three Bool -> Product')
-> (Product' -> Product')
-> Three ThreeValue
-> [Product']
_genericSynthesis' Three ThreeValue -> Three Bool
upperbound Int -> Three Bool -> Three ThreeValue -> Maybe (Int, Product')
extractProduct Int -> Product' -> Three Bool -> Product'
minimizeProduct Product' -> Product'
forall a. a -> a
id

-- | Create a sum-of-products for the given function of 'ThreeValue'.
synthesisPOS'
  :: Three ThreeValue  -- ^ The 'Three' of 'ThreeValue's for which we want to make a logical formula.
  -> ProductOfSums'  -- ^ The sum of products that work with the function defined in the 'Three'.
synthesisPOS' :: Three ThreeValue -> [Product']
synthesisPOS' = (Three ThreeValue -> Three Bool)
-> (Int -> Three Bool -> Three ThreeValue -> Maybe (Int, Product'))
-> (Int -> Product' -> Three Bool -> Product')
-> (Product' -> Product')
-> Three ThreeValue
-> [Product']
_genericSynthesis' Three ThreeValue -> Three Bool
lowerbound Int -> Three Bool -> Three ThreeValue -> Maybe (Int, Product')
extractSum Int -> Product' -> Three Bool -> Product'
minimizeSum Product' -> Product'
forall a. Opposite a => a -> a
opposite

_genericSynthesis'
  :: (Three ThreeValue -> Three Bool)
  -> (Int -> Three Bool -> Three ThreeValue -> Maybe WeightedItem)
  -> (Int -> Item' -> Three Bool -> Item')
  -> (Item' -> Item')
  -> Three ThreeValue
  -> ProductOfSums'
_genericSynthesis' :: (Three ThreeValue -> Three Bool)
-> (Int -> Three Bool -> Three ThreeValue -> Maybe (Int, Product'))
-> (Int -> Product' -> Three Bool -> Product')
-> (Product' -> Product')
-> Three ThreeValue
-> [Product']
_genericSynthesis' Three ThreeValue -> Three Bool
toBound Int -> Three Bool -> Three ThreeValue -> Maybe (Int, Product')
_extractItem Int -> Product' -> Three Bool -> Product'
minimize Product' -> Product'
post Three ThreeValue
th = Three ThreeValue -> [Product']
_synthesis Three ThreeValue
_simp
  where _bound :: Three Bool
_bound = Three ThreeValue -> Three Bool
toBound Three ThreeValue
_simp
        _n :: Int
_n = Three ThreeValue -> Int
forall a. Three a -> Int
depth Three ThreeValue
_simp
        _simp :: Three ThreeValue
_simp = Three ThreeValue -> Three ThreeValue
forall a. Simplify a => a -> a
simplify Three ThreeValue
th
        _takeItem :: Three ThreeValue -> Maybe (Int, Product')
_takeItem = Int -> Three Bool -> Three ThreeValue -> Maybe (Int, Product')
_extractItem Int
_n Three Bool
_bound
        _synthesis :: Three ThreeValue -> [Product']
_synthesis Three ThreeValue
thr
          | Just (~(Int
k, Product'
j)) <- Three ThreeValue -> Maybe (Int, Product')
_takeItem Three ThreeValue
thr = let j' :: Product'
j' = Int -> Product' -> Three Bool -> Product'
minimize Int
k Product'
j Three Bool
_bound in Product' -> Product'
post Product'
j' Product' -> [Product'] -> [Product']
forall a. a -> [a] -> [a]
: Three ThreeValue -> [Product']
_synthesis (Product' -> Three ThreeValue -> Three ThreeValue
wipeout Product'
j' Three ThreeValue
thr)
          | Bool
otherwise = []