liquid-fixpoint-0.7.0.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

Cstr !Integer

constraint-id which creates a dependency

data KVGraph Source #

Constructors

KVGraph 

Fields

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 # 

Methods

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

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

Show Slice Source # 

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 # 

Methods

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

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

Show Rank Source # 

Methods

showsPrec :: Int -> Rank -> ShowS #

show :: Rank -> String #

showList :: [Rank] -> ShowS #

PPrint Rank Source # 

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