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
extractConstFromSigned :: Signed a -> (a, Bool)
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 a b. (a -> b) -> a -> b
$
forall k a. Map k a -> Bool
M.null forall a b. (a -> b) -> a -> b
$
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 a b. (a -> b) -> a -> b
$
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