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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Solver.Types

Synopsis

Documentation

type CId = Integer Source

Dramatis Personae

type CSucc = CId -> [CId] Source

type CMap a = HashMap CId a Source

type KVRead = HashMap KVar [CId] Source

type DepEdge = (CId, CId, [CId]) Source

data Slice Source

Constructors

Slice 

Fields

slKVarCs :: [CId]

CIds that transitively "reach" below

slConcCs :: [CId]

CIds with Concrete RHS

slEdges :: [DepEdge]

Dependencies between slKVarCs

Instances

data CGraph Source

Constructors

CGraph 

Fields

gEdges :: [DepEdge]
 
gRanks :: CMap Int
 
gSucc :: CSucc
 
gSccs :: Int
 

lookupCMap :: (?callStack :: CallStack) => CMap a -> CId -> a Source

CMap API -------------------------------------------------------------