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

Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Types.Graphs

Contents

Graphs
Components
Printing

Description

This module contains the types for representing dependency graphs between kvars and constraints.

Synopsis

Graphs

data CVertex Source

Constructors

KVar KVar	real kvar vertex
DKVar KVar	dummy to ensure each kvar has a successor
Cstr Integer	constraint-id which creates a dependency

Instances

Eq CVertex Source
Ord CVertex Source
Show CVertex Source
Generic CVertex Source
Hashable CVertex Source
PPrint CVertex Source
type Rep CVertex Source

type CEdge = (CVertex, CVertex) Source

type KVGraph = [(CVertex, CVertex, [CVertex])] Source

Components

type Comps a = [[a]] Source

type KVComps = Comps CVertex Source

Printing

writeGraph :: FilePath -> KVGraph -> IO () Source