Copyright | (c) Jonathan von Schroeder DFKI GmbH 2010 |
---|---|

License | GPLv2 or higher, see LICENSE.txt |

Maintainer | <jonathan.von_schroeder@dfki.de> |

Stability | experimental |

Portability | non-portable (imports Logic.Logic) |

Safe Haskell | Safe |

Sublogics for Propositional Logic

## Synopsis

- slBasicSpec :: QBFSL -> BASICSPEC -> QBFSL
- data QBFFormulae
- data QBFSL = QBFSL {}
- sublogicsMax :: QBFSL -> QBFSL -> QBFSL
- top :: QBFSL
- bottom :: QBFSL
- sublogicsAll :: [QBFSL]
- sublogicsName :: QBFSL -> String
- slSig :: QBFSL -> Sign -> QBFSL
- slForm :: QBFSL -> FORMULA -> QBFSL
- slSym :: QBFSL -> Symbol -> QBFSL
- slSymit :: QBFSL -> SYMBITEMS -> QBFSL
- slMor :: QBFSL -> Morphism -> QBFSL
- slSymmap :: QBFSL -> SYMBMAPITEMS -> QBFSL
- prSymbolM :: QBFSL -> Symbol -> Maybe Symbol
- prSig :: QBFSL -> Sign -> Sign
- prMor :: QBFSL -> Morphism -> Morphism
- prSymMapM :: QBFSL -> SYMBMAPITEMS -> Maybe SYMBMAPITEMS
- prSymM :: QBFSL -> SYMBITEMS -> Maybe SYMBITEMS
- prFormulaM :: QBFSL -> FORMULA -> Maybe FORMULA
- prBasicSpec :: QBFSL -> BASICSPEC -> BASICSPEC
- isProp :: QBFSL -> Bool
- isHC :: QBFSL -> Bool

# Documentation

data QBFFormulae Source #

types of propositional formulae

#### Instances

Eq QBFFormulae Source # | |

Defined in QBF.Sublogic (==) :: QBFFormulae -> QBFFormulae -> Bool (/=) :: QBFFormulae -> QBFFormulae -> Bool | |

Data QBFFormulae Source # | |

Defined in QBF.Sublogic gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QBFFormulae -> c QBFFormulae gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QBFFormulae toConstr :: QBFFormulae -> Constr dataTypeOf :: QBFFormulae -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c QBFFormulae) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QBFFormulae) gmapT :: (forall b. Data b => b -> b) -> QBFFormulae -> QBFFormulae gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QBFFormulae -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QBFFormulae -> r gmapQ :: (forall d. Data d => d -> u) -> QBFFormulae -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> QBFFormulae -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> QBFFormulae -> m QBFFormulae gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QBFFormulae -> m QBFFormulae gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QBFFormulae -> m QBFFormulae | |

Ord QBFFormulae Source # | |

Defined in QBF.Sublogic compare :: QBFFormulae -> QBFFormulae -> Ordering (<) :: QBFFormulae -> QBFFormulae -> Bool (<=) :: QBFFormulae -> QBFFormulae -> Bool (>) :: QBFFormulae -> QBFFormulae -> Bool (>=) :: QBFFormulae -> QBFFormulae -> Bool max :: QBFFormulae -> QBFFormulae -> QBFFormulae min :: QBFFormulae -> QBFFormulae -> QBFFormulae | |

Show QBFFormulae Source # | |

Defined in QBF.Sublogic showsPrec :: Int -> QBFFormulae -> ShowS show :: QBFFormulae -> String showList :: [QBFFormulae] -> ShowS | |

Generic QBFFormulae | |

Defined in QBF.ATC_QBF type Rep QBFFormulae :: Type -> Type from :: QBFFormulae -> Rep QBFFormulae x to :: Rep QBFFormulae x -> QBFFormulae | |

FromJSON QBFFormulae | |

Defined in QBF.ATC_QBF parseJSON :: Value -> Parser QBFFormulae parseJSONList :: Value -> Parser [QBFFormulae] | |

ToJSON QBFFormulae | |

Defined in QBF.ATC_QBF toJSON :: QBFFormulae -> Value toEncoding :: QBFFormulae -> Encoding toJSONList :: [QBFFormulae] -> Value toEncodingList :: [QBFFormulae] -> Encoding | |

ShATermConvertible QBFFormulae | |

Defined in QBF.ATC_QBF toShATermAux :: ATermTable -> QBFFormulae -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [QBFFormulae] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, QBFFormulae) fromShATermList' :: Int -> ATermTable -> (ATermTable, [QBFFormulae]) | |

type Rep QBFFormulae | |

Defined in QBF.ATC_QBF type Rep QBFFormulae = D1 ('MetaData "QBFFormulae" "QBF.Sublogic" "main" 'False) (C1 ('MetaCons "PlainFormula" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "HornClause" 'PrefixI 'False) (U1 :: Type -> Type)) |

sublogics for propositional logic

#### Instances

sublogicsAll :: [QBFSL] Source #

all sublogics

sublogicsName :: QBFSL -> String Source #

prSymMapM :: QBFSL -> SYMBMAPITEMS -> Maybe SYMBMAPITEMS Source #