{- |
Description: Conjunctive normal form
Copyright: Copyright (C) 2023 Yoo Chung
License: GPL-3.0-or-later
Maintainer: dev@chungyc.org

Some solutions to "Problems.P52" of Ninety-Nine Haskell "Problems".
-}
module Solutions.P52 (toConjunctiveNormalForm) where

import           Data.List      (partition)
import           Problems.Logic (Formula (..))

{- |
Return the conjunctive normal form of a boolean formula.
The value returned should always be a conjunction of disjunctions.
-}
toConjunctiveNormalForm :: Formula -> Formula
toConjunctiveNormalForm :: Formula -> Formula
toConjunctiveNormalForm Formula
f
  | Formula -> Bool
isLiteral Formula
f' = [Formula] -> Formula
Conjoin [ [Formula] -> Formula
Disjoin [Formula
f'] ]
  | Conjoin [Formula]
fs <- Formula
f' = [Formula] -> Formula
Conjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ (Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map Formula -> Formula
toDisjoin [Formula]
fs
  | Disjoin [Formula]
fs <- Formula
f', (Formula -> Bool) -> [Formula] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Formula -> Bool
isLiteral [Formula]
fs = [Formula] -> Formula
Conjoin [Formula
f']
  | Disjoin [Formula]
_ <- Formula
f' = Formula -> Formula
explodeDisjunction Formula
f'
  | Bool
otherwise = [Char] -> Formula
forall a. HasCallStack => [Char] -> a
error ([Char] -> Formula) -> [Char] -> Formula
forall a b. (a -> b) -> a -> b
$ [Char]
"unexpected form: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Formula -> [Char]
forall a. Show a => a -> [Char]
show Formula
f'
  where f' :: Formula
f' = Formula -> Formula
flatten (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ Formula -> Formula
normalizeFormulaOrder (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ Formula -> Formula
normalizeComplement (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ Formula -> Formula
normalizeEmptyClauses Formula
f

-- Normalize a formula so that it has no conjunction or disjunction
-- has an empty set of clauses.  This allows us to avoid having
-- to treat such conjunctions or disjunctions specially.
normalizeEmptyClauses :: Formula -> Formula
normalizeEmptyClauses :: Formula -> Formula
normalizeEmptyClauses f :: Formula
f@(Value Bool
_)    = Formula
f
normalizeEmptyClauses f :: Formula
f@(Variable [Char]
_) = Formula
f
normalizeEmptyClauses (Complement Formula
f) = Formula -> Formula
Complement (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ Formula -> Formula
normalizeEmptyClauses Formula
f
normalizeEmptyClauses (Disjoin [])   = Bool -> Formula
Value Bool
False
normalizeEmptyClauses (Conjoin [])   = Bool -> Formula
Value Bool
True
normalizeEmptyClauses (Disjoin [Formula]
fs)   = [Formula] -> Formula
Disjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ (Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map Formula -> Formula
normalizeEmptyClauses [Formula]
fs
normalizeEmptyClauses (Conjoin [Formula]
fs)   = [Formula] -> Formula
Conjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ (Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map Formula -> Formula
normalizeEmptyClauses [Formula]
fs

-- Ensure that complement only applies to values or variables.
-- I.e., return value will only have complement in literals.
normalizeComplement :: Formula -> Formula
normalizeComplement :: Formula -> Formula
normalizeComplement f :: Formula
f@(Value Bool
_) = Formula
f
normalizeComplement f :: Formula
f@(Variable [Char]
_) = Formula
f
normalizeComplement (Complement (Value Bool
v)) = Bool -> Formula
Value (Bool -> Formula) -> Bool -> Formula
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
v
normalizeComplement f :: Formula
f@(Complement (Variable [Char]
_)) = Formula
f
normalizeComplement (Complement (Complement Formula
f)) = Formula -> Formula
normalizeComplement Formula
f
normalizeComplement (Disjoin [Formula]
fs) = [Formula] -> Formula
Disjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ (Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map Formula -> Formula
normalizeComplement [Formula]
fs
normalizeComplement (Conjoin [Formula]
fs) = [Formula] -> Formula
Conjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ (Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map Formula -> Formula
normalizeComplement [Formula]
fs
normalizeComplement (Complement (Disjoin [Formula]
fs)) =
  [Formula] -> Formula
Conjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ (Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map (Formula -> Formula
normalizeComplement (Formula -> Formula) -> (Formula -> Formula) -> Formula -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> Formula
Complement) [Formula]
fs
normalizeComplement (Complement (Conjoin [Formula]
fs)) =
  [Formula] -> Formula
Disjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ (Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map (Formula -> Formula
normalizeComplement (Formula -> Formula) -> (Formula -> Formula) -> Formula -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> Formula
Complement) [Formula]
fs

-- Normalize the order of clauses in the formula so that:
--
-- * For conjunctions, the clauses are in the order of
--   conjunctions, compound disjunctions, flat disjunctions, and literals.
--
-- * For disjunctions, the clauses are in the order of
--   disjunctions, compound conjunctions, flat disjunctions, and literals.
--
-- This makes it more convenient to merge clauses or apply the distributive law.
normalizeFormulaOrder :: Formula -> Formula
normalizeFormulaOrder :: Formula -> Formula
normalizeFormulaOrder f :: Formula
f@(Value Bool
_)    = Formula
f
normalizeFormulaOrder f :: Formula
f@(Variable [Char]
_) = Formula
f
normalizeFormulaOrder (Complement Formula
f) = Formula -> Formula
Complement (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ Formula -> Formula
normalizeFormulaOrder Formula
f
normalizeFormulaOrder (Disjoin [Formula]
fs)   = Formula -> Formula
normalizeDisjunction (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [Formula] -> Formula
Disjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ (Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map Formula -> Formula
normalizeFormulaOrder [Formula]
fs
normalizeFormulaOrder (Conjoin [Formula]
fs)   = Formula -> Formula
normalizeConjunction (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [Formula] -> Formula
Conjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ (Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map Formula -> Formula
normalizeFormulaOrder [Formula]
fs

-- Normalize the order of clauses in a disjunction.
-- It does not order the clauses in sub-clauses.
normalizeDisjunction :: Formula -> Formula
normalizeDisjunction :: Formula -> Formula
normalizeDisjunction (Disjoin [Formula]
fs) =
  [Formula] -> Formula
Disjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ [Formula]
disjunctions [Formula] -> [Formula] -> [Formula]
forall a. [a] -> [a] -> [a]
++ [Formula]
compoundConjunctions [Formula] -> [Formula] -> [Formula]
forall a. [a] -> [a] -> [a]
++ [Formula]
flatConjunctions [Formula] -> [Formula] -> [Formula]
forall a. [a] -> [a] -> [a]
++ [Formula]
literals
  where ([Formula]
disjunctions, [Formula]
remainder) = (Formula -> Bool) -> [Formula] -> ([Formula], [Formula])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Formula -> Bool
isDisjunction [Formula]
fs
        ([Formula]
conjunctions, [Formula]
literals) = (Formula -> Bool) -> [Formula] -> ([Formula], [Formula])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Formula -> Bool
isConjunction [Formula]
remainder
        ([Formula]
compoundConjunctions, [Formula]
flatConjunctions) = (Formula -> Bool) -> [Formula] -> ([Formula], [Formula])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Bool -> Bool
not (Bool -> Bool) -> (Formula -> Bool) -> Formula -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> Bool
isFlat) [Formula]
conjunctions
normalizeDisjunction Formula
f = Formula
f

-- Normalize the order of clauses in a conjunction.
-- It does not order the clauses in sub-clauses.
normalizeConjunction :: Formula -> Formula
normalizeConjunction :: Formula -> Formula
normalizeConjunction (Conjoin [Formula]
fs) =
  [Formula] -> Formula
Conjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ [Formula]
conjunctions [Formula] -> [Formula] -> [Formula]
forall a. [a] -> [a] -> [a]
++ [Formula]
compoundDisjunctions [Formula] -> [Formula] -> [Formula]
forall a. [a] -> [a] -> [a]
++ [Formula]
flatDisjunctions [Formula] -> [Formula] -> [Formula]
forall a. [a] -> [a] -> [a]
++ [Formula]
literals
  where ([Formula]
conjunctions, [Formula]
remainder) = (Formula -> Bool) -> [Formula] -> ([Formula], [Formula])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Formula -> Bool
isConjunction [Formula]
fs
        ([Formula]
disjunctions, [Formula]
literals) = (Formula -> Bool) -> [Formula] -> ([Formula], [Formula])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Formula -> Bool
isDisjunction [Formula]
remainder
        ([Formula]
compoundDisjunctions, [Formula]
flatDisjunctions) = (Formula -> Bool) -> [Formula] -> ([Formula], [Formula])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Bool -> Bool
not (Bool -> Bool) -> (Formula -> Bool) -> Formula -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> Bool
isFlat) [Formula]
disjunctions
normalizeConjunction Formula
f = Formula
f

isLiteral :: Formula -> Bool
isLiteral :: Formula -> Bool
isLiteral (Value Bool
_)                 = Bool
True
isLiteral (Variable [Char]
_)              = Bool
True
isLiteral (Complement (Value Bool
_))    = Bool
True
isLiteral (Complement (Variable [Char]
_)) = Bool
True
isLiteral Formula
_                         = Bool
False

isDisjunction :: Formula -> Bool
isDisjunction :: Formula -> Bool
isDisjunction (Disjoin [Formula]
_) = Bool
True
isDisjunction Formula
_           = Bool
False

isConjunction :: Formula -> Bool
isConjunction :: Formula -> Bool
isConjunction (Conjoin [Formula]
_) = Bool
True
isConjunction Formula
_           = Bool
False

isFlat :: Formula -> Bool
isFlat :: Formula -> Bool
isFlat (Conjoin [Formula]
fs) = (Formula -> Bool) -> [Formula] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Formula -> Bool
isLiteral [Formula]
fs
isFlat (Disjoin [Formula]
fs) = (Formula -> Bool) -> [Formula] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Formula -> Bool
isLiteral [Formula]
fs
isFlat Formula
f | Formula -> Bool
isLiteral Formula
f = Bool
True
         | Bool
otherwise = Bool
False

-- Turn the given formula into a disjunction,
-- if it is not already a disjunction.
-- Used for turning a simpler representation to
-- the full conjunctive normal form.
toDisjoin :: Formula -> Formula
toDisjoin :: Formula -> Formula
toDisjoin f :: Formula
f@(Disjoin [Formula]
_) = Formula
f
toDisjoin Formula
f             = [Formula] -> Formula
Disjoin [Formula
f]

-- Flattens a boolean formula until it is at most two levels deep.
-- At all levels, the formula as it is transformed will be in a normalized form;
-- i.e., no empty set of clauses, complement only applies to values and variables,
-- and clauses are in normalized order.
flatten :: Formula -> Formula
flatten :: Formula -> Formula
flatten f :: Formula
f@(Value Bool
_)                 = Formula
f
flatten f :: Formula
f@(Variable [Char]
_)              = Formula
f
flatten f :: Formula
f@(Complement (Value Bool
_))    = Formula
f
flatten f :: Formula
f@(Complement (Variable [Char]
_)) = Formula
f
flatten (Complement (Complement Formula
f)) = Formula
f
flatten f :: Formula
f@(Disjoin [Formula]
_)               = Formula -> Formula
flattenDisjunction Formula
f
flatten f :: Formula
f@(Conjoin [Formula]
_)               = Formula -> Formula
flattenConjunction Formula
f
flatten Formula
f                           = [Char] -> Formula
forall a. HasCallStack => [Char] -> a
error ([Char] -> Formula) -> [Char] -> Formula
forall a b. (a -> b) -> a -> b
$ [Char]
"unexpected form: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Formula -> [Char]
forall a. Show a => a -> [Char]
show Formula
f

flattenDisjunction :: Formula -> Formula
flattenDisjunction :: Formula -> Formula
flattenDisjunction f :: Formula
f@(Disjoin [Formula]
fs)
  | [] <- [Formula]
fs = Bool -> Formula
Value Bool
False
  | (Formula -> Bool) -> [Formula] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Formula -> Bool
isLiteral [Formula]
fs = Formula
f
  | [Formula
f'] <- [Formula]
fs = Formula -> Formula
flatten Formula
f'
  | Disjoin [Formula]
fs' : [Formula]
fs'' <- [Formula]
fs = Formula -> Formula
flattenAgain (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [Formula] -> Formula
Disjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ [Formula]
fs' [Formula] -> [Formula] -> [Formula]
forall a. [a] -> [a] -> [a]
++ [Formula]
fs''
  | (Formula -> Bool) -> [Formula] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Formula -> Bool
isFlat [Formula]
fs = Formula
f
  -- Apply the distributive law.  In particular, it raises the disjunction
  -- to a higher level so that it can be merged with this level.
  | Conjoin (Disjoin [Formula]
fs' : [Formula]
fs'') : [Formula]
fs''' <- [Formula]
fs =
      let distributed :: Formula
distributed = [Formula] -> Formula
Disjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ (Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map (\Formula
x -> Formula -> Formula
normalizeConjunction (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [Formula] -> Formula
Conjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ Formula
x Formula -> [Formula] -> [Formula]
forall a. a -> [a] -> [a]
: [Formula]
fs'') [Formula]
fs'
      in Formula -> Formula
flattenAgain (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [Formula] -> Formula
Disjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ Formula
distributed Formula -> [Formula] -> [Formula]
forall a. a -> [a] -> [a]
: [Formula]
fs'''
  | Bool
otherwise = Formula -> Formula
flattenAgain (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [Formula] -> Formula
Disjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ (Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map Formula -> Formula
flatten [Formula]
fs
  where flattenAgain :: Formula -> Formula
flattenAgain = Formula -> Formula
flatten (Formula -> Formula) -> (Formula -> Formula) -> Formula -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> Formula
normalizeDisjunction
flattenDisjunction Formula
f = Formula
f

flattenConjunction :: Formula -> Formula
flattenConjunction :: Formula -> Formula
flattenConjunction f :: Formula
f@(Conjoin [Formula]
fs)
  | [] <- [Formula]
fs = Bool -> Formula
Value Bool
True
  | (Formula -> Bool) -> [Formula] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Formula -> Bool
isLiteral [Formula]
fs = Formula
f
  | [Formula
f'] <- [Formula]
fs = Formula -> Formula
flatten Formula
f'
  | Conjoin [Formula]
fs' : [Formula]
fs'' <- [Formula]
fs = Formula -> Formula
flattenAgain (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [Formula] -> Formula
Conjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ [Formula]
fs' [Formula] -> [Formula] -> [Formula]
forall a. [a] -> [a] -> [a]
++ [Formula]
fs''
  | (Formula -> Bool) -> [Formula] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Formula -> Bool
isFlat [Formula]
fs = Formula
f
  -- Apply the distributive law.  In particular, it raises the conjunction
  -- to a higher level so that it can be merged with this level.
  | Disjoin (Conjoin [Formula]
fs' : [Formula]
fs'') : [Formula]
fs''' <- [Formula]
fs =
      let distributed :: Formula
distributed = [Formula] -> Formula
Conjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ (Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map (\Formula
x -> Formula -> Formula
normalizeDisjunction (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [Formula] -> Formula
Disjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ Formula
x Formula -> [Formula] -> [Formula]
forall a. a -> [a] -> [a]
: [Formula]
fs'') [Formula]
fs'
      in Formula -> Formula
flattenAgain (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [Formula] -> Formula
Conjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ Formula
distributed Formula -> [Formula] -> [Formula]
forall a. a -> [a] -> [a]
: [Formula]
fs'''
  | Bool
otherwise = Formula -> Formula
flattenAgain (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [Formula] -> Formula
Conjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ (Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map Formula -> Formula
flatten [Formula]
fs
  where flattenAgain :: Formula -> Formula
flattenAgain = Formula -> Formula
flatten (Formula -> Formula) -> (Formula -> Formula) -> Formula -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> Formula
normalizeConjunction
flattenConjunction Formula
f = Formula
f

-- Combine all the terms in the conjunctions in a disjunction so that
-- the result is an equivalent conjunction of disjunctions.
explodeDisjunction :: Formula -> Formula
explodeDisjunction :: Formula -> Formula
explodeDisjunction (Disjoin [Formula]
fs) = [Formula] -> Formula
Conjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ ([Formula] -> Formula) -> [[Formula]] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map [Formula] -> Formula
Disjoin ([[Formula]] -> [Formula]) -> [[Formula]] -> [Formula]
forall a b. (a -> b) -> a -> b
$ [[Formula]] -> [[Formula]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([[Formula]] -> [[Formula]]) -> [[Formula]] -> [[Formula]]
forall a b. (a -> b) -> a -> b
$ [Formula] -> [[Formula]]
toList [Formula]
fs
  where toList :: [Formula] -> [[Formula]]
toList (Conjoin [Formula]
fs' : [Formula]
fs'') = [Formula]
fs' [Formula] -> [[Formula]] -> [[Formula]]
forall a. a -> [a] -> [a]
: [Formula] -> [[Formula]]
toList [Formula]
fs''
        toList (Formula
f : [Formula]
fs')            = [Formula
f] [Formula] -> [[Formula]] -> [[Formula]]
forall a. a -> [a] -> [a]
: [Formula] -> [[Formula]]
toList [Formula]
fs'
        toList []                   = []
explodeDisjunction Formula
f = Formula
f