{- |

Module : $Header$

Description : Translation to conjunctive normal form

Copyright : (c) Immanuel Normann, Uni Bremen 2007

License : GPLv2 or higher, see LICENSE.txt

Maintainer : inormann@jacobs-university.de

Stability : provisional

Portability : portable

-}

module Search.CNF where

import Search.Utils.List -- fuer mapShow

import Data.List

data Term = T Connective [Term] | V Int

data Connective = And | Or | Not deriving (Eq,Show)

instance Show (Term) where

show (T c args) = "(" ++ show c ++ " " ++ (mapShow " " args) ++ ")"

show (V n) = show n

stripOff :: [Term] -> [Term]

stripOff ((T _ fs1):fs2) = fs1 ++ (stripOff fs2)

stripOff (f:fs2) = f:(stripOff fs2)

stripOff [] = []

isC :: Connective -> Term -> Bool

isC c (T a _) = c == a

isC _ _ = False

makeOrAndTree :: Term -> Term

makeOrAndTree (T And ts) = (T And (ands ++ others))

where (ands',others) = partition (isC And) ts

ands = stripOff ands'

makeOrAndTree (T Or ts) = (T Or (ands ++ ors ++ nots))

where (ands,others) = partition (isC And) ts

(ors',nots) = partition (isC Or) others

ors = stripOff ors'

makeOrAndTree f = f

isLiteral :: Term -> Bool

isLiteral (V _) = True

isLiteral (T Not [V _]) = True

isLiteral _ = False

isClause :: Term -> Bool

isClause (T Or ts) = all isLiteral ts

isClause t = isLiteral t

isCNF :: Term -> Bool

isCNF (T And ts) = all isClause ts

isCNF t = isClause t

distOr :: Term -> [Term]

distOr (T Or ((T And (f:fs1)):fs2)) =

(T Or (f:fs2)):(distOr (T Or ((T And fs1):fs2)))

distOr (T Or ((T And []):fs2)) = []

distOr f = [f]

data TermType = CNF | OrAndTree | OtherTree deriving Show

termType :: Term -> TermType

termType (T Or ((T And _):_)) = OrAndTree

termType t = if (isCNF t) then CNF else OtherTree

cnf t = case (termType t)

of CNF -> t

OrAndTree -> cnf (T And (distOr t))

OtherTree -> cnf $ makeOrAndTree $ cnfChildren t

where cnfChildren (T c ts) = (T c (map cnf ts))

cnfChildren t = t

f1 = T And [V 1,T And [V 2,V 3],V 4,T Or [V 5,V 6],T And [V 7,V 8],T Not [V 9]]

f2 = T Or [T And [V 1,T And [V 2,V 3]],V 4]

f3 = T Or [T Or [T Not [V 1],V 2,T And [V 3,V 4]],T Or [T And [T And [V 5,V 6],T Or [V 7,V 9]]]]

tt = termType

ft = makeOrAndTree