0N/A{- |

3364N/AModule : $Header$

0N/ADescription : Abstract syntax for propositional logic extended with QBFs

0N/ACopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010

0N/ALicense : GPLv2 or higher, see LICENSE.txt

0N/A

0N/AMaintainer : <jonathan.von_schroeder@dfki.de>

0N/AStability : experimental

0N/APortability : portable

0N/A

0N/ADefinition of abstract syntax for propositional logic extended with QBFs

0N/A

0N/A Ref.

0N/A <http://en.wikipedia.org/wiki/Propositional_logic>

0N/A <http://www.voronkov.com/lics.cgi>

0N/A-}

0N/A

0N/Amodule QBF.AS_BASIC_QBF

1472N/A ( FORMULA (..) -- datatype for Propositional Formulas

1472N/A , BASICITEMS (..) -- Items of a Basic Spec

1472N/A , BASICSPEC (..) -- Basic Spec

0N/A , SYMBITEMS (..) -- List of symbols

0N/A , SYMB (..) -- Symbols

0N/A , SYMBMAPITEMS (..) -- Symbol map

0N/A , SYMBORMAP (..) -- Symbol or symbol map

0N/A , PREDITEM (..) -- Predicates

0N/A , isPrimForm

1123N/A , ID (..)

1123N/A ) where

1123N/A

1123N/Aimport Common.Id as Id

1123N/Aimport Common.Doc

0N/Aimport Common.DocUtils

2790N/Aimport Common.Keywords

3364N/Aimport Common.AS_Annotation as AS_Anno

2790N/A

3364N/Aimport qualified Data.List as List

2790N/Aimport Data.Maybe (isJust)

0N/A

0N/A-- DrIFT command

2790N/A{-! global: GetRange !-}

2790N/A

3364N/A-- | predicates = propositions

0N/Adata PREDITEM = PredItem [Id.Token] Id.Range

0N/A deriving Show

0N/A

0N/Anewtype BASICSPEC = BasicSpec [AS_Anno.Annoted BASICITEMS]

0N/A deriving Show

0N/A

0N/Adata BASICITEMS =

0N/A PredDecl PREDITEM

0N/A | AxiomItems [AS_Anno.Annoted FORMULA]

0N/A -- pos: dots

0N/A deriving Show

3393N/A

0N/A-- | Datatype for QBF formulas

0N/Adata FORMULA =

3393N/A FalseAtom Id.Range

1123N/A -- pos: "False

3364N/A | TrueAtom Id.Range

3393N/A -- pos: "True"

3393N/A | Predication Id.Token

3393N/A -- pos: Propositional Identifiers

3393N/A | Negation FORMULA Id.Range

3393N/A -- pos: not

3393N/A | Conjunction [FORMULA] Id.Range

2790N/A -- pos: "/\"s

3393N/A | Disjunction [FORMULA] Id.Range

3393N/A -- pos: "\/"s

3393N/A | Implication FORMULA FORMULA Id.Range

3393N/A -- pos: "=>"

2790N/A | Equivalence FORMULA FORMULA Id.Range

2790N/A -- pos: "<=>"

2790N/A | ForAll [Id.Token] FORMULA Id.Range

2790N/A | Exists [Id.Token] FORMULA Id.Range

2790N/A deriving (Show, Ord)

2790N/A

2790N/Adata ID = ID Id.Token (Maybe Id.Token)

2790N/A

2790N/Ainstance Eq ID where

3364N/A ID t1 (Just t2) == ID t3 (Just t4) =

3364N/A ((t1 == t3) && (t2 == t4))

3364N/A || ((t2 == t3) && (t1 == t4))

3364N/A ID t1 Nothing == ID t2 t3 = (t1 == t2) || (Just t1 == t3)

3364N/A ID _ (Just _) == ID _ Nothing = False

2790N/A

0N/A-- two QBFs are equivalent if bound variables

0N/A-- can be renamed such that the QBFs are equal

0N/AqbfMakeEqual :: Maybe [ID] -> FORMULA -> [Id.Token]

2790N/A -> FORMULA -> [Id.Token] -> Maybe [ID]

2790N/AqbfMakeEqual (Just ids) f ts f1 ts1 = if length ts /= length ts1 then

3364N/A Nothing

3364N/A else case (f, f1) of

0N/A (Predication t, Predication t1) -> if t == t1 then Just ids else

0N/A if t `elem` ts && t1 `elem` ts1 then

0N/A if ID t (Just t1) `elem` ids then

Just ids

else

if ID t Nothing `notElem` ids && ID t1 Nothing `notElem` ids then

Just (ID t (Just t1) : ids)

else

Nothing

else Nothing

(Negation f_ _, Negation f1_ _) -> qbfMakeEqual (Just ids) f_ ts f1_ ts1

(Conjunction (f_ : fs) _, Conjunction (f1_ : fs1) _) ->

if length fs /= length fs1 then Nothing else

case r of

Nothing -> Nothing

_ -> qbfMakeEqual r

(Conjunction fs nullRange) ts

(Conjunction fs1 nullRange) ts1

where

r = qbfMakeEqual (Just ids) f_ ts f1_ ts1

(Disjunction fs r, Disjunction fs1 r1) -> qbfMakeEqual (Just ids)

(Conjunction fs r) ts (Conjunction fs1 r1) ts1

(Implication f_ f1_ _, Implication f2 f3 _) -> case r of

Nothing -> Nothing

_ -> qbfMakeEqual r f1_ ts f3 ts1

where

r = qbfMakeEqual (Just ids) f_ ts f2 ts1

(Equivalence f_ f1_ r1, Equivalence f2 f3 _) -> qbfMakeEqual (Just ids)

(Implication f_ f1_ r1) ts

(Implication f2 f3 r1) ts1

(ForAll ts_ f_ _, ForAll ts1_ f1_ _) -> case r of

Nothing -> Nothing

(Just ids_) -> Just (ids ++ filter (\ (ID x (Just y)) ->

(x `elem` ts_ && y `notElem` ts1_) ||

(x `elem` ts1_ && y `notElem` ts_)) d)

where

d = (List.\\) ids_ ids

where

r = qbfMakeEqual (Just ids) f_ (ts ++ ts_) f1_ (ts1 ++ ts1_)

(Exists ts_ f_ r, Exists ts1_ f1_ r1) -> qbfMakeEqual (Just ids)

(Exists ts_ f_ r) ts

(Exists ts1_ f1_ r1) ts1

(_1, _2) -> Nothing

qbfMakeEqual Nothing _ _ _ _ = Nothing

-- ranges are always equal (see Common/Id.hs) - thus they can be ignored

instance Eq FORMULA where

FalseAtom _ == FalseAtom _ = True

TrueAtom _ == TrueAtom _ = True

Predication t == Predication t1 = t == t1

Negation f _ == Negation f1 _ = f == f1

Conjunction xs _ == Conjunction xs1 _ = xs == xs1

Disjunction xs _ == Disjunction xs1 _ = xs == xs1

Implication f f1 _ == Implication f2 f3 _ = (f == f2) && (f1 == f3)

Equivalence f f1 _ == Equivalence f2 f3 _ = (f == f2) && (f1 == f3)

ForAll ts f _ == ForAll ts1 f1 _ = isJust (qbfMakeEqual (Just []) f ts f1 ts1)

Exists ts f _ == Exists ts1 f1 _ = isJust (qbfMakeEqual (Just []) f ts f1 ts1)

_ == _ = False

data SYMBITEMS = SymbItems [SYMB] Id.Range

-- pos: SYMB_KIND, commas

deriving (Show, Eq)

newtype SYMB = SymbId Id.Token

-- pos: colon

deriving (Show, Eq)

data SYMBMAPITEMS = SymbMapItems [SYMBORMAP] Id.Range

-- pos: SYMB_KIND, commas

deriving (Show, Eq)

data SYMBORMAP = Symb SYMB

| SymbMap SYMB SYMB Id.Range

-- pos: "|->"

deriving (Show, Eq)

-- All about pretty printing

-- we chose the easy way here :)

instance Pretty FORMULA where

pretty = printFormula

instance Pretty BASICSPEC where

pretty = printBasicSpec

instance Pretty SYMB where

pretty = printSymbol

instance Pretty SYMBITEMS where

pretty = printSymbItems

instance Pretty SYMBMAPITEMS where

pretty = printSymbMapItems

instance Pretty BASICITEMS where

pretty = printBasicItems

instance Pretty SYMBORMAP where

pretty = printSymbOrMap

instance Pretty PREDITEM where

pretty = printPredItem

isPrimForm :: FORMULA -> Bool

isPrimForm f = case f of

TrueAtom _ -> True

FalseAtom _ -> True

Predication _ -> True

Negation _ _ -> True

_ -> False

-- Pretty printing for formulas

printFormula :: FORMULA -> Doc

printFormula frm =

let ppf p f = (if p f then id else parens) $ printFormula f

isJunctForm f = case f of

Implication _ _ _ -> False

Equivalence _ _ _ -> False

ForAll _ _ _ -> False

Exists _ _ _ -> False

_ -> True

in case frm of

FalseAtom _ -> text falseS

TrueAtom _ -> text trueS

Predication x -> pretty x

Negation f _ -> notDoc <+> ppf isPrimForm f

Conjunction xs _ -> sepByArbitrary andDoc $ map (ppf isPrimForm) xs

Disjunction xs _ -> sepByArbitrary orDoc $ map (ppf isPrimForm) xs

Implication x y _ -> ppf isJunctForm x <+> implies <+> ppf isJunctForm y

Equivalence x y _ -> ppf isJunctForm x <+> equiv <+> ppf isJunctForm y

ForAll xs y _ -> forallDoc <+> sepByArbitrary comma (map pretty xs)

<+> space

<+> ppf isJunctForm y

Exists xs y _ -> exists <+> sepByArbitrary comma (map pretty xs)

<+> space

<+> ppf isJunctForm y

sepByArbitrary :: Doc -> [Doc] -> Doc

sepByArbitrary d = fsep . prepPunctuate (d <> space)

printPredItem :: PREDITEM -> Doc

printPredItem (PredItem xs _) = fsep $ map pretty xs

printBasicSpec :: BASICSPEC -> Doc

printBasicSpec (BasicSpec xs) = vcat $ map pretty xs

printBasicItems :: BASICITEMS -> Doc

printBasicItems (AxiomItems xs) = vcat $ map pretty xs

printBasicItems (PredDecl x) = pretty x

printSymbol :: SYMB -> Doc

printSymbol (SymbId sym) = pretty sym

printSymbItems :: SYMBITEMS -> Doc

printSymbItems (SymbItems xs _) = fsep $ map pretty xs

printSymbOrMap :: SYMBORMAP -> Doc

printSymbOrMap (Symb sym) = pretty sym

printSymbOrMap (SymbMap source dest _) =

pretty source <+> mapsto <+> pretty dest

printSymbMapItems :: SYMBMAPITEMS -> Doc

printSymbMapItems (SymbMapItems xs _) = fsep $ map pretty xs