package pds-reachability

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

Signature

module Stack_element = Basis.Stack_element

The decorated stack element type used by the PDS.

module Node = Types.Node

The decorated node type in the reachability structure.

module Edge = Types.Edge

The decorated edge type in the reachability structure.

module Targeted_dynamic_pop_action = Types.Targeted_dynamic_pop_action

The decorated type of targeted dynamic pop actions in this structure.

module Untargeted_dynamic_pop_action = Types.Untargeted_dynamic_pop_action

The decorated type of untargeted dynamic pop actions in this structure.

The type of the PDS reachability data structure.

include Pds_reachability_utils.Decorated_type
type t
val equal : t -> t -> bool
val compare : t -> t -> int
val show : t -> string
val to_yojson : t -> Yojson.Safe.json
val to_yojson_delta : t -> t -> Yojson.Safe.json

Produces a Yojson structure representing the contents of a latter analysis which do not appear in the former.

val empty : t

The empty PDS reachability structure.

val add_edge : Edge.t -> t -> t

Adds an edge to a reachability structure.

val has_edge : Edge.t -> t -> bool

Determines if a structure has a particular edge.

val add_untargeted_dynamic_pop_action : Node.t -> Untargeted_dynamic_pop_action.t -> t -> t

Adds an untargeted dynamic pop action to a reachability structure.

val has_untargeted_dynamic_pop_action : Node.t -> Untargeted_dynamic_pop_action.t -> t -> bool

Determines if a given untargeted dynamic pop action is present in a reachability structure.

Query functions.
val find_push_edges_by_source : Node.t -> t -> (Node.t * Stack_element.t) Batteries.Enum.t
val find_pop_edges_by_source : Node.t -> t -> (Node.t * Stack_element.t) Batteries.Enum.t
val find_nop_edges_by_source : Node.t -> t -> Node.t Batteries.Enum.t
val find_targeted_dynamic_pop_edges_by_source : Node.t -> t -> (Node.t * Targeted_dynamic_pop_action.t) Batteries.Enum.t
val find_untargeted_dynamic_pop_actions_by_source : Node.t -> t -> Untargeted_dynamic_pop_action.t Batteries.Enum.t
val find_push_edges_by_target : Node.t -> t -> (Node.t * Stack_element.t) Batteries.Enum.t
val find_pop_edges_by_target : Node.t -> t -> (Node.t * Stack_element.t) Batteries.Enum.t
val find_nop_edges_by_target : Node.t -> t -> Node.t Batteries.Enum.t
val enumerate_nodes : t -> Node.t Batteries.Enum.t
val enumerate_edges : t -> Edge.t Batteries.Enum.t
Submodules.
module Node_set : Batteries.Set.S with type elt = Node.t