smtLib-1.0.8: A library for working with the SMTLIB format.

Safe Haskell | Safe
Language | Haskell98

SMTLib1

Synopsis

- newtype Name = N String
- data Ident = I Name [Integer]
- data Quant
  - = Exists
  - | Forall
- data Conn
  - = Not
  - | Implies
  - | And
  - | Or
  - | Xor
  - | Iff
  - | IfThenElse
- data Formula
  - = FTrue
  - | FFalse
  - | FPred Ident [Term]
  - | FVar Name
  - | Conn Conn [Formula]
  - | Quant Quant [Binder] Formula
  - | Let Name Term Formula
  - | FLet Name Formula Formula
  - | FAnnot Formula [Annot]
- type Sort = Ident
- data Binder = Bind {
  - bindVar :: Name
  - bindSort :: Sort
  }
- data Term
  - = Var Name
  - | App Ident [Term]
  - | Lit Literal
  - | ITE Formula Term Term
  - | TAnnot Term [Annot]
- data Literal
  - = LitNum Integer
  - | LitFrac Rational
  - | LitStr String
- data Annot = Attr {
  - attrName :: Name
  - attrVal :: Maybe String
  }
- data FunDecl = FunDecl {
  - funName :: Ident
  - funArgs :: [Sort]
  - funRes :: Sort
  - funAnnots :: [Annot]
  }
- data PredDecl = PredDecl {
  - predName :: Ident
  - predArgs :: [Sort]
  - predAnnots :: [Annot]
  }
- data Status
  - = Sat
  - | Unsat
  - | Unknown
- data Command
  - = CmdLogic Ident
  - | CmdAssumption Formula
  - | CmdFormula Formula
  - | CmdStatus Status
  - | CmdExtraSorts [Sort]
  - | CmdExtraFuns [FunDecl]
  - | CmdExtraPreds [PredDecl]
  - | CmdNotes String
  - | CmdAnnot Annot
- data Script = Script {
  - scrName :: Ident
  - scrCommands :: [Command]
  }
- (===) :: Term -> Term -> Formula
- (=/=) :: Term -> Term -> Formula
- (.<.) :: Term -> Term -> Formula
- (.>.) :: Term -> Term -> Formula
- tInt :: Sort
- funDef :: Ident -> [Sort] -> Sort -> Command
- constDef :: Ident -> Sort -> Command
- logic :: Ident -> Command
- assume :: Formula -> Command
- goal :: Formula -> Command
- class PP t where

# Documentation

newtype Name Source #

Constructors

N String |

Instances

Eq Name Source # |
Methods (==) :: Name -> Name -> Bool # (/=) :: Name -> Name -> Bool #
Data Name Source # |

Methods

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

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

toConstr :: Name -> Constr #

dataTypeOf :: Name -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> Name -> Name #

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

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

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

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

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

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

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

Ord Name Source # |
Methods compare :: Name -> Name -> Ordering # (<) :: Name -> Name -> Bool # (<=) :: Name -> Name -> Bool # (>) :: Name -> Name -> Bool # (>=) :: Name -> Name -> Bool # max :: Name -> Name -> Name # min :: Name -> Name -> Name #
Show Name Source # |
Methods showsPrec :: Int -> Name -> ShowS # show :: Name -> String # showList :: [Name] -> ShowS #
IsString Name Source # |
Methods fromString :: String -> Name #
PP Name Source # |
Methods pp :: Name -> Doc Source #

data Ident Source #

Constructors

I Name [Integer] |

Instances

Eq Ident Source # |
Methods (==) :: Ident -> Ident -> Bool # (/=) :: Ident -> Ident -> Bool #
Data Ident Source # |

Methods

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

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

toConstr :: Ident -> Constr #

dataTypeOf :: Ident -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> Ident -> Ident #

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

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

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

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

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

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

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

Ord Ident Source # |
Methods compare :: Ident -> Ident -> Ordering # (<) :: Ident -> Ident -> Bool # (<=) :: Ident -> Ident -> Bool # (>) :: Ident -> Ident -> Bool # (>=) :: Ident -> Ident -> Bool # max :: Ident -> Ident -> Ident # min :: Ident -> Ident -> Ident #
Show Ident Source # |
Methods showsPrec :: Int -> Ident -> ShowS # show :: Ident -> String # showList :: [Ident] -> ShowS #
IsString Ident Source # |
Methods fromString :: String -> Ident #
PP Ident Source # |
Methods pp :: Ident -> Doc Source #

data Quant Source #

Constructors

Exists |
Forall |

Instances

Eq Quant Source # |
Methods (==) :: Quant -> Quant -> Bool # (/=) :: Quant -> Quant -> Bool #
Data Quant Source # |

Methods

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

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

toConstr :: Quant -> Constr #

dataTypeOf :: Quant -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> Quant -> Quant #

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

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

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

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

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

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

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

Ord Quant Source # |
Methods compare :: Quant -> Quant -> Ordering # (<) :: Quant -> Quant -> Bool # (<=) :: Quant -> Quant -> Bool # (>) :: Quant -> Quant -> Bool # (>=) :: Quant -> Quant -> Bool # max :: Quant -> Quant -> Quant # min :: Quant -> Quant -> Quant #
Show Quant Source # |
Methods showsPrec :: Int -> Quant -> ShowS # show :: Quant -> String # showList :: [Quant] -> ShowS #
PP Quant Source # |
Methods pp :: Quant -> Doc Source #

data Conn Source #

Constructors

Not |
Implies |
And |
Or |
Xor |
Iff |
IfThenElse |

Instances

Eq Conn Source # |
Methods (==) :: Conn -> Conn -> Bool # (/=) :: Conn -> Conn -> Bool #
Data Conn Source # |

Methods

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

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

toConstr :: Conn -> Constr #

dataTypeOf :: Conn -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> Conn -> Conn #

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

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

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

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

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

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

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

Ord Conn Source # |
Methods compare :: Conn -> Conn -> Ordering # (<) :: Conn -> Conn -> Bool # (<=) :: Conn -> Conn -> Bool # (>) :: Conn -> Conn -> Bool # (>=) :: Conn -> Conn -> Bool # max :: Conn -> Conn -> Conn # min :: Conn -> Conn -> Conn #
Show Conn Source # |
Methods showsPrec :: Int -> Conn -> ShowS # show :: Conn -> String # showList :: [Conn] -> ShowS #
PP Conn Source # |
Methods pp :: Conn -> Doc Source #

data Formula Source #

Constructors

FTrue |
FFalse |
FPred Ident [Term] |
FVar Name |
Conn Conn [Formula] |
Quant Quant [Binder] Formula |
Let Name Term Formula |
FLet Name Formula Formula |
FAnnot Formula [Annot] |

Instances

Eq Formula Source # |
Methods (==) :: Formula -> Formula -> Bool # (/=) :: Formula -> Formula -> Bool #
Data Formula Source # |

Methods

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

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

toConstr :: Formula -> Constr #

dataTypeOf :: Formula -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> Formula -> Formula #

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

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

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

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

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

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

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

Ord Formula Source # |
Methods compare :: Formula -> Formula -> Ordering # (<) :: Formula -> Formula -> Bool # (<=) :: Formula -> Formula -> Bool # (>) :: Formula -> Formula -> Bool # (>=) :: Formula -> Formula -> Bool # max :: Formula -> Formula -> Formula # min :: Formula -> Formula -> Formula #
Show Formula Source # |
Methods showsPrec :: Int -> Formula -> ShowS # show :: Formula -> String # showList :: [Formula] -> ShowS #
PP Formula Source # |
Methods pp :: Formula -> Doc Source #

type Sort = Ident Source #

data Binder Source #

Constructors

Bind |

Fields

- bindVar :: Name
- bindSort :: Sort

Instances

Eq Binder Source # |
Methods (==) :: Binder -> Binder -> Bool # (/=) :: Binder -> Binder -> Bool #
Data Binder Source # |

Methods

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

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

toConstr :: Binder -> Constr #

dataTypeOf :: Binder -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> Binder -> Binder #

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

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

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

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

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

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

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

Ord Binder Source # |
Methods compare :: Binder -> Binder -> Ordering # (<) :: Binder -> Binder -> Bool # (<=) :: Binder -> Binder -> Bool # (>) :: Binder -> Binder -> Bool # (>=) :: Binder -> Binder -> Bool # max :: Binder -> Binder -> Binder # min :: Binder -> Binder -> Binder #
Show Binder Source # |
Methods showsPrec :: Int -> Binder -> ShowS # show :: Binder -> String # showList :: [Binder] -> ShowS #
PP Binder Source # |
Methods pp :: Binder -> Doc Source #

data Term Source #

Constructors

Var Name |
App Ident [Term] |
Lit Literal |
ITE Formula Term Term |
TAnnot Term [Annot] |

Instances

Eq Term Source # |
Methods (==) :: Term -> Term -> Bool # (/=) :: Term -> Term -> Bool #
Fractional Term Source # |
Methods (/) :: Term -> Term -> Term # recip :: Term -> Term # fromRational :: Rational -> Term #
Data Term Source # |

Methods

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

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

toConstr :: Term -> Constr #

dataTypeOf :: Term -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> Term -> Term #

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

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

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

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

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

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

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

Num Term Source # |
Methods (+) :: Term -> Term -> Term # (-) :: Term -> Term -> Term # (*) :: Term -> Term -> Term # negate :: Term -> Term # abs :: Term -> Term # signum :: Term -> Term # fromInteger :: Integer -> Term #
Ord Term Source # |
Methods compare :: Term -> Term -> Ordering # (<) :: Term -> Term -> Bool # (<=) :: Term -> Term -> Bool # (>) :: Term -> Term -> Bool # (>=) :: Term -> Term -> Bool # max :: Term -> Term -> Term # min :: Term -> Term -> Term #
Show Term Source # |
Methods showsPrec :: Int -> Term -> ShowS # show :: Term -> String # showList :: [Term] -> ShowS #
IsString Term Source # |
Methods fromString :: String -> Term #
PP Term Source # |
Methods pp :: Term -> Doc Source #

data Literal Source #

Constructors

LitNum Integer |
LitFrac Rational |
LitStr String |

Instances

Eq Literal Source # |
Methods (==) :: Literal -> Literal -> Bool # (/=) :: Literal -> Literal -> Bool #
Data Literal Source # |

Methods

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

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

toConstr :: Literal -> Constr #

dataTypeOf :: Literal -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> Literal -> Literal #

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

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

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

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

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

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

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

Ord Literal Source # |
Methods compare :: Literal -> Literal -> Ordering # (<) :: Literal -> Literal -> Bool # (<=) :: Literal -> Literal -> Bool # (>) :: Literal -> Literal -> Bool # (>=) :: Literal -> Literal -> Bool # max :: Literal -> Literal -> Literal # min :: Literal -> Literal -> Literal #
Show Literal Source # |
Methods showsPrec :: Int -> Literal -> ShowS # show :: Literal -> String # showList :: [Literal] -> ShowS #
PP Literal Source # |
Methods pp :: Literal -> Doc Source #

data Annot Source #

Constructors

Attr |

Fields

- attrName :: Name
- attrVal :: Maybe String

Instances

Eq Annot Source # |
Methods (==) :: Annot -> Annot -> Bool # (/=) :: Annot -> Annot -> Bool #
Data Annot Source # |

Methods

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

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

toConstr :: Annot -> Constr #

dataTypeOf :: Annot -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> Annot -> Annot #

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

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

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

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

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

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

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

Ord Annot Source # |
Methods compare :: Annot -> Annot -> Ordering # (<) :: Annot -> Annot -> Bool # (<=) :: Annot -> Annot -> Bool # (>) :: Annot -> Annot -> Bool # (>=) :: Annot -> Annot -> Bool # max :: Annot -> Annot -> Annot # min :: Annot -> Annot -> Annot #
Show Annot Source # |
Methods showsPrec :: Int -> Annot -> ShowS # show :: Annot -> String # showList :: [Annot] -> ShowS #
PP Annot Source # |
Methods pp :: Annot -> Doc Source #

data FunDecl Source #

Constructors

FunDecl |

Fields

- funName :: Ident
- funArgs :: [Sort]
- funRes :: Sort
- funAnnots :: [Annot]

Instances

Data FunDecl Source # |

Methods

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

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

toConstr :: FunDecl -> Constr #

dataTypeOf :: FunDecl -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> FunDecl -> FunDecl #

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

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

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

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

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

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

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

PP FunDecl Source # |
Methods pp :: FunDecl -> Doc Source #

data PredDecl Source #

Constructors

PredDecl |

Fields

- predName :: Ident
- predArgs :: [Sort]
- predAnnots :: [Annot]

Instances

Data PredDecl Source # |

Methods

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

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

toConstr :: PredDecl -> Constr #

dataTypeOf :: PredDecl -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> PredDecl -> PredDecl #

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

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

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

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

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

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

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

PP PredDecl Source # |
Methods pp :: PredDecl -> Doc Source #

data Status Source #

Constructors

Sat |
Unsat |
Unknown |

Instances

Data Status Source # |

Methods

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

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

toConstr :: Status -> Constr #

dataTypeOf :: Status -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> Status -> Status #

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

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

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

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

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

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

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

PP Status Source # |
Methods pp :: Status -> Doc Source #

data Command Source #

Constructors

CmdLogic Ident |
CmdAssumption Formula |
CmdFormula Formula |
CmdStatus Status |
CmdExtraSorts [Sort] |
CmdExtraFuns [FunDecl] |
CmdExtraPreds [PredDecl] |
CmdNotes String |
CmdAnnot Annot |

Instances

Data Command Source # |

Methods

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

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

toConstr :: Command -> Constr #

dataTypeOf :: Command -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> Command -> Command #

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

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

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

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

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

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

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

PP Command Source # |
Methods pp :: Command -> Doc Source #

data Script Source #

Constructors

Script |

Fields

- scrName :: Ident
- scrCommands :: [Command]

Instances

PP Script Source # |
Methods pp :: Script -> Doc Source #

(===) :: Term -> Term -> Formula Source #

(=/=) :: Term -> Term -> Formula Source #

(.<.) :: Term -> Term -> Formula Source #

For `Int`

(.>.) :: Term -> Term -> Formula Source #

For `Int`

tInt :: Sort Source #

funDef :: Ident -> [Sort] -> Sort -> Command Source #

constDef :: Ident -> Sort -> Command Source #

logic :: Ident -> Command Source #

assume :: Formula -> Command Source #

goal :: Formula -> Command Source #

class PP t where Source #

Minimal complete definition

pp

Methods

pp :: t -> Doc Source #

Instances

PP Script Source # |
Methods pp :: Script -> Doc Source #
PP Command Source # |
Methods pp :: Command -> Doc Source #
PP Status Source # |
Methods pp :: Status -> Doc Source #
PP PredDecl Source # |
Methods pp :: PredDecl -> Doc Source #
PP FunDecl Source # |
Methods pp :: FunDecl -> Doc Source #
PP Annot Source # |
Methods pp :: Annot -> Doc Source #
PP Literal Source # |
Methods pp :: Literal -> Doc Source #
PP Term Source # |
Methods pp :: Term -> Doc Source #
PP Binder Source # |
Methods pp :: Binder -> Doc Source #
PP Formula Source # |
Methods pp :: Formula -> Doc Source #
PP Conn Source # |
Methods pp :: Conn -> Doc Source #
PP Quant Source # |
Methods pp :: Quant -> Doc Source #
PP Ident Source # |
Methods pp :: Ident -> Doc Source #
PP Name Source # |
Methods pp :: Name -> Doc Source #