-- SPDX-License-Identifier: MPL-2.0

{- | Finite-width bits, relations and propositional logic. Widths are explicit;
zero has both leading- and trailing-zero count equal to its width. Boolean
matrices use the OR/AND semiring. Logic enumerations are bounded to 12 inputs.
-}
module HMath.Discrete (
    MultiSet,
    multiset,
    multiplicity,
    multisetEntries,
    multisetInsert,
    multisetDelete,
    multisetUnion,
    multisetIntersection,
    multisetDifference,
    BitSet,
    bitSet,
    bitWidth,
    bitValue,
    bitMember,
    bitInsert,
    bitDelete,
    bitUnion,
    bitIntersection,
    bitDifference,
    resizeBitSet,
    populationCount,
    leadingZeros,
    trailingZeros,
    rotateBits,
    reverseBits,
    grayEncode,
    grayDecode,
    hammingDistance,
    setUnion,
    setIntersection,
    setDifference,
    symmetricDifference,
    transitiveClosure,
    equivalenceClosure,
    isEquivalence,
    booleanMultiply,
    Prop (..),
    evaluateProp,
    truthTable,
    Implicant (..),
    quineMcCluskey,
    implicantCovers,
) where

import Data.Bits hiding (And, Iff, Xor)
import Data.List (nub, sort)
import qualified Data.Map.Strict as M
import qualified Data.Set as S
import HMath.Error (MathError (..))

{- | Finite multiset with exact nonnegative multiplicities. Union adds
multiplicities; intersection takes minima and difference truncates at zero.
-}
newtype MultiSet a = MultiSet (M.Map a Integer) deriving (MultiSet a -> MultiSet a -> Bool
(MultiSet a -> MultiSet a -> Bool)
-> (MultiSet a -> MultiSet a -> Bool) -> Eq (MultiSet a)
forall a. Eq a => MultiSet a -> MultiSet a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => MultiSet a -> MultiSet a -> Bool
== :: MultiSet a -> MultiSet a -> Bool
$c/= :: forall a. Eq a => MultiSet a -> MultiSet a -> Bool
/= :: MultiSet a -> MultiSet a -> Bool
Eq, Int -> MultiSet a -> ShowS
[MultiSet a] -> ShowS
MultiSet a -> String
(Int -> MultiSet a -> ShowS)
-> (MultiSet a -> String)
-> ([MultiSet a] -> ShowS)
-> Show (MultiSet a)
forall a. Show a => Int -> MultiSet a -> ShowS
forall a. Show a => [MultiSet a] -> ShowS
forall a. Show a => MultiSet a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> MultiSet a -> ShowS
showsPrec :: Int -> MultiSet a -> ShowS
$cshow :: forall a. Show a => MultiSet a -> String
show :: MultiSet a -> String
$cshowList :: forall a. Show a => [MultiSet a] -> ShowS
showList :: [MultiSet a] -> ShowS
Show)

{- | Construct a finite multiset by counting equal ordered values with exact nonnegative
Integer multiplicities.
-}
multiset :: (Ord a) => [a] -> MultiSet a
multiset :: forall a. Ord a => [a] -> MultiSet a
multiset [a]
xs = Map a Integer -> MultiSet a
forall a. Map a Integer -> MultiSet a
MultiSet ((Integer -> Integer -> Integer) -> [(a, Integer)] -> Map a Integer
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) [(a
x, Integer
1) | a
x <- [a]
xs])

-- | Given value then multiset, return its Integer frequency, or zero when absent.
multiplicity :: (Ord a) => a -> MultiSet a -> Integer
multiplicity :: forall a. Ord a => a -> MultiSet a -> Integer
multiplicity a
x (MultiSet Map a Integer
m) = Integer -> a -> Map a Integer -> Integer
forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault Integer
0 a
x Map a Integer
m

-- | Return (value,positive multiplicity) pairs in ascending value order.
multisetEntries :: MultiSet a -> [(a, Integer)]
multisetEntries :: forall a. MultiSet a -> [(a, Integer)]
multisetEntries (MultiSet Map a Integer
m) = Map a Integer -> [(a, Integer)]
forall k a. Map k a -> [(k, a)]
M.toAscList Map a Integer
m

-- | Given value then multiset, increment its multiplicity by one and return a new multiset.
multisetInsert :: (Ord a) => a -> MultiSet a -> MultiSet a
multisetInsert :: forall a. Ord a => a -> MultiSet a -> MultiSet a
multisetInsert a
x (MultiSet Map a Integer
m) = Map a Integer -> MultiSet a
forall a. Map a Integer -> MultiSet a
MultiSet ((Integer -> Integer -> Integer)
-> a -> Integer -> Map a Integer -> Map a Integer
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) a
x Integer
1 Map a Integer
m)

{- | Given value then multiset, remove one occurrence, deleting its entry at zero. Absent
values are a no-op.
-}
multisetDelete :: (Ord a) => a -> MultiSet a -> MultiSet a
multisetDelete :: forall a. Ord a => a -> MultiSet a -> MultiSet a
multisetDelete a
x (MultiSet Map a Integer
m) = Map a Integer -> MultiSet a
forall a. Map a Integer -> MultiSet a
MultiSet ((Integer -> Maybe Integer) -> a -> Map a Integer -> Map a Integer
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
M.update (\Integer
n -> if Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
1 then Maybe Integer
forall a. Maybe a
Nothing else Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)) a
x Map a Integer
m)

multisetUnion
    , multisetIntersection
    , multisetDifference ::
        (Ord a) => MultiSet a -> MultiSet a -> MultiSet a

{- | Add multiplicities of two multisets, retaining all distinct values. This is multiset
sum rather than maximum-multiplicity union.
-}
multisetUnion :: forall a. Ord a => MultiSet a -> MultiSet a -> MultiSet a
multisetUnion (MultiSet Map a Integer
a) (MultiSet Map a Integer
b) = Map a Integer -> MultiSet a
forall a. Map a Integer -> MultiSet a
MultiSet ((Integer -> Integer -> Integer)
-> Map a Integer -> Map a Integer -> Map a Integer
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) Map a Integer
a Map a Integer
b)

-- | Return shared values with minimum of the two multiplicities.
multisetIntersection :: forall a. Ord a => MultiSet a -> MultiSet a -> MultiSet a
multisetIntersection (MultiSet Map a Integer
a) (MultiSet Map a Integer
b) = Map a Integer -> MultiSet a
forall a. Map a Integer -> MultiSet a
MultiSet ((Integer -> Integer -> Integer)
-> Map a Integer -> Map a Integer -> Map a Integer
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Map a Integer
a Map a Integer
b)

-- | Subtract right multiplicities from left, truncating at zero and removing empty entries.
multisetDifference :: forall a. Ord a => MultiSet a -> MultiSet a -> MultiSet a
multisetDifference (MultiSet Map a Integer
a) (MultiSet Map a Integer
b) = Map a Integer -> MultiSet a
forall a. Map a Integer -> MultiSet a
MultiSet ((Integer -> Bool) -> Map a Integer -> Map a Integer
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0) ((a -> Integer -> Integer) -> Map a Integer -> Map a Integer
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey (\a
x Integer
n -> Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer -> a -> Map a Integer -> Integer
forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault Integer
0 a
x Map a Integer
b) Map a Integer
a))

-- | Opaque arbitrary-size dynamic bitset; bits outside its width are zero.
data BitSet = BitSet Int Integer deriving (BitSet -> BitSet -> Bool
(BitSet -> BitSet -> Bool)
-> (BitSet -> BitSet -> Bool) -> Eq BitSet
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BitSet -> BitSet -> Bool
== :: BitSet -> BitSet -> Bool
$c/= :: BitSet -> BitSet -> Bool
/= :: BitSet -> BitSet -> Bool
Eq, Int -> BitSet -> ShowS
[BitSet] -> ShowS
BitSet -> String
(Int -> BitSet -> ShowS)
-> (BitSet -> String) -> ([BitSet] -> ShowS) -> Show BitSet
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BitSet -> ShowS
showsPrec :: Int -> BitSet -> ShowS
$cshow :: BitSet -> String
show :: BitSet -> String
$cshowList :: [BitSet] -> ShowS
showList :: [BitSet] -> ShowS
Show)

{- | Given width in [0,1048576] then nonnegative Integer less than 2^width, construct an
opaque bitset. Invalid width/value fails; bit zero is least significant.
-}
bitSet :: Int -> Integer -> Either MathError BitSet
bitSet :: Int -> Integer -> Either MathError BitSet
bitSet Int
w Integer
v
    | Int
w Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
w Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1048576 Bool -> Bool -> Bool
|| Integer
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 Bool -> Bool -> Bool
|| Integer
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
w =
        MathError -> Either MathError BitSet
forall a b. a -> Either a b
Left (String -> MathError
InvalidArgument String
"bitset width/value out of range")
    | Bool
otherwise = BitSet -> Either MathError BitSet
forall a b. b -> Either a b
Right (Int -> Integer -> BitSet
BitSet Int
w Integer
v)

-- | Return declared number of bits, including leading zeros.
bitWidth :: BitSet -> Int
bitWidth :: BitSet -> Int
bitWidth (BitSet Int
w Integer
_) = Int
w

-- | Return unsigned Integer value of all bits within the declared width.
bitValue :: BitSet -> Integer
bitValue :: BitSet -> Integer
bitValue (BitSet Int
_ Integer
v) = Integer
v

bitIndex :: BitSet -> Int -> Either MathError ()
bitIndex :: BitSet -> Int -> Either MathError ()
bitIndex (BitSet Int
w Integer
_) Int
i
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
w = MathError -> Either MathError ()
forall a b. a -> Either a b
Left (String -> MathError
InvalidArgument String
"bit index out of bounds")
    | Bool
otherwise = () -> Either MathError ()
forall a b. b -> Either a b
Right ()

{- | Given bitset then zero-based bit index, return membership. Out-of-width or negative
indices return Left InvalidArgument.
-}
bitMember :: BitSet -> Int -> Either MathError Bool
bitMember :: BitSet -> Int -> Either MathError Bool
bitMember BitSet
b Int
i = do BitSet -> Int -> Either MathError ()
bitIndex BitSet
b Int
i; Bool -> Either MathError Bool
forall a. a -> Either MathError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit (BitSet -> Integer
bitValue BitSet
b) Int
i)

{- | Given bitset then valid bit index, return a new bitset with that bit set. Invalid index
fails.
-}
bitInsert :: BitSet -> Int -> Either MathError BitSet
bitInsert :: BitSet -> Int -> Either MathError BitSet
bitInsert b :: BitSet
b@(BitSet Int
w Integer
v) Int
i = do BitSet -> Int -> Either MathError ()
bitIndex BitSet
b Int
i; BitSet -> Either MathError BitSet
forall a. a -> Either MathError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Integer -> BitSet
BitSet Int
w (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
setBit Integer
v Int
i))

{- | Given bitset then valid bit index, return a new bitset with that bit cleared. Invalid
index fails.
-}
bitDelete :: BitSet -> Int -> Either MathError BitSet
bitDelete :: BitSet -> Int -> Either MathError BitSet
bitDelete b :: BitSet
b@(BitSet Int
w Integer
v) Int
i = do BitSet -> Int -> Either MathError ()
bitIndex BitSet
b Int
i; BitSet -> Either MathError BitSet
forall a. a -> Either MathError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Integer -> BitSet
BitSet Int
w (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
clearBit Integer
v Int
i))

bitCombine :: (Integer -> Integer -> Integer) -> BitSet -> BitSet -> Either MathError BitSet
bitCombine :: (Integer -> Integer -> Integer)
-> BitSet -> BitSet -> Either MathError BitSet
bitCombine Integer -> Integer -> Integer
f (BitSet Int
w Integer
a) (BitSet Int
v Integer
b)
    | Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
v = MathError -> Either MathError BitSet
forall a b. a -> Either a b
Left (String -> MathError
InvalidArgument String
"bit widths differ")
    | Bool
otherwise = BitSet -> Either MathError BitSet
forall a b. b -> Either a b
Right (Int -> Integer -> BitSet
BitSet Int
w (Integer -> Integer -> Integer
f Integer
a Integer
b Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. (Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)))
bitUnion, bitIntersection, bitDifference :: BitSet -> BitSet -> Either MathError BitSet

{- | Return bitwise OR of equal-width bitsets. Different widths fail; no implicit resize
occurs.
-}
bitUnion :: BitSet -> BitSet -> Either MathError BitSet
bitUnion = (Integer -> Integer -> Integer)
-> BitSet -> BitSet -> Either MathError BitSet
bitCombine Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
(.|.)

-- | Return bitwise AND of equal-width bitsets; mismatched widths fail.
bitIntersection :: BitSet -> BitSet -> Either MathError BitSet
bitIntersection = (Integer -> Integer -> Integer)
-> BitSet -> BitSet -> Either MathError BitSet
bitCombine Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
(.&.)

-- | Return left bits with right bits cleared, requiring equal widths. Width mismatch fails.
bitDifference :: BitSet -> BitSet -> Either MathError BitSet
bitDifference = (Integer -> Integer -> Integer)
-> BitSet -> BitSet -> Either MathError BitSet
bitCombine (\Integer
a Integer
b -> Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
b)

-- | Shrinking explicitly discards high bits.
resizeBitSet :: Int -> BitSet -> Either MathError BitSet
resizeBitSet :: Int -> BitSet -> Either MathError BitSet
resizeBitSet Int
w (BitSet Int
_ Integer
v) = Int -> Integer -> Either MathError BitSet
bitSet Int
w (Integer
v Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. (Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
0 Int
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1))

-- | Count set bits within declared width, returning Int.
populationCount :: BitSet -> Int
populationCount :: BitSet -> Int
populationCount = Integer -> Int
forall a. Bits a => a -> Int
popCount (Integer -> Int) -> (BitSet -> Integer) -> BitSet -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitSet -> Integer
bitValue

-- | Count high-end zero bits within declared width. All-zero bitset returns its full width.
leadingZeros :: BitSet -> Int
leadingZeros :: BitSet -> Int
leadingZeros (BitSet Int
w Integer
v) = Int
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Integer -> Int
forall {t} {t}. (Num t, Num t, Bits t) => t -> t
go Integer
v
  where
    go :: t -> t
go t
0 = t
0; go t
x = t
1 t -> t -> t
forall a. Num a => a -> a -> a
+ t -> t
go (t -> Int -> t
forall a. Bits a => a -> Int -> a
shiftR t
x Int
1)

-- | Count low-end zero bits; an all-zero bitset returns its declared width.
trailingZeros :: BitSet -> Int
trailingZeros :: BitSet -> Int
trailingZeros (BitSet Int
w Integer
v) = if Integer
v Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Int
w else Integer -> Int
forall {t} {t}. (Integral t, Bits t, Num t) => t -> t
go Integer
v
  where
    go :: t -> t
go t
x | t -> Bool
forall a. Integral a => a -> Bool
odd t
x = t
0 | Bool
otherwise = t
1 t -> t -> t
forall a. Num a => a -> a -> a
+ t -> t
go (t -> Int -> t
forall a. Bits a => a -> Int -> a
shiftR t
x Int
1)

{- | Given signed rotation count then bitset, rotate left modulo width (negative counts
rotate right). Width-zero input is unchanged.
-}
rotateBits :: Int -> BitSet -> BitSet
rotateBits :: Int -> BitSet -> BitSet
rotateBits Int
_ b :: BitSet
b@(BitSet Int
0 Integer
_) = BitSet
b
rotateBits Int
k (BitSet Int
w Integer
v) = let j :: Int
j = Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
w in Int -> Integer -> BitSet
BitSet Int
w ((Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
v Int
j Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR Integer
v (Int
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
j)) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. (Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1))

{- | Reverse exactly the declared width of bits, preserving width and leading/trailing zero
positions.
-}
reverseBits :: BitSet -> BitSet
reverseBits :: BitSet -> BitSet
reverseBits (BitSet Int
w Integer
v) = Int -> Integer -> BitSet
BitSet Int
w ([Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [if Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
v Int
i then Int -> Integer
forall a. Bits a => Int -> a
bit (Int
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) else Integer
0 | Int
i <- [Int
0 .. Int
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]])

-- | Return width-preserving reflected Gray code v xor (v shifted right one).
grayEncode :: BitSet -> BitSet
grayEncode :: BitSet -> BitSet
grayEncode (BitSet Int
w Integer
v) = Int -> Integer -> BitSet
BitSet Int
w (Integer
v Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR Integer
v Int
1)

-- | Decode reflected Gray bits to the corresponding width-preserving binary value.
grayDecode :: BitSet -> BitSet
grayDecode :: BitSet -> BitSet
grayDecode (BitSet Int
w Integer
v) = Int -> Integer -> BitSet
BitSet Int
w (Integer -> Integer -> Integer
forall {t}. (Num t, Bits t) => t -> t -> t
go Integer
v Integer
0)
  where
    go :: t -> t -> t
go t
0 t
r = t
r; go t
x t
r = t -> t -> t
go (t -> Int -> t
forall a. Bits a => a -> Int -> a
shiftR t
x Int
1) (t
r t -> t -> t
forall a. Bits a => a -> a -> a
`xor` t
x)

{- | Count differing bit positions between equal-width bitsets. Different widths return Left
InvalidArgument.
-}
hammingDistance :: BitSet -> BitSet -> Either MathError Int
hammingDistance :: BitSet -> BitSet -> Either MathError Int
hammingDistance BitSet
a BitSet
b = BitSet -> Int
populationCount (BitSet -> Int) -> Either MathError BitSet -> Either MathError Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer -> Integer -> Integer)
-> BitSet -> BitSet -> Either MathError BitSet
bitCombine Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
xor BitSet
a BitSet
b

setUnion, setIntersection, setDifference, symmetricDifference :: (Ord a) => [a] -> [a] -> [a]

{- | Treat lists as finite sets and return their sorted unique union; input order and
multiplicity are discarded.
-}
setUnion :: forall a. Ord a => [a] -> [a] -> [a]
setUnion [a]
a [a]
b = Set a -> [a]
forall a. Set a -> [a]
S.toAscList (Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
S.union ([a] -> Set a
forall a. Ord a => [a] -> Set a
S.fromList [a]
a) ([a] -> Set a
forall a. Ord a => [a] -> Set a
S.fromList [a]
b))

-- | Return sorted unique values present in both input lists.
setIntersection :: forall a. Ord a => [a] -> [a] -> [a]
setIntersection [a]
a [a]
b = Set a -> [a]
forall a. Set a -> [a]
S.toAscList (Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
S.intersection ([a] -> Set a
forall a. Ord a => [a] -> Set a
S.fromList [a]
a) ([a] -> Set a
forall a. Ord a => [a] -> Set a
S.fromList [a]
b))

-- | Return sorted unique left values absent from the right list.
setDifference :: forall a. Ord a => [a] -> [a] -> [a]
setDifference [a]
a [a]
b = Set a -> [a]
forall a. Set a -> [a]
S.toAscList (Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
S.difference ([a] -> Set a
forall a. Ord a => [a] -> Set a
S.fromList [a]
a) ([a] -> Set a
forall a. Ord a => [a] -> Set a
S.fromList [a]
b))

-- | Return sorted unique values present in exactly one input list.
symmetricDifference :: forall a. Ord a => [a] -> [a] -> [a]
symmetricDifference [a]
a [a]
b = [a] -> [a] -> [a]
forall a. Ord a => [a] -> [a] -> [a]
setUnion ([a] -> [a] -> [a]
forall a. Ord a => [a] -> [a] -> [a]
setDifference [a]
a [a]
b) ([a] -> [a] -> [a]
forall a. Ord a => [a] -> [a] -> [a]
setDifference [a]
b [a]
a)

square :: [[a]] -> Either MathError Int
square :: forall a. [[a]] -> Either MathError Int
square [[a]]
a
    | [[a]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[a]]
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
512 Bool -> Bool -> Bool
|| ([a] -> Bool) -> [[a]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [[a]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[a]]
a) (Int -> Bool) -> ([a] -> Int) -> [a] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length) [[a]]
a =
        MathError -> Either MathError Int
forall a b. a -> Either a b
Left (String -> MathError
InvalidArgument String
"expected square matrix of order at most 512")
    | Bool
otherwise = Int -> Either MathError Int
forall a b. b -> Either a b
Right ([[a]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[a]]
a)

{- | Warshall closure. Paths must have positive length; use
'equivalenceClosure' when a reflexive closure is wanted.
-}
transitiveClosure :: [[Bool]] -> Either MathError [[Bool]]
transitiveClosure :: [[Bool]] -> Either MathError [[Bool]]
transitiveClosure [[Bool]]
a = do
    n <- [[Bool]] -> Either MathError Int
forall a. [[a]] -> Either MathError Int
square [[Bool]]
a
    pure
        ( foldl
            (\[[Bool]]
m Int
k -> [[[[Bool]]
m [[Bool]] -> Int -> [Bool]
forall a. HasCallStack => [a] -> Int -> a
!! Int
i [Bool] -> Int -> Bool
forall a. HasCallStack => [a] -> Int -> a
!! Int
j Bool -> Bool -> Bool
|| ([[Bool]]
m [[Bool]] -> Int -> [Bool]
forall a. HasCallStack => [a] -> Int -> a
!! Int
i [Bool] -> Int -> Bool
forall a. HasCallStack => [a] -> Int -> a
!! Int
k Bool -> Bool -> Bool
&& [[Bool]]
m [[Bool]] -> Int -> [Bool]
forall a. HasCallStack => [a] -> Int -> a
!! Int
k [Bool] -> Int -> Bool
forall a. HasCallStack => [a] -> Int -> a
!! Int
j) | Int
j <- [Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]] | Int
i <- [Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]])
            a
            [0 .. n - 1]
        )

{- | Given square Bool relation matrix, add reflexivity and symmetry then compute transitive
closure. Reject nonsquare or oversized (>512) relations.
-}
equivalenceClosure :: [[Bool]] -> Either MathError [[Bool]]
equivalenceClosure :: [[Bool]] -> Either MathError [[Bool]]
equivalenceClosure [[Bool]]
a = do
    n <- [[Bool]] -> Either MathError Int
forall a. [[a]] -> Either MathError Int
square [[Bool]]
a
    transitiveClosure [[i == j || a !! i !! j || a !! j !! i | j <- [0 .. n - 1]] | i <- [0 .. n - 1]]

{- | Return whether a bounded square Bool relation is already reflexive, symmetric and
transitive. Invalid matrix shape/size fails.
-}
isEquivalence :: [[Bool]] -> Either MathError Bool
isEquivalence :: [[Bool]] -> Either MathError Bool
isEquivalence [[Bool]]
a = ([[Bool]] -> [[Bool]] -> Bool
forall a. Eq a => a -> a -> Bool
== [[Bool]]
a) ([[Bool]] -> Bool)
-> Either MathError [[Bool]] -> Either MathError Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Bool]] -> Either MathError [[Bool]]
equivalenceClosure [[Bool]]
a

{- | Multiply compatible square Bool relation matrices over OR/AND, representing relational
composition. Invalid dimensions or size bounds fail.
-}
booleanMultiply :: [[Bool]] -> [[Bool]] -> Either MathError [[Bool]]
booleanMultiply :: [[Bool]] -> [[Bool]] -> Either MathError [[Bool]]
booleanMultiply [[Bool]]
a [[Bool]]
b = do
    n <- [[Bool]] -> Either MathError Int
forall a. [[a]] -> Either MathError Int
square [[Bool]]
a
    m <- square b
    if n /= m
        then Left (InvalidArgument "Boolean matrix dimensions differ")
        else
            pure [[or [a !! i !! k && b !! k !! j | k <- [0 .. n - 1]] | j <- [0 .. n - 1]] | i <- [0 .. n - 1]]

{- | Boolean proposition tree. Literal and Variable leaves combine through
Not,And,Or,Xor,Implies,Iff; Variable indices address the assignment list passed to
evaluateProp.
-}
data Prop
    = Literal Bool
    | Variable Int
    | Not Prop
    | And Prop Prop
    | Or Prop Prop
    | Xor Prop Prop
    | Implies Prop Prop
    | Iff Prop Prop
    deriving (Prop -> Prop -> Bool
(Prop -> Prop -> Bool) -> (Prop -> Prop -> Bool) -> Eq Prop
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Prop -> Prop -> Bool
== :: Prop -> Prop -> Bool
$c/= :: Prop -> Prop -> Bool
/= :: Prop -> Prop -> Bool
Eq, Int -> Prop -> ShowS
[Prop] -> ShowS
Prop -> String
(Int -> Prop -> ShowS)
-> (Prop -> String) -> ([Prop] -> ShowS) -> Show Prop
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Prop -> ShowS
showsPrec :: Int -> Prop -> ShowS
$cshow :: Prop -> String
show :: Prop -> String
$cshowList :: [Prop] -> ShowS
showList :: [Prop] -> ShowS
Show)

{- | Given variable Bool assignment list then proposition, evaluate
literals/variables/connectives. Invalid variable index or excessive expression depth
returns Left MathError.
-}
evaluateProp :: [Bool] -> Prop -> Either MathError Bool
evaluateProp :: [Bool] -> Prop -> Either MathError Bool
evaluateProp [Bool]
values = Int -> Prop -> Either MathError Bool
forall {t}. (Ord t, Num t) => t -> Prop -> Either MathError Bool
go (Int
0 :: Int)
  where
    go :: t -> Prop -> Either MathError Bool
go t
d Prop
_ | t
d t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
1024 = MathError -> Either MathError Bool
forall a b. a -> Either a b
Left (String -> MathError
InvalidArgument String
"proposition nesting exceeds 1024")
    go t
_ (Literal Bool
b) = Bool -> Either MathError Bool
forall a b. b -> Either a b
Right Bool
b
    go t
_ (Variable Int
i)
        | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [Bool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bool]
values = MathError -> Either MathError Bool
forall a b. a -> Either a b
Left (String -> MathError
InvalidArgument String
"unbound proposition variable")
        | Bool
otherwise = Bool -> Either MathError Bool
forall a b. b -> Either a b
Right ([Bool]
values [Bool] -> Int -> Bool
forall a. HasCallStack => [a] -> Int -> a
!! Int
i)
    go t
d (Not Prop
p) = Bool -> Bool
not (Bool -> Bool) -> Either MathError Bool -> Either MathError Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> Prop -> Either MathError Bool
go (t
d t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) Prop
p
    go t
d (And Prop
p Prop
q) = t
-> (Bool -> Bool -> Bool) -> Prop -> Prop -> Either MathError Bool
binary t
d Bool -> Bool -> Bool
(&&) Prop
p Prop
q
    go t
d (Or Prop
p Prop
q) = t
-> (Bool -> Bool -> Bool) -> Prop -> Prop -> Either MathError Bool
binary t
d Bool -> Bool -> Bool
(||) Prop
p Prop
q
    go t
d (Xor Prop
p Prop
q) = t
-> (Bool -> Bool -> Bool) -> Prop -> Prop -> Either MathError Bool
binary t
d Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(/=) Prop
p Prop
q
    go t
d (Implies Prop
p Prop
q) = t
-> (Bool -> Bool -> Bool) -> Prop -> Prop -> Either MathError Bool
binary t
d (\Bool
a Bool
b -> Bool -> Bool
not Bool
a Bool -> Bool -> Bool
|| Bool
b) Prop
p Prop
q
    go t
d (Iff Prop
p Prop
q) = t
-> (Bool -> Bool -> Bool) -> Prop -> Prop -> Either MathError Bool
binary t
d Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==) Prop
p Prop
q
    binary :: t
-> (Bool -> Bool -> Bool) -> Prop -> Prop -> Either MathError Bool
binary t
d Bool -> Bool -> Bool
f Prop
p Prop
q = Bool -> Bool -> Bool
f (Bool -> Bool -> Bool)
-> Either MathError Bool -> Either MathError (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> Prop -> Either MathError Bool
go (t
d t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) Prop
p Either MathError (Bool -> Bool)
-> Either MathError Bool -> Either MathError Bool
forall a b.
Either MathError (a -> b)
-> Either MathError a -> Either MathError b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Prop -> Either MathError Bool
go (t
d t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) Prop
q

-- | Assignments in binary order, variable zero the least-significant bit.
truthTable :: Int -> Prop -> Either MathError [([Bool], Bool)]
truthTable :: Int -> Prop -> Either MathError [([Bool], Bool)]
truthTable Int
n Prop
p
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
12 = MathError -> Either MathError [([Bool], Bool)]
forall a b. a -> Either a b
Left (String -> MathError
InvalidArgument String
"truth table input count exceeds 12")
    | Bool
otherwise =
        (Int -> Either MathError ([Bool], Bool))
-> [Int] -> Either MathError [([Bool], Bool)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM
            (\Int
i -> let a :: [Bool]
a = [Int -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Int
i Int
j | Int
j <- [Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]] in (,) [Bool]
a (Bool -> ([Bool], Bool))
-> Either MathError Bool -> Either MathError ([Bool], Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Bool] -> Prop -> Either MathError Bool
evaluateProp [Bool]
a Prop
p)
            [Int
0 :: Int .. Int
2 Int -> Int -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

{- | Value bits and a don't-care mask. Both fields are bounded by the supplied
input width when returned by 'quineMcCluskey'.
-}
data Implicant = Implicant
    { Implicant -> Integer
implicantValue :: Integer
    -- ^ Fixed bit values of a Boolean implicant; positions masked by implicantMask are ignored.
    , Implicant -> Integer
implicantMask :: Integer
    -- ^ Bit mask whose set bits denote don't-care positions in an implicant.
    }
    deriving (Implicant -> Implicant -> Bool
(Implicant -> Implicant -> Bool)
-> (Implicant -> Implicant -> Bool) -> Eq Implicant
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Implicant -> Implicant -> Bool
== :: Implicant -> Implicant -> Bool
$c/= :: Implicant -> Implicant -> Bool
/= :: Implicant -> Implicant -> Bool
Eq, Eq Implicant
Eq Implicant =>
(Implicant -> Implicant -> Ordering)
-> (Implicant -> Implicant -> Bool)
-> (Implicant -> Implicant -> Bool)
-> (Implicant -> Implicant -> Bool)
-> (Implicant -> Implicant -> Bool)
-> (Implicant -> Implicant -> Implicant)
-> (Implicant -> Implicant -> Implicant)
-> Ord Implicant
Implicant -> Implicant -> Bool
Implicant -> Implicant -> Ordering
Implicant -> Implicant -> Implicant
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Implicant -> Implicant -> Ordering
compare :: Implicant -> Implicant -> Ordering
$c< :: Implicant -> Implicant -> Bool
< :: Implicant -> Implicant -> Bool
$c<= :: Implicant -> Implicant -> Bool
<= :: Implicant -> Implicant -> Bool
$c> :: Implicant -> Implicant -> Bool
> :: Implicant -> Implicant -> Bool
$c>= :: Implicant -> Implicant -> Bool
>= :: Implicant -> Implicant -> Bool
$cmax :: Implicant -> Implicant -> Implicant
max :: Implicant -> Implicant -> Implicant
$cmin :: Implicant -> Implicant -> Implicant
min :: Implicant -> Implicant -> Implicant
Ord, Int -> Implicant -> ShowS
[Implicant] -> ShowS
Implicant -> String
(Int -> Implicant -> ShowS)
-> (Implicant -> String)
-> ([Implicant] -> ShowS)
-> Show Implicant
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Implicant -> ShowS
showsPrec :: Int -> Implicant -> ShowS
$cshow :: Implicant -> String
show :: Implicant -> String
$cshowList :: [Implicant] -> ShowS
showList :: [Implicant] -> ShowS
Show)

{- | Given implicant then Integer minterm, compare bits where implicantMask is clear. True
means this Boolean cube covers the minterm.
-}
implicantCovers :: Implicant -> Integer -> Bool
implicantCovers :: Implicant -> Integer -> Bool
implicantCovers (Implicant Integer
v Integer
m) Integer
x = (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
m) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
v

{- | Exact Quine--McCluskey prime generation followed by branch-and-bound cover
selection. Objective is fewest terms, then literals, then lexical order.
The explicit budget counts prime comparisons and covering-search nodes.
-}
quineMcCluskey :: Int -> Int -> [Integer] -> [Integer] -> Either MathError [Implicant]
quineMcCluskey :: Int
-> Int -> [Integer] -> [Integer] -> Either MathError [Implicant]
quineMcCluskey Int
fuel Int
n [Integer]
on [Integer]
dc
    | Int
fuel Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
        Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
        Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
12
        Bool -> Bool -> Bool
|| (Integer -> Bool) -> [Integer] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Integer
x -> Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 Bool -> Bool -> Bool
|| Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
n) ([Integer]
on [Integer] -> [Integer] -> [Integer]
forall a. [a] -> [a] -> [a]
++ [Integer]
dc)
        Bool -> Bool -> Bool
|| Bool -> Bool
not ([Integer] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Integer] -> [Integer] -> [Integer]
forall a. Ord a => [a] -> [a] -> [a]
setIntersection [Integer]
on [Integer]
dc)) =
        MathError -> Either MathError [Implicant]
forall a b. a -> Either a b
Left (String -> MathError
InvalidArgument String
"invalid minimizer inputs")
    | Bool
otherwise = do
        (primes, remaining) <- Int
-> [Implicant]
-> [Implicant]
-> Either MathError ([Implicant], Int)
generate Int
fuel ((Integer -> Implicant) -> [Integer] -> [Implicant]
forall a b. (a -> b) -> [a] -> [b]
map (Integer -> Integer -> Implicant
`Implicant` Integer
0) ([Integer] -> [Integer]
forall a. Ord a => [a] -> [a]
sort ([Integer] -> [Integer]
forall a. Eq a => [a] -> [a]
nub ([Integer]
on [Integer] -> [Integer] -> [Integer]
forall a. [a] -> [a] -> [a]
++ [Integer]
dc)))) []
        let useful = (Implicant -> Bool) -> [Implicant] -> [Implicant]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Implicant
p -> (Integer -> Bool) -> [Integer] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Implicant -> Integer -> Bool
implicantCovers Implicant
p) [Integer]
on) [Implicant]
primes
        fst <$> cover remaining (sort (nub on)) [] useful Nothing
  where
    consume :: b -> Either MathError b
consume b
k | b
k b -> b -> Bool
forall a. Ord a => a -> a -> Bool
<= b
0 = MathError -> Either MathError b
forall a b. a -> Either a b
Left (String -> Int -> MathError
NonConvergence String
"Quine-McCluskey" Int
fuel) | Bool
otherwise = b -> Either MathError b
forall a b. b -> Either a b
Right (b
k b -> b -> b
forall a. Num a => a -> a -> a
- b
1)
    combine :: Implicant -> Implicant -> Maybe Implicant
combine (Implicant Integer
a Integer
m) (Implicant Integer
b Integer
q)
        | Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
q Bool -> Bool -> Bool
&& Integer -> Int
forall a. Bits a => a -> Int
popCount (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
b) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = Implicant -> Maybe Implicant
forall a. a -> Maybe a
Just (Integer -> Integer -> Implicant
Implicant (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
b) (Integer
m Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
b)))
        | Bool
otherwise = Maybe Implicant
forall a. Maybe a
Nothing
    generate :: Int
-> [Implicant]
-> [Implicant]
-> Either MathError ([Implicant], Int)
generate Int
k [] [Implicant]
acc = ([Implicant], Int) -> Either MathError ([Implicant], Int)
forall a b. b -> Either a b
Right ([Implicant] -> [Implicant]
forall a. Ord a => [a] -> [a]
sort ([Implicant] -> [Implicant]
forall a. Eq a => [a] -> [a]
nub [Implicant]
acc), Int
k)
    generate Int
k [Implicant]
terms [Implicant]
acc = do
        let pairs :: [(Implicant, Implicant)]
pairs = [(Implicant
a, Implicant
b) | (Int
i, Implicant
a) <- [Int] -> [Implicant] -> [(Int, Implicant)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] [Implicant]
terms, Implicant
b <- Int -> [Implicant] -> [Implicant]
forall a. Int -> [a] -> [a]
drop (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Implicant]
terms]
        if [(Implicant, Implicant)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Implicant, Implicant)]
pairs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
k
            then MathError -> Either MathError ([Implicant], Int)
forall a b. a -> Either a b
Left (String -> Int -> MathError
NonConvergence String
"Quine-McCluskey primes" Int
fuel)
            else do
                let merged :: [(Implicant, Implicant, Implicant)]
merged = [(Implicant
a, Implicant
b, Implicant
c) | (Implicant
a, Implicant
b) <- [(Implicant, Implicant)]
pairs, Just Implicant
c <- [Implicant -> Implicant -> Maybe Implicant
combine Implicant
a Implicant
b]]
                    used :: Set Implicant
used = [Implicant] -> Set Implicant
forall a. Ord a => [a] -> Set a
S.fromList ([Implicant
a | (Implicant
a, Implicant
_, Implicant
_) <- [(Implicant, Implicant, Implicant)]
merged] [Implicant] -> [Implicant] -> [Implicant]
forall a. [a] -> [a] -> [a]
++ [Implicant
b | (Implicant
_, Implicant
b, Implicant
_) <- [(Implicant, Implicant, Implicant)]
merged])
                    old :: [Implicant]
old = (Implicant -> Bool) -> [Implicant] -> [Implicant]
forall a. (a -> Bool) -> [a] -> [a]
filter (Implicant -> Set Implicant -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set Implicant
used) [Implicant]
terms
                Int
-> [Implicant]
-> [Implicant]
-> Either MathError ([Implicant], Int)
generate (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- [(Implicant, Implicant)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Implicant, Implicant)]
pairs) ([Implicant] -> [Implicant]
forall a. Ord a => [a] -> [a]
sort ([Implicant] -> [Implicant]
forall a. Eq a => [a] -> [a]
nub [Implicant
c | (Implicant
_, Implicant
_, Implicant
c) <- [(Implicant, Implicant, Implicant)]
merged])) ([Implicant]
old [Implicant] -> [Implicant] -> [Implicant]
forall a. [a] -> [a] -> [a]
++ [Implicant]
acc)
    score :: [Implicant] -> (Int, Int, [Implicant])
score [Implicant]
ps = ([Implicant] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Implicant]
ps, [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Integer -> Int
forall a. Bits a => a -> Int
popCount (Implicant -> Integer
implicantMask Implicant
p) | Implicant
p <- [Implicant]
ps], [Implicant] -> [Implicant]
forall a. Ord a => [a] -> [a]
sort [Implicant]
ps)
    improve :: [Implicant] -> Maybe [Implicant] -> Maybe [Implicant]
improve [Implicant]
ps Maybe [Implicant]
Nothing = [Implicant] -> Maybe [Implicant]
forall a. a -> Maybe a
Just ([Implicant] -> [Implicant]
forall a. Ord a => [a] -> [a]
sort [Implicant]
ps)
    improve [Implicant]
ps (Just [Implicant]
old) = [Implicant] -> Maybe [Implicant]
forall a. a -> Maybe a
Just (if [Implicant] -> (Int, Int, [Implicant])
score [Implicant]
ps (Int, Int, [Implicant]) -> (Int, Int, [Implicant]) -> Bool
forall a. Ord a => a -> a -> Bool
< [Implicant] -> (Int, Int, [Implicant])
score [Implicant]
old then [Implicant] -> [Implicant]
forall a. Ord a => [a] -> [a]
sort [Implicant]
ps else [Implicant]
old)
    cover :: t
-> [Integer]
-> [Implicant]
-> [Implicant]
-> Maybe [Implicant]
-> Either MathError ([Implicant], t)
cover t
k [] [Implicant]
chosen [Implicant]
_ Maybe [Implicant]
best = do k' <- t -> Either MathError t
forall {b}. (Ord b, Num b) => b -> Either MathError b
consume t
k; pure (maybe chosen id (improve chosen best), k')
    cover t
k [Integer]
todo [Implicant]
chosen [Implicant]
ps Maybe [Implicant]
best = do
        k' <- t -> Either MathError t
forall {b}. (Ord b, Num b) => b -> Either MathError b
consume t
k
        if maybe False (\[Implicant]
old -> [Implicant] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Implicant]
chosen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [Implicant] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Implicant]
old) best
            then pure (maybe [] id best, k')
            else
                let x = [Integer]
todo [Integer] -> Int -> Integer
forall a. HasCallStack => [a] -> Int -> a
!! Int
0; options = (Implicant -> Bool) -> [Implicant] -> [Implicant]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Implicant
p -> Implicant -> Integer -> Bool
implicantCovers Implicant
p Integer
x) [Implicant]
ps
                 in if null options
                        then Left (InvalidArgument "uncoverable minterm")
                        else
                            foldl
                                ( \Either MathError ([Implicant], t)
prev Implicant
p -> do
                                    (current, f) <- Either MathError ([Implicant], t)
prev
                                    cover
                                        f
                                        (filter (not . implicantCovers p) todo)
                                        (p : chosen)
                                        (filter (/= p) ps)
                                        (if null current then best else Just current)
                                )
                                (Right (maybe [] id best, k'))
                                options