-- | Definitional CNF.
--
-- Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.Logic.ATP.DefCNF
    ( NumAtom(ma, ai)
    , defcnfs
    , defcnf1
    , defcnf2
    , defcnf3
    -- * Instance
    , Atom(N)
    -- * Tests
    , testDefCNF
    ) where

import Data.Function (on)
import Data.List as List
import Data.Logic.ATP.Formulas as P
import Data.Logic.ATP.Lit ((.~.), (¬), convertLiteral, IsLiteral, JustLiteral, LFormula)
import Data.Logic.ATP.Pretty (assertEqual', HasFixity, Pretty(pPrint), prettyShow, text)
import Data.Logic.ATP.Prop (cnf', foldPropositional, IsPropositional(foldPropositional'), JustPropositional,
                            list_conj, list_disj, nenf, PFormula, Prop(P), simpcnf,
                            (∨), (∧), (.<=>.), (.&.), (.|.), BinOp(..))
import Data.Map.Strict as Map hiding (fromList)
import Data.Set as Set
import Test.HUnit

-- | Example (p. 74)
test01 :: Test
test01 :: Test
test01 =
    let p :: PFormula Prop
        q :: PFormula Prop
        r :: PFormula Prop
        [PFormula Prop
p, PFormula Prop
q, PFormula Prop
r] = ((String -> PFormula Prop) -> [String] -> [PFormula Prop]
forall a b. (a -> b) -> [a] -> [b]
List.map (AtomOf (PFormula Prop) -> PFormula Prop
Prop -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (Prop -> PFormula Prop)
-> (String -> Prop) -> String -> PFormula Prop
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Prop
P) [String
"p", String
"q", String
"r"]) in
    Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> PFormula Prop -> PFormula Prop -> Assertion
forall a.
(?loc::CallStack, Eq a, Pretty a) =>
String -> a -> a -> Assertion
assertEqual' String
"cnf test (p. 74)"
                 ((PFormula Prop
pPFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∨PFormula Prop
qPFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∨PFormula Prop
r)PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∧(PFormula Prop
pPFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∨PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(¬)PFormula Prop
qPFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∨PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(¬)PFormula Prop
r)PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∧(PFormula Prop
qPFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∨PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(¬)PFormula Prop
pPFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∨PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(¬)PFormula Prop
r)PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∧(PFormula Prop
rPFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∨PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(¬)PFormula Prop
pPFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∨PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(¬)PFormula Prop
q))
                 (PFormula Prop -> PFormula Prop
forall pf. (JustPropositional pf, Ord pf) => pf -> pf
cnf' (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. PFormula Prop
r)) :: PFormula Prop)

class NumAtom atom where
    ma :: Integer -> atom
    ai :: atom -> Integer

data Atom = N String Integer deriving (Atom -> Atom -> Bool
(Atom -> Atom -> Bool) -> (Atom -> Atom -> Bool) -> Eq Atom
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Atom -> Atom -> Bool
== :: Atom -> Atom -> Bool
$c/= :: Atom -> Atom -> Bool
/= :: Atom -> Atom -> Bool
Eq, Eq Atom
Eq Atom =>
(Atom -> Atom -> Ordering)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Atom)
-> (Atom -> Atom -> Atom)
-> Ord Atom
Atom -> Atom -> Bool
Atom -> Atom -> Ordering
Atom -> Atom -> Atom
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Atom -> Atom -> Ordering
compare :: Atom -> Atom -> Ordering
$c< :: Atom -> Atom -> Bool
< :: Atom -> Atom -> Bool
$c<= :: Atom -> Atom -> Bool
<= :: Atom -> Atom -> Bool
$c> :: Atom -> Atom -> Bool
> :: Atom -> Atom -> Bool
$c>= :: Atom -> Atom -> Bool
>= :: Atom -> Atom -> Bool
$cmax :: Atom -> Atom -> Atom
max :: Atom -> Atom -> Atom
$cmin :: Atom -> Atom -> Atom
min :: Atom -> Atom -> Atom
Ord, Int -> Atom -> ShowS
[Atom] -> ShowS
Atom -> String
(Int -> Atom -> ShowS)
-> (Atom -> String) -> ([Atom] -> ShowS) -> Show Atom
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Atom -> ShowS
showsPrec :: Int -> Atom -> ShowS
$cshow :: Atom -> String
show :: Atom -> String
$cshowList :: [Atom] -> ShowS
showList :: [Atom] -> ShowS
Show)

instance Pretty Atom where
    pPrint :: Atom -> Doc
pPrint (N String
s Integer
n) = String -> Doc
text (String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ if Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then String
"" else Integer -> String
forall a. Show a => a -> String
show Integer
n)

instance NumAtom Atom where
    ma :: Integer -> Atom
ma = String -> Integer -> Atom
N String
"p_"
    ai :: Atom -> Integer
ai (N String
_ Integer
n) = Integer
n

instance HasFixity Atom

instance IsAtom Atom

-- | Make a stylized variable and update the index.
mkprop :: forall pf. (IsPropositional pf, NumAtom (AtomOf pf)) => Integer -> (pf, Integer)
mkprop :: forall pf.
(IsPropositional pf, NumAtom (AtomOf pf)) =>
Integer -> (pf, Integer)
mkprop Integer
n = (AtomOf pf -> pf
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (Integer -> AtomOf pf
forall atom. NumAtom atom => Integer -> atom
ma Integer
n :: AtomOf pf), Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)

-- |  Core definitional CNF procedure.
maincnf :: (IsPropositional pf, Ord pf, NumAtom (AtomOf pf)) => (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
maincnf :: forall pf.
(IsPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
maincnf trip :: (pf, Map pf pf, Integer)
trip@(pf
fm, Map pf pf
_defs, Integer
_n) =
    (pf -> (pf, Map pf pf, Integer))
-> (pf -> BinOp -> pf -> (pf, Map pf pf, Integer))
-> (pf -> (pf, Map pf pf, Integer))
-> (Bool -> (pf, Map pf pf, Integer))
-> (AtomOf pf -> (pf, Map pf pf, Integer))
-> pf
-> (pf, Map pf pf, Integer)
forall formula r.
IsPropositional formula =>
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(pf -> r)
-> (pf -> BinOp -> pf -> r)
-> (pf -> r)
-> (Bool -> r)
-> (AtomOf pf -> r)
-> pf
-> r
foldPropositional' pf -> (pf, Map pf pf, Integer)
forall {p}. p -> (pf, Map pf pf, Integer)
ho pf -> BinOp -> pf -> (pf, Map pf pf, Integer)
co pf -> (pf, Map pf pf, Integer)
forall {p}. p -> (pf, Map pf pf, Integer)
ne Bool -> (pf, Map pf pf, Integer)
forall {p}. p -> (pf, Map pf pf, Integer)
tf AtomOf pf -> (pf, Map pf pf, Integer)
forall {p}. p -> (pf, Map pf pf, Integer)
at pf
fm
    where
      ho :: p -> (pf, Map pf pf, Integer)
ho p
_ = (pf, Map pf pf, Integer)
trip
      co :: pf -> BinOp -> pf -> (pf, Map pf pf, Integer)
co pf
p BinOp
(:&:) pf
q = (pf -> pf -> pf)
-> (pf, pf) -> (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, NumAtom (AtomOf pf), Ord pf) =>
(pf -> pf -> pf)
-> (pf, pf) -> (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
defstep pf -> pf -> pf
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.&.) (pf
p,pf
q) (pf, Map pf pf, Integer)
trip
      co pf
p BinOp
(:|:) pf
q = (pf -> pf -> pf)
-> (pf, pf) -> (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, NumAtom (AtomOf pf), Ord pf) =>
(pf -> pf -> pf)
-> (pf, pf) -> (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
defstep pf -> pf -> pf
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.|.) (pf
p,pf
q) (pf, Map pf pf, Integer)
trip
      co pf
p BinOp
(:<=>:) pf
q = (pf -> pf -> pf)
-> (pf, pf) -> (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, NumAtom (AtomOf pf), Ord pf) =>
(pf -> pf -> pf)
-> (pf, pf) -> (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
defstep pf -> pf -> pf
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.<=>.) (pf
p,pf
q) (pf, Map pf pf, Integer)
trip
      co pf
_ BinOp
(:=>:) pf
_ = (pf, Map pf pf, Integer)
trip
      ne :: p -> (pf, Map pf pf, Integer)
ne p
_ = (pf, Map pf pf, Integer)
trip
      tf :: p -> (pf, Map pf pf, Integer)
tf p
_ = (pf, Map pf pf, Integer)
trip
      at :: p -> (pf, Map pf pf, Integer)
at p
_ = (pf, Map pf pf, Integer)
trip

defstep :: (IsPropositional pf, NumAtom (AtomOf pf), Ord pf) =>
           (pf -> pf -> pf) -> (pf, pf) -> (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
defstep :: forall pf.
(IsPropositional pf, NumAtom (AtomOf pf), Ord pf) =>
(pf -> pf -> pf)
-> (pf, pf) -> (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
defstep pf -> pf -> pf
op (pf
p,pf
q) (pf
_fm, Map pf pf
defs, Integer
n) =
  let (pf
fm1,Map pf pf
defs1,Integer
n1) = (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
maincnf (pf
p,Map pf pf
defs,Integer
n) in
  let (pf
fm2,Map pf pf
defs2,Integer
n2) = (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
maincnf (pf
q,Map pf pf
defs1,Integer
n1) in
  let fm' :: pf
fm' = pf -> pf -> pf
op pf
fm1 pf
fm2 in
  case pf -> Map pf pf -> Maybe pf
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup pf
fm' Map pf pf
defs2 of
    Just pf
_ -> (pf
fm', Map pf pf
defs2, Integer
n2)
    Maybe pf
Nothing -> let (pf
v,Integer
n3) = Integer -> (pf, Integer)
forall pf.
(IsPropositional pf, NumAtom (AtomOf pf)) =>
Integer -> (pf, Integer)
mkprop Integer
n2 in (pf
v, pf -> pf -> Map pf pf -> Map pf pf
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert pf
v (pf
v pf -> pf -> pf
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. pf
fm') Map pf pf
defs2,Integer
n3)

-- | Make n large enough that "v_m" won't clash with s for any m >= n
max_varindex :: NumAtom atom =>  atom -> Integer -> Integer
max_varindex :: forall atom. NumAtom atom => atom -> Integer -> Integer
max_varindex atom
atom Integer
n = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
n (atom -> Integer
forall atom. NumAtom atom => atom -> Integer
ai atom
atom)

-- | Overall definitional CNF.
defcnf1 :: forall pf. (IsPropositional pf, JustPropositional pf, NumAtom (AtomOf pf), Ord pf) => pf -> pf
defcnf1 :: forall pf.
(IsPropositional pf, JustPropositional pf, NumAtom (AtomOf pf),
 Ord pf) =>
pf -> pf
defcnf1 = Set pf -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj (Set pf -> pf) -> (pf -> Set pf) -> pf -> pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set (LFormula (AtomOf pf)) -> pf)
-> Set (Set (LFormula (AtomOf pf))) -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Set pf -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_disj (Set pf -> pf)
-> (Set (LFormula (AtomOf pf)) -> Set pf)
-> Set (LFormula (AtomOf pf))
-> pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LFormula (AtomOf pf) -> pf)
-> Set (LFormula (AtomOf pf)) -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((AtomOf (LFormula (AtomOf pf)) -> AtomOf pf)
-> LFormula (AtomOf pf) -> pf
forall lit1 lit2.
(JustLiteral lit1, IsLiteral lit2) =>
(AtomOf lit1 -> AtomOf lit2) -> lit1 -> lit2
convertLiteral AtomOf (LFormula (AtomOf pf)) -> AtomOf pf
AtomOf (LFormula (AtomOf pf)) -> AtomOf (LFormula (AtomOf pf))
forall a. a -> a
id)) (Set (Set (LFormula (AtomOf pf))) -> Set pf)
-> (pf -> Set (Set (LFormula (AtomOf pf)))) -> pf -> Set pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((AtomOf pf -> AtomOf (LFormula (AtomOf pf)))
-> ((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
-> pf
-> Set (Set (LFormula (AtomOf pf)))
forall pf lit.
(IsPropositional pf, JustPropositional pf, IsLiteral lit,
 JustLiteral lit, Ord lit, NumAtom (AtomOf pf)) =>
(AtomOf pf -> AtomOf lit)
-> ((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
-> pf
-> Set (Set lit)
mk_defcnf AtomOf pf -> AtomOf pf
AtomOf pf -> AtomOf (LFormula (AtomOf pf))
forall a. a -> a
id (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
maincnf :: pf -> Set (Set (LFormula (AtomOf pf))))

mk_defcnf :: forall pf lit.
             (IsPropositional pf, JustPropositional pf,
              IsLiteral lit, JustLiteral lit, Ord lit,
              NumAtom (AtomOf pf)) =>
             (AtomOf pf -> AtomOf lit)
          -> ((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
          -> pf -> Set (Set lit)
mk_defcnf :: forall pf lit.
(IsPropositional pf, JustPropositional pf, IsLiteral lit,
 JustLiteral lit, Ord lit, NumAtom (AtomOf pf)) =>
(AtomOf pf -> AtomOf lit)
-> ((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
-> pf
-> Set (Set lit)
mk_defcnf AtomOf pf -> AtomOf lit
ca (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
fn pf
fm =
  let (pf
fm' :: pf) = pf -> pf
forall formula. IsPropositional formula => formula -> formula
nenf pf
fm in
  let n :: Integer
n = Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ (AtomOf pf -> Integer -> Integer) -> pf -> Integer -> Integer
forall formula r.
IsFormula formula =>
(AtomOf formula -> r -> r) -> formula -> r -> r
forall r. (AtomOf pf -> r -> r) -> pf -> r -> r
overatoms AtomOf pf -> Integer -> Integer
forall atom. NumAtom atom => atom -> Integer -> Integer
max_varindex pf
fm' Integer
0 in
  let (pf
fm'',Map pf pf
defs,Integer
_) = (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
fn (pf
fm',Map pf pf
forall k a. Map k a
Map.empty,Integer
n) in
  let ([pf]
deflist :: [pf]) = Map pf pf -> [pf]
forall k a. Map k a -> [a]
Map.elems Map pf pf
defs in
  [Set (Set lit)] -> Set (Set lit)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((pf -> Set (Set lit)) -> [pf] -> [Set (Set lit)]
forall a b. (a -> b) -> [a] -> [b]
List.map ((AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf AtomOf pf -> AtomOf lit
ca :: pf -> Set (Set lit)) (pf
fm'' pf -> [pf] -> [pf]
forall a. a -> [a] -> [a]
: [pf]
deflist))

testfm :: PFormula Atom
testfm :: PFormula Atom
testfm = let (PFormula Atom
p, PFormula Atom
q, PFormula Atom
r, PFormula Atom
s) = (AtomOf (PFormula Atom) -> PFormula Atom
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Integer -> Atom
N String
"p" Integer
0), AtomOf (PFormula Atom) -> PFormula Atom
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Integer -> Atom
N String
"q" Integer
0), AtomOf (PFormula Atom) -> PFormula Atom
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Integer -> Atom
N String
"r" Integer
0), AtomOf (PFormula Atom) -> PFormula Atom
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Integer -> Atom
N String
"s" Integer
0)) in
     (PFormula Atom
p PFormula Atom -> PFormula Atom -> PFormula Atom
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (PFormula Atom
q PFormula Atom -> PFormula Atom -> PFormula Atom
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Atom -> PFormula Atom
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Atom
r))) PFormula Atom -> PFormula Atom -> PFormula Atom
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Atom
s

-- Example.
{-
START_INTERACTIVE;;
defcnf1 <<(p \/ (q /\ ~r)) /\ s>>;;
END_INTERACTIVE;;
-}

test02 :: Test
test02 :: Test
test02 =
    let input :: [[String]]
input = Set (Set (LFormula Atom)) -> [[String]]
forall a. Pretty a => Set (Set a) -> [[String]]
strings ((AtomOf (PFormula Atom) -> AtomOf (LFormula Atom))
-> ((PFormula Atom, Map (PFormula Atom) (PFormula Atom), Integer)
    -> (PFormula Atom, Map (PFormula Atom) (PFormula Atom), Integer))
-> PFormula Atom
-> Set (Set (LFormula Atom))
forall pf lit.
(IsPropositional pf, JustPropositional pf, IsLiteral lit,
 JustLiteral lit, Ord lit, NumAtom (AtomOf pf)) =>
(AtomOf pf -> AtomOf lit)
-> ((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
-> pf
-> Set (Set lit)
mk_defcnf AtomOf (PFormula Atom) -> AtomOf (LFormula Atom)
Atom -> Atom
forall a. a -> a
id (PFormula Atom, Map (PFormula Atom) (PFormula Atom), Integer)
-> (PFormula Atom, Map (PFormula Atom) (PFormula Atom), Integer)
forall pf.
(IsPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
maincnf PFormula Atom
testfm :: Set (Set (LFormula Atom)))
        expected :: [[String]]
expected = [[String
"p_3"],
                    [String
"p_2",String
"¬p"],
                    [String
"p_2",String
"¬p_1"],
                    [String
"p_2",String
"¬p_3"],
                    [String
"q",String
"¬p_1"],
                    [String
"s",String
"¬p_3"],
                    [String
"¬p_1",String
"¬r"],
                    [String
"p",String
"p_1",String
"¬p_2"],
                    [String
"p_1",String
"r",String
"¬q"],
                    [String
"p_3",String
"¬p_2",String
"¬s"]] in
    Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> [[String]] -> [[String]] -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"defcnf1 (p. 77)" [[String]]
expected [[String]]
input

strings :: Pretty a => Set (Set a) -> [[String]]
strings :: forall a. Pretty a => Set (Set a) -> [[String]]
strings Set (Set a)
ss = ([String] -> [String] -> Ordering) -> [[String]] -> [[String]]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> ([String] -> Int) -> [String] -> [String] -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length) ([[String]] -> [[String]])
-> (Set [String] -> [[String]]) -> Set [String] -> [[String]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[String]] -> [[String]]
forall a. Ord a => [a] -> [a]
sort ([[String]] -> [[String]])
-> (Set [String] -> [[String]]) -> Set [String] -> [[String]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set [String] -> [[String]]
forall a. Set a -> [a]
Set.toList (Set [String] -> [[String]]) -> Set [String] -> [[String]]
forall a b. (a -> b) -> a -> b
$ (Set a -> [String]) -> Set (Set a) -> Set [String]
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ([String] -> [String]
forall a. Ord a => [a] -> [a]
sort ([String] -> [String]) -> (Set a -> [String]) -> Set a -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set String -> [String]
forall a. Set a -> [a]
Set.toList (Set String -> [String])
-> (Set a -> Set String) -> Set a -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> String) -> Set a -> Set String
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map a -> String
forall a. Pretty a => a -> String
prettyShow) Set (Set a)
ss

-- | Version tweaked to exploit initial structure.
defcnf2 :: (IsPropositional pf, JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> pf
defcnf2 :: forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
pf -> pf
defcnf2 pf
fm = Set pf -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj ((Set (LFormula (AtomOf pf)) -> pf)
-> Set (Set (LFormula (AtomOf pf))) -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Set pf -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_disj (Set pf -> pf)
-> (Set (LFormula (AtomOf pf)) -> Set pf)
-> Set (LFormula (AtomOf pf))
-> pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LFormula (AtomOf pf) -> pf)
-> Set (LFormula (AtomOf pf)) -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((AtomOf (LFormula (AtomOf pf)) -> AtomOf pf)
-> LFormula (AtomOf pf) -> pf
forall lit1 lit2.
(JustLiteral lit1, IsLiteral lit2) =>
(AtomOf lit1 -> AtomOf lit2) -> lit1 -> lit2
convertLiteral AtomOf (LFormula (AtomOf pf)) -> AtomOf pf
AtomOf (LFormula (AtomOf pf)) -> AtomOf (LFormula (AtomOf pf))
forall a. a -> a
id)) (pf -> Set (Set (LFormula (AtomOf pf)))
forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
pf -> Set (Set (LFormula (AtomOf pf)))
defcnfs pf
fm))

defcnfs :: (IsPropositional pf, JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Set (Set (LFormula (AtomOf pf)))
defcnfs :: forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
pf -> Set (Set (LFormula (AtomOf pf)))
defcnfs pf
fm = (AtomOf pf -> AtomOf (LFormula (AtomOf pf)))
-> ((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
-> pf
-> Set (Set (LFormula (AtomOf pf)))
forall pf lit.
(IsPropositional pf, JustPropositional pf, IsLiteral lit,
 JustLiteral lit, Ord lit, NumAtom (AtomOf pf)) =>
(AtomOf pf -> AtomOf lit)
-> ((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
-> pf
-> Set (Set lit)
mk_defcnf AtomOf pf -> AtomOf pf
AtomOf pf -> AtomOf (LFormula (AtomOf pf))
forall a. a -> a
id (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
andcnf pf
fm

andcnf :: (IsPropositional pf, JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
andcnf :: forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
andcnf trip :: (pf, Map pf pf, Integer)
trip@(pf
fm,Map pf pf
_defs,Integer
_n) =
    (pf -> BinOp -> pf -> (pf, Map pf pf, Integer))
-> (pf -> (pf, Map pf pf, Integer))
-> (Bool -> (pf, Map pf pf, Integer))
-> (AtomOf pf -> (pf, Map pf pf, Integer))
-> pf
-> (pf, Map pf pf, Integer)
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional pf -> BinOp -> pf -> (pf, Map pf pf, Integer)
co (\ pf
_ -> (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
orcnf (pf, Map pf pf, Integer)
trip) (\ Bool
_ -> (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
orcnf (pf, Map pf pf, Integer)
trip) (\ AtomOf pf
_ -> (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
orcnf (pf, Map pf pf, Integer)
trip) pf
fm
    where
      co :: pf -> BinOp -> pf -> (pf, Map pf pf, Integer)
co pf
p BinOp
(:&:) pf
q = ((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
-> (pf -> pf -> pf)
-> pf
-> pf
-> (pf, Map pf pf, Integer)
-> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, NumAtom (AtomOf pf)) =>
((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
-> (pf -> pf -> pf)
-> pf
-> pf
-> (pf, Map pf pf, Integer)
-> (pf, Map pf pf, Integer)
subcnf (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
andcnf pf -> pf -> pf
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.&.) pf
p pf
q (pf, Map pf pf, Integer)
trip
      co pf
_ BinOp
_ pf
_ = (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
orcnf (pf, Map pf pf, Integer)
trip

orcnf :: (IsPropositional pf, JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
orcnf :: forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
orcnf trip :: (pf, Map pf pf, Integer)
trip@(pf
fm,Map pf pf
_defs,Integer
_n) =
    (pf -> BinOp -> pf -> (pf, Map pf pf, Integer))
-> (pf -> (pf, Map pf pf, Integer))
-> (Bool -> (pf, Map pf pf, Integer))
-> (AtomOf pf -> (pf, Map pf pf, Integer))
-> pf
-> (pf, Map pf pf, Integer)
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional pf -> BinOp -> pf -> (pf, Map pf pf, Integer)
co (\ pf
_ -> (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
maincnf (pf, Map pf pf, Integer)
trip) (\ Bool
_ -> (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
maincnf (pf, Map pf pf, Integer)
trip) (\ AtomOf pf
_ -> (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
maincnf (pf, Map pf pf, Integer)
trip) pf
fm
    where
      co :: pf -> BinOp -> pf -> (pf, Map pf pf, Integer)
co pf
p BinOp
(:|:) pf
q = ((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
-> (pf -> pf -> pf)
-> pf
-> pf
-> (pf, Map pf pf, Integer)
-> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, NumAtom (AtomOf pf)) =>
((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
-> (pf -> pf -> pf)
-> pf
-> pf
-> (pf, Map pf pf, Integer)
-> (pf, Map pf pf, Integer)
subcnf (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
orcnf pf -> pf -> pf
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.|.) pf
p pf
q (pf, Map pf pf, Integer)
trip
      co pf
_ BinOp
_ pf
_ = (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
maincnf (pf, Map pf pf, Integer)
trip

subcnf :: (IsPropositional pf, NumAtom (AtomOf pf)) =>
          ((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
       -> (pf -> pf -> pf)
       -> pf
       -> pf
       -> (pf, Map pf pf, Integer)
       -> (pf, Map pf pf, Integer)
subcnf :: forall pf.
(IsPropositional pf, NumAtom (AtomOf pf)) =>
((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
-> (pf -> pf -> pf)
-> pf
-> pf
-> (pf, Map pf pf, Integer)
-> (pf, Map pf pf, Integer)
subcnf (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
sfn pf -> pf -> pf
op pf
p pf
q (pf
_fm,Map pf pf
defs,Integer
n) =
  let (pf
fm1,Map pf pf
defs1,Integer
n1) = (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
sfn (pf
p,Map pf pf
defs,Integer
n) in
  let (pf
fm2,Map pf pf
defs2,Integer
n2) = (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
sfn (pf
q,Map pf pf
defs1,Integer
n1) in
  (pf -> pf -> pf
op pf
fm1 pf
fm2, Map pf pf
defs2, Integer
n2)

-- | Version that guarantees 3-CNF.
defcnf3 :: forall pf. (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> pf
defcnf3 :: forall pf.
(JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
pf -> pf
defcnf3 = Set pf -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj (Set pf -> pf) -> (pf -> Set pf) -> pf -> pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set (LFormula (AtomOf pf)) -> pf)
-> Set (Set (LFormula (AtomOf pf))) -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Set pf -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_disj (Set pf -> pf)
-> (Set (LFormula (AtomOf pf)) -> Set pf)
-> Set (LFormula (AtomOf pf))
-> pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LFormula (AtomOf pf) -> pf)
-> Set (LFormula (AtomOf pf)) -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((AtomOf (LFormula (AtomOf pf)) -> AtomOf pf)
-> LFormula (AtomOf pf) -> pf
forall lit1 lit2.
(JustLiteral lit1, IsLiteral lit2) =>
(AtomOf lit1 -> AtomOf lit2) -> lit1 -> lit2
convertLiteral AtomOf (LFormula (AtomOf pf)) -> AtomOf pf
AtomOf (LFormula (AtomOf pf)) -> AtomOf (LFormula (AtomOf pf))
forall a. a -> a
id)) (Set (Set (LFormula (AtomOf pf))) -> Set pf)
-> (pf -> Set (Set (LFormula (AtomOf pf)))) -> pf -> Set pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((AtomOf pf -> AtomOf (LFormula (AtomOf pf)))
-> ((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
-> pf
-> Set (Set (LFormula (AtomOf pf)))
forall pf lit.
(IsPropositional pf, JustPropositional pf, IsLiteral lit,
 JustLiteral lit, Ord lit, NumAtom (AtomOf pf)) =>
(AtomOf pf -> AtomOf lit)
-> ((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
-> pf
-> Set (Set lit)
mk_defcnf AtomOf pf -> AtomOf pf
AtomOf pf -> AtomOf (LFormula (AtomOf pf))
forall a. a -> a
id (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
andcnf3 :: pf -> Set (Set (LFormula (AtomOf pf))))

andcnf3 :: (IsPropositional pf, JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
andcnf3 :: forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
andcnf3 trip :: (pf, Map pf pf, Integer)
trip@(pf
fm,Map pf pf
_defs,Integer
_n) =
    (pf -> BinOp -> pf -> (pf, Map pf pf, Integer))
-> (pf -> (pf, Map pf pf, Integer))
-> (Bool -> (pf, Map pf pf, Integer))
-> (AtomOf pf -> (pf, Map pf pf, Integer))
-> pf
-> (pf, Map pf pf, Integer)
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional pf -> BinOp -> pf -> (pf, Map pf pf, Integer)
co (\ pf
_ -> (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
maincnf (pf, Map pf pf, Integer)
trip) (\ Bool
_ -> (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
maincnf (pf, Map pf pf, Integer)
trip) (\ AtomOf pf
_ -> (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
maincnf (pf, Map pf pf, Integer)
trip) pf
fm
    where
      co :: pf -> BinOp -> pf -> (pf, Map pf pf, Integer)
co pf
p BinOp
(:&:) pf
q = ((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
-> (pf -> pf -> pf)
-> pf
-> pf
-> (pf, Map pf pf, Integer)
-> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, NumAtom (AtomOf pf)) =>
((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
-> (pf -> pf -> pf)
-> pf
-> pf
-> (pf, Map pf pf, Integer)
-> (pf, Map pf pf, Integer)
subcnf (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
andcnf3 pf -> pf -> pf
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.&.) pf
p pf
q (pf, Map pf pf, Integer)
trip
      co pf
_ BinOp
_ pf
_ = (pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
forall pf.
(IsPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
maincnf (pf, Map pf pf, Integer)
trip

test03 :: Test
test03 :: Test
test03 =
    let input :: [[String]]
input = Set (Set (LFormula Atom)) -> [[String]]
forall a. Pretty a => Set (Set a) -> [[String]]
strings ((AtomOf (PFormula Atom) -> AtomOf (LFormula Atom))
-> ((PFormula Atom, Map (PFormula Atom) (PFormula Atom), Integer)
    -> (PFormula Atom, Map (PFormula Atom) (PFormula Atom), Integer))
-> PFormula Atom
-> Set (Set (LFormula Atom))
forall pf lit.
(IsPropositional pf, JustPropositional pf, IsLiteral lit,
 JustLiteral lit, Ord lit, NumAtom (AtomOf pf)) =>
(AtomOf pf -> AtomOf lit)
-> ((pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer))
-> pf
-> Set (Set lit)
mk_defcnf AtomOf (PFormula Atom) -> AtomOf (LFormula Atom)
Atom -> Atom
forall a. a -> a
id (PFormula Atom, Map (PFormula Atom) (PFormula Atom), Integer)
-> (PFormula Atom, Map (PFormula Atom) (PFormula Atom), Integer)
forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
(pf, Map pf pf, Integer) -> (pf, Map pf pf, Integer)
andcnf3 PFormula Atom
testfm :: Set (Set (LFormula Atom)))
        expected :: [[String]]
expected = [[String
"p_2"],
                    [String
"s"],
                    [String
"p_2",String
"¬p"],
                    [String
"p_2",String
"¬p_1"],
                    [String
"q",String
"¬p_1"],
                    [String
"¬p_1",String
"¬r"],
                    [String
"p",String
"p_1",String
"¬p_2"],
                    [String
"p_1",String
"r",String
"¬q"]] in
    Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> [[String]] -> [[String]] -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"defcnf1 (p. 77)" [[String]]
expected [[String]]
input

testDefCNF :: Test
testDefCNF :: Test
testDefCNF = String -> Test -> Test
TestLabel String
"DefCNF" ([Test] -> Test
TestList [Test
test01, Test
test02, Test
test03])