-- |
-- 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
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> Bool
M.null
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter ((forall a. Ord a => a -> a -> Bool
> Int
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> Int
S.size)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith forall a. Semigroup a => a -> a -> a
(<>)
    forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Set a
S.singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)) =
  forall a. Disj (Conj (Signed a)) -> DNF a
DNF forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Disj a
Disj forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
L.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)) = 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 = forall a. Ord a => DNF a -> Bool
isAlwaysFalse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => DNF a -> DNF a
simplifyDNF forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
BAnd (forall a. Ord a => Map a Bool -> BoolExpr a -> BoolExpr a
replace Map a Bool
f BoolExpr a
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) = forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
BOr (forall a. Ord a => Map a Bool -> BoolExpr a -> BoolExpr a
replace Map a Bool
f BoolExpr a
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) = forall a. BoolExpr a -> BoolExpr a
BNot (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 = forall a. BoolExpr a
BTrue
replace Map a Bool
_ BoolExpr a
BFalse = forall a. BoolExpr a
BFalse
replace Map a Bool
m c :: BoolExpr a
c@(BConst Signed a
x) = case 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 forall a. BoolExpr a
BTrue
      else forall a. BoolExpr a
BFalse
 where
  (a
varname, Bool
isPositive) = forall a. Signed a -> (a, Bool)
extractConstFromSigned Signed a
x
  txform :: Bool -> Bool
txform = if Bool
isPositive then forall a. a -> a
id else Bool -> Bool
not