package alt-ergo-lib

  1. Overview
  2. Docs

Printer module

Printer

val print_std : ?flushed:bool -> ('a, Format.formatter, unit) format -> 'a

Print message on the standard formatter accessible with Options.get_fmt_std and set by default to stdout The std formatter is flushed after the print if flushed is set

val print_err : ?flushed:bool -> ?header:bool -> ?error:bool -> ('a, Format.formatter, unit) format -> 'a

Print error message on the error formatter accessible with Options.get_fmt_err and set by default to stderr. Prints only if error (true by default) is true. If header is set, prints a header "Error". The err formatter is flushed after the print if flushed is set

val print_wrn : ?flushed:bool -> ?header:bool -> ?warning:bool -> ('a, Format.formatter, unit) format -> 'a

Print warning message on the warning formatter accessible with Options.get_fmt_wrn and set by default to stderr. Prints only if warning (true by default) is true. If header is set, prints a header "Warning". The wrn formatter is flushed after the print if flushed is set

val print_dbg : ?flushed:bool -> ?header:bool -> ?module_name:string -> ?function_name:string -> ('a, Format.formatter, unit) format -> 'a

Print debug message on the debug formatter accessible with Options.get_fmt_dbg and set by default to stderr. If header is set, prints a header "Debug<module_name><function_name>" if module_name and function_name are set. The dbg formatter is flushed after the print if flushed is set

val print_fmt : ?flushed:bool -> Format.formatter -> ('a, Format.formatter, unit) format -> 'a

Print message on the given formatter. The given formatter is flushed after the print if flushed is set

Utils

val init_colors : unit -> unit

Initialisation function used to add colors to the formatters

val init_output_format : unit -> unit

Initialisation function used to configure formatters corresponding of the output format set. Add ";" at the beginning of the lines if output is set to smtlib2

val pp_list_no_space : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit

Print list without separator

Status Printer

val print_status_unsat : ?validity_mode:bool -> Loc.t option -> float option -> int option -> string option -> unit

Print unsat status message from the frontend on the standard output. If validity_mode is set, the status print : `Valid (<time>s) (<steps> steps) (goal <goal_name>)` else, we print `unsat`. If a location is given, we report it only in validity_mode before printing the status.

val print_status_sat : ?validity_mode:bool -> Loc.t option -> float option -> int option -> string option -> unit

Print sat status message from the frontend on the standard output. If validity_mode is set, the status print : `Invalid (<time>s) (<steps> steps) (goal <goal_name>)` else, we print `sat`. If a location is given, we report it only in validity_mode before printing the status.

val print_status_unknown : ?validity_mode:bool -> Loc.t option -> float option -> int option -> string option -> unit

Print unknown status message from the frontend on the standard output. If validity_mode is set, the status print : `I don't Know (<time>s) (<steps> steps) (goal <goal_name>)` else, we print `unknown`. If a location is given, we report it only in validity_mode before printing the status.

val print_status_timeout : ?validity_mode:bool -> Loc.t option -> float option -> int option -> string option -> unit

Print timeout status message from the frontend on the standard output. If validity_mode is set, the status print : `Timeout (<time>s) (<steps> steps) (goal <goal_name>)` else, we print `timeout`. If a location is given, we report it only in validity_mode before printing the status.

val print_status_inconsistent : ?validity_mode:bool -> Loc.t option -> float option -> int option -> string option -> unit

Print inconsistent status message from the frontend on the standard output. If validity_mode is set, the status print : `Inconsistent assumption (<time>s) (<steps> steps) (goal <goal_name>)` else, we print nothing. If a location is given, we report it only in validity_mode before printing the status.

val print_status_preprocess : ?validity_mode:bool -> float option -> int option -> unit

Print preprocess status message from the frontend on the standard output. If validity_mode is set, the status print : `Preprocess (<time>s) (<steps> steps)` else, we print nothing.

OCaml

Innovation. Community. Security.