liquid-fixpoint-0.5.0.1: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Language.Fixpoint.Solver.Types
Synopsis
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
Fields
CIds that transitively "reach" below
CIds with Concrete RHS
Dependencies between slKVarCs
Instances
data CGraph Source
lookupCMap :: (?callStack :: CallStack) => CMap a -> CId -> a Source
CMap API -------------------------------------------------------------