Language.Fixpoint.Smt.Interface

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) Expr

Distinct [Expr]

GetValue [Symbol]

CMany [Command]

Instances

Eq Command

Show 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

Types that can be serialized

Minimal complete definition

smt2

Methods

defunc :: a -> SMT2 a

smt2 :: a -> Text

runSmt2 :: SMTEnv -> a -> Text

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

smtenv :: SMTEnv

makeContext :: Bool -> SMTSolver -> FilePath -> IO Context

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

makeContextNoLog :: Bool -> SMTSolver -> IO Context

makeContextWithSEnv :: Bool -> SMTSolver -> FilePath -> SMTEnv -> IO Context

cleanupContext :: Context -> IO ExitCode

Execute Queries

command :: Context -> Command -> IO Response

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

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

Query API

smtDecl :: Context -> Symbol -> Sort -> IO ()

smtAssert :: Context -> Expr -> IO ()

smtCheckUnsat :: Context -> IO Bool

smtCheckSat :: Context -> Expr -> IO Bool

smtBracket :: Context -> IO a -> IO a

smtDistinct :: Context -> [Expr] -> IO ()

Theory Symbols

Check Validity

checkValid :: Bool -> FilePath -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool

type ClosedPred E = {v:Pred | subset (vars v) (keys E) } checkValid :: e:Env -> ClosedPred e -> ClosedPred e -> IO Bool

checkValidWithContext :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool

checkValids :: Bool -> FilePath -> [(Symbol, Sort)] -> [Expr] -> IO [Bool]

If you already HAVE a context, where all the variables have declared types (e.g. if you want to make MANY repeated Queries)

makeZ3Context :: FilePath -> [(Symbol, Sort)] -> IO Context