module Data.Logic.Harrison.Normal
( trivial
, simpdnf
, simpdnf'
, simpcnf
, simpcnf'
) where
import Data.Logic.Classes.Combine (Combination(..), BinOp(..))
import Data.Logic.Classes.Constants (Constants(..))
import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), fromFirstOrder)
import Data.Logic.Classes.Formula (Formula(atomic))
import Data.Logic.Classes.Literal (Literal)
import Data.Logic.Classes.Negate (Negatable, negated, (.~.))
import Data.Logic.Failing (failing)
import Data.Logic.Harrison.Lib (setAny, allpairs)
import Data.Logic.Harrison.Skolem (nnf)
import qualified Data.Set.Extra as Set
import Prelude hiding (negate)
distrib' :: (Eq formula, Ord formula) => Set.Set (Set.Set formula) -> Set.Set (Set.Set formula) -> Set.Set (Set.Set formula)
distrib' s1 s2 = allpairs (Set.union) s1 s2
trivial :: (Negatable lit, Ord lit) => Set.Set lit -> Bool
trivial lits =
not . Set.null $ Set.intersection neg (Set.map (.~.) pos)
where (neg, pos) = Set.partition negated lits
simpdnf :: (FirstOrderFormula fof atom v, Eq fof, Ord fof) =>
fof -> Set.Set (Set.Set fof)
simpdnf fm =
foldFirstOrder qu co tf at fm
where
qu _ _ _ = def
co _ = def
tf False = Set.empty
tf True = Set.singleton Set.empty
at _ = Set.singleton (Set.singleton fm)
def = Set.filter keep djs
keep x = not (setAny (`Set.isProperSubsetOf` x) djs)
djs = Set.filter (not . trivial) (purednf (nnf fm))
purednf :: (FirstOrderFormula fof atom v, Ord fof) => fof -> Set.Set (Set.Set fof)
purednf fm =
foldFirstOrder qu co tf at fm
where
qu _ _ _ = Set.singleton (Set.singleton fm)
co (BinOp p (:&:) q) = distrib' (purednf p) (purednf q)
co (BinOp p (:|:) q) = Set.union (purednf p) (purednf q)
co _ = Set.singleton (Set.singleton fm)
tf = Set.singleton . Set.singleton . fromBool
at _ = Set.singleton (Set.singleton fm)
simpdnf' :: forall lit fof atom v. (FirstOrderFormula fof atom v, Literal lit atom, Formula lit atom, Ord lit) =>
fof -> Set.Set (Set.Set lit)
simpdnf' fm =
foldFirstOrder qu co tf at fm
where
qu _ _ _ = def
co _ = def
tf False = Set.empty
tf True = Set.singleton Set.empty
at = Set.singleton . Set.singleton . atomic
def = Set.filter keep djs
keep x = not (setAny (`Set.isProperSubsetOf` x) djs)
djs = Set.filter (not . trivial) (purednf' (nnf fm))
purednf' :: forall lit fof atom v. (FirstOrderFormula fof atom v, Literal lit atom, Ord lit) =>
fof -> Set.Set (Set.Set lit)
purednf' fm =
foldFirstOrder (\ _ _ _ -> x) co (\ _ -> x) (\ _ -> x) fm
where
co (BinOp p (:&:) q) = Set.distrib (purednf' p) (purednf' q)
co (BinOp p (:|:) q) = Set.union (purednf' p) (purednf' q)
co _ = x
x = failing (const (error "purednf'")) (Set.singleton . Set.singleton) (fromFirstOrder id fm)
simpcnf :: forall fof atom v. (FirstOrderFormula fof atom v, Ord fof) => fof -> Set.Set (Set.Set fof)
simpcnf fm =
foldFirstOrder qu co tf at fm
where
qu _ _ _ = def
co _ = def
tf False = Set.singleton Set.empty
tf True = Set.empty
at x = Set.singleton (Set.singleton (atomic x))
def = Set.filter keep cjs
keep x = not (setAny (`Set.isProperSubsetOf` x) cjs)
cjs = Set.filter (not . trivial) (purecnf fm)
purecnf :: forall fof atom v. (FirstOrderFormula fof atom v, Ord fof) => fof -> Set.Set (Set.Set fof)
purecnf fm = Set.map (Set.map ( (.~.))) (purednf (nnf ((.~.) fm)))
simpcnf' :: forall lit fof atom v. (FirstOrderFormula fof atom v, Literal lit atom, Ord lit) => fof -> Set.Set (Set.Set lit)
simpcnf' fm =
foldFirstOrder (\ _ _ _ -> cjs') co tf at fm
where
co _ = cjs'
at = Set.singleton . Set.singleton . atomic
tf False = Set.singleton Set.empty
tf True = Set.empty
cjs' = Set.filter keep cjs
keep x = not (Set.or (Set.map (`Set.isProperSubsetOf` x) cjs))
cjs = Set.filter (not . trivial) (purecnf' (nnf fm))
purecnf' :: forall lit fof atom v. (FirstOrderFormula fof atom v, Literal lit atom, Ord lit) => fof -> Set.Set (Set.Set lit)
purecnf' fm = Set.map (Set.map (.~.)) (purednf' (nnf ((.~.) fm)))