smtLib-1.0.7: 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
  - pp :: t -> Doc

# Documentation

newtype Name Source

Constructors

N String |

Instances

Eq 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 |
Ord Ident Source |
Show Ident Source |
IsString Ident Source |
PP Ident Source |

data Quant Source

Constructors

Exists |
Forall |

Instances

Eq 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 |
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 |
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 |
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 |
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 |
Ord Literal Source |
Show Literal Source |
PP Literal Source |

data Annot Source

Constructors

Attr |

Fields

attrName :: Name
attrVal :: Maybe String

Instances

Eq 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

PP FunDecl Source |

data PredDecl Source

Constructors

PredDecl |

Fields

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

Instances

PP PredDecl Source |

data Status Source

Constructors

Sat |
Unsat |
Unknown |

Instances

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

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

PP Script Source |
PP Command Source |
PP Status Source |
PP PredDecl Source |
PP FunDecl Source |
PP Annot Source |
PP Literal Source |
PP Term Source |
PP Binder Source |
PP Formula Source |
PP Conn Source |
PP Quant Source |
PP Ident Source |
PP Name Source |