Module `Invs`

Invariants are stored in two hash tables mapping them to their certificate. One table is for one-state invariants, the other is for two-state invariants.

type t: Stores invariants.

val copy : t -> t
val empty : unit -> t: The empty collection of invariants.

val is_empty : t -> bool: True if no invariants.

val len : t -> int * int: Number of invariants (one-state, two-state).

val of_bound : t -> bool -> Numeral.t -> Term.t list

Bumps invariants.

If second parameter is true, include two-state invariants.

val filter : (bool -> Term.t -> Certificate.t -> bool) -> t -> t

Filters some invariants.

Function takes a boolean flag indicating if the invariant is two state.

val add_os : t -> Term.t -> Certificate.t -> unit

Adds a one-state invariant.

Adds a two-state invariant.

val add_ts : t -> Term.t -> Certificate.t -> unit

Adds a two-state invariant.

Remove all the invariants.

val clear : t -> unit: Remove all the invariants.

val get_os : t -> Term.TermSet.t

The one-state invariants.

The two-state invariants.

val get_ts : t -> Term.TermSet.t: The two-state invariants.

val mem : t -> Term.t -> bool: Checks if a term is a known invariant.

val find : t -> Term.t -> Certificate.t option: Returns Some cert if term is a known invariant, or None otherwise.

val flatten : t -> (Term.t * Certificate.t) list: **Temporary.** Flattens some invariants into a list.

val merge : t -> t -> t: Merges two collections of invariants (non-destructive).

val fmt : Stdlib.Format.formatter -> t -> unit: Formats some invariants.