Language.Fixpoint.Smt.Interface

Commands

data Command

Responses

data Response

Typeclass for SMTLIB2 conversion

class SMTLIB2 a

Creating and killing SMTLIB2 Process

data Context

makeContext

makeContextNoLog

makeContextWithSEnv

cleanupContext

Execute Queries

command

smtWrite

Query API

smtDecl

smtAssert

smtCheckUnsat

smtCheckSat

smtBracket

smtDistinct

Theory Symbols

Check Validity

checkValid

checkValidWithContext

checkValids

makeZ3Context