module GMPSAT where

import qualified Data.Set as Set

import GMPAS

import ModalLogic

-------------------------------------------------------------------------------

-- 1. Guess Pseudovaluation H for f -- guessPV

-------------------------------------------------------------------------------

{- extract modal atoms from a given formula

- @ param f : formula

- @ return : list of modal atoms of f -}

extractMA :: Ord t => Formula t -> Set.Set (Formula t)

extractMA f =

case f of

T -> Set.empty

F -> Set.empty

Neg g -> extractMA g

Junctor g _ h -> Set.union (extractMA g) (extractMA h)

_ -> Set.singleton f

{- generate the powerset of a given set

- @ param s : set

- @ return : list of subsets of s -}

powerSet :: Ord t => Set.Set t -> [Set.Set t]

powerSet s =

if not (Set.null s)

then let (e,r) = Set.deleteFindMin s

aux = powerSet r

in (map (Set.insert e) aux) ++ aux

else [Set.empty]

{- evaluate pseudovaluation of formula

- @ param f : formula

- @ param p : the pseudovaluation, ie the positive modal atoms

- @ return : True if the pseudovaluation is good, False otherwise -}

evalPV :: Ord t => Formula t -> Set.Set (Formula t) -> Bool

evalPV f p =

case f of

T -> True

F -> False

Neg g -> not (evalPV g p)

Junctor g j h -> let jeval w x y =

case w of

And -> and [x,y]

Or -> or [x,y]

If -> or [not x,y]

Fi -> or [x, not y]

Iff -> and [or [not x, y],or [x, not y]]

in jeval j (evalPV g p) (evalPV h p)

_ -> if (Set.member f p) then True

else False

{- drop variables from the pseudovaluations

- @ param l : list of pseudovaluations

- @ return : list of pseudovaluations in l without var items -}

dropLVars :: (Ord t) => [Set.Set (Formula t)] -> [Set.Set (Formula t)]

dropLVars l =

case l of

[] -> []

x:xs -> (dropVars x):(dropLVars xs)

{- drop variables from a particular pseudovaluation

- @ param s : pseudovaluation

- @ return : pseudovaluation without var items -}

dropVars :: (Ord t) => Set.Set (Formula t) -> Set.Set (Formula t)

dropVars s =

if not (Set.null s)

then let (x,y) = Set.deleteFindMin s

aux = dropVars y

in case x of

Var _ _ -> aux

_ -> Set.insert x aux

else Set.empty

{- generate all valid pseudovaluations out of a formula

- @ param f : formula

- @ param ma : list of modal atoms of f

- @ return : list of valid pseudovaluations -}

guessPV :: Ord t => Formula t -> Set.Set (Formula t) -> [Set.Set (Formula t)]

guessPV f ma = let pv = powerSet ma

aux = filter (evalPV f) pv

in dropLVars aux

-------------------------------------------------------------------------------

-- 2. Choose a ctr. cl. Ro /= F over MA(H) s.t. H "entails" ~Ro -- contrClause

-------------------------------------------------------------------------------

-- 3. Choose a rule matching the previous contracted clause -- matchR

-------------------------------------------------------------------------------

-- 4. Guess a clause c from the premise of the matching rule -- guessClause

-------------------------------------------------------------------------------

-- 5. Recursively check that ~c(R,Rho) is satisfiable -- checkSAT

-------------------------------------------------------------------------------

{- substitute the clause literals with the formulae under the MAs and negate it

- @ param c : clause guessed at Step 4

- @ param ro : contracted clause from Step 2

- @ return : the negated clause as described above -}

negSubst :: (Show a) => Clause -> [MATV a] -> Formula a

negSubst c ro =

case c of

Cl [] ->

case ro of

[] -> T

_ -> error ("error @ GMPSAT.negSubst 1 "

++ show c ++ " " ++ show ro)

Cl (PLit _ : ll) ->

case ro of

MATV (Mapp _ ff,_):ml -> let g = negSubst (Cl ll) ml

in Junctor (Neg ff) And g

_ -> error ("error @ GMPSAT.negSubst 2 "

++ show c ++ " " ++ show ro)

Cl (NLit _ : ll) ->

case ro of

MATV (Mapp _ ff,_):ml -> let g = negSubst (Cl ll) ml

in Junctor ff And g

_ -> error ("error @ GMPSAT.negSubst 3 "

++ show c ++ " " ++ show ro)

{- main recursive function

- @ param f : formula to be checked for satisfiability

- @ return : the answer to "Is the formula Satisfiable ?" -}

checksat :: (Show a, Ord a, ModalLogic a b) => Formula a -> Bool

checksat f =

let ma = extractMA f

mav = dropVars ma

tList (Implies (p,n)) =

map MATV [(x,True)|x <- p] ++ map MATV [(y,False)|y <- n]

in any(\h->all(\ro->all(\mr->any(\cl-> let rr = tList ro

in checksat(negSubst cl rr))

(guessClause mr))

(matchR ro))

(contrClause h mav))

(guessPV f ma)

{- auxiliary function to preprocess the formula depending on the ML flag

- @ param f : formula to be preprocessed

- @ return : processed formula -}

preprocess :: (ModalLogic a b) => Formula a -> Formula a

preprocess f =

let aux = flagML f

in case f of

T -> T

F -> F

Neg ff -> Neg (preprocess ff)

Junctor f1 j f2 -> Junctor (preprocess f1) j (preprocess f2)

Mapp (Mop i Angle) ff -> if (aux == Sqr)

then Neg $ Mapp (Mop i Square) (Neg ff)

else f

Mapp (Mop i Square) ff -> if (aux == Ang)

then Neg $ Mapp (Mop i Angle) (Neg ff)

else f

_ -> f

-- preprocess formula and check satisfiability --------------------------------

{- function to preprocess formula and check satisfiability

- @ param f : starting formula

- @ return : same as "checksat" -}

checkSAT :: (ModalLogic a b, Ord a, Show a) => Formula a -> Bool

checkSAT f = let ff = preprocess f

in checksat ff

-------------------------------------------------------------------------------

-------------------------------------------------------------------------------