Module AltErgoLib.Models

Models module

val output_concrete_model : Format.formatter -> Expr.Set.t -> functions:ModelMap.t -> constants:ModelMap.t -> arrays:ModelMap.t -> unit

Print the given counterexample on the given formatter with the corresponding format set with Options.get_output_format.

  • functions: the functions of the model;
  • constants: the variables of the model;
  • arrays: (experimental) the arrays of the model.