Skip to content

Commit

Permalink
Update documentation about output_concrete_model
Browse files Browse the repository at this point in the history
I also remove the mention about the different kind of formats used
to print models. Indeed, we use only the SMT-LIB format and
the Why3 format is slightly different but probably outdated.
  • Loading branch information
Halbaroth committed Sep 22, 2023
1 parent 7ed39b7 commit 14c8ffe
Showing 1 changed file with 2 additions and 6 deletions.
8 changes: 2 additions & 6 deletions src/lib/frontend/models.mli
Original file line number Diff line number Diff line change
Expand Up @@ -37,10 +37,6 @@ type t = {
arrays : ModelMap.t;
}

(** 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.
*)
val output_concrete_model : Format.formatter -> t -> unit
(** [output_concrete_model ppf mdl] prints the model [mdl] on
the formatter [ppf]. *)

0 comments on commit 14c8ffe

Please sign in to comment.