From 69f576b054ef911c5bee5d0cafb187b2e13330cc Mon Sep 17 00:00:00 2001
From: reijix <leon.vatthauer@fau.de>
Date: Sun, 4 Jun 2023 18:11:28 +0200
Subject: [PATCH] Worked on fixing issues

---
 app/Main.hs | 28 ++++++++++++++++++++++++++--
 1 file changed, 26 insertions(+), 2 deletions(-)

diff --git a/app/Main.hs b/app/Main.hs
index e4d6308..f13f5e2 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -160,12 +160,22 @@ renameBinders f = fst $ go f []
         go f' vs = (f', vs)
 
 -- prenex normalform
+-- TODO make it so that forall has higher priority to be moved left (makes skolem functions smaller)
 makePNF :: Formula -> Formula
 makePNF form = go $ renameBinders . makeNNF $ form
     where
         go f = let f' = pnfStep f in
             if f == f' then f else go f'
         -- swapping rules
+        pnfStep (Conj phi (All x psi)) = All x (Conj phi psi)
+        pnfStep (Disj phi (All x psi)) = All x (Disj phi psi)
+        pnfStep (Conj (All x psi) phi) = All x (Conj psi phi)
+        pnfStep (Disj (All x psi) phi) = All x (Disj psi phi)
+        pnfStep (Conj phi (Exists x psi)) = Exists x (Conj phi psi)
+        pnfStep (Disj phi (Exists x psi)) = Exists x (Disj phi psi)
+        pnfStep (Conj (Exists x psi) phi) = Exists x (Conj psi phi)
+        pnfStep (Disj (Exists x psi) phi) = Exists x (Disj psi phi)
+        {-
         pnfStep (Conj phi (Exists x psi)) = Exists x (Conj phi psi)
         pnfStep (Conj phi (All x psi)) = All x (Conj phi psi)
         pnfStep (Disj phi (Exists x psi)) = Exists x (Disj phi psi)
@@ -174,6 +184,7 @@ makePNF form = go $ renameBinders . makeNNF $ form
         pnfStep (Conj (All x psi) phi) = All x (Conj psi phi)
         pnfStep (Disj (Exists x psi) phi) = Exists x (Disj psi phi)
         pnfStep (Disj (All x psi) phi) = All x (Disj psi phi)
+        -}
         -- descent rules
         pnfStep (All x f) = All x (pnfStep f)
         pnfStep (Exists x f) = Exists x (pnfStep f)
@@ -214,7 +225,7 @@ makeSkolem form = go (makePNF form) [] []
         substTermInFormula f@(All y f') x s = if x == y then f else All y (substTermInFormula f' x s)
         substTermInFormula f@(Exists y f') x s = if x == y then f else Exists y (substTermInFormula f' x s)
         substTermInFormula f _ _ = f
-        go (All x f) vs skolems = All x (go f (Var x : vs) skolems)
+        go (All x f) vs skolems = All x (go f (vs ++ [Var x]) skolems)
         go (Exists x f) vs skolems = go (substTermInFormula f x (Fun newSkolem vs)) vs (newSkolem : skolems)
             where newSkolem = fromJust $ find (`notElem` skolems) skolemFuns
         go f _ _ = f
@@ -227,12 +238,13 @@ makeCNF form = go $ makeSkolem form
             if f == f' then f else go f'
         cnfStep (Conj phi psi) = Conj (makeCNF phi) (makeCNF psi)
         cnfStep (Disj (Conj phi psi) xi) = Conj (makeCNF $ Disj phi xi) (makeCNF $ Disj psi xi)
-        --cnfStep (Disj f1 f2) = Disj (makeCNF f1) (makeCNF f2)
+        cnfStep (Disj xi (Conj phi psi)) = Conj (makeCNF $ Disj xi phi) (makeCNF $ Disj xi psi)
         cnfStep (All _ f) = makeCNF f
         cnfStep (Exists _ f) = makeCNF f
         cnfStep f = f
 
 -- create the list of clauses from a formula
+-- TODO not working correctly for `makeCNFList formula5`
 makeCNFList :: Formula -> [[Formula]]
 makeCNFList form = go $ makeCNF form
     where
@@ -347,6 +359,18 @@ formula6 = [
     [Pred "D" [Fun "a" []]],
     [Pred "Q" [Fun "a" []]]]
 
+-- Drogenschmuggel but already as clauses
+formula7 :: [[Formula]]
+formula7 = [
+    [Neg $ Pred "E" [Var "x2"], Pred "I" [Var "x2"], Pred "Z" [Fun "f" [Var "x2"]]],
+    [Neg $ Pred "E" [Var "x3"], Pred "I" [Var "x3"], Pred "S" [Var "x3", Fun "f" [Var "x3"]]],
+    [Pred "D" [Fun "c" []]],
+    [Pred "E" [Fun "c" []]],
+    [Neg $ Pred "S" [Fun "c" [], Var "y"], Pred "D" [Var "y"]],
+    [Neg $ Pred "I" [Var "x4"], Neg $ Pred "D" [Var "x4"]],
+    [Neg $ Pred "Z" [Var "x5"], Neg $ Pred "D" [Var "x5"]]
+    ]
+
 main :: IO ()
 main = do
     putStrLn $ "Now making NNF of formula: " ++ show formula1