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

Part of Ninety-Nine Haskell "Problems".  Some solutions are in "Solutions.P52".
-}
module Problems.P52
  ( toConjunctiveNormalForm
  , Formula (..)
    -- * Supporting functions
    -- | The function below is not part of the problem.
  , evaluateFormula
) where

import           Problems.Logic (Formula (..), evaluateFormula)
import qualified Solutions.P52  as Solution

{- | It is known that any boolean function can be represented in conjunctive normal form.
These are conjunctions of disjunctions of literals,
where literals are one of boolean values, variables, or the complement of values or variables.
For example, the boolean formula \(\neg(x \wedge \neg y) \wedge (z \vee w)\)
is equivalent to the conjunctive normal form \( (\neg x \vee y) \wedge (z \vee w) \).

Return the conjunctive normal form of a boolean formula.
The value returned should always be a conjunction of disjunctions.

=== Examples

>>> toConjunctiveNormalForm $ Value True
Conjoin [Disjoin [Value True]]

>>> toConjunctiveNormalForm $ Complement $ Disjoin [Variable "X", Variable "Y"]
Conjoin [Disjoin [Complement (Variable "X")],Disjoin [Complement (Variable "Y")]]

>>> :{
toConjunctiveNormalForm $ Disjoin [ Variable "X"
                                  , Conjoin [ Complement $ Variable "Y"
                                            , Variable "Z"
                                            ]
                                  ]
:}
Conjoin [Disjoin [Variable "X",Complement (Variable "Y")],Disjoin ...

=== __Hint__

Transform a boolean formula using De Morgan's law, the distributive law,
and double negation elimination to reduce nesting.
Alternatively, the conjunctive normal form can be obtained
easily from the truth table, although this will always require
a running time exponential to the number of variables.
-}
toConjunctiveNormalForm :: Formula -> Formula
toConjunctiveNormalForm :: Formula -> Formula
toConjunctiveNormalForm = Formula -> Formula
Solution.toConjunctiveNormalForm