module Exercise_9 where
{-WETT-}
import Data.Maybe
import Data.List
import Data.Ord
import Data.Function
-- import Data.Array ()
import Data.Sequence ()
import Control.Arrow

type Name = String
type Valuation = [(Name,Bool)]
data Atom = T | Var Name
  deriving (Eq, Show)
data Literal = Pos Atom | Neg Atom
  deriving (Eq, Show)
data Form = L Literal | Form :&: Form | Form :|: Form
  deriving (Eq, Show)
type Clause = [Literal]
type ConjForm = [Clause]

{-T9.3.2-}
top :: Literal
top = Pos T

bottom :: Literal
bottom = Neg T

{-T9.3.3-}
clauseToForm :: Clause -> Form
clauseToForm [] = L bottom
clauseToForm ls = foldr ((:|:) . L) (L $ last ls) (init ls)

conjToForm :: ConjForm -> Form
conjToForm [] = L top
conjToForm ds = foldr ((:&:) . clauseToForm) (clauseToForm $ last ds) (init ds)

{-T9.3.4-}
substLiteral :: Valuation -> Literal -> Literal
substLiteral v l@(Pos (Var n)) = case lookup n v of
  Just b -> if b then top else bottom
  Nothing -> l
substLiteral v l@(Neg (Var n)) = case lookup n v of
  Just b -> if b then bottom else top
  Nothing -> l
substLiteral v l = l

substClause :: Valuation -> Clause -> Clause
substClause = map . substLiteral

substConj :: Valuation -> ConjForm -> ConjForm
substConj = map . substClause

{-H9.2.1-}
simpConj :: ConjForm -> ConjForm
simpConj xs= if null ls then [] else if [] `elem` ls then [[]] else ls
 where ls= [[l|l<-x, l/= bottom] |x<-xs, top `notElem` x]

--where simplify clause = if top `elem` clause then [top] else [l|l<-clause, l/= bottom] 
--ls= [simplify x|x<-xs, (simplify x)/= [top]]
{-H9.2.2-}
cnf :: Form -> ConjForm
cnf (L l)= [[l]]
cnf ((L l1) :&: (L l2))= [l1]:[l2]:[]
cnf ((L l1) :|: (L l2))= [[l1,l2]]
cnf (f1 :&: f2) = (cnf f1)++ (cnf f2)
cnf (f1 :|: f2) = [cl1++cl2|cl1<-(cnf f1), cl2<-(cnf f2)]

{-H9.2.3-}
selectV :: ConjForm -> Maybe (Name, Bool)
selectV [] = Nothing
selectV (x:xs)= if null new then selectV xs else head new
 where new= [go l|l<-x, go l/= Nothing]

go (Pos T) = Nothing
go (Neg T) = Nothing
go (Pos (Var name)) = Just (name, True)
go (Neg (Var name)) = Just (name, False)


{-H9.2.5-}

satConj :: ConjForm -> Maybe Valuation
satConj f = satConj2 f

{-
Fisrt, make use of unitPropagation to eliminates one-literal-clauses 
Check if formula contains at least one positive (negative) literal each clause
Then apply cdcl for the remaining clauses
-}
satConj2 :: ConjForm -> Maybe Valuation
satConj2 f
 |null f'= Just v
 |f'== [[]] || [] `elem` f'=Nothing
 |length f' ==1 = Just (v++[eval (head (head f'))])
--case every clause contains at least 1 positive (negative) literal -> evaluate every literals as True (False)
 |all (any (\l-> case l of
                  Pos _ -> True
                  Neg _ -> False)) f'= Just (v++(zip (allVariables f') (repeat True)))
 |all (any (\l-> case l of
                  Pos _ -> False
                  Neg _ -> True)) f'= Just (v++(zip (allVariables f') (repeat False)))
 |otherwise= let (x,_)= cdcl (zip f' (repeat [])) v in if isNothing x then Nothing else Just ((fromJust x))
 where (v, f') = unitPropagation f

{-based on CDCL - reference: page 132 https://www.cis.upenn.edu/~alur/CIS673/sat-cdcl.pdf
idea: receive a modified cnf f as parameter: each clause contains (remembers) the evaluated literals and their value, used for conflict analysis
 (notice: f doesn't contain one-literal-clauses)
 g: simplified, sorted f
 In each step: pick the shorted clause (head g) and a branching variable l  (with prioritization of frequency and purity),
then apply unitPropagation' (modified unitPropagation for modified cnf) 

 return value: (Just x, _) -> f is satisfied (SAT) with the evaluation xs
               (Nothing, vals)-> f is UNSAT, vals is the evaluations that cause conflict
			//if the branching variable in this step isn't the reason, then return (Nothing, vals), else solve the conflict
-}
cdcl :: [(Clause, Valuation)] -> Valuation -> (Maybe Valuation, Valuation)
cdcl f acc
 |null g = (Just acc, [])
 |null (fst (head g))= (Nothing, [])
 |isNothing a && null bs = cdcl (subst (neg l) g) (acc ++ [eval (neg l)])
 |isNothing a = (Nothing, bs)
 |isJust a = case cdcl (fromJust a) (acc++[eval l]++bs) of
              (Nothing, vals) -> if (not.null) (intersect ((eval l):bs) vals) then cdcl (subst (valToLit (last vals)) (fromJust a)) (acc++ bs++ [last vals, eval l])  else (Nothing, vals)
              (Just vals, _) -> (Just vals, [])
 where g= simpConj3 f
       ls= sortFrequent (head g) g
       l = head ls
       f'= subst' l g
       (a, bs)= unitPropagation' (simpConj3 f') [eval l] 


{-remove one-literal-clauses (on the beginning)
returns (valuations of the removed literals, new ConjForm)
-}
unitPropagation :: ConjForm-> (Valuation, ConjForm)
unitPropagation f
 |null f'= ([], [])
 |f' == [[]] = ([], [[]])
 |otherwise = case f' of
               ([l]:ls)-> let (vals, cjnf)= unitPropagation (subst0 l ls) in if cjnf == [[]] then ([], [[]]) else ((eval l): vals, cjnf)
               y -> ([], y)
 where f' = simpConj2 f

{-remove one-literal-clauses
when one-literal-clause is detected -> evaluate the forced variable -> use unitPropagationAux
vs: an Accumulator, remember all the valuations in individual step, the braching variable is on the beginning. If a clause is reduced by a variable in this step, it won't have to remmeber any more
return: (Just _, [] ) when satisfied, otherwise (Nothing, conflict Analysis) 
-}
unitPropagation':: [(Clause, Valuation)]-> [(Name, Bool)] -> (Maybe [(Clause, Valuation)], Valuation) --(Maybe Valuation, [(Clause, Valuation)])
unitPropagation' f vs
 |null f'= (Just [], [])
 |length f'== 1 && null (fst (head f'))= (Nothing, [])   -- == [([], x)]chua chac
 |otherwise = case f' of
               (([l1], val1):ls) -> let (a, b)= unitPropagationAux l1 val1 (tail f') vs in if isNothing a then (a, b) else let (c, d)= (unitPropagation' (fromJust a) (vs++ [eval l1])) in if isNothing c then (c,d) else (c, (eval l1):d)
               f'' -> (Just f'', [])
 where f' = simpConj3 f

--auxiliary function fo unitPropagation', it helps to identify conflict
unitPropagationAux :: Literal -> Valuation -> [(Clause, Valuation)]-> [(Name, Bool)] -> (Maybe [(Clause, Valuation)], Valuation) -- (Maybe Valuation, [(Clause, Valuation)])
unitPropagationAux l1 v1 [] vs= (Just [], [])
unitPropagationAux l1 v1 ((clause, val):fs) vs 
 |null cl = (Nothing, conflictAna v1 val vs)
-- |null cl = (Nothing,(if null v1 then [] else [neg' (head v1)])++ (if null val then [] else [neg' (head val)]) )
 |cl == [top] = unitPropagationAux l1 v1 fs vs
 |otherwise= let (a, bs)= unitPropagationAux l1 v1 fs vs in if isNothing a then (a, bs) else (Just ((cl, vals):(fromJust a)), [])
 where (cl, vals)= if or[v `elem` val|v<-vs] then substAux l1 (clause, val)  else substAux' l1 (clause, val)

{-
xs: evaluated variables in individual step, cause after choosing a branching variable
return value: 
 []      : conflict is caused in this step, the previous ones don't affect
 x:y:z:[]: z is the value which have to be set after evaluating x or y (the closer one is chosen //by implementation in function cdcl)
-}
conflictAna :: Valuation -> Valuation -> Valuation -> Valuation
conflictAna v1 v2 vs 
 |null v1 || null v2 = []
 |length v1 == 1 && length v2 == 1 = []
 |length v1 == 1 && length v2 == 2 = (head v2):(neg' (head xs)):[]
 |length v1 == 2 && length v2 == 1 = (head v1):(neg' (head xs)):[] 
 |length v1 == 2 && length v2 == 2 = (head v1): (head v2): (neg' (head xs)): []
 |otherwise = []
 where xs= intersect vs (v1++v2)

--an optimized version of simpConj, which returns [[]] immediately when empty clause is recognized
--returns a sorted cnf
simpConj2 :: ConjForm -> ConjForm
simpConj2 [] = []
simpConj2 (x:xs)
 |top `elem` x= simpConj2 xs
 |null x= [[]]
 |otherwise= case nub [l|l<-x, l/= bottom] of
              [] -> [[]]
              a -> insertBy (comparing length) a (simpConj2 xs)

--same as simpConj2, but used for modified ConjForm
--used insertBy to make sure the return formula is sorted
simpConj3 :: [(Clause, Valuation)] -> [(Clause, Valuation)]
simpConj3 [] = []
simpConj3 ((cl, val):xs)
 |top `elem` cl= simpConj3 xs
 |null cl = [([], val)]
 |otherwise= case nub [l|l<-cl, l/= bottom] of
              [] -> [([], val)]
              a -> insertBy (comparing (length.fst)) (a, val) (simpConj3 xs)

eval (Pos (Var name)) = (name, True)
eval (Neg (Var name)) = (name, False)

-- a modified version of substClause, returns [top] when top is found, eliminates bottom
substClause2 :: Valuation -> Clause -> Clause
substClause2 _ []= []
substClause2 val (l:ls)= case (substLiteral val l) of
                          Pos T-> [top]
                          Neg T-> (substClause2 val ls)
                          l' -> let x= (substClause2 val ls) in if x==[Pos T] then [top] else  l':x
--below are different functions for substituting a literal in a ConjForm
--same as substConj but receive a literal parameter
subst0 :: Literal -> ConjForm -> ConjForm
subst0 (Pos (Var name)) g= substConj [(name, True)] g
subst0 (Neg (Var name)) g= substConj [(name, False)] g

--used for modified cnf
subst :: Literal -> [(Clause , Valuation)] -> [(Clause, Valuation)]
subst l []= []
subst l ((cl, val):gs)
 |null x= [([], val)]
 |x== [top] = subst l gs
 |otherwise= (x, val):(subst l gs)
 where x= substClause2 [eval l] cl 
--subst (Pos (Var name)) g= map (\(cl, val) -> (substClause2 [(name, True)] cl,val)) g
--subst (Neg (Var name)) g= map (\(cl, val) -> (substClause2 [(name, False)] cl,val)) g

substAux l (cl, val)=(substClause2 [eval l] cl,val)

--used for modified cnf, each clause must 'remember' the evaluated literals (maximum 2 literals each clause, the further ones are ignored)
subst' :: Literal -> [(Clause , Valuation)] -> [(Clause, Valuation)]
subst' l []= []
subst' l (g:gs)
 |null cl= [([], val)]
 |cl==[top] = subst' l gs
 |otherwise= (cl, val):(subst' l gs)
 where (cl, val)= substAux' l g
--subst' l g = map (substAux' l) g  --inefficient

--auxiliary function for subst'
substAux' :: Literal -> (Clause, Valuation)-> (Clause, Valuation)
substAux' l (cl, val)=  if ((neg l) `elem` cl) then (substClause2 [eval l] cl,if length val >= 2 then (tail val)++[eval l] else val ++ [eval l]) else (substClause2 [eval l] cl, val)


neg :: Literal -> Literal
neg (Pos a) = (Neg a)
neg (Neg a) = (Pos a)

neg' :: (Name, Bool) -> (Name, Bool)
neg' (x, b)= (x, not b)

--sort literals in a clause with respect to their frequency and purity in g
sortFrequent:: (Clause, Valuation) -> [(Clause, Valuation)] -> [Literal]
sortFrequent (cl, val) g
 |length cl == 1 = cl
 |otherwise=  map fst (sortBy (compare `on` snd) [(l,length [1|x<- g, l `notElem` (fst x) ])|l<-cl ])
--  where isPure lit= all (notElem (neg lit)) g
-- |otherwise=  map fst (sortOn snd [(l,if l `elem` (pureLiteral g) then -1 else length [1|x<- g, l `notElem` x])|l<-cl ])

--list out all variables of the formula
allVariables :: ConjForm -> [Name]
allVariables []= []
allVariables xs= allVariablesAcc xs []
 where allVariablesAcc [] ys= ys
       allVariablesAcc (x:xs) ys= allVariablesAcc xs (nub(ys ++ (map name x)))


name :: Literal -> Name
name (Pos (Var str))= str
name (Neg (Var str))= str

isPos (Pos _)= True
isPos (Neg _)= False

valToLit :: (Name, Bool)-> Literal 
valToLit (name, b)= if b then Pos (Var name) else Neg (Var name)


{-
--old version, used only DPLL (no CDCL)
satConj :: ConjForm -> Maybe Valuation
satConj f = satConj2 (sortOn length f)


satConj2 :: ConjForm -> Maybe Valuation
satConj2 f
 |null f'= Just []
 |f'== [[]] || [] `elem` f'=Nothing
 |length f' ==1 = Just [eval (head (head f'))]
 |all (any (\l-> case l of
                  Pos _ -> True
                  Neg _ -> False)) f'= Just (zip (allVariables f') (repeat True))
 |all (any (\l-> case l of
                  Pos _ -> False
                  Neg _ -> True)) f'= Just (zip (allVariables f') (repeat False))
 |otherwise = smpf
 where f' = simpConj2 f
       smpf = (simplForm (sortFrequent (head f') f') [] f')
--       pure = pureLiteral f'
--       smpf = if isNothing findOL then (simplForm (head f') f') else (simplForm (fromJust findOL) f')
--       findOL= oneLiteral f'

--an optimized version of simpConj, which returns [[]] immediately when empty clause is recognized
simpConj2 :: ConjForm -> ConjForm
simpConj2 [] = []
simpConj2 (x:xs)
 |top `elem` x= simpConj2 xs
 |null x= [[]]
 |otherwise= case nub [l|l<-x, l/= bottom] of
              [] -> [[]]
              a -> insertBy (comparing length) a (simpConj2 xs)

 
simplForm :: Clause -> Valuation -> ConjForm ->Maybe Valuation
simplForm [] val f' = if isSatisfied f' then Just val else Nothing
simplForm (l:ls) val f'= if isJust short then Just ((eval l): (val ++ (fromJust short))) else (simplForm ls ((eval (neg l)):val) (subst (neg l)f')) 
 where short= (satConj2(simpConj2 (subst l f')))

eval (Pos (Var name)) = (name, True)
eval (Neg (Var name)) = (name, False)

substClause2 :: Valuation -> Clause -> Clause
substClause2 _ []= []
substClause2 val (l:ls)= case (substLiteral val l) of
                          Pos T-> [top]
                          Neg T-> (substClause2 val ls)
                          l' -> let x= (substClause2 val ls) in if x==[Pos T] then [top] else  l':x


subst :: Literal -> ConjForm -> ConjForm
subst l []= []
subst l (c:cs)
 |null x= [[]]
 |x== [top] = subst l cs
 |otherwise= x:(subst l cs)
 where x= substClause2 [eval l] c
--subst (Pos (Var name)) g= substConj [(name, True)] g
--subst (Neg (Var name)) g= substConj [(name, False)] g

minimumLength :: [[a]]-> [a]
minimumLength = minimumBy (comparing length)

oneLiteral :: ConjForm -> Maybe Clause
oneLiteral = find (\cl -> length cl ==1) 

pureLiteral :: ConjForm -> [Literal]
pureLiteral [] =[]
pureLiteral (c:cs)= [l|l<-c, all (notElem (neg l)) (c:cs)] ++ pureLiteral [cl \\ c|cl<-cs]

neg :: Literal -> Literal
neg (Pos a) = (Neg a)
neg (Neg a) = (Pos a)

sortFrequent:: Clause -> ConjForm -> [Literal]
sortFrequent cl g
 |length cl == 1 = cl
 |otherwise=  map fst (sortBy (compare `on` snd) [(l,length [1|x<- g, l `notElem` x ])|l<-cl ])
--  where isPure lit= all (notElem (neg lit)) g
-- |otherwise=  map fst (sortOn snd [(l,if l `elem` (pureLiteral g) then -1 else length [1|x<- g, l `notElem` x])|l<-cl ])

allVariables :: ConjForm -> [Name]
allVariables []= []
allVariables xs= allVariablesAcc xs []
 where allVariablesAcc [] ys= ys
       allVariablesAcc (x:xs) ys= allVariablesAcc xs (nub(ys ++ (map name x)))

name :: Literal -> Name
name (Pos (Var str))= str
name (Neg (Var str))= str

isSatisfied :: ConjForm -> Bool
isSatisfied g= all (elem top) g

isPos (Pos _)= True
isPos (Neg _)= False


-}
{-H9.2.6-}
sat :: Form -> Maybe Valuation
sat f= satConj (cnf f) 

{-TTEW-}