Module AltErgoLib.ModelMap

type t

Type of model.

val add : Id.typed -> Expr.t list -> Expr.t -> t -> t

add sy args ret mdl adds the binding args -> ret to the partial graph associated with the symbol sy.

val empty : suspicious:bool -> Id.typed list -> t

An empty model. The suspicious flag is used to remember that this model may be wrong as it involves symbols from theories for which the model generation is known to be incomplete.

val subst : Id.t -> Expr.t -> t -> t

subst id e mdl substitutes all the occurrences of the identifier id in the model mdl by the model term e.

@Raise Error if the expression e is not a model term or the type of e doesn't agree with some occurrence of id in the model.

val pp : t Fmt.t

pp ppf mdl prints the model mdl on the formatter ppf using the SMT-LIB format.