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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Smt.Types

Contents

Description

This module contains the types defining an SMTLIB2 interface.

Synopsis

Serialized Representation

Commands

data Command Source #

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

Commands issued to SMT engine

Instances
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
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
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 #

SMTLIB2 Process Context

data Context Source #

Information about the external SMT process

Constructors

Ctx