Module InvGenGraph.BV

Graph of signed bitvectors with less than or equal.

Parameters

module L : sig ... end

Signature

Domain with an order relation.

type graph

A graph.

val mk : term -> set -> graph

Creates a graph from a single equivalence class and its representative.

val has_svars : graph -> bool

Checks whether at least one candidate mentions a state variable.

val mine : bool -> bool -> Analysis.param -> TransSys.t -> (TransSys.t -> unit) -> (TransSys.t * graph * set * set) list

Mines a system and creates the relevant graphs.

First boolean is top_only, then two_state. Input function is applied to each subsystem. It is used to create the pruning checkers.

val clone : graph -> graph

Clones a graph.

val term_count : graph -> int

Total number of terms in the graph.

val class_count : graph -> int

Total number of classes in the graph.

val is_stale : graph -> bool

Returns true if all classes in the graph only have one candidate term.

val drop_class_member : graph -> term -> term -> unit

Drops a term from the class corresponding to a representative.

val fmt_graph_dot : Stdlib.Format.formatter -> graph -> unit

Formats a graph in dot format. Only the representatives will appear.

val fmt_graph_classes_dot : Stdlib.Format.formatter -> graph -> unit

Formats the eq classes of a graph in dot format.

val check_graph : graph -> bool

Checks that a graph makes sense. Dumps the graph and its classes in dot format in the current directory if the graph does not make sense.

val terms_of : graph -> (term -> bool) -> term list

Minimal list of terms encoding the current state of the graph. Contains

  • equality between representatives and their class, and
  • comparison terms between representatives.

Input function returns true for candidates we want to ignore, typically candidates we have already proved true.

Used when querying the base instance of the LSD (graph stabilization). See also equalities_of and relations_of, used for the step instance (induction check).

val equalities_of : graph -> (term -> bool) -> (term * (term * term)) list

Equalities coming from the equivalence classes of a graph.

Input function returns true for candidates we want to ignore, typically candidates we have already proved true.

Generates a list of pairs term * (term * term). The first term is the candidate invariant, while the second element stores the representative of the class the candidate comes from, and the term that can be dropped from it if the candidate is indeed invariant.

val relations_of : graph -> (term * unit) list -> (term -> bool) -> (term * unit) list

Appends the relations from a graph to the input term list.

Input function returns true for candidates we want to ignore, typically candidates we have already proved true.

More precisely, generates implications between representatives and the representative and terms of each equivalence class they're a parent of.

Generates a list of pairs term * unit. The useless unit second element is just there to be compatible with the signature of the lsd step query function. This is to accomodate with the information we need to keep around for the equalities of a graph (see equalities_of).

val stabilize : graph -> 'a InputSystem.t -> TransSys.t -> (term -> bool) -> Lsd.base -> unit

Queries the lsd and updates the graph. Terminates when the graph is stable, meaning all terms the graph represents are unfalsifiable in the current lsd.

Input function returns true for candidates we want to ignore, typically candidates we have already proved true.

val step_stabilize : bool -> graph -> 'a InputSystem.t -> TransSys.t -> (term -> bool) -> Lsd.step -> ((Term.t * Certificate.t) list -> unit) -> Term.t list

Clones the graph, and splits it in step.

Stabilizes eq classes one by one, communicates invariants at each step. Then stabilizes relations, communicating by packs.