liquid-fixpoint-0.9.2.5: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Fixpoint.Smt.Types

Description

This module contains the types defining an SMTLIB2 interface.

Synopsis

Serialized Representation

Commands

data Command Source #

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

Commands issued to SMT engine

Instances

Instances details
Show Command Source # 
Instance details

Defined in Language.Fixpoint.Smt.Types

Eq Command Source # 
Instance details

Defined in Language.Fixpoint.Smt.Types

Methods

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

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

Inputable Command Source # 
Instance details

Defined in Language.Fixpoint.Parse

SMTLIB2 Command Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

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

PPrint Command Source # 
Instance details

Defined in Language.Fixpoint.Smt.Types

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
Show Response Source # 
Instance details

Defined in Language.Fixpoint.Smt.Types

Eq 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 Command Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Command -> 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 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 Expr Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

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

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 Int Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Int -> 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 #

Additional information around the SMT solver backend

Constructors

Ctx 

Fields