Hets - the Heterogeneous Tool Set

Copyright(c) Jonathan von Schroeder DFKI GmbH 2010
LicenseGPLv2 or higher, see LICENSE.txt
Maintainer<jonathan.von_schroeder@dfki.de>
Stabilityexperimental
Portabilitynon-portable (imports Logic.Logic)
Safe HaskellSafe

QBF.Sublogic

Description

Sublogics for Propositional Logic

Synopsis

Documentation

slBasicSpec :: QBFSL -> BASICSPEC -> QBFSL Source #

determines sublogic for basic spec

data QBFFormulae Source #

types of propositional formulae

Constructors

PlainFormula 
HornClause 

Instances

Eq QBFFormulae Source # 

Methods

(==) :: QBFFormulae -> QBFFormulae -> Bool

(/=) :: QBFFormulae -> QBFFormulae -> Bool

Data QBFFormulae Source # 

Methods

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 :: (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 # 
Show QBFFormulae Source # 

Methods

showsPrec :: Int -> QBFFormulae -> ShowS

show :: QBFFormulae -> String

showList :: [QBFFormulae] -> ShowS

data QBFSL Source #

sublogics for propositional logic

Constructors

QBFSL 

Fields

Instances

Eq QBFSL Source # 

Methods

(==) :: QBFSL -> QBFSL -> Bool

(/=) :: QBFSL -> QBFSL -> Bool

Data QBFSL Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QBFSL -> c QBFSL

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QBFSL

toConstr :: QBFSL -> Constr

dataTypeOf :: QBFSL -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c QBFSL)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QBFSL)

gmapT :: (forall b. Data b => b -> b) -> QBFSL -> QBFSL

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QBFSL -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QBFSL -> r

gmapQ :: (forall d. Data d => d -> u) -> QBFSL -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> QBFSL -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> QBFSL -> m QBFSL

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QBFSL -> m QBFSL

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QBFSL -> m QBFSL

Ord QBFSL Source # 

Methods

compare :: QBFSL -> QBFSL -> Ordering

(<) :: QBFSL -> QBFSL -> Bool

(<=) :: QBFSL -> QBFSL -> Bool

(>) :: QBFSL -> QBFSL -> Bool

(>=) :: QBFSL -> QBFSL -> Bool

max :: QBFSL -> QBFSL -> QBFSL

min :: QBFSL -> QBFSL -> QBFSL

Show QBFSL Source # 

Methods

showsPrec :: Int -> QBFSL -> ShowS

show :: QBFSL -> String

showList :: [QBFSL] -> ShowS

Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source #

Instance of Logic for propositional logc

Methods

parse_basic_sen :: QBF -> Maybe (BASICSPEC -> AParser st FORMULA) Source #

stability :: QBF -> Stability Source #

data_logic :: QBF -> Maybe AnyLogic Source #

top_sublogic :: QBF -> QBFSL Source #

all_sublogics :: QBF -> [QBFSL] Source #

bottomSublogic :: QBF -> Maybe QBFSL Source #

sublogicDimensions :: QBF -> [[QBFSL]] Source #

parseSublogic :: QBF -> String -> Maybe QBFSL Source #

proj_sublogic_epsilon :: QBF -> QBFSL -> Sign -> Morphism Source #

provers :: QBF -> [Prover Sign FORMULA Morphism QBFSL ProofTree] Source #

default_prover :: QBF -> String Source #

cons_checkers :: QBF -> [ConsChecker Sign FORMULA QBFSL Morphism ProofTree] Source #

conservativityCheck :: QBF -> [ConservativityChecker Sign FORMULA Morphism] Source #

empty_proof_tree :: QBF -> ProofTree Source #

syntaxTable :: QBF -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: QBF -> Maybe OMCD Source #

export_symToOmdoc :: QBF -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: QBF -> NameMap Symbol -> FORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: QBF -> SigMap Symbol -> Sign -> [Named FORMULA] -> Result [TCElement] Source #

omdocToSym :: QBF -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: QBF -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source #

addOMadtToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source #

addOmdocToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source #

Comorphism Prop2QBF Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Comorphism QBF2Prop QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 

sublogicsAll :: [QBFSL] Source #

all sublogics

slSig :: QBFSL -> Sign -> QBFSL Source #

determines the sublogic for a Signature

slForm :: QBFSL -> FORMULA -> QBFSL Source #

determines sublogic for formula

slSym :: QBFSL -> Symbol -> QBFSL Source #

determines the sublogic for symbols

slSymit :: QBFSL -> SYMBITEMS -> QBFSL Source #

determines the sublogic for Symbol items

slMor :: QBFSL -> Morphism -> QBFSL Source #

determines the sublogic for a morphism

slSymmap :: QBFSL -> SYMBMAPITEMS -> QBFSL Source #

determines the sublogic for symbol map items

isProp :: QBFSL -> Bool Source #

isHC :: QBFSL -> Bool Source #