liquid-fixpoint-0.4.0.0: 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

type Raw = Text Source

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

Commands

data Command Source

Commands issued to SMT engine

Constructors

Push 
Pop 
CheckSat 
Declare Symbol [Sort] Sort 
Define Sort 
Assert (Maybe Int) Pred 
Distinct [Expr] 
GetValue [Symbol] 

Instances

Responses

data Response Source

Responses received from SMT engine

Constructors

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

Instances

Typeclass for SMTLIB2 conversion

class SMTLIB2 a where Source

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

Types that can be serialized

Methods

smt2 :: a -> Text Source

Instances

SMTLIB2 Process Context

data Context Source

Information about the external SMT process

Constructors

Ctx 

Fields

pId :: ProcessHandle
 
cIn :: Handle
 
cOut :: Handle
 
cLog :: Maybe Handle
 
verbose :: Bool
 

Theory Symbol

data TheorySymbol Source

Theory Symbol

Constructors

Thy 

Fields

tsSym :: Symbol
 
tsRaw :: Raw
 
tsSort :: Sort
 

Instances