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, Stdlib.Format.formatter, unit) Stdlib.format ->
'aPrint 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, Stdlib.Format.formatter, unit) Stdlib.format ->
'aPrint 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, Stdlib.Format.formatter, unit) Stdlib.format ->
'aPrint 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 ->
Stdlib.Format.formatter ->
('a, Stdlib.Format.formatter, unit) Stdlib.format ->
'aPrint message on the given formatter. The given formatter is flushed after the print if flushed is set
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 :
(Stdlib.Format.formatter -> 'a -> unit) ->
Stdlib.Format.formatter ->
'a list ->
unitPrint list without separator
val pp_list_space :
(Stdlib.Format.formatter -> 'a -> unit) ->
Stdlib.Format.formatter ->
'a list ->
unitPrint list with separator
val print_status_unsat :
?validity_mode:bool ->
Loc.t option ->
float option ->
int option ->
string option ->
unitPrint 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 ->
unitPrint 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 ->
unitPrint 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 ->
unitPrint 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 ->
unitPrint 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.
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.