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

Safe Haskell	Safe
Language	Haskell98

SMTLib1

Synopsis

Documentation

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 Conn Source

Constructors

Not
Implies
And
Or
Xor
Iff
IfThenElse

Instances

Eq Conn Source
Data Conn Source
Ord Conn Source
Show Conn Source
PP Conn 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
Data Formula Source
Ord Formula Source
Show Formula Source
PP Formula Source

type Sort = Ident Source

data Binder Source

Constructors

Bind
Fields bindVar :: Name bindSort :: Sort

Instances

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

data Term Source

Constructors

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

Instances

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

data Literal Source

Constructors

LitNum Integer
LitFrac Rational
LitStr String

Instances

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

data Annot Source

Constructors

Attr
Fields attrName :: Name attrVal :: Maybe String

Instances

Eq Annot Source
Data Annot Source
Ord Annot Source
Show Annot Source
PP Annot Source

data FunDecl Source

Constructors

FunDecl
Fields funName :: Ident funArgs :: [Sort] funRes :: Sort funAnnots :: [Annot]

Instances

Data FunDecl Source
PP FunDecl Source

data PredDecl Source

Constructors

PredDecl
Fields predName :: Ident predArgs :: [Sort] predAnnots :: [Annot]

Instances

Data PredDecl Source
PP PredDecl Source

data Status Source

Constructors

Sat
Unsat
Unknown

Instances

Data Status Source
PP Status 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
PP Command Source

data Script Source

Constructors

Script
Fields scrName :: Ident scrCommands :: [Command]

Instances

PP Script 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

Methods

pp :: t -> Doc Source

Instances