-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Simplification logic for boolean expressions that is not
-- provided in the 'boolexpr' package.
module Data.BoolExpr.Simplify (
  cannotBeTrue,
  replace,
) where

import Data.BoolExpr
import Data.List qualified as L
import Data.Map (Map)
import Data.Map qualified as M
import Data.Set qualified as S

-- | Used only by "hasContradiction".
-- Note that the Booleans returned in this tuple are not actually used
-- as conditions, and therefore their semantic convention (e.g. associating
-- True = Positive and False = Negative) is irrelevant.
-- Rather, they are collected into sets
-- to determine whether both True and False exist for a key.
extractConstFromSigned :: Signed a -> (a, Bool)
extractConstFromSigned :: forall a. Signed a -> (a, Bool)
extractConstFromSigned Signed a
v = case Signed a
v of
  Negative a
x -> (a
x, Bool
False)
  Positive a
x -> (a
x, Bool
True)

hasContradiction :: Ord a => Conj (Signed a) -> Bool
hasContradiction :: forall a. Ord a => Conj (Signed a) -> Bool
hasContradiction (Conj [Signed a]
items) =
  Bool -> Bool
not
    (Bool -> Bool)
-> ([(a, Set Bool)] -> Bool) -> [(a, Set Bool)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a (Set Bool) -> Bool
forall k a. Map k a -> Bool
M.null
    (Map a (Set Bool) -> Bool)
-> ([(a, Set Bool)] -> Map a (Set Bool)) -> [(a, Set Bool)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set Bool -> Bool) -> Map a (Set Bool) -> Map a (Set Bool)
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (Int -> Bool) -> (Set Bool -> Int) -> Set Bool -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Bool -> Int
forall a. Set a -> Int
S.size)
    (Map a (Set Bool) -> Map a (Set Bool))
-> ([(a, Set Bool)] -> Map a (Set Bool))
-> [(a, Set Bool)]
-> Map a (Set Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set Bool -> Set Bool -> Set Bool)
-> [(a, Set Bool)] -> Map a (Set Bool)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith Set Bool -> Set Bool -> Set Bool
forall a. Semigroup a => a -> a -> a
(<>)
    ([(a, Set Bool)] -> Bool) -> [(a, Set Bool)] -> Bool
forall a b. (a -> b) -> a -> b
$ (Signed a -> (a, Set Bool)) -> [Signed a] -> [(a, Set Bool)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Bool -> Set Bool) -> (a, Bool) -> (a, Set Bool)
forall a b. (a -> b) -> (a, a) -> (a, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Set Bool
forall a. a -> Set a
S.singleton ((a, Bool) -> (a, Set Bool))
-> (Signed a -> (a, Bool)) -> Signed a -> (a, Set Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signed a -> (a, Bool)
forall a. Signed a -> (a, Bool)
extractConstFromSigned) [Signed a]
items

simplifyDNF :: Ord a => DNF a -> DNF a
simplifyDNF :: forall a. Ord a => DNF a -> DNF a
simplifyDNF (DNF (Disj [Conj (Signed a)]
disjunctions)) =
  Disj (Conj (Signed a)) -> DNF a
forall a. Disj (Conj (Signed a)) -> DNF a
DNF (Disj (Conj (Signed a)) -> DNF a)
-> Disj (Conj (Signed a)) -> DNF a
forall a b. (a -> b) -> a -> b
$ [Conj (Signed a)] -> Disj (Conj (Signed a))
forall a. [a] -> Disj a
Disj ([Conj (Signed a)] -> Disj (Conj (Signed a)))
-> [Conj (Signed a)] -> Disj (Conj (Signed a))
forall a b. (a -> b) -> a -> b
$ (Conj (Signed a) -> Bool) -> [Conj (Signed a)] -> [Conj (Signed a)]
forall a. (a -> Bool) -> [a] -> [a]
L.filter (Bool -> Bool
not (Bool -> Bool)
-> (Conj (Signed a) -> Bool) -> Conj (Signed a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Conj (Signed a) -> Bool
forall a. Ord a => Conj (Signed a) -> Bool
hasContradiction) [Conj (Signed a)]
disjunctions

isAlwaysFalse :: Ord a => DNF a -> Bool
isAlwaysFalse :: forall a. Ord a => DNF a -> Bool
isAlwaysFalse (DNF (Disj [Conj (Signed a)]
disjunctions)) = [Conj (Signed a)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
L.null [Conj (Signed a)]
disjunctions

cannotBeTrue :: Ord a => BoolExpr a -> Bool
cannotBeTrue :: forall a. Ord a => BoolExpr a -> Bool
cannotBeTrue = DNF a -> Bool
forall a. Ord a => DNF a -> Bool
isAlwaysFalse (DNF a -> Bool) -> (BoolExpr a -> DNF a) -> BoolExpr a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DNF a -> DNF a
forall a. Ord a => DNF a -> DNF a
simplifyDNF (DNF a -> DNF a) -> (BoolExpr a -> DNF a) -> BoolExpr a -> DNF a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BoolExpr a -> DNF a
forall a. BoolExpr a -> DNF a
boolTreeToDNF

replace :: Ord a => Map a Bool -> BoolExpr a -> BoolExpr a
replace :: forall a. Ord a => Map a Bool -> BoolExpr a -> BoolExpr a
replace Map a Bool
f (BAnd BoolExpr a
a BoolExpr a
b) = BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
BAnd (Map a Bool -> BoolExpr a -> BoolExpr a
forall a. Ord a => Map a Bool -> BoolExpr a -> BoolExpr a
replace Map a Bool
f BoolExpr a
a) (Map a Bool -> BoolExpr a -> BoolExpr a
forall a. Ord a => Map a Bool -> BoolExpr a -> BoolExpr a
replace Map a Bool
f BoolExpr a
b)
replace Map a Bool
f (BOr BoolExpr a
a BoolExpr a
b) = BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
BOr (Map a Bool -> BoolExpr a -> BoolExpr a
forall a. Ord a => Map a Bool -> BoolExpr a -> BoolExpr a
replace Map a Bool
f BoolExpr a
a) (Map a Bool -> BoolExpr a -> BoolExpr a
forall a. Ord a => Map a Bool -> BoolExpr a -> BoolExpr a
replace Map a Bool
f BoolExpr a
b)
replace Map a Bool
f (BNot BoolExpr a
t) = BoolExpr a -> BoolExpr a
forall a. BoolExpr a -> BoolExpr a
BNot (Map a Bool -> BoolExpr a -> BoolExpr a
forall a. Ord a => Map a Bool -> BoolExpr a -> BoolExpr a
replace Map a Bool
f BoolExpr a
t)
replace Map a Bool
_ BoolExpr a
BTrue = BoolExpr a
forall a. BoolExpr a
BTrue
replace Map a Bool
_ BoolExpr a
BFalse = BoolExpr a
forall a. BoolExpr a
BFalse
replace Map a Bool
m c :: BoolExpr a
c@(BConst Signed a
x) = case a -> Map a Bool -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
varname Map a Bool
m of
  Maybe Bool
Nothing -> BoolExpr a
c
  Just Bool
val ->
    if Bool -> Bool
txform Bool
val
      then BoolExpr a
forall a. BoolExpr a
BTrue
      else BoolExpr a
forall a. BoolExpr a
BFalse
 where
  (a
varname, Bool
isPositive) = Signed a -> (a, Bool)
forall a. Signed a -> (a, Bool)
extractConstFromSigned Signed a
x
  txform :: Bool -> Bool
txform = if Bool
isPositive then Bool -> Bool
forall a. a -> a
id else Bool -> Bool
not