Frama-C:
Plug-ins:
Libraries:

Frama-C API - Subst

type t = sigma
val create : ?pool:pool -> unit -> t
val copy : sigma -> sigma
val fresh : t -> tau -> var
val find : t -> term -> term
val filter : t -> term -> bool
val add : t -> term -> term -> unit

Must bind lc-closed terms, or raise Invalid_argument

val add_fun : t -> (term -> term) -> unit

Must bind lc-closed terms, or raise Invalid_argument

val add_filter : t -> (term -> bool) -> unit

Only modifies terms that pass the filter.

val add_var : t -> var -> unit

To the pool

val add_vars : t -> Vars.t -> unit

To the pool

val add_term : t -> term -> unit

To the pool