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

Safe Haskell	Safe
Language	Haskell98

SMTLib2

Documentation

newtype Script Source

Constructors

Script [Command]

Instances

PP Script Source

data Binder Source

Constructors

Bind
Fields bindVar :: Name bindType :: Type

Instances

Eq Binder Source
Data Binder Source
Ord Binder Source
Show Binder Source
PP Binder Source

data Defn Source

Constructors

Defn
Fields defVar :: Name defExpr :: Expr

Instances

Eq Defn Source
Data Defn Source
Ord Defn Source
Show Defn Source
PP Defn Source

data Type Source

Constructors

TApp Ident [Type]
TVar Name

Instances

Eq Type Source
Data Type Source
Ord Type Source
Show Type Source
IsString Type Source
PP Type Source

data Expr Source

Constructors

Lit Literal
App Ident (Maybe Type) [Expr]
Quant Quant [Binder] Expr
Let [Defn] Expr
Annot Expr [Attr]

Instances

Eq Expr Source
Fractional Expr Source
Data Expr Source
Num Expr Source
Ord Expr Source
Show Expr Source
IsString Expr Source
PP Expr Source

newtype Name Source

Constructors

Instances

Eq Name Source
Data Name Source
Ord Name Source
Show Name Source
IsString Name Source
PP Name Source

data Ident Source

Constructors

I Name [Integer]

Instances

Eq Ident Source
Data Ident Source
Ord Ident Source
Show Ident Source
IsString Ident Source
PP Ident Source

data Quant Source

Constructors

Exists
Forall

Instances

Eq Quant Source
Data Quant Source
Ord Quant Source
Show Quant Source
PP Quant Source

data Literal Source

Constructors

LitBV Integer Integer	value, width (in bits)
LitNum Integer
LitFrac Rational
LitStr String

Instances

Eq Literal Source
Data Literal Source
Ord Literal Source
Show Literal Source
PP Literal Source

data Attr Source

Constructors

Attr
Fields attrName :: Name attrVal :: Maybe AttrVal

Instances

Eq Attr Source
Data Attr Source
Ord Attr Source
Show Attr Source
PP Attr Source

type AttrVal = Expr Source

data InfoFlag Source

Constructors

InfoAllStatistics
InfoErrorBehavior
InfoName
InfoAuthors
InfoVersion
InfoStatus
InfoReasonUnknown
InfoAttr Attr

Instances

Data InfoFlag Source
PP InfoFlag Source

app :: Ident -> [Expr] -> Expr Source

class PP t where Source

Methods

pp :: t -> Doc Source

Instances