Copyright | (c) Jonathan von Schroeder DFKI GmbH 2010 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | <jonathan.von_schroeder@dfki.de> |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe |
QBF.AS_BASIC_QBF
Description
Definition of abstract syntax for propositional logic extended with QBFs
Ref. http://en.wikipedia.org/wiki/Propositional_logic http://www.voronkov.com/lics.cgi
Synopsis
- data FORMULA
- data BASICITEMS
- newtype BASICSPEC = BasicSpec [Annoted BASICITEMS]
- data SYMBITEMS = SymbItems [SYMB] Range
- newtype SYMB = SymbId Token
- data SYMBMAPITEMS = SymbMapItems [SYMBORMAP] Range
- data SYMBORMAP
- data PREDITEM = PredItem [Token] Range
- isPrimForm :: FORMULA -> Bool
- data ID = ID Token (Maybe Token)
Documentation
Datatype for QBF formulas
Constructors
Instances
data BASICITEMS Source #
Constructors
PredDecl PREDITEM | |
AxiomItems [Annoted FORMULA] |
Instances
Data BASICITEMS Source # | |
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BASICITEMS -> c BASICITEMS gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BASICITEMS toConstr :: BASICITEMS -> Constr dataTypeOf :: BASICITEMS -> DataType dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c BASICITEMS) dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASICITEMS) gmapT :: (forall b. Data b => b -> b) -> BASICITEMS -> BASICITEMS gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BASICITEMS -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BASICITEMS -> r gmapQ :: (forall d. Data d => d -> u) -> BASICITEMS -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BASICITEMS -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS | |
Show BASICITEMS Source # | |
Methods showsPrec :: Int -> BASICITEMS -> ShowS show :: BASICITEMS -> String showList :: [BASICITEMS] -> ShowS | |
GetRange BASICITEMS Source # | |
Pretty BASICITEMS Source # | |
Constructors
BasicSpec [Annoted BASICITEMS] |
Instances
Instances
Instances
Eq SYMB Source # | |
Data SYMB Source # | |
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMB -> c SYMB gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMB dataTypeOf :: SYMB -> DataType dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SYMB) dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB) gmapT :: (forall b. Data b => b -> b) -> SYMB -> SYMB gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB -> r gmapQ :: (forall d. Data d => d -> u) -> SYMB -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB -> m SYMB gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB -> m SYMB gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB -> m SYMB | |
Ord SYMB Source # | |
Show SYMB Source # | |
GetRange SYMB Source # | |
Pretty SYMB Source # | |
data SYMBMAPITEMS Source #
Constructors
SymbMapItems [SYMBORMAP] Range |
Instances
Instances
Eq SYMBORMAP Source # | |
Data SYMBORMAP Source # | |
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMBORMAP -> c SYMBORMAP gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMBORMAP toConstr :: SYMBORMAP -> Constr dataTypeOf :: SYMBORMAP -> DataType dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SYMBORMAP) dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMBORMAP) gmapT :: (forall b. Data b => b -> b) -> SYMBORMAP -> SYMBORMAP gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMBORMAP -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMBORMAP -> r gmapQ :: (forall d. Data d => d -> u) -> SYMBORMAP -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMBORMAP -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP | |
Ord SYMBORMAP Source # | |
Show SYMBORMAP Source # | |
GetRange SYMBORMAP Source # | |
Pretty SYMBORMAP Source # | |
predicates = propositions
Instances
Data PREDITEM Source # | |
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PREDITEM -> c PREDITEM gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PREDITEM toConstr :: PREDITEM -> Constr dataTypeOf :: PREDITEM -> DataType dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c PREDITEM) dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PREDITEM) gmapT :: (forall b. Data b => b -> b) -> PREDITEM -> PREDITEM gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PREDITEM -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PREDITEM -> r gmapQ :: (forall d. Data d => d -> u) -> PREDITEM -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> PREDITEM -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM | |
Show PREDITEM Source # | |
GetRange PREDITEM Source # | |
Pretty PREDITEM Source # | |
isPrimForm :: FORMULA -> Bool Source #
Instances
Eq ID Source # | |
Data ID Source # | |
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ID -> c ID gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ID dataTypeOf :: ID -> DataType dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ID) dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ID) gmapT :: (forall b. Data b => b -> b) -> ID -> ID gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ID -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ID -> r gmapQ :: (forall d. Data d => d -> u) -> ID -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ID -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ID -> m ID gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ID -> m ID gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ID -> m ID | |
GetRange ID Source # | |