package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module type DisjointDomain.RepresentativeCongruenceSource

Buckets defined by a coarse projection and a fine congruence. Congruent elements must have the same representative, but not vice versa (Representative would then suffice).

include Representative
include Printable.S
Sourcetype t
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
Sourceval compare : t -> t -> int
Sourceval show : t -> string
Sourceval pretty : unit -> t -> Printable.Pretty.doc
Sourceval printXml : 'a BatInnerIO.output -> t -> unit
Sourceval name : unit -> string
Sourceval to_yojson : t -> Yojson.Safe.t
Sourceval tag : t -> int

Unique ID, given by HConsed, for context identification in witness

Sourceval arbitrary : unit -> t QCheck.arbitrary
Sourceval relift : t -> t
Sourcetype elt

Type of elements, i.e. the domain of the projection function of_elt.

Sourceval of_elt : elt -> t

Projection function.

include Congruence with type elt := elt
Sourceval cong : elt -> elt -> bool

Congruence relation on elements.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct