Language.Fixpoint.SmtLib2

This module contains an SMTLIB2 interface for 1. checking the validity, and, 2. computing satisfying assignments for formulas. By implementing a binary interface over the SMTLIB2 format defined at http://www.smt-lib.org/ http://www.grammatech.com/resource/smt/SMTLIBTutorial.pdf

Commands

data Command

Commands issued to SMT engine

Constructors

Push

Pop

CheckSat

Declare Symbol [Sort] Sort

Define Sort

Assert (Maybe Int) Pred

Distinct [Expr]

GetValue [Symbol]

Instances

Eq Command

Show Command

SMTLIB2 Command

Inputable Command

Inputable [Command]

Responses

data Response

Responses received from SMT engine

Constructors

Ok

Sat

Unsat

Unknown

Values [(Symbol, Raw)]

Error Raw

Instances

Eq Response

Show Response

Typeclass for SMTLIB2 conversion

class SMTLIB2 a where

AST Conversion ---------------------------------------------------

Types that can be serialized

Methods

smt2 :: a -> Text

Instances

SMTLIB2 Symbol

SMTLIB2 LocSymbol

SMTLIB2 Pred

SMTLIB2 Expr

SMTLIB2 Bop

SMTLIB2 Brel

SMTLIB2 Constant

SMTLIB2 SymConst

SMTLIB2 Sort

SMTLIB2 Command

Creating and killing SMTLIB2 Process

data Context

Information about the external SMT process

Constructors

Ctx

Fields

pId :: ProcessHandle

cIn :: Handle

cOut :: Handle

cLog :: Maybe Handle

verbose :: Bool

makeContext :: SMTSolver -> IO Context

SMT Context ---------------------------------------------------------

makeContextNoLog :: SMTSolver -> IO Context

cleanupContext :: Context -> IO ExitCode

Execute Queries

command :: Context -> Command -> IO Response

SMT IO --------------------------------------------------------------

smtWrite :: Context -> Text -> IO ()

smt_set_funs :: HashMap Symbol Raw