liquid-fixpoint-0.8.10.2: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Smt.Interface

Description

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

Synopsis

Commands

data Command Source #

Types ---------------------------------------------------------------------

Commands issued to SMT engine

Instances

Instances details
Eq Command Source # 
Instance details

Defined in Language.Fixpoint.Smt.Types

Methods

(==) :: Command -> Command -> Bool #

(/=) :: Command -> Command -> Bool #

Show Command Source # 
Instance details

Defined in Language.Fixpoint.Smt.Types

PPrint Command Source # 
Instance details

Defined in Language.Fixpoint.Smt.Types

SMTLIB2 Command Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Command -> Builder Source #

Inputable Command Source # 
Instance details

Defined in Language.Fixpoint.Parse

Inputable [Command] Source # 
Instance details

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> [Command] Source #

rr' :: String -> String -> [Command] Source #

Responses

data Response Source #

Responses received from SMT engine

Constructors

Ok 
Sat 
Unsat 
Unknown 
Values [(Symbol, Text)] 
Error !Text 

Instances

Instances details
Eq Response Source # 
Instance details

Defined in Language.Fixpoint.Smt.Types

Show Response Source # 
Instance details

Defined in Language.Fixpoint.Smt.Types

Typeclass for SMTLIB2 conversion

class SMTLIB2 a where Source #

AST Conversion: Types that can be serialized ------------------------------

Methods

smt2 :: SymEnv -> a -> Builder Source #

Instances

Instances details
SMTLIB2 Int Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Int -> Builder Source #

SMTLIB2 LocSymbol Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

SMTLIB2 Symbol Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Symbol -> Builder Source #

SMTLIB2 Expr Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Expr -> Builder Source #

SMTLIB2 Bop Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Bop -> Builder Source #

SMTLIB2 Brel Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Brel -> Builder Source #

SMTLIB2 Constant Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

SMTLIB2 SymConst Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

SMTLIB2 SmtSort Source # 
Instance details

Defined in Language.Fixpoint.Smt.Theories

Methods

smt2 :: SymEnv -> SmtSort -> Builder Source #

SMTLIB2 Command Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Command -> Builder Source #

SMTLIB2 (Triggered Expr) Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

SMTLIB2 (Symbol, Sort) Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> (Symbol, Sort) -> Builder Source #

Creating and killing SMTLIB2 Process

data Context Source #

Information about the external SMT process

Constructors

Ctx 

makeContext :: Config -> FilePath -> IO Context Source #

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

Execute Queries

command :: Context -> Command -> IO Response Source #

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

Query API

smtDecls :: Context -> [(Symbol, Sort)] -> IO () Source #

smtPush :: Context -> IO () Source #

SMT Commands -----------------------------------------------------------

smtPop :: Context -> IO () Source #

SMT Commands -----------------------------------------------------------

Check Validity

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

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

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

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