smtLib-1.0.7: 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 |
Ord Binder Source |
Show Binder Source |
PP Binder Source |

data Defn Source

Constructors

Defn |

Fields

defVar :: Name
defExpr :: Expr

Instances

Eq Defn Source |
Ord Defn Source |
Show Defn Source |
PP Defn Source |

data Type Source

Constructors

TApp Ident [Type] |
TVar Name |

Instances

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

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

Constructors

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

Instances

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

type AttrVal = Expr Source

data Command Source

Constructors

CmdSetLogic Name |
CmdSetOption Option |
CmdSetInfo Attr |
CmdDeclareType Name Integer |
CmdDefineType Name [Name] Type |
CmdDeclareFun Name [Type] Type |
CmdDefineFun Name [Binder] Type Expr |
CmdPush Integer |
CmdPop Integer |
CmdAssert Expr |
CmdCheckSat |
CmdGetAssertions |
CmdGetValue [Expr] |
CmdGetProof |
CmdGetUnsatCore |
CmdGetInfo InfoFlag |
CmdGetOption Name |
CmdExit |

Instances

PP Command Source |

data Option Source

Constructors

OptPrintSuccess Bool |
OptExpandDefinitions Bool |
OptInteractiveMode Bool |
OptProduceProofs Bool |
OptProduceUnsatCores Bool |
OptProduceModels Bool |
OptProduceAssignments Bool |
OptRegularOutputChannel String |
OptDiagnosticOutputChannel String |
OptRandomSeed Integer |
OptVerbosity Integer |
OptAttr Attr |

Instances

PP Option Source |

data InfoFlag Source

Constructors

InfoAllStatistics |
InfoErrorBehavior |
InfoName |
InfoAuthors |
InfoVersion |
InfoStatus |
InfoReasonUnknown |
InfoAttr Attr |

Instances

PP InfoFlag Source |

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

class PP t where Source

Methods

pp :: t -> Doc Source

Instances

PP Bool Source |
PP Integer Source |
PP Script Source |
PP Command Source |
PP InfoFlag Source |
PP Option Source |
PP Attr Source |
PP Expr Source |
PP Type Source |
PP Literal Source |
PP Defn Source |
PP Binder Source |
PP Quant Source |
PP Ident Source |
PP Name Source |