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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Graph.Types

Contents

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
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

Show CVertex Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

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 #

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

data KVGraph Source #

Constructors

KVGraph 

Fields

Instances
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

Slice of relevant constraints

data Slice Source #

Constructors

Slice 

Fields

Instances
Eq Slice Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

Methods

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

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

Show Slice Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

Methods

showsPrec :: Int -> Slice -> ShowS #

show :: Slice -> String #

showList :: [Slice] -> ShowS #

Constraint Dependency Graphs

data CGraph Source #

Constructors

CGraph 

Fields

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
Eq Rank Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

Methods

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

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

Show Rank Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

Methods

showsPrec :: Int -> Rank -> ShowS #

show :: Rank -> String #

showList :: [Rank] -> ShowS #

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