liquid-fixpoint-0.7.0.7: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Smt.Interface

Contents

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

Responses

data Response Source #

Responses received from SMT engine

Constructors

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

Typeclass for SMTLIB2 conversion

class SMTLIB2 a where Source #

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

Minimal complete definition

smt2

Methods

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

Creating and killing SMTLIB2 Process

data Context Source #

Information about the external SMT process

Constructors

Ctx 

Fields

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)