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

Language.Fixpoint.Graph.Types

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

EBind !Symbol

existentially bound "ghost paramter" to solve for

Cstr !Integer

constraint-id which creates a dependency

Instances

Instances details
Generic CVertex Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

Associated Types

type Rep CVertex :: Type -> Type #

Methods

from :: CVertex -> Rep CVertex x #

to :: Rep CVertex x -> CVertex #

Show CVertex Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

Eq CVertex Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

Methods

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

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

Ord CVertex Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

Hashable CVertex Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

Methods

hashWithSalt :: Int -> CVertex -> Int #

hash :: CVertex -> Int #

PPrint CVertex Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

type Rep CVertex Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

newtype KVGraph Source #

Constructors

KVGraph 

Fields

Instances

Instances details
PPrint KVGraph Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

Components

type Comps a = [[a]] Source #

Printing

Constraints

type KVRead = HashMap KVar [SubcId] Source #

Dramatis Personae

type DepEdge = (SubcId, SubcId, [SubcId]) Source #

(Constraint id, vertex key, edges to other constraints)

The vertex key is always equal to the constraint id. The redundancy is imposed by how containers:Data.Graph requires graphs to be created.

Slice of relevant constraints

data Slice Source #

Constructors

Slice 

Fields

Instances

Instances details
Show Slice Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

Methods

showsPrec :: Int -> Slice -> ShowS #

show :: Slice -> String #

showList :: [Slice] -> ShowS #

Eq Slice Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

Methods

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

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

Constraint Dependency Graphs

data CGraph Source #

Constructors

CGraph 

Fields

  • gEdges :: [DepEdge]
     
  • gRanks :: !(CMap Int)

    Maps a constraint id to an index identifying the strongly connected component to which it belongs. The scc indices correspond with a topological ordering of the sccs.

  • gSucc :: !(CMap [SubcId])

    Tells for each constraint C, which constraints read any kvars that C writes.

    This is redundant with gEdges, so both fields need to express the exact same dependencies.

  • gSccs :: !Int

    Amount of strongly connected components

Alias for Constraint Maps

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

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

Ranks

data Rank Source #

Ranks ---------------------------------------------------------------------

Constructors

Rank 

Fields

  • rScc :: !Int

    SCC number with ALL dependencies

  • rIcc :: !Int

    SCC number without CUT dependencies

  • rTag :: !Tag

    The constraint's Tag

Instances

Instances details
Show Rank Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

Methods

showsPrec :: Int -> Rank -> ShowS #

show :: Rank -> String #

showList :: [Rank] -> ShowS #

Eq Rank Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

Methods

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

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

PPrint Rank Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

Constraint Dependencies

data CDeps Source #

Constraint Dependencies ---------------------------------------------------

Constructors

CDs 

Fields

Solver Info

data SolverInfo a b Source #

SolverInfo contains all the stuff needed to produce a result, and is the the essential ingredient of the state needed by solve_

Constructors

SI 

Fields