package alt-ergo-lib

Type of model.

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

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.

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.

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